...

[helm.git] / helm / software / matita / nlibrary / topology / igft.ma

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 21194951bc91831f211012245fae1737f245f311..39497ac7be003b12f12e36925b323a986e0b0a77 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -192,9 +192,9 @@ with `C A`.
 D*)
 
 nrecord Ax : Type[1] ≝ { 
-  S :> setoid;
+  S :> Type[0];
   I :  S → Type[0];
-  C :  ∀a:S. I a → Ω ^ S
+  C :  ∀a:S. I a → Ω^S
 }.
 
 (*D
@@ -440,8 +440,8 @@ the premise of infinity.
 D*)
 
 ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ 
-| creflexivity : ∀a. a ∈ U → cover ? U a
-| cinfinity    : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
+| creflexivity : ∀a. a ∈ U → cover A U a
+| cinfinity    : ∀a. ∀i. 𝐂 a i ◃ U → cover A U a.
 (** screenshot "cover". *) 
 napply cover;
 nqed.
@@ -575,11 +575,11 @@ nlet corec fish_rec (A:Ax) (U: Ω^A)
  (P: Ω^A) (H1: P ⊆ U)
   (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
                                        (** screenshot "def-fish-rec-1".   *)
-#a; #p; napply cfish;                  (** screenshot "def-fish-rec-2".   *)
+#a; #a_in_P; napply cfish;                  (** screenshot "def-fish-rec-2".   *)
 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *) 
     napply H1;                         (** screenshot "def-fish-rec-3".   *) 
     nassumption;
-##| #i; ncases (H2 a p i);             (** screenshot "def-fish-rec-5".   *) 
+##| #i; ncases (H2 a a_in_P i);             (** screenshot "def-fish-rec-5".   *) 
     #x; *; #xC; #xP;                   (** screenshot "def-fish-rec-5-1". *) 
     @;                                 (** screenshot "def-fish-rec-6".   *)
     ##[ napply x
@@ -756,8 +756,8 @@ in the new definition of the axiom set with `n`.
 
 D*)
 
-nrecord nAx : Type[2] ≝ { 
-  nS:> setoid; 
+nrecord nAx : Type[1] ≝ { 
+  nS:> Type[0]; 
   nI: nS → Type[0];
   nD: ∀a:nS. nI a → Type[0];
   nd: ∀a:nS. ∀i:nI a. nD a i → nS
@@ -823,6 +823,8 @@ construction that has to be proved extensional
 
 D*)
 
+include "logic/equality.ma".
+
 ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
 
 notation > "𝐈𝐦  [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
@@ -851,6 +853,19 @@ ndefinition nAx_of_Ax : Ax → nAx.
 ##]
 nqed.
 
+nlemma Ax_nAx_equiv : 
+  ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
+               C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.               
+#A; #a; #i; @; #b; #H;
+##[  ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; 
+     nwhd in H; ncases H; #x; #E; nrewrite > E;
+     ncases x in E; #b; #Hb; #_; nnormalize; nassumption;
+##|  ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
+     ##[ @ b; nassumption;
+     ##| nnormalize; @; ##]
+##]
+nqed.
+
 (*D
 
 We then define the inductive type of ordinals, parametrized over an axiom
@@ -912,7 +927,8 @@ of the tutorial works only for the old axiom set.
 
 D*)
   
-ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
+ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ 
+  λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
 
 ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
   ∀y.y ∈ C → y ∈ c A U.
@@ -943,6 +959,13 @@ to provide the witness for the second.
 
 D*)
 
