From f6a58913ab59cd0e706d577c5363b03a126731a2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 23 Sep 2009 14:58:40 +0000
Subject: [PATCH] ...

---
 .../software/matita/nlibrary/topology/igft.ma | 208 ++++++++++++++----
 1 file changed, 168 insertions(+), 40 deletions(-)

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 50a62bff4..235583819 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -3,30 +3,77 @@
 Matita Tutorial: inductively generated formal topologies
 ======================================================== 
 
-Small intro...
+This is a not so short introduction to Matita, based on
+the formalization of the paper
 
-Initial setup
--------------
+> 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. 
+
+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):
 
-- `Ω` can be typed \Omega 
-- `∀` \Forall
-- `λ` \lambda
-- `≝` \def
-- `→` ->
+- ∀ `\Forall`
+- λ `\lambda`
+- ≝ `\def`
+- → `->`
+
+Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
 
-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
 
-Axiom set
----------
+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, ...
 
@@ -38,37 +85,125 @@ nrecord Ax : Type[1] ≝ {
   C: ∀a:S. I a → Ω ^ S
 }.
 
-(*HIDE*)
-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 }.
-(*UNHIDE*)
+(*DOCBEGIN
+
+TODO: coercion S.
+
+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
 
-Notation for the axiom set
---------------------------
+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`). Matita performs 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, and to fix this minor issue
+we have to introduce the notational support built in Matita.
+
+Notation for I and C
+--------------------
+
+Matita is quipped qith 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. 
 
-bla bla
+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 `𝐂`. Notationa 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).
 
 (*DOCBEGIN
 
-The first definition
---------------------
+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.
 
-![bla bla][def-fish-rec]
+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*)
 
-ndefinition cover_set ≝ λc:∀A:Ax.Ω^A → A → CProp[0].λA,C,U.
-  ∀y.y ∈ C → c A U y.
+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
@@ -83,7 +218,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.
@@ -274,9 +409,11 @@ 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;(** screenshot "topology/figure1". *)  
+#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'; 
@@ -287,17 +424,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.
@@ -341,15 +473,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;
@@ -364,3 +487,8 @@ nelim o;
 ##]
 nqed.
 
+(*DOCBEGIN
+
+[1]: http://upsilon.cc/~zack/research/publications/notation.pdf 
+
+*)
\ No newline at end of file
-- 
2.39.2