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, ...
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
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.
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';
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 / commitdiff