+nlemma AC_fake : ∀A,a,i,U.
+  (∀j:𝐃 a i.Σx:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
+#A; #a; #i; #U; #H; @;
+##[ #j; ncases (H j); #x; #_; napply x;
+##| #j; ncases (H j); #x; #Hx; napply Hx; ##]
+nqed. 
+
 naxiom AC : ∀A,a,i,U.
   (∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
 
@@ -982,6 +1005,9 @@ We now proceed with the proof of the infinity rule.
 D*)
 
 
+alias symbol "exists" (instance 1) = "exists".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
 alias symbol "covers" = "new covers set".
 alias symbol "covers" = "new covers".
 alias symbol "covers" = "new covers set".
@@ -990,14 +1016,14 @@ ntheorem new_coverage_infinity:
 #A; #U; #a;                                   (** screenshot "n-cov-inf-1". *)  
 *; #i; #H; nnormalize in H;                   (** screenshot "n-cov-inf-2". *)
 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[    (** screenshot "n-cov-inf-3". *)
-  #z; napply H; @ z; napply #; ##] #H';       (** screenshot "n-cov-inf-4". *)
+  #z; napply H; @ z; @; ##] #H';       (** screenshot "n-cov-inf-4". *)
 ncases (AC … H'); #f; #Hf;                    (** screenshot "n-cov-inf-5". *)
 ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
   ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
 @ (Λ f+1);                                    (** screenshot "n-cov-inf-7". *)
 @2;                                           (** screenshot "n-cov-inf-8". *) 
 @i; #x; *; #d; #Hd;                           (** screenshot "n-cov-inf-9". *)  
-napply (U_x_is_ext … Hd); napply Hf';
+nrewrite > Hd; napply Hf';
 nqed.
 
 (*D
@@ -1015,8 +1041,7 @@ We thus assert (`ncut`) the nicer form of `H` and prove it.
 D[n-cov-inf-3]
 After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`). 
 What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that 
-becomes trivial if `j` is chosen to be `z`. In the command `napply #`,
-the `#` is a standard notation for the reflexivity property of the equality. 
+becomes trivial if `j` is chosen to be `z`. 
 
 D[n-cov-inf-4]
 Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and 
@@ -1071,7 +1096,7 @@ nlemma new_coverage_min :
 *; #o;                                          (** screenshot "n-cov-min-3". *)
 ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
 nelim o;                                        (** screenshot "n-cov-min-5". *) 
-##[ #b; #bU0; napply HUV; napply bU0;
+##[ napply HUV; 
 ##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
     #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
@@ -1133,7 +1158,8 @@ We assume the dual of the axiom of choice, as in the paper proof.
 
 D*)
 naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F. 
- (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
+ (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x))
+    → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
 
 (*D
 
@@ -1206,7 +1232,7 @@ subset of `S`, while `Ω^A` means just a subset (note that the former is bold).
 
 D*)
 ntheorem max_new_fished: 
-  ∀A:nAx.∀G:𝛀^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
+  ∀A:nAx.∀G:Ω^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
 #A; #G; #F; #GF; #H; #b; #HbG; #o; 
 ngeneralize in match HbG; ngeneralize in match b;
 nchange with (G ⊆ F⎽o);
@@ -1214,9 +1240,8 @@ nelim o;
 ##[ napply GF;
 ##| #p; #IH; napply (subseteq_intersection_r … IH);
     #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
-    @d; napply IH;                                (** screenshot "n-f-max-1". *)
-    alias symbol "prop2" = "prop21".
-    napply (. Ed^-1‡#); napply cG;    
+    @d; napply IH;                                 (** screenshot "n-f-max-1". *)
+    nrewrite < Ed; napply cG;    
 ##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) }); 
     #b; #Hb; #d; napply (Hf d); napply Hb;
 ##]
@@ -1262,9 +1287,9 @@ in terms of sequent calculus rules annotated with proofs.
 The `:` separator has to be read as _is a proof of_, in the spirit
 of the Curry-Howard isomorphism.
 
-                  Γ ⊢  f  :  A1 → … → An → B    Γ ⊢ ?1 : A1 … ?n  :  An 
+                  Γ ⊢  f  :  A_1 → … → A_n → B     Γ ⊢ ?_i  :  A_i 
     napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
-                           Γ ⊢ (f ?1 … ?n )  :  B
+                           Γ ⊢ (f ?_1 … ?_n )  :  B
  
                    Γ ⊢  ?  :  F → B       Γ ⊢ f  :  F 
     nlapply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