X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=3c97b9c25000735971c09018c1a1f4c42a6e86a3;hb=a8aaa095aad443c8eca8f64e3f22f54615e8dd9b;hp=7f4f5e3591724cfef8502d4659fbc1e3574a89c9;hpb=e956eab1116ae48a298e3c6701f93178e53ab24f;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 7f4f5e359..3c97b9c25 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -1,22 +1,241 @@
+(*DOCBEGIN
+
+Matita Tutorial: inductively generated formal topologies
+======================================================== 
+
+This is a not so short introduction to Matita, based on
+the formalization of the paper
+
+> Between formal topology and game theory: an
+> explicit solution for the conditions for an
+> inductive generation of formal topologies
+
+by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi. 
+
+Orientering
+-----------
+
+TODO 
+
+buttons, PG-interaction-model, sequent window, script window
+
+The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
+Symbols (see menu: View ▹ TeX/UTF-8 Table):
+
+- ∀ `\Forall`
+- λ `\lambda`
+- ≝ `\def`
+- → `->`
+
+Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
+
+The standard library and the `include` command
+----------------------------------------------
+
+Some basic notions, like subset, membership, intersection and union
+are part of the standard library of Matita.
+
+These notions come with
+some notation attached to them:
+
+- A ∪ B `A \cup B`
+- A ∩ B `A \cap B` 
+- x ∈ A `x \in A` 
+- Ω^A, that is the type of the subsets of A, `\Omega ^ A` 
+
+The `include` command tells Matita to load a part of the library, 
+in particular the part that we will use can be loaded as follows: 
+
+DOCEND*)
+
 include "sets/sets.ma".
 
+(*HIDE*)
+(* move away *)
+nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
+#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
+nqed.
+
+nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
+#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
+nqed. 
+
+nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
+#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
+nqed. 
+(*UNHIDE*)
+
+(*DOCBEGIN
+
+Some basic results that we will use are also part of the sets library:
+
+- subseteq\_union\_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W
+- subseteq\_intersection\_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V
+
+Defining Axiom set
+------------------
+
+records, projections, types of projections..
+
+DOCEND*)
+
 nrecord Ax : Type[1] ≝ { 
-  S:> setoid; (* Type[0]; *)
-  I: S → Type[0];
-  C: ∀a:S. I a → Ω ^ S
+  S :> setoid;
+  I :  S → Type[0];
+  C :  ∀a:S. I a → Ω ^ S
 }.
 
-notation "𝐈  \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
-notation "𝐂 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
+(*DOCBEGIN
+
+Note that the field `S` was declared with `:>` instead of a simple `:`.
+This declares the `S` projection to be a coercion. A coercion is 
+a function case the system automatically inserts when it is needed.
+In that case, the projection `S` has type `Ax → setoid`, and whenever
+the expected type of a term is `setoid` while its type is `Ax`, the 
+system inserts the coercion around it, to make the whole term well types.
+
+When formalizing an algebraic structure, declaring the carrier as a 
+coercion is a common practice, since it allows to write statements like
+
+    ∀G:Group.∀x:G.x * x^-1 = 1 
+
+The quantification over `x` of type `G` is illtyped, since `G` is a term
+(of type `Group`) and thus not a type. Since the carrier projection 
+`carr` of `G` is a coercion, that maps a `Group` into the type of 
+its elements, the system automatically inserts `carr` around `G`, 
+obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
+when it displays a term.
+
+In this particular case, the coercion `S` allows to write
+
+    ∀A:Ax.∀a:A.…
+
+Since `A` is not a type, but it can be turned into a `setoid` by `S`
+and a `setoid` can be turned into a type by its `carr` projection, the 
+composed coercion `carr ∘ S` is silently inserted.
+
+Implicit arguments
+------------------
+
+Something that is not still satisfactory, in that the dependent type
+of `I` and `C` are abstracted over the Axiom set. To obtain the
+precise type of a term, you can use the `ncheck` command as follows.
+
+DOCEND*) 
+
+(* ncheck I. *)
+(* ncheck C. *)
+
+(*DOCBEGIN
+
+One would like to write `I a` and not `I A a` under a context where
+`A` is an axiom set and `a` has type `S A` (or thanks to the coercion
+mecanism simply `A`). In Matita, a question mark represents an implicit
+argument, i.e. a missing piece of information the system is asked to
+infer. Matita performs some sort of type inference, thus writing
+`I ? a` is enough: since the second argument of `I` is typed by the 
+first one, the first one can be inferred just computing the type of `a`.
+
+DOCEND*) 
+
+(* ncheck (∀A:Ax.∀a:A.I ? a). *)
+
+(*DOCBEGIN
+
+This is still not completely satisfactory, since you have always type 
+`?`; to fix this minor issue we have to introduce the notational
+support built in Matita.
+
+Notation for I and C
+--------------------
+
+Matita is quipped with a quite complex notational support,
+allowing the user to define and use mathematical notations 
+([From Notation to Semantics: There and Back Again][1]). 
+
+Since notations are usually ambiguous (e.g. the frequent overloading of 
+symbols) Matita distinguishes between the term level, the 
+content level, and the presentation level, allowing multiple 
+mappings between the contenet and the term level. 
+
+The mapping between the presentation level (i.e. what is typed on the 
+keyboard and what is displayed in the sequent window) and the content
+level is defined with the `notation` command. When followed by
+`>`, it defines an input (only) notation.   
+
+DOCEND*)
 
 notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }.
 notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }.
 
