more comments

[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 8bba1228176ee0eea57c91bb723636f196916928..e6caecc6360e01dd232b3cf54328562abcf75f93 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -14,7 +14,7 @@ by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
 
 The tutorial spends a considerable amount of effort in defining 
 notations that resemble the ones used in the original paper. We believe
 
 The tutorial spends a considerable amount of effort in defining 
 notations that resemble the ones used in the original paper. We believe

-this a important part of every formalization, not only for the aesthetic 
+this is a important part of every formalization, not only from the aesthetic 

 point of view, but also from the practical point of view. Being 
 consistent allows to follow the paper in a pedantic way, and hopefully
 to make the formalization (at least the definitions and proved
 point of view, but also from the practical point of view. Being 
 consistent allows to follow the paper in a pedantic way, and hopefully
 to make the formalization (at least the definitions and proved


@@ -74,17 +74,38 @@ implements two unusual input facilities:
 CIC (as implemented in Matita) in a nutshell
 -------------------------------------------- 
 
 CIC (as implemented in Matita) in a nutshell
 -------------------------------------------- 
 

-...
+CIC is a full and functional Pure Type System (all products do exist,
+and their sort is is determined by the target) with an impedicative sort
+Prop and a predicative sort Type. The environment can be populated with
+well typed definitions or theorems, (co)inductive types validating positivity
+conditions and recursive functions provably total by simple syntactical 
+analysis (recursive call on structurally smaller subterms). Co-recursive 
+functions can be defined as well, and must satisfy a dual condition, that is
+performing the recursive call only after having generated a constructor (a piece
+of output).
+
+The λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment that combined with the definable total 
+structural recursive functions allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly types 
+local definitions (let in) that in the degenerate case work as casts (i.e.
+the type annotation `(t : T)`  is implemented as `let x : T ≝ t in x`). 
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).

 
 

-Type is a set equipped with the Id equality (i.e. an intensional,
+Since we are going to formalize constructive and predicative mathematics
+in an intensional type theory like CIC, we try to establish some terminology. 
+Type is the sort of sets equipped with the Id equality (i.e. an intensional,

 not quotiented set). We will avoid using Leibnitz equality Id, 
 thus we will explicitly equip a set with an equality when needed.
 We will call this structure `setoid`. Note that we will
 not quotiented set). We will avoid using Leibnitz equality Id, 
 thus we will explicitly equip a set with an equality when needed.
 We will call this structure `setoid`. Note that we will

-attach the infix = symbols only to the equality of a setoid,
+attach the infix = symbol only to the equality of a setoid,

 not to Id.
 
 not to Id.
 

-...
-

 We write Type[i] to mention a Type in the predicative hierarchy 
 of types. To ease the comprehension we will use Type[0] for sets, 
 and Type[1] for classes.
 We write Type[i] to mention a Type in the predicative hierarchy 
 of types. To ease the comprehension we will use Type[0] for sets, 
 and Type[1] for classes.


@@ -92,8 +113,6 @@ and Type[1] for classes.
 For every Type[i] there is a corresponding level of predicative
 propositions CProp[i].
 
 For every Type[i] there is a corresponding level of predicative
 propositions CProp[i].
 

-CIC is also equipped with an impredicative sort Prop that we will not
-use in this tutorial.

 
 The standard library and the `include` command
 ----------------------------------------------
 
 The standard library and the `include` command
 ----------------------------------------------


@@ -116,26 +135,6 @@ D*)
 
 include "sets/sets.ma".
 
 
 include "sets/sets.ma".
 

-(*HIDE*)
-(* move away *)
-nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
-#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
-nqed.
-
-nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
-#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
-nqed. 
-
-nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
-#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
-nqed. 
-
-ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ 
- sig_intro : ∀x:A.P x → sigma A P. 
-
-interpretation "sigma" 'sigma \eta.p = (sigma ? p). 
-(*UNHIDE*)
-

 (*D
 
 Some basic results that we will use are also part of the sets library:
 (*D
 
 Some basic results that we will use are also part of the sets library:


@@ -541,18 +540,18 @@ D*)
 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 ≝ ?.
 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". *)
+                                       (** screenshot "def-fish-rec-1".   *)
+#a; #p; napply cfish;                  (** screenshot "def-fish-rec-2".   *)

 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *) 
 ##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *) 

-    napply H1;                         (** screenshot "def-fish-rec-3". *) 
+    napply H1;                         (** screenshot "def-fish-rec-3".   *) 

     nassumption;
     nassumption;

-##| #i; ncases (H2 a p i);             (** screenshot "def-fish-rec-5". *) 
+##| #i; ncases (H2 a p i);             (** screenshot "def-fish-rec-5".   *) 

     #x; *; #xC; #xP;                   (** screenshot "def-fish-rec-5-1". *) 
     #x; *; #xC; #xP;                   (** screenshot "def-fish-rec-5-1". *) 

-    @;                                 (** screenshot "def-fish-rec-6". *)
+    @;                                 (** screenshot "def-fish-rec-6".   *)

     ##[ napply x
     ##[ napply x

-    ##| @;                             (** screenshot "def-fish-rec-7". *)
+    ##| @;                             (** screenshot "def-fish-rec-7".   *)

         ##[ napply xC; 
         ##[ napply xC; 

-        ##| napply (fish_rec ? U P);   (** screenshot "def-fish-rec-9". *)
+        ##| napply (fish_rec ? U P);   (** screenshot "def-fish-rec-9".   *)

             nassumption;
         ##]
     ##]
             nassumption;
         ##]
     ##]


@@ -662,7 +661,7 @@ ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝  λA,U,X.
 
 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
 #A; #U; #a; @; #H;
 
 ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
 #A; #U; #a; @; #H;

-##[ nelim H; #b; (* manca clear *)
+##[ nelim H; #b; 

     ##[ #bU; @1; nassumption;
     ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
         ##[ #E; @; napply E;
     ##[ #bU; @1; nassumption;
     ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
         ##[ #E; @; napply E;


@@ -755,25 +754,32 @@ The paper defines the image as
 
 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
 
 
 > Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
 

-but this cannot be ..... MAIL
+but this not so formal notation poses some problems. The image is
+often used as the left hand side of the ⊆ predicate

 
 > Im[d(a,i)] ⊆ V
 
 
 > Im[d(a,i)] ⊆ V
 

-Allora ha una comoda interpretazione (che voi usate liberamente)
+Of course this writing is interpreted by the authors as follows 

 
 > ∀j:D(a,i). d(a,i,j) ∈ V
 
 
 > ∀j:D(a,i). d(a,i,j) ∈ V
 

-Ma se voglio usare Im per definire C, che è un subset di S, devo per
-forza (almeno credo) definire un subset, ovvero dire che
+If we need to use the image to define 𝐂 (a subset of S) we are obliged to
+form a subset, i.e. to place a single variable `{ here | … }`.

 
 

-> Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
+> Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }

 
 

-Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua
-uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si
-scatenano i setoidi. Ovvero Im[d(a,i)] ⊆ V diventa il seguente
+This poses no theoretical problems, since `S` is a setoid and thus equipped
+with an equality.
+
+Unless we difene two different images, one for stating the image is ⊆ of
+something and another one to define 𝐂, we end up using always the latter.
+Thus the statement `Im[d(a,i)] ⊆ V` unfolds to

 
 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
 
 
 > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
 

+That up to rewriting with the equation defining `x` is what we mean. The 
+technical problem arises when `V` is a complex construction that has to
+be proved extensional (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).

 
 D*)
 
 
 D*)
 


@@ -786,7 +792,10 @@ interpretation "image" 'Im a i = (image ? a i).
 
 (*D
 
 
 (*D
 

-
+Thanks to our definition of image, we ca trivially a function mapping a
+new axiom set to an old one and viceversa. Note that in the second
+definition, when defining 𝐝, the projection of the Σ type is inlined
+(constructed on the fly by `*;`) while in the paper it was named `fst`.

 
 D*)
 
 
 D*)
 


@@ -823,18 +832,23 @@ interpretation "ordinals Succ" 'oS x = (oS ? x).
 
 (*D
 
 
 (*D
 

+The dfinition of `U_x` is by recursion over the ordinal `x`. 
+We thus define a recursive function. The `on x` directive tells
+the system on which argument the function is (structurally) recursive.
+
+In the `oS` case we use a local definition to name the recursive call
+since it is used twice.
+

 Note that Matita does not support notation in the left hand side
 of a pattern match, and thus the names of the constructors have to 
 be spelled out verbatim.
 
 Note that Matita does not support notation in the left hand side
 of a pattern match, and thus the names of the constructors have to 
 be spelled out verbatim.
 

-BLA let rec. Bla let_in.
-

 D*)
 
 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝ 
   match x with
   [ oO ⇒ U
 D*)
 
 nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝ 
   match x with
   [ oO ⇒ U

-  | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un} 
+  | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n} 

   | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
   
 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
   | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
   
 notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.


