CSC proof made by paramod

diff --git a/helm/software/matita/nlibrary/algebra/bool.ma b/helm/software/matita/nlibrary/algebra/bool.ma
new file mode 100644 (file)
index 0000000..0e171fc
--- /dev/null
+++ b/helm/software/matita/nlibrary/algebra/bool.ma
@@ -0,0 +1,90 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/connectives.ma".
+
+ninductive eq (A: Type[1]) (a: A) : A → CProp[0] ≝
+ refl: eq A a a. 
+
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+ 
+nlemma eq_ind_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.a = b → P b.
+#A; #a; #P; #p; #b; #E; ncases E; nassumption;
+nqed.
+
+nlemma eq_ind_r_CProp0 : ∀A:Type[1].∀a:A.∀P:A → CProp[0].P a → ∀b:A.b = a → P b.
+#A; #a; #P; #p; #b; #E; ncases E in p; nauto;
+nqed. 
+
+nlemma csc : 
+ (∀x,y,z.(x∨(y∨z)) = ((x∨y)∨z)) →
+ (∀x,y,z.(x∧(y∧z)) = ((x∧y)∧z)) →
+ (∀x,y.(x∨y) = (y∨x)) →
+ (∀x,y.(x∧y) = (y∧x)) →
+ (∀x,y,z.(x∧(y∨z)) = ((x∧y)∨(x∧z))) →
+ (∀x.(x∨False) = (x)) →
+ (∀x.(x∧True) = (x)) →
+ (∀x.(x∧False) = (False)) →
+ (∀x.(x∨x) = (x)) →
+ (∀x.(x∧x) = (x)) →
+ (∀x,y.(x∧(x∨y)) = (x)) →
+ (∀x,y.(x∨(x∧y)) = (x)) →
+ (∀x,y,z.(x∨(y∧z)) = ((x∨y)∧(x∨z))) →
+ (∀x.(x∨True) = (True)) →
+ (∀x.(x∧¬x) = (False)) →
+ (∀x.(x∨¬x) = (True)) →
+ ∀a,b.((a ∧ ¬b) ∨ b) = (a ∨ b).
+#H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10; #H11; #H12;
+#H13; #H14; #H15; #H16; #a; #b;
+nletin proof ≝ (
+let clause_11: ∀x24. eq CProp[0] (And x24 True) x24
+ ≝ λx24. H7 x24 in
+ let clause_2: ∀x2. eq CProp[0] (Or x2 (Not x2)) True
+  ≝ λx2. H16 x2 in
+  let clause_5:
+   ∀x8.
+    ∀x9.
+     ∀x10.
+      eq CProp[0] (Or x8 (And x9 x10)) (And (Or x8 x9) (Or x8 x10))
+   ≝ λx8. λx9. λx10. H13 x8 x9 x10
+   in
+   let clause_15:
+    ∀x35.
+     ∀x36. eq CProp[0] (Or x35 x36) (Or x36 x35)
+    ≝ λx35. λx36. H3 x35 x36 in
+    let clause_194: eq CProp[0] (Or a b) (Or a b)
+     ≝ refl ?? in
+     let clause_193: eq CProp[0] (And (Or a b) True) (Or a b)
+      ≝ eq_ind_r_CProp0 CProp[0] (Or a b)
+            (λx:CProp[0]. eq CProp[0] x (Or a b)) clause_194
+            (And (Or a b) True) (clause_11 (Or a b)) in
+      let clause_192: eq CProp[0] (And (Or a b) (Or b (Not b))) (Or a b)
+       ≝ eq_ind_r_CProp0 CProp[0] True
+             (λx:CProp[0]. eq CProp[0] (And (Or a b) x) (Or a b)) clause_193
+             (Or b (Not b)) (clause_2 b) in
+       let clause_191: eq CProp[0] (And (Or b a) (Or b (Not b))) (Or a b)
+        ≝ eq_ind_r_CProp0 CProp[0] (Or a b)
+              (λx:CProp[0]. eq CProp[0] (And x (Or b (Not b))) (Or a b))
+              clause_192 (Or b a) (clause_15 b a) in
+        let clause_190: eq CProp[0] (Or b (And a (Not b))) (Or a b)
+         ≝ eq_ind_r_CProp0 CProp[0] (And (Or b a) (Or b (Not b)))
+               (λx:CProp[0]. eq CProp[0] x (Or a b)) clause_191
+               (Or b (And a (Not b))) (clause_5 b a (Not b)) in
+         let clause_1: eq CProp[0] (Or (And a (Not b)) b) (Or a b)
+          ≝ eq_ind_r_CProp0 CProp[0] (Or b (And a (Not b)))
+                (λx:CProp[0]. eq CProp[0] x (Or a b)) clause_190
+                (Or (And a (Not b)) b) (clause_15 (And a (Not b)) b) in
+          clause_1);
+napply proof;
+nqed.

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index 17adeb06f84a6d62513c69f6e3c978c0daac8190..f01e964701fd4ea1a920a8e4bbf5b1254bda2602 100644 (file)
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,25 +1,29 @@
-logic/cprop.ma hints_declaration.ma sets/setoids1.ma
-sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
-topology/igft.ma logic/equality.ma sets/sets.ma
+algebra/bool.ma logic/equality.ma
+algebra/abelian_magmas.ma algebra/magmas.ma
+logic/destruct_bb.ma logic/equality.ma
 datatypes/bool.ma logic/pts.ma
