...

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 6b2b73f881f5aa4ef29989ee24a763a212c459db..b372d94a3842fd3999a943f8c832aeb2eec1eb83 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -322,6 +322,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 +412,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 +440,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 +550,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.
+
+*)
+

 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.
+
+*)
+

 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 +600,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.
+
+*) 
+

 notation "⋉F" non associative with precedence 55
 for @{ 'fished $F }.
 
 notation "⋉F" non associative with precedence 55
 for @{ 'fished $F }.
 


@@ -592,8 +631,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
+-----------------------------
+
+*)
+

 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