+(*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
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.
(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;
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;
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.
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;
##]
nqed.
+(*DOCBEGIN
+
+[1]: http://upsilon.cc/~zack/research/publications/notation.pdf
+
+*)
\ No newline at end of file
projects / helm.git / blobdiff