[helm.git] / helm / software / matita / nlibrary / topology / igft.ma

(*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;
  I :  S → Type[0];
  C :  ∀a:S. I a → Ω ^ S
}.

(*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).

(*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
for @{ 'covers $a $b }.

interpretation "covers set temp" 'covers C U = (cover_set ?? C U).

ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ 
| creflexivity : ∀a:A. a ∈ U → cover ? U a
| cinfinity    : ∀a:A.∀i:𝐈 a. 𝐂 a i ◃ U → cover ? U a.
napply cover;
nqed.

interpretation "covers" 'covers a U = (cover ? U a).
(* interpretation "covers set" 'covers a U = (cover_set cover ? a U). *)

ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0].
 λA,U,V.
  ∃a.a ∈ V ∧ f A U a.

(* a \ltimes b *)
notation "hvbox(a break ⋉ b)" non associative with precedence 45
for @{ 'fish $a $b }. 

interpretation "fish set temp" 'fish A U = (fish_set ?? U A).

ncoinductive fish (A : Ax) (F : Ω^A) : A → CProp[0] ≝ 
| cfish : ∀a. a ∈ F → (∀i:𝐈 a .𝐂  a i ⋉ F) → fish A F a.
napply fish;
nqed.

interpretation "fish set" 'fish A U = (fish_set fish ? U A).
interpretation "fish" 'fish a U = (fish ? U a).

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; (** 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;
##]
nqed.

notation "◃U" non associative with precedence 55
for @{ 'coverage $U }.

ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }.

interpretation "coverage cover" 'coverage U = (coverage ? U).

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).  

ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
#A; #U; #a; @; #H;
##[ nelim H; #b; (* manca clear *)
    ##[ #bU; @1; nassumption;
    ##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
        ##[ #E; @; napply E;
        ##| #_; napply CaiU; nassumption; ##] ##]
##| ncases H; ##[ #E; @; nassumption]
    *; #j; #Hj; @2 j; #w; #wC; napply Hj; nassumption;
##]
nqed. 

ntheorem coverage_min_cover_equation : 
  ∀A,U,W. cover_equation A U W → ◃U ⊆ W.
#A; #U; #W; #H; #a; #aU; nelim aU; #b;
##[ #bU; ncases (H b); #_; #H1; napply H1; @1; nassumption;
##| #i; #CbiU; #IH; ncases (H b); #_; #H1; napply H1; @2; @i; napply IH;
##]
nqed.

notation "⋉F" non associative with precedence 55
for @{ 'fished $F }.

ndefinition fished : ∀A:Ax.∀F:Ω^A.Ω^A ≝ λA,F.{ a | a ⋉ F }.

interpretation "fished fish" 'fished F = (fished ? F).

ndefinition fish_equation : ∀A:Ax.∀F,X:Ω^A.CProp[0] ≝ λA,F,X.
  ∀a. a ∈ X ↔ a ∈ F ∧ ∀i:𝐈 a.∃y.y ∈ 𝐂 a i ∧ y ∈ X. 
  
ntheorem fised_fish_equation : ∀A,F. fish_equation A F (⋉F).
#A; #F; #a; @; (* bug, fare case sotto diverso da farlo sopra *) #H; ncases H;
##[ #b; #bF; #H2; @ bF; #i; ncases (H2 i); #c; *; #cC; #cF; @c; @ cC;
    napply cF;  
##| #aF; #H1; @ aF; napply H1;
##]
nqed.

ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F.
#A; #F; #G; #H; #a; #aG; napply (fish_rec … aG);
#b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; 
nqed. 

nrecord nAx : Type[2] ≝ { 
  nS:> setoid; (*Type[0];*)
  nI: nS → Type[0];
  nD: ∀a:nS. nI a → Type[0];
  nd: ∀a:nS. ∀i:nI a. nD a i → nS
}.

(*
TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.

a = b → I a = I b
*)

notation "𝐃 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'D $a $i }.
notation "𝐝 \sub ( ❨a,\emsp i,\emsp j❩ )" non associative with precedence 70 for @{ 'd $a $i $j}.

notation > "𝐃 term 90 a term 90 i" non associative with precedence 70 for @{ 'D $a $i }.
notation > "𝐝 term 90 a term 90 i term 90 j" non associative with precedence 70 for @{ 'd $a $i $j}.

interpretation "D" 'D a i = (nD ? a i).
interpretation "d" 'd a i j = (nd ? a i j).
interpretation "new I" 'I a = (nI ? a).

ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.

notation > "𝐈𝐦  [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
notation "𝐈𝐦  [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.

interpretation "image" 'Im a i = (image ? a i).

ndefinition Ax_of_nAx : nAx → Ax.
#A; @ A (nI ?); #a; #i; napply (𝐈𝐦 [𝐝 a i]);
nqed.

ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ 
 sig_intro : ∀x:A.P x → sigma A P. 

interpretation "sigma" 'sigma \eta.p = (sigma ? p). 

ndefinition nAx_of_Ax : Ax → nAx.
#A; @ A (I ?);
##[ #a; #i; napply (Σx:A.x ∈ 𝐂 a i);
##| #a; #i; *; #x; #_; napply x;
##]
nqed.

ninductive Ord (A : nAx) : Type[0] ≝ 
 | oO : Ord A
 | oS : Ord A → Ord A
 | oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.

notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
notation "x+1" non associative with precedence 50 for @{'oS $x }.

interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
interpretation "ordinals Succ" 'oS x = (oS ? x).

nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝ 
  match x with
  [ oO ⇒ U
  | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un} 
  | oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
  
notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.

interpretation "famU" 'famU U x = (famU ? U x).
  
ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.

ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
  ∀y.y ∈ C → y ∈ c A U.

interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).

ntheorem new_coverage_reflexive:
  ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
#A; #U; #a; #H; @ (oO A); napply H;
nqed.

nlemma ord_subset:
  ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
#A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
nqed.

naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).

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;(** 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;
ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
  ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
@ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd; 
napply (setoidification … Hd); napply Hf';
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_l; ##[ nassumption; ##]
    #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
nqed.

nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝ 
  match x with
  [ oO ⇒ F
  | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo } 
  | oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
  ].

interpretation "famF" 'famU U x = (famF ? U x).

ndefinition ord_fished : ∀A:nAx.∀F:Ω^A.Ω^A ≝ λA,F.{ y | ∀x:Ord A. y ∈ F⎽x }.

interpretation "fished new fish" 'fished U = (ord_fished ? U).
interpretation "new fish" 'fish a U = (mem ? (ord_fished ? U) a).

ntheorem new_fish_antirefl:
 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
#A; #F; #a; #H; nlapply (H (oO ?)); #aFo; napply aFo;
nqed.

nlemma co_ord_subset:
 ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
#A; #F; #a; #i; #f; #j; #x; #H; napply H;
nqed.

naxiom AC_dual : 
  ∀A:nAx.∀a:A.∀i,F. (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.


ntheorem new_fish_compatible: 
 ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ⋉ F.
#A; #F; #a; #aF; #i; nnormalize;
napply AC_dual; #f;
nlapply (aF (Λf+1)); #aLf;
nchange in aLf with (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f));
ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
  ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
napply aLf';
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;
nchange with (G ⊆ F⎽o);
nelim o;
##[ napply GF;
##| #p; #IH; napply (subseteq_intersection_r … IH);
    #x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
    @d; napply IH; napply (setoidification … Ed^-1); napply cG;   
##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) }); 
    #b; #Hb; #d; napply (Hf d); napply Hb;
##]
nqed.

(*DOCBEGIN

[1]: http://upsilon.cc/~zack/research/publications/notation.pdf 

*)