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 6b2b73f881f5aa4ef29989ee24a763a212c459db..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 
 


@@ -322,6 +317,9 @@ interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
 
 (*D
 
 
 (*D
 

+The cover relation
+------------------
+

 We can now define the cover relation using the `◃` notation for 
 the premise of infinity. 
 
 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
 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*)
 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
 
 
 (*D
 

+Introction rule for fish
+------------------------
+

 Matita is able to generate elimination rules for inductive types,
 but not introduction rules for the coinductive case. 
 
 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*)
 

+(*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).
 
 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).  
 
 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.
 
 ##]
 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 }.
 
 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. 
 
 #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] ≝ { 
 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
   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.
 
 ##]
 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