+(*DOCBEGIN
+
+The forst notation defines the writing `𝐈 a` where `a` is a generic
+term of precedence 90, the maximum one. This high precedence forces
+parentheses around any term of a lower precedence. For example `𝐈 x`
+would be accepted, since identifiers have precedence 90, but
+`𝐈 f x` would be interpreted as `(𝐈 f) x`. In the latter case, parentheses
+have to be put around `f x`, thus the accepted writing would be `𝐈 (f x)`.
+
+To obtain the `𝐈` is enough to type `I` and then cycle between its
+similar symbols with ALT-L. The same for `𝐂`. Notations cannot use
+regular letters or the round parentheses, thus their variants (like the 
+bold ones) have to be used.
+
+The first notation associates `𝐈 a` with `'I $a` where `'I` is a 
+new content element to which a term `$a` is passed.
+
+Content elements have to be interpreted, and possibly multiple, 
+incompatible, interpretations can be defined.
+
+DOCEND*)
+
 interpretation "I" 'I a = (I ? a).
 interpretation "C" 'C a i = (C ? a i).
 
-ndefinition cover_set ≝ λc:∀A:Ax.Ω^A → A → CProp[0].λA,C,U.
-  ∀y.y ∈ C → c A U y.
+(*DOCBEGIN
+
+The `interpretation` command allows to define the mapping between
+the content level and the terms level. Here we associate the `I` and
+`C` projections of the Axiom set record, where the Axiom set is an implicit 
+argument `?` to be inferred by the system.
+
+Interpretation are bi-directional, thus when displaying a term like 
+`C _ a i`, the system looks for a presentation for the content element
+`'C a i`. 
+
+DOCEND*)
+
+notation < "𝐈  \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }.
+notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }.
+
+(*DOCBEGIN
+
+For output purposes we can define more complex notations, for example
+we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing
+the size of the arguments and lowering their baseline (i.e. putting them
+as subscript), separating them with a comma followed by a little space.
+
+The first (technical) definition
+--------------------------------
+
+
+
+DOCEND*)
+
+ndefinition cover_set : 
+  ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0] 
+≝ 
+  λc: ∀A:Ax.Ω^A → A → CProp[0]. λA,C,U.∀y.y ∈ C → c A U y.
+
+ndefinition cover_set_interactive : 
+  ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]. 
+#cover; #A; #C; #U; napply (∀y:A.y ∈ C → ?); napply cover;
+##[ napply A;
+##| napply U;
+##| napply y;
+##]
+nqed.
 
 (* a \ltri b *)
 notation "hvbox(a break ◃ b)" non associative with precedence 45
@@ -31,7 +250,7 @@ napply cover;
 nqed.
 
 interpretation "covers" 'covers a U = (cover ? U a).
-interpretation "covers set" 'covers a U = (cover_set cover ? a U).
+(* interpretation "covers set" 'covers a U = (cover_set cover ? a U). *)
 
 ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
  λA,U,V.
@@ -55,7 +274,7 @@ nlet corec fish_rec (A:Ax) (U: Ω^A)
  (P: Ω^A) (H1: P ⊆ U)
   (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P):
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
-#a; #p; napply cfish;
+#a; #p; napply cfish; (** screenshot "def-fish-rec". *)
 ##[ napply H1; napply p;
 ##| #i; ncases (H2 a p i); #x; *; #xC; #xP; @; ##[napply x]
     @; ##[ napply xC ] napply (fish_rec ? U P); nassumption;
@@ -207,12 +426,27 @@ naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.
 naxiom setoidification :
   ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
 
+(*DOCBEGIN
+
+Bla Bla, 
+
+<div id="figure1" class="img" ><img src="figure1.png"/>foo</div>
+
+DOCEND*)
+
+alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
 alias symbol "covers" = "new covers".
 alias symbol "covers" = "new covers set".
 alias symbol "covers" = "new covers".
 ntheorem new_coverage_infinity:
   ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
-#A; #U; #a; *; #i; #H; nnormalize in H;
+#A; #U; #a;(** screenshot "figure1". *)  
+*; #i; #H; nnormalize in H;
 ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[
   #y; napply H; @ y; napply #; ##] #H'; 
 ncases (AC … H'); #f; #Hf;
@@ -222,17 +456,12 @@ ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
 napply (setoidification … Hd); napply Hf';
 nqed.
 
-(* move away *)
-nlemma subseteq_union: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
-#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
-nqed. 
-
 nlemma new_coverage_min :  
   ∀A:nAx.∀U:qpowerclass A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃(pc ? U) ⊆ V.
 #A; #U; #V; #HUV; #Im;  #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)⎽o ⊆ V);
 nelim o;
 ##[ #b; #bU0; napply HUV; napply bU0;
-##| #p; #IH; napply subseteq_union; ##[ nassumption; ##]
+##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
     #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
 ##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
 nqed.
@@ -276,15 +505,6 @@ ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
 napply aLf';
 nqed.
 
-(* move away *)
-nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
-#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption;
-nqed.
-
-nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
-#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption;
-nqed. 
- 
 ntheorem max_new_fished: 
   ∀A:nAx.∀G,F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
 #A; #G; #F; #GF; #H; #b; #HbG; #o; ngeneralize in match HbG; ngeneralize in match b;
@@ -299,3 +519,8 @@ nelim o;
 ##]
 nqed.
 
+(*DOCBEGIN
+
+[1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
+
+*)
\ No newline at end of file