From ac2780dc65e14efb3fc6315825696b0b44ec230f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Oct 2009 09:21:04 +0000
Subject: [PATCH] more comments

---
 .../software/matita/nlibrary/topology/igft.ma | 122 +++++++++++-------
 1 file changed, 76 insertions(+), 46 deletions(-)

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 59ccd5601..e6caecc63 100644
--- 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
-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
@@ -74,17 +74,38 @@ implements two unusual input facilities:
 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
-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.
 
-...
-
 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].
 
-CIC is also equipped with an impredicative sort Prop that we will not
-use in this tutorial.
 
 The standard library and the `include` command
 ----------------------------------------------
@@ -521,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 ≝ ?.
-                                       (** 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". *) 
-    napply H1;                         (** screenshot "def-fish-rec-3". *) 
+    napply H1;                         (** screenshot "def-fish-rec-3".   *) 
     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". *) 
-    @;                                 (** screenshot "def-fish-rec-6". *)
+    @;                                 (** screenshot "def-fish-rec-6".   *)
     ##[ napply x
-    ##| @;                             (** screenshot "def-fish-rec-7". *)
+    ##| @;                             (** screenshot "def-fish-rec-7".   *)
         ##[ napply xC; 
-        ##| napply (fish_rec ? U P);   (** screenshot "def-fish-rec-9". *)
+        ##| napply (fish_rec ? U P);   (** screenshot "def-fish-rec-9".   *)
             nassumption;
         ##]
     ##]
@@ -642,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;
-##[ nelim H; #b; (* manca clear *)
+##[ nelim H; #b; 
     ##[ #bU; @1; nassumption;
     ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
         ##[ #E; @; napply E;
@@ -735,25 +754,32 @@ The paper defines the image as
 
 > 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
 
-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
 
-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 | ∃j:D(a,i). y = d(a,i,j) }
 
-> Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
+This poses no theoretical problems, since `S` is a setoid and thus equipped
+with an equality.
 
-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
+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
 
+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*)
 
@@ -766,7 +792,10 @@ interpretation "image" 'Im a i = (image ? a i).
 
 (*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*)
 
@@ -803,18 +832,23 @@ interpretation "ordinals Succ" 'oS x = (oS ? x).
 
 (*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.
 
-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
-  | 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 }.
@@ -853,8 +887,7 @@ infinity rule.
 
 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.
 
@@ -876,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:
 
-> 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 
@@ -884,8 +917,7 @@ tutorial and we thus assume it.
 
 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
 
@@ -893,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*)
-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.
 
@@ -910,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 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". *)  
@@ -975,7 +1007,7 @@ D*)
 (*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:
 
@@ -1017,14 +1049,14 @@ 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
-  | 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) }
   ].
 
@@ -1038,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 
-factored out. 
+proved outside the mail proof. 
 
 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.
 
@@ -1051,18 +1082,17 @@ nqed.
 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
 
-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*)
-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.
 
-- 
2.39.2