From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Aug 2009 11:36:33 +0000 (+0000)
Subject: initial and incomplete port of the old demo about inductively generated formal
X-Git-Tag: make_still_working~3518
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5bfea0766a39d05605b6e88508f5376a88351331;p=helm.git

initial and incomplete port of the old demo about inductively generated formal
topologies. we try to make slightly different choices...
---

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index f39678fb8..301939368 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,21 +1,23 @@
-sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
 logic/cprop.ma sets/setoids1.ma
+sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
+topology/igft.ma logic/connectives.ma
 datatypes/bool.ma logic/pts.ma
 sets/setoids1.ma properties/relations1.ma sets/setoids.ma
-sets/setoids.ma logic/connectives.ma properties/relations.ma
 logic/equality.ma logic/connectives.ma properties/relations.ma
+sets/setoids.ma logic/connectives.ma properties/relations.ma
+.unnamed.ma logic/pts.ma
 logic/connectives.ma logic/pts.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
 nat/minus.ma nat/order.ma
 algebra/magmas.ma sets/sets.ma
-nat/nat.ma logic/equality.ma sets/setoids.ma
-nat/big_ops.ma algebra/magmas.ma nat/order.ma
 properties/relations1.ma logic/pts.ma
-nat/compare.ma datatypes/bool.ma nat/order.ma
+nat/big_ops.ma algebra/magmas.ma nat/order.ma
+nat/nat.ma logic/equality.ma sets/setoids.ma
 properties/relations.ma logic/pts.ma
+nat/compare.ma datatypes/bool.ma nat/order.ma
+logic/pts.ma 
 nat/order.ma nat/nat.ma sets/sets.ma
 algebra/unital_magmas.ma algebra/magmas.ma
