Type printed as such, CProp printed as such

[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 b372d94a3842fd3999a943f8c832aeb2eec1eb83..ce02f95df55f5327341d25fa8fc4d4ffcac88bb3 100644 (file)
--- 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
 -----------
 
 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 
 
 
 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.
 
 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 }.
 
 
 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.
 
 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).  
 
 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.
 
 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 }.
 
 notation "⋉F" non associative with precedence 55
 for @{ 'fished $F }.


@@ -636,7 +631,7 @@ nqed.
 Part 2, the new set of axioms
 -----------------------------
 
 Part 2, the new set of axioms
 -----------------------------
 

-*)
+D*)

 
 nrecord nAx : Type[2] ≝ { 
   nS:> setoid; 
 
 nrecord nAx : Type[2] ≝ { 
   nS:> setoid; 


@@ -822,6 +817,58 @@ nelim o;
 ##]
 nqed.
 
 ##]
 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 
 (*D
 
 [1]: http://upsilon.cc/~zack/research/publications/notation.pdf