From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 14 Oct 2009 15:13:27 +0000 (+0000)
Subject: cantor...
X-Git-Tag: make_still_working~3297
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c2b39b7ef14ab610cb2056fb6b75492c7068288e;hp=2f9e86d966ef765b9eff2483983ff1fe635bb138;p=helm.git

cantor...
---

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index c5d90654b..ac05db24a 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -6,6 +6,7 @@ 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 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
@@ -14,6 +15,7 @@ algebra/magmas.ma sets/sets.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
 nat/compare.ma datatypes/bool.ma nat/order.ma
 hints_declaration.ma logic/pts.ma
diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 8af49c5d8..6bedead7f 100644
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -23,12 +23,12 @@ digraph g {
   "sets/setoids.ma" -> "properties/relations.ma" [];
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.ma" [];
+  "topology/cantor.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" [];
-  "topology/igft-setoid.ma" [];
-  "topology/igft-setoid.ma" -> "sets/sets.ma" [];
   "nat/plus.ma" [];
   "nat/plus.ma" -> "algebra/abelian_magmas.ma" [];
   "nat/plus.ma" -> "algebra/unital_magmas.ma" [];
@@ -46,6 +46,8 @@ digraph g {
   "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" [];
diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index fc6f14ecd..63d436047 100644
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ
diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
new file mode 100644
index 000000000..95cf6b3aa
--- /dev/null
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -0,0 +1,46 @@
+
+
+include "topology/igft.ma".
+
+ninductive unit : Type[0] ≝ one : unit.
+
+naxiom E: setoid.
+naxiom R: E → Ω^E.
+
+ndefinition axs: Ax.
+@ E (λ_.unit) (λa,x.R a);
+nqed.
+
+unification hint 0 ≔ ;
+         x ≟ axs  
+  (* -------------- *) ⊢
+         S x ≡ E. 
+         
+ndefinition emptyset: Ω^axs ≝ {x | False}.
+
+ndefinition Z: Ω^axs ≝ {x | x ◃ emptyset}.
+
+alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
+alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
+ntheorem cover_trans: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+#A; #a; #U; #V; #aU; #UV;
+nelim aU;
+##[ #c; #H; napply (UV … H);
+##| #c; #i; #HCU; #H; napply (cinfinity … i); napply H;
+##]
+nqed.
+
+ntheorem cantor: ∀a:axs. ¬ (Z ⊆ R a ∧ R a ⊆ Z).
+#a; *; #ZRa; #RaZ;
+ncut (a ◃ R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
+ncut (a ◃ emptyset); ##[
+  napply (cover_trans … H1); 
+  #x; #H; nlapply (RaZ … H); #ABS; napply ABS; ##] #H2;
+ncut (a ∈ R a); ##[ napply ZRa; napply H2; ##] #H3;
+nelim H2 in H3; 
+##[ nauto.
+##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
+nqed.
+
diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index d0068dbf7..21194951b 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -982,6 +982,8 @@ We now proceed with the proof of the infinity rule.
 D*)
 
 
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
 alias symbol "covers" = "new covers set".
 ntheorem new_coverage_infinity:
   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.