-sets/setoids1.ma properties/relations1.ma sets/setoids.ma
 logic/equality.ma logic/connectives.ma properties/relations.ma
-sets/setoids.ma logic/connectives.ma properties/relations.ma
-logic/connectives.ma logic/pts.ma
-topology/cantor.ma nat/nat.ma topology/igft.ma
-datatypes/pairs.ma logic/pts.ma
-algebra/abelian_magmas.ma algebra/magmas.ma
-nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
+sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
+logic/cprop.ma hints_declaration.ma sets/setoids1.ma
+topology/igft.ma logic/equality.ma sets/sets.ma
 nat/minus.ma nat/order.ma
 algebra/magmas.ma sets/sets.ma
+hints_declaration.ma logic/pts.ma
 properties/relations1.ma logic/pts.ma
-nat/big_ops.ma algebra/magmas.ma nat/order.ma
-nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma
-logic/destruct_bb.ma logic/equality.ma
-properties/relations.ma logic/pts.ma
+algebra/unital_magmas.ma algebra/magmas.ma
 nat/compare.ma datatypes/bool.ma nat/order.ma
-hints_declaration.ma logic/pts.ma
+logic/connectives.ma logic/pts.ma
+nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma
+topology/igft-setoid.ma sets/sets.ma
+sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
 logic/pts.ma 
 nat/order.ma nat/nat.ma sets/sets.ma
-algebra/unital_magmas.ma algebra/magmas.ma
-sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
+nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
+datatypes/pairs.ma logic/pts.ma
+topology/cantor.ma nat/nat.ma topology/igft.ma
+sets/setoids1.ma properties/relations1.ma sets/setoids.ma
+nat/big_ops.ma algebra/magmas.ma nat/order.ma
+topology/igft2.ma topology/igft.ma
+logic/markov.ma nat/order.ma
+properties/relations.ma logic/pts.ma
+sets/setoids.ma logic/connectives.ma properties/relations.ma

diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 8771aee6a9749e06141485f46f6e61693e5975da..a26055a4eb633fdfed6451d10e539298b87dc07e 100644 (file)
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -1,73 +1,81 @@
 digraph g {
+  "algebra/bool.ma" [];
+  "algebra/bool.ma" -> "logic/equality.ma" [];
+  "algebra/abelian_magmas.ma" [];
+  "algebra/abelian_magmas.ma" -> "algebra/magmas.ma" [];
+  "logic/destruct_bb.ma" [];
+  "logic/destruct_bb.ma" -> "logic/equality.ma" [];
+  "datatypes/bool.ma" [];
+  "datatypes/bool.ma" -> "logic/pts.ma" [];
+  "logic/equality.ma" [];
+  "logic/equality.ma" -> "logic/connectives.ma" [];
+  "logic/equality.ma" -> "properties/relations.ma" [];
+  "sets/partitions.ma" [];
+  "sets/partitions.ma" -> "datatypes/pairs.ma" [];
+  "sets/partitions.ma" -> "nat/compare.ma" [];
+  "sets/partitions.ma" -> "nat/minus.ma" [];
+  "sets/partitions.ma" -> "nat/plus.ma" [];
+  "sets/partitions.ma" -> "sets/sets.ma" [];
   "logic/cprop.ma" [];
   "logic/cprop.ma" -> "hints_declaration.ma" [];
   "logic/cprop.ma" -> "sets/setoids1.ma" [];
-  "sets/sets.ma" [];
-  "sets/sets.ma" -> "hints_declaration.ma" [];
-  "sets/sets.ma" -> "logic/connectives.ma" [];
-  "sets/sets.ma" -> "logic/cprop.ma" [];
-  "sets/sets.ma" -> "properties/relations1.ma" [];
-  "sets/sets.ma" -> "sets/setoids1.ma" [];
   "topology/igft.ma" [];
   "topology/igft.ma" -> "logic/equality.ma" [];
   "topology/igft.ma" -> "sets/sets.ma" [];
-  "datatypes/bool.ma" [];
-  "datatypes/bool.ma" -> "logic/pts.ma" [];
-  "sets/setoids1.ma" [];
-  "sets/setoids1.ma" -> "properties/relations1.ma" [];
-  "sets/setoids1.ma" -> "sets/setoids.ma" [];
-  "logic/equality.ma" [];
-  "logic/equality.ma" -> "logic/connectives.ma" [];
-  "logic/equality.ma" -> "properties/relations.ma" [];
-  "sets/setoids.ma" [];
-  "sets/setoids.ma" -> "logic/connectives.ma" [];
-  "sets/setoids.ma" -> "properties/relations.ma" [];
-  "logic/connectives.ma" [];
-  "logic/connectives.ma" -> "logic/pts.ma" [];
-  "topology/cantor.ma" [];
-  "topology/cantor.ma" -> "nat/nat.ma" [];
-  "topology/cantor.ma" -> "topology/igft.ma" [];
-  "datatypes/pairs.ma" [];
-  "datatypes/pairs.ma" -> "logic/pts.ma" [];
-  "algebra/abelian_magmas.ma" [];
-  "algebra/abelian_magmas.ma" -> "algebra/magmas.ma" [];
-  "nat/plus.ma" [];
-  "nat/plus.ma" -> "algebra/abelian_magmas.ma" [];
-  "nat/plus.ma" -> "algebra/unital_magmas.ma" [];
-  "nat/plus.ma" -> "nat/big_ops.ma" [];
   "nat/minus.ma" [];
   "nat/minus.ma" -> "nat/order.ma" [];
   "algebra/magmas.ma" [];
   "algebra/magmas.ma" -> "sets/sets.ma" [];
+  "hints_declaration.ma" [];
+  "hints_declaration.ma" -> "logic/pts.ma" [];
   "properties/relations1.ma" [];
   "properties/relations1.ma" -> "logic/pts.ma" [];
-  "nat/big_ops.ma" [];
-  "nat/big_ops.ma" -> "algebra/magmas.ma" [];
-  "nat/big_ops.ma" -> "nat/order.ma" [];
+  "algebra/unital_magmas.ma" [];
+  "algebra/unital_magmas.ma" -> "algebra/magmas.ma" [];
+  "nat/compare.ma" [];
+  "nat/compare.ma" -> "datatypes/bool.ma" [];
+  "nat/compare.ma" -> "nat/order.ma" [];
+  "logic/connectives.ma" [];
+  "logic/connectives.ma" -> "logic/pts.ma" [];
   "nat/nat.ma" [];
   "nat/nat.ma" -> "hints_declaration.ma" [];
   "nat/nat.ma" -> "logic/equality.ma" [];
   "nat/nat.ma" -> "sets/setoids.ma" [];
-  "logic/destruct_bb.ma" [];
-  "logic/destruct_bb.ma" -> "logic/equality.ma" [];
-  "properties/relations.ma" [];
-  "properties/relations.ma" -> "logic/pts.ma" [];
-  "nat/compare.ma" [];
-  "nat/compare.ma" -> "datatypes/bool.ma" [];
-  "nat/compare.ma" -> "nat/order.ma" [];
-  "hints_declaration.ma" [];
-  "hints_declaration.ma" -> "logic/pts.ma" [];
+  "topology/igft-setoid.ma" [];
+  "topology/igft-setoid.ma" -> "sets/sets.ma" [];
+  "sets/sets.ma" [];
+  "sets/sets.ma" -> "hints_declaration.ma" [];
+  "sets/sets.ma" -> "logic/connectives.ma" [];
+  "sets/sets.ma" -> "logic/cprop.ma" [];
+  "sets/sets.ma" -> "properties/relations1.ma" [];
+  "sets/sets.ma" -> "sets/setoids1.ma" [];
   "logic/pts.ma" [];
   "nat/order.ma" [];
   "nat/order.ma" -> "nat/nat.ma" [];
   "nat/order.ma" -> "sets/sets.ma" [];
-  "algebra/unital_magmas.ma" [];
-  "algebra/unital_magmas.ma" -> "algebra/magmas.ma" [];
-  "sets/partitions.ma" [];
-  "sets/partitions.ma" -> "datatypes/pairs.ma" [];
-  "sets/partitions.ma" -> "nat/compare.ma" [];
-  "sets/partitions.ma" -> "nat/minus.ma" [];
-  "sets/partitions.ma" -> "nat/plus.ma" [];
-  "sets/partitions.ma" -> "sets/sets.ma" [];
+  "nat/plus.ma" [];
+  "nat/plus.ma" -> "algebra/abelian_magmas.ma" [];
+  "nat/plus.ma" -> "algebra/unital_magmas.ma" [];
+  "nat/plus.ma" -> "nat/big_ops.ma" [];
+  "datatypes/pairs.ma" [];
+  "datatypes/pairs.ma" -> "logic/pts.ma" [];
+  "topology/cantor.ma" [];
+  "topology/cantor.ma" -> "nat/nat.ma" [];
+  "topology/cantor.ma" -> "topology/igft.ma" [];
+  "sets/setoids1.ma" [];
+  "sets/setoids1.ma" -> "properties/relations1.ma" [];
+  "sets/setoids1.ma" -> "sets/setoids.ma" [];
+  "nat/big_ops.ma" [];
+  "nat/big_ops.ma" -> "algebra/magmas.ma" [];
+  "nat/big_ops.ma" -> "nat/order.ma" [];
+  "topology/igft2.ma" [];
+  "topology/igft2.ma" -> "topology/igft.ma" [];
+  "logic/markov.ma" [];
+  "logic/markov.ma" -> "nat/order.ma" [];
+  "properties/relations.ma" [];
+  "properties/relations.ma" -> "logic/pts.ma" [];
+  "sets/setoids.ma" [];
+  "sets/setoids.ma" -> "logic/connectives.ma" [];
+  "sets/setoids.ma" -> "properties/relations.ma" [];
   
   }
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index 289e400a92d43e0a8e854b5c462b963eceb6ce75..d70a17341c327f4c4f61adafc18ebce1009f223b 100644 (file)
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