@@ -873,8 +887,7 @@ infinity rule.
 
 D*)
 
 
 D*)
 

-nlemma ord_subset:
-  ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
+nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).

 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
 nqed.
 
 #A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
 nqed.
 


@@ -896,7 +909,7 @@ naxiom AC : ∀A,a,i,U.
 In the proof of infinity, we have to rewrite under the ∈ predicate.
 It is clearly possible to show that U_x is an extensional set:
 
 In the proof of infinity, we have to rewrite under the ∈ predicate.
 It is clearly possible to show that U_x is an extensional set:
 

-> a=b → a ∈ U_x → b ∈ U_x
+> a = b → a ∈ U_x → b ∈ U_x

 
 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
 declared as morphisms. This poses to problem, but goes out of the scope of the 
 
 Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
 declared as morphisms. This poses to problem, but goes out of the scope of the 


@@ -904,8 +917,7 @@ tutorial and we thus assume it.
 
 D*)
 
 
 D*)
 

-naxiom setoidification :
-  ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
+naxiom setoidification: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.

 
 (*D
 
 
 (*D
 


@@ -913,8 +925,7 @@ The reflexivity proof is trivial, it is enough to provide the ordinal 0
 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
 
 D*)
 as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
 
 D*)

-ntheorem new_coverage_reflexive:
-  ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
+ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.

 #A; #U; #a; #H; @ (0); napply H;
 nqed.
 
 #A; #U; #a; #H; @ (0); napply H;
 nqed.
 


@@ -930,6 +941,7 @@ 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".
 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.
 #A; #U; #a;                                   (** screenshot "n-cov-inf-1". *)  
 ntheorem new_coverage_infinity:
   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
 #A; #U; #a;                                   (** screenshot "n-cov-inf-1". *)  


@@ -995,7 +1007,7 @@ D*)
 (*D
 
 The next proof is that ◃(U) is mininal. The hardest part of the proof
 (*D
 
 The next proof is that ◃(U) is mininal. The hardest part of the proof

-it to prepare the goal for the induction. The desiderata is to prove
+is to prepare the goal for the induction. The desiderata is to prove

 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
 unfolding all definitions:
 
 `U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
 unfolding all definitions:
 


@@ -1037,14 +1049,14 @@ D*)
 
 (*D
 
 
 (*D
 

-bla bla
+The notion `F_x` is again defined by recursion over the ordinal `x`.

 
 D*)
 
 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝ 
   match x with
   [ oO ⇒ F
 
 D*)
 
 nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝ 
   match x with
   [ oO ⇒ F

-  | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo } 
+  | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o } 

   | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
   ].
 
   | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
   ].
 


@@ -1058,11 +1070,10 @@ interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).
 (*D
 
 The proof of compatibility uses this little result, that we 
 (*D
 
 The proof of compatibility uses this little result, that we 

-factored out. 
+proved outside the mail proof. 

 
 D*)
 
 D*)

-nlemma co_ord_subset:
- ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
+nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).

 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
 nqed.
 
 #A; #F; #a; #i; #f; #j; #x; #H; napply H;
 nqed.
 


@@ -1071,18 +1082,17 @@ nqed.
 We assume the dual of the axiom of choice, as in the paper proof.
 
 D*)
 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.
+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.

 
 (*D
 
 
 (*D
 

-Proving the anti-reflexivity property is simce, since the
+Proving the anti-reflexivity property is simple, since the

 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
 
 D*)
 assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
 `a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
 
 D*)

-ntheorem new_fish_antirefl:
- ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
+ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.

 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
 nqed.
 
 #A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
 nqed.