From: Enrico Tassi Date: Fri, 23 Oct 2009 13:45:01 +0000 (+0000) Subject: CSC proof made by paramod X-Git-Tag: make_still_working~3257 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b7555a8732a9a304ac45c4e8024f122e261506af;p=helm.git 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 index 000000000..0e171fc58 --- /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 17adeb06f..f01e96470 100644 --- 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 8771aee6a..a26055a4e 100644 --- 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 289e400a9..d70a17341 100644 Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