From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 25 Sep 2009 15:39:03 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3434
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a436718fd9b50340f5535cef223399c5813d9869;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 6b2b73f88..b372d94a3 100644
--- 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
 
+The cover relation
+------------------
+
 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
+
+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 +440,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 +550,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.
+
+*)
+
 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).  
 
@@ -569,6 +600,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.
+
+*) 
+
 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. 
 
+(*D
+
+Part 2, the new set of axioms
+-----------------------------
+
+*)
+
 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