some more work

[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 e98696589e2f30f48fdfa9011a8df7c1c2692285..d595882bcd1f746c40a40c43e2a5cdb342028fa4 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -1,7 +1,7 @@
 (*D
 
-Matita Tutorial: inductively generated formal topologies
-======================================================== 
+Inductively generated formal topologies in Matita
+================================================= 
 
 This is a not so short introduction to [Matita][2], based on
 the formalization of the paper
@@ -11,16 +11,31 @@ the formalization of the paper
 > inductive generation of formal topologies
 
 by Stefano Berardi and Silvio Valentini. 
+
 The tutorial is by Enrico Tassi. 
 
-The tutorial spends a considerable amount of effort in defining 
+The reader should be familiar with inductively generated
+formal topologies and have some basic knowledge of type theory and λ-calculus.  
+
+A considerable part of this tutorial is devoted to explain how to define 
 notations that resemble the ones used in the original paper. We believe
-this is a important part of every formalization, not only from the aesthetic 
+this is an 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
 statements) readable to the author of the paper. 
 
+The formalization uses the "new generation" version of Matita
+(that will be named 1.x when finally released). 
+Last stable release of the "old" system is named 0.5.7; the ng system
+is coexisting with the old one in all development release 
+(named "nightly builds" in the download page of Matita) 
+with a version strictly greater than 0.5.7.
+
+To read this tutorial in HTML format, you need a decent browser
+equipped with a unicode capable font. Use the PDF format if some
+symbols are not displayed correctly.
+
 Orienteering
 ------------
 
@@ -72,6 +87,11 @@ implements two unusual input facilities:
   example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, … 
   Variants are listed in the aforementioned TeX/UTF-8 table. 
 
+The syntax of terms (and types) is the one of the λ-calculus CIC
+on which Matita is based. The main syntactical difference w.r.t. 
+the usual mathematical notation is the function application, written
+`(f x y)` in place of `f(x,y)`. 
+
 Pressing `F1` opens the Matita manual.
 
 CIC (as [implemented in Matita][3]) in a nutshell
@@ -108,11 +128,7 @@ computation).
 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 `Id` (Leibniz equality), 
-thus we will explicitly equip a set with an equivalence relation when needed.
-We will call this structure a _setoid_. Note that we will
-attach the infix `=` symbol only to the equality of a setoid,
-not to Id.
+not quotiented set). 
 
 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, 
@@ -121,12 +137,93 @@ universes are declared by the user. The standard library defines
 
 > Type[0] < Type[1] < Type[2]
 
+<object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
+
 For every `Type[i]` there is a corresponding level of predicative
-propositions `CProp[i]`. A predicative proposition cannot be eliminated toward
-`Type[j]` unless it holds no computational content (i.e. it is an inductive type
+propositions `CProp[i]` (the C initial is due to historical reasons, and
+stands for constructive, `PProp` would be more appropriate). 
+A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
 with 0 or 1 constructors with propositional arguments, like `Id` and `And` 
 but not like `Or`). 
 
+The distinction between predicative propositions and predicative data types
+is a peculirity of Matita (for example in CIC as implemented by Coq they are the
+same). The additional restriction of not allowing the elimination of a CProp
+toward a Type makes the theory of Matita minimal in the following sense: 
+
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
+
+Theorems proved in CIC as implemented in Matita can be reused in a classical 
+and impredicative framework (i.e. forcing Matita to collapse the hierarchy of 
+constructive propositions and assuming the excluded middle on them). 
+Alternatively, one can decide to collapse predicative propositions and 
+datatypes recovering the Axiom of Choice in the sense of Martin Löf 
+(i.e. ∃ really holds a witness and can be eliminated to inhabit a type).
+
+This implementation of CIC is the result of the collaboration with Maietti M.,
+Sambin G. and Valentini S. of the University of Padua.
+
+Formalization choices
+---------------------
+
+There are many different ways of formalizing the same piece of mathematics
+in CIC, depending on what our interests are. There is usually a tradeoff 
+between the possibility of reuse the formalization we did and its complexity.
+
+In this work, our decisions mainly regarded the following two areas
+
+- Equality: Id or not
+- Axiom of Choice: controlled use or not
+
+### Equality
+
+TODO
+We will avoid using `Id` (Leibniz equality), 
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,
+not to Id.
+
+### Axiom of Choice
+
+In this paper it is clear that the author is interested in using the Axiom
+of Choice, thus choosing to identify ∃ and Σ (i.e. working in the 
+leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision 
+(that is, the author of the paper would not complain we formalized something
+diffrent from what he had in mind).
+
+Anyway, we may benefit from the minimality of CIC as implemented in Matita,
+"asking" the type system to ensure we do no use the Axiom of Choice elswhere
+in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
+very beginnig, the system will not complain if we use the Axiom of Choice at all.
+Moreover, the elimination of an inductive type (like ∃) is a so common operation
+that the syntax chosen for the elimination command is very compact and non 
+informative, hard to spot for a human being 
+(in fact it is just two characters long!). 
+
+We decided to formalize the whole paper without identifying
+CProp and Type and assuming the Axiom of Choice as a real axiom 
+(i.e. a black hole with no computational content, a function with no body). 
+
+It is clear that this approach give us full control on when/where we really use
+the Axiom of Choice. But, what are we loosing? What happens to the computational
+content of the proofs if the Axiom of Choice gives no content back? 
+
+It really
+depends on when we actually look at the computational content of the proof and 
+we "run" that program. We can extract the content and run it before or after 
+informing the system that our propositions are actually code (i.e. identifying
+∃ and Σ). If we run the program before, as soon as the computation reaches the 
+Axiom of Choice it stops, giving no output. If we tell the system that CProp and
+Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection)
+and the extracted code would compute an output. 
+
+Note that the computational
+content is there even if the Axiom of Choice is an axiom, the difference is
+just that we cannot use it (the typing rules inhibit the elimination of the 
+existential). This is possible only thanks to the minimality of CIC as implemented
+in Matita. 
 
 The standard library and the `include` command
 ----------------------------------------------
@@ -175,9 +272,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
@@ -423,8 +520,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.
@@ -558,11 +655,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
@@ -739,8 +836,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
@@ -806,6 +903,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 }.
@@ -834,6 +933,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
@@ -895,7 +1007,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.
@@ -926,6 +1039,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)).
 
@@ -965,20 +1085,26 @@ 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".
+alias symbol "covers" = "new covers".
 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". *)  
 *; #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
@@ -996,8 +1122,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 
@@ -1052,7 +1177,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; ##]
@@ -1114,7 +1239,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
 
@@ -1187,7 +1313,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);
@@ -1195,9 +1321,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;
 ##]
@@ -1243,9 +1368,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;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