X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=ce02f95df55f5327341d25fa8fc4d4ffcac88bb3;hb=e91e815449698c6f2595958f94cd06c10ba10398;hp=6b2b73f881f5aa4ef29989ee24a763a212c459db;hpb=3cb42e0873c101c6c5a8b9967d765b5135882685;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 6b2b73f88..ce02f95df 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -22,13 +22,8 @@ statements) readable to the author of the paper.
 
 Orientering
 -----------
-                                 ? : A 
-apply (f : A -> B):    --------------------
-                            (f ? ) :   B
 
-                         f: A1 -> ... -> An -> B    ?1: A1 ... ?n: An
-apply (f : A -> B):    ------------------------------------------------
-                            apply f == f \ldots == f ? ... ? :   B
+
 
 TODO 
 
@@ -322,6 +317,9 @@ interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
 
 (*D
 
+The cover relation
+------------------
+
 We can now define the cover relation using the `◃` notation for 
 the premise of infinity. 
 
@@ -409,6 +407,10 @@ subproof and `##]` ends the branching.
 D*)
 
 (*D
+
+The fish relation
+-----------------
+
 The definition of fish works exactly the same way as for cover, except 
 that it is defined as a coinductive proposition.
 D*)
@@ -433,6 +435,9 @@ interpretation "fish" 'fish a U = (fish ? U a).
 
 (*D
 
+Introction rule for fish
+------------------------
+
 Matita is able to generate elimination rules for inductive types,
 but not introduction rules for the coinductive case. 
 
@@ -540,12 +545,33 @@ in the context. Instead of explicitly mention them, we use the
 
 D*)
 
+(*D
+
+Subset of covered/fished points
+-------------------------------
+
+We now have to define the subset of `S` of points covered by `U`.
+We also define a prefix notation for it. Remember that the precedence
+of the prefix form of a symbol has to be lower than the precedence 
+of its infix form.
+
+D*)
+
 ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.
 
 notation "◃U" non associative with precedence 55 for @{ 'coverage $U }.
 
 interpretation "coverage cover" 'coverage U = (coverage ? U).
 
+(*D
+
+Here we define the equation characterizing the cover relation. 
+In the igft.ma file we proved that `◃U` is the minimum solution for
+such equation, the interested reader should be able to reply the proof
+with Matita.
+
+D*)
+
 ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝  λA,U,X. 
   ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X).  
 
@@ -569,6 +595,14 @@ ntheorem coverage_min_cover_equation :
 ##]
 nqed.
 
+(*D
+
+We similarly define the subset of point fished by `F`, the 
+equation characterizing `⋉F` and prove that fish is
+the biggest solution for such equation.
+
+D*) 
+
 notation "⋉F" non associative with precedence 55
 for @{ 'fished $F }.
 
@@ -592,8 +626,15 @@ ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
 #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; 
 nqed. 
 
+(*D
+
+Part 2, the new set of axioms
+-----------------------------
+
+D*)
+
 nrecord nAx : Type[2] ≝ { 
-  nS:> setoid; (*Type[0];*)
+  nS:> setoid; 
   nI: nS → Type[0];
   nD: ∀a:nS. nI a → Type[0];
   nd: ∀a:nS. ∀i:nI a. nD a i → nS
@@ -776,6 +817,58 @@ nelim o;
 ##]
 nqed.
 
+
+(*D
+Appendix: natural deduction like tactics explanation
+-----------------------------------------------------
+
+In this appendix we try to give a description of tactics
+in terms of natural deduction 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 
+    napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                           (f ?1 … ?n )  :  B
+ 
+foo  
+
+                               [x : T]
+                                  ⋮  
+                               ?  :  P(x) 
+    #x;         ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                            λx:T.?  :  ∀x:T.P(x)
+
+baz
+                       
+                 (?1 args1)  :  P(k1 args1)  …  (?n argsn)  :  P(kn argsn)         
+    ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                   match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n  :  P(x)                    
+
+bar
+
+                                             [ IH  :  P(t) ]
+                                                   ⋮
+                 x  :  T      ?1  :  P(k1)  …  ?n  :  P(kn t)         
+    nelim x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                   (T_rect_CProp0 ?1 … ?n)  :  P(x)                    
+
+Where `T_rect_CProp0` is the induction principle for the 
+inductive type `T`.
+
+                           ?  :  Q     Q ≡ P          
+    nchange with Q;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                           ?  :  P                    
+
+Where the equivalence relation between types `≡` keeps into account
+β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).
+
+D*)
+
+
 (*D
 
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf