From 9730627f1ab5a6071f7e3f615e23bf6696f7041e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 25 Sep 2009 18:01:44 +0000
Subject: [PATCH] ...

---
 .../software/matita/nlibrary/topology/igft.ma | 67 ++++++++++++++++---
 1 file changed, 57 insertions(+), 10 deletions(-)

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index b372d94a3..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 
 
@@ -560,7 +555,7 @@ 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 }.
 
@@ -575,7 +570,7 @@ 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).  
@@ -606,7 +601,7 @@ 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 }.
@@ -636,7 +631,7 @@ nqed.
 Part 2, the new set of axioms
 -----------------------------
 
-*)
+D*)
 
 nrecord nAx : Type[2] ≝ { 
   nS:> setoid; 
@@ -822,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 
-- 
2.39.2