...

[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 1cb932184a64e9fc03d69969a52865a18e0018c1..66c7dd3a14e9dd9811d43847bb3aef37d7c0d829 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -16,14 +16,16 @@ 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 estetic 
 point of view, but also from the practical point of view. Being 
 notations that resemble the ones used in the original paper. We believe
 this a important part of every formalization, not only for the estetic 
 point of view, but also from the practical point of view. Being 

-consistent allows to follow the paper in a pedantic way. 
+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. 

 
 Orientering
 -----------
 
 TODO 
 
 
 Orientering
 -----------
 
 TODO 
 

-buttons, PG-interaction-model, sequent window, script window
+buttons, PG-interaction-model, sequent window, script window, ncheck

 
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):
 
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):


@@ -446,32 +448,69 @@ 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". *)
  (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". *) napply H1;
-    (** screenshot "def-fish-rec-3". *) napply p;
+(*DOCBEGIN
+![fish proof step][def-fish-rec-1]
+Note the first item of the context, it is the corecursive function we are 
+defining. This item allows to perform the recursive call, but we will be
+allowed to do such call only after having generated a constructor of
+the fish coinductive type.
+
+We introduce `a` and `p`, and then return the fish constructor `cfish`.
+Since the constructor accepts two arguments, the system asks for them.
+DOCEND*)
+#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
+(*DOCBEGIN
+![fish proof step][def-fish-rec-2]
+The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
+With the `nchange` tactic we change `H1` into an equivalent form (this step
+can be skipped, since the systeem would be able to unfold the definition
+of inclusion by itself)
+DOCEND*) 
+##[ nchange in H1 with (∀b.b∈P → b∈U);
+
+    (** screenshot "def-fish-rec-2-1". *) napply H1;
+    (** screenshot "def-fish-rec-3". *) nassumption;
+(*DOCBEGIN
+![fish proof step][def-fish-rec-2-1]
+It is now clear that `H1` can be applied. Again `napply` adds two 
+implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
+that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
+`a`, and it asks a proof that `a ∈ P`.
+![fish proof step][def-fish-rec-3]
+The `nassumption` tactic looks for the required proof in the context, and in
+that cases finds it in the last context position. 
+
+We move now to the second branch of the proof, corresponding to the second
+argument of the `cfish` constructor.
+![fish proof step][def-fish-rec-4]
+DOCEND*)

 ##| (** screenshot "def-fish-rec-4". *) #i; ncases (H2 a p i); 
     (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP;
 ##| (** screenshot "def-fish-rec-4". *) #i; ncases (H2 a p i); 
     (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP;

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

     ##[ (** screenshot "def-fish-rec-6". *) napply x
     ##| (** screenshot "def-fish-rec-7". *)
         @; ##[ napply xC; 
            ##| (** screenshot "def-fish-rec-8". *) 
                napply (fish_rec ? U P); 
     ##[ (** screenshot "def-fish-rec-6". *) napply x
     ##| (** screenshot "def-fish-rec-7". *)
         @; ##[ napply xC; 
            ##| (** screenshot "def-fish-rec-8". *) 
                napply (fish_rec ? U P); 

+               (** screenshot "def-fish-rec-9". *)

                nassumption;
            ##]
     ##]
 ##]
 nqed.
                nassumption;
            ##]
     ##]
 ##]
 nqed.

-

 (*DOCBEGIN
 (*DOCBEGIN

-![fish proof step][def-fish-rec-1]
-![fish proof step][def-fish-rec-2]
-![fish proof step][def-fish-rec-3]
-![fish proof step][def-fish-rec-4]
+We introduce `i` and then we destruct `H2 a p i`, that being a proof
+of an overlap predicate, give as an element and a proof that it is 
+both in `𝐂 a i` and `P`.

 ![fish proof step][def-fish-rec-5]
 ![fish proof step][def-fish-rec-5]

+We then introduce `x`, break the conjunction (the `*;` command is the
+equivalent of `ncases` but operates on the first hypothesis that can
+be introduced. We then introduce the two sides of the conjuction.
+![fish proof step][def-fish-rec-5-1]

 ![fish proof step][def-fish-rec-6]
 ![fish proof step][def-fish-rec-7]
 ![fish proof step][def-fish-rec-8]
 ![fish proof step][def-fish-rec-6]
 ![fish proof step][def-fish-rec-7]
 ![fish proof step][def-fish-rec-8]

+![fish proof step][def-fish-rec-9]

 DOCEND*)
 
 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 DOCEND*)
 
 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.