X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=66c7dd3a14e9dd9811d43847bb3aef37d7c0d829;hb=8d321a03cf328b85fe7c084bb22685673633d2ee;hp=a4ac5d46914340de617c304a9b3d40937c53113a;hpb=590b41b39d52ae1e320bf1c01220b06fadb1ba8d;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index a4ac5d469..66c7dd3a1 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -448,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". *)
-#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-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-9". *)
                nassumption;
            ##]
     ##]
 ##]
 nqed.
-
 (*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]
+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-9]
 DOCEND*)
 
 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.