-logic/pts.ma 
 sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 6a1e65939..ec3b85946 100644
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -1,19 +1,64 @@
 digraph g {
+  "logic/cprop.ma" [];
+  "logic/cprop.ma" -> "sets/setoids1.ma" [];
   "sets/sets.ma" [];
-  "sets/sets.ma" -> "logic/equality.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/connectives.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/equality.ma" [];
-  "logic/equality.ma" -> "logic/connectives.ma" [];
+  ".unnamed.ma" [];
+  ".unnamed.ma" -> "logic/pts.ma" [];
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.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" [];
+  "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" [];
+  "nat/nat.ma" [];
+  "nat/nat.ma" -> "logic/equality.ma" [];
+  "nat/nat.ma" -> "sets/setoids.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" [];
   "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" [];
   
   }
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index cb081dd85..fe86e43b3 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/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
new file mode 100644
index 000000000..29e1f1af3
--- /dev/null
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -0,0 +1,174 @@
+include "logic/connectives.ma".
+
+nrecord powerset (X : Type[0]) : Type[1] ≝ { char : X → CProp[0] }.
+
+interpretation "char" 'subset p = (mk_powerset ? p).  
+
+interpretation "pwset" 'powerset a = (powerset a). 
+
+interpretation "in" 'mem a X = (char ? X a). 
+
+ndefinition subseteq ≝ λA.λU,V : Ω^A. 
+  ∀x.x ∈ U → x ∈ V.
+
+interpretation "subseteq" 'subseteq u v = (subseteq ? u v).
+
+ndefinition overlaps ≝ λA.λU,V : Ω^A. 
+  ∃x.x ∈ U ∧ x ∈ V.
+
+interpretation "overlaps" 'overlaps u v = (overlaps ? u v).
+(*
+ndefinition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
+
+interpretation "intersect" 'intersects u v = (intersect ? u v). 
+*)
+nrecord axiom_set : Type[1] ≝ { 
+  S:> Type[0];
+  I: S → Type[0];
+  C: ∀a:S. I a → Ω ^ S
+}.
+
+ndefinition cover_set ≝ λc:∀A:axiom_set.Ω^A → A → CProp[0].λA,C,U.
+  ∀y.y ∈ C → c A U y.
+
+notation "hvbox(a break ◃ b)" non associative with precedence 45
+for @{ 'covers $a $b }. (* a \ltri b *)
+
+interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
+
+ninductive cover (A : axiom_set) (U : Ω^A) : A → CProp[0] ≝ 
+| creflexivity : ∀a:A. a ∈ U → cover ? U a
+| cinfinity    : ∀a:A. ∀i:I ? a. (C ? a i ◃ U) → cover ? U a.
+napply cover;
+nqed.
+
+interpretation "covers" 'covers a U = (cover ? U a).
+interpretation "covers set" 'covers a U = (cover_set cover ? a U).
+
+ndefinition fish_set ≝ λf:∀A:axiom_set.Ω^A → A → CProp[0].
+ λA,U,V.
+  ∃a.a ∈ V ∧ f A U a.
+
+notation "hvbox(a break ⋉ b)" non associative with precedence 45
+for @{ 'fish $a $b }. (* a \ltimes b *)
+
+interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
+
+ncoinductive fish (A : axiom_set) (F : Ω^A) : A → CProp[0] ≝ 
+| cfish : ∀a. a ∈ F → (∀i:I ? a.C A a i ⋉ F) → fish A F a.
+napply fish;
+nqed.
+
+interpretation "fish set" 'fish A U = (fish_set fish ? U A).
+interpretation "fish" 'fish a U = (fish ? U a).
+
+nlet corec fish_rec (A:axiom_set) (U: Ω^A)
+ (P: Ω^A) (H1: P ⊆ U)
+  (H2: ∀a:A. a ∈ P → ∀j: I ? a. C ? a j ≬ P):
+   ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
+#a; #p; napply cfish;
+##[ napply H1; napply p;
+##| #i; ncases (H2 a p i); #x; *; #xC; #xP; napply ex_intro; ##[napply x]
+    napply conj; ##[ napply xC ] napply (fish_rec ? U P); nassumption;
+##]
+nqed.
+
+STOP
+
+theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
+ intros;
+ apply refl;
+ assumption.
+qed.
+
+theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+ intros;
+ apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
+  [ cases H1 in H2; apply H2;
+  | apply infinity;
+     [ assumption
+     | constructor 1;
+       assumption]]
+qed.
+
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+  (∀a:A. a ∈ U → P a) →
+   (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+     ∀a:A. a ◃ U → P a.
+ intros;
+ change with (a ∈ {a | P a});
+ apply (covers_elim ?????? H2);
+  [ intros 2; simplify; apply H; assumption
+  | intros;
+    simplify in H4 ⊢ %;
+    apply H1;
+     [ apply (C ? a1 j);
+     | autobatch; 
+     | assumption;
+     | assumption]]
+qed.
+
+theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
+ intros;
+ cases H;
+ assumption.
+qed.
+
+theorem cotransitivity:
+ ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
+ intros;
+ apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros;
+  [ apply H1; apply H2;
+  | cases H2 in j; clear H2; intro i;
+    cases (H4 i); clear H4; exists[apply a3] assumption]
+qed.
+
+theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
+ intros;
+ generalize in match H; clear H; 
+ apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
+ clear H1; simplify; intros;
+  [ exists [apply x] assumption
+  | cases H2 in j H H1; clear H2 a1; intros; 
+    cases (H1 i); clear H1; apply (H3 a1); assumption]
+qed.
+
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
+
+interpretation "covered by one" 'leq a b = (leq ? a b).
+
+theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
+ intros;
+ apply refl;
+ normalize;
+ reflexivity.
+qed.
+
+theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
+ intros;
+ unfold in H H1 ⊢ %;
+ apply (transitivity ???? H);
+ constructor 1;
+ intros;
+ normalize in H2;
+ rewrite < H2;
+ assumption.
+qed.
+
+definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
+
+interpretation "uparrow" 'uparrow a = (uparrow ? a).
+
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
+
+interpretation "downarrow" 'downarrow a = (downarrow ? a).
+
+definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
+
+interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
+
+record convergent_generated_topology : Type ≝
+ { AA:> axiom_set;
+   convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
+ }.