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

(*D

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. 

The tutorial spends a considerable amount of effort in defining 
notations that resemble the ones used in the original paper. We believe
this a important part of every formalization, not only for the estetic 
point of view, but also from the practical point of view. Being 
consistent allows to follow the paper in a pedantic way, and hopefully
to make the formalization (at least the definitions and proved
statements) readable to the author of the paper. 

Orientering
-----------



TODO 

buttons, PG-interaction-model, sequent window, script window, ncheck

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` 
- A ≬ B `A \between 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: 

D*)

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

(*D

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

D*)

nrecord Ax : Type[1] ≝ { 
  S :> setoid;
  I :  S → Type[0];
  C :  ∀a:S. I a → Ω ^ S
}.

(*D

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.

D*) 

(* ncheck I. *)
(* ncheck C. *)

(*D

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

D*) 

(* ncheck (∀A:Ax.∀a:A.I ? a). *)

(*D

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.   

D*)

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

(*D

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.

D*)

interpretation "I" 'I a = (I ? a).
interpretation "C" 'C a i = (C ? a i).

(*D

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

D*)

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

(*D

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

Before defining the cover relation as an inductive predicate, one
has to notice that the infinity rule uses, in its hypotheses, the 
cover relation between two subsets, while the inductive predicate 
we are going to define relates an element and a subset.

An option would be to unfold the definition of cover between subsets,
but we prefer to define the abstract notion of cover between subsets
(so that we can attach a (ambiguous) notation to it).

Anyway, to ease the understaing of the definition of the cover relation 
between subsets, we first define the inductive predicate unfolding the 
definition, and we later refine it with.

D*)

ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ 
| xcreflexivity : ∀a:A. a ∈ U → xcover A U a
| xcinfinity    : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a.

(*D

We defined the xcover (x will be removed in the final version of the 
definition) as an inductive predicate. The arity of the inductive
predicate has to be carefully analyzed:

>  (A : Ax) (U : Ω^A) : A → CProp[0]

The syntax separates with `:` abstractions that are fixed for every
constructor (introduction rule) and abstractions that can change. In that 
case the parameter `U` is abstracted once and forall in front of every 
constructor, and every occurrence of the inductive predicate is applied to
`U` in a consistent way. Arguments abstracted on the right of `:` are not
constant, for example the xcinfinity constructor introduces `a ◃ U`,
but under the assumption that (for every y) `y ◃ U`. In that rule, the left
had side of the predicate changes, thus it has to be abstrated (in the arity
of the inductive predicate) on the right of `:`.

D*)

(* ncheck xcreflexivity. *)

(*D

We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define
a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached.

This notion has to be abstracted over the cover relation (whose
type is the arity of the inductive `xcover` predicate just defined).

Then it has to be abstracted over the arguments of that cover relation,
i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
sitting on the left hand side of `◃`. 

D*)

ndefinition cover_set : 
  ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0] 
≝ 
  λcover.                           λA,    C,U.     ∀y.y ∈ C → cover A U y.

(*D

The `ndefinition` command takes a name, a type and body (of that type).
The type can be omitted, and in that case it is inferred by the system.
If the type is given, the system uses it to infer implicit arguments
of the body. In that case all types are left implicit in the body.

We now define the notation `a ◃ b`. Here the keywork `hvbox`
and `break` tell the system how to wrap text when it does not
fit the screen (they can be safely ignore for the scope of
this tutorial). we also add an interpretation for that notation, 
where the (abstracted) cover relation is implicit. The system
will not be able to infer it from the other arguments `C` and `U`
and will thus prompt the user for it. This is also why we named this 
interpretation `covers set temp`: we will later define another 
interpretation in which the cover relation is the one we are going to 
define.

D*)

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

(*D

The cover relation
------------------

We can now define the cover relation using the `◃` notation for 
the premise of infinity. 

D*)

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

(*D

Note that the system accepts the definition
but prompts the user for the relation the `cover_set` notion is
abstracted on.



The orizontal line separates the hypotheses from the conclusion.
The `napply cover` command tells the system that the relation
it is looking for is exactly our first context entry (i.e. the inductive
predicate we are defining, up to α-conversion); while the `nqed` command
ends a definition or proof.

We can now define the interpretation for the cover relation between an
element and a subset fist, then between two subsets (but this time
we fixed the relation `cover_set` is abstracted on).

D*)

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

(*D

We will proceed similarly for the fish relation, but before going
on it is better to give a short introduction to the proof mode of Matita.
We define again the `cover_set` term, but this time we will build
its body interactively. In λ-calculus Matita is based on, CIC, proofs
and terms share the same syntax, and it thus possible to use the
commands devoted to build proof term to build regular definitions.

D*)

ndefinition xcover_set : 
  ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]. 
                         (** screenshot "xcover-set-1". *)
#cover; #A; #C; #U;      (** screenshot "xcover-set-2". *) 
napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *)
napply cover;            (** screenshot "xcover-set-4". *)
##[ napply A;
##| napply U;
##| napply y;
##]
nqed.

(*D[xcover-set-1]
The system asks for a proof of the full statement, in an empty context.

The `#` command is the ∀-introduction rule, it gives a name to an 
assumption putting it in the context, and generates a λ-abstraction
in the proof term.

D[xcover-set-2]
We have now to provide a proposition, and we exhibit it. We left
a part of it implicit; since the system cannot infer it it will
ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
whenever `?` is.

D[xcover-set-3]
The proposition we want to provide is an application of the
cover relation we have abstracted in the context. The command
`napply`, if the given term has not the expected type (in that
case it is a product versus a proposition) it applies it to as many 
implicit arguments as necessary (in that case `? ? ?`).

D[xcover-set-4]
The system will now ask in turn the three implicit arguments 
passed to cover. The syntax `##[` allows to start a branching
to tackle every sub proof individually, otherwise every command
is applied to every subrpoof. The command `##|` switches to the next
subproof and `##]` ends the branching.  
D*)

(*D

The fish relation
-----------------

The definition of fish works exactly the same way as for cover, except 
that it is defined as a coinductive proposition.
D*)

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

(*D

Introction rule for fish
------------------------

Matita is able to generate elimination rules for inductive types,
but not introduction rules for the coinductive case. 

D*)

(* ncheck cover_rect_CProp0. *) 

(*D

We thus have to define the introduction rule for fish by corecursion.
Here we again use the proof mode of Matita to exhibit the body of the
corecursive function.

D*)

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 ≝ ?.
                                       (** screenshot "def-fish-rec-1". *)
#a; #p; napply cfish;                  (** screenshot "def-fish-rec-2". *)
##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *) 
    napply H1;                         (** screenshot "def-fish-rec-3". *) 
    nassumption;
##| #i; ncases (H2 a p i);             (** screenshot "def-fish-rec-5". *) 
    #x; *; #xC; #xP;                   (** screenshot "def-fish-rec-5-1". *) 
    @;                                 (** screenshot "def-fish-rec-6". *)
    ##[ napply x
    ##| @;                             (** screenshot "def-fish-rec-7". *)
        ##[ napply xC; 
        ##| napply (fish_rec ? U P);   (** screenshot "def-fish-rec-9". *)
            nassumption;
        ##]
    ##]
##]
nqed.

(*D
D[def-fish-rec-1]
Note the first item of the context, it is the corecursive function we are 
defining. This item allows to perform the recursive call, but we will be
allowed to do such call only after having generated a constructor of
the fish coinductive type.

We introduce `a` and `p`, and then return the fish constructor `cfish`.
Since the constructor accepts two arguments, the system asks for them.

D[def-fish-rec-2]
The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`.
With the `nchange` tactic we change `H1` into an equivalent form (this step
can be skipped, since the systeem would be able to unfold the definition
of inclusion by itself)

D[def-fish-rec-2-1]
It is now clear that `H1` can be applied. Again `napply` adds two 
implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof
that `? ∈ P`. Thanks to unification, the system understands that `?` is actually
`a`, and it asks a proof that `a ∈ P`.

D[def-fish-rec-3]
The `nassumption` tactic looks for the required proof in the context, and in
that cases finds it in the last context position. 

We move now to the second branch of the proof, corresponding to the second
argument of the `cfish` constructor.

We introduce `i` and then we destruct `H2 a p i`, that being a proof
of an overlap predicate, give as an element and a proof that it is 
both in `𝐂 a i` and `P`.

D[def-fish-rec-5]
We then introduce `x`, break the conjunction (the `*;` command is the
equivalent of `ncases` but operates on the first hypothesis that can
be introduced. We then introduce the two sides of the conjuction.

D[def-fish-rec-5-1]
The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
We thus need to use the introduction rulle for the existential quantifier.
In CIC it is a defined notion, that is an inductive type with just
one constructor (one introduction rule) holding the witness and the proof
that the witness satisfies a proposition.

> ncheck Ex.

Instead of trying to remember the name of the constructor, that should
be used as the argument of `napply`, we can ask the system to find by
itself the constructor name and apply it with the `@` tactic. 
Note that some inductive predicates, like the disjunction, have multiple
introduction rules, and thus `@` can be followed by a number identifying
the constructor.

D[def-fish-rec-6]
After choosing `x` as the witness, we have to prove a conjunction,
and we again apply the introduction rule for the inductively defined
predicate `∧`.

D[def-fish-rec-7]
The left hand side of the conjunction is trivial to prove, since it 
is already in the context. The right hand side needs to perform
the co-recursive call.

D[def-fish-rec-9]
The co-recursive call needs some arguments, but all of them live
in the context. Instead of explicitly mention them, we use the
`nassumption` tactic, that simply tries to apply every context item.

D*)

(*D

Subset of covered/fished points
-------------------------------

We now have to define the subset of `S` of points covered by `U`.
We also define a prefix notation for it. Remember that the precedence
of the prefix form of a symbol has to be lower than the precedence 
of its infix form.

D*)

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

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

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

(*D

Here we define the equation characterizing the cover relation. 
In the igft.ma file we proved that `◃U` is the minimum solution for
such equation, the interested reader should be able to reply the proof
with Matita.

D*)

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.

(*D

We similarly define the subset of point fished by `F`, the 
equation characterizing `⋉F` and prove that fish is
the biggest solution for such equation.

D*) 

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. 

(*D

Part 2, the new set of axioms
-----------------------------

D*)

nrecord nAx : Type[2] ≝ { 
  nS:> setoid; 
  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.

(*D

Bla Bla, 


D*)

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.


(*D
Appendix: natural deduction like tactics explanation
-----------------------------------------------------

In this appendix we try to give a description of tactics
in terms of natural deduction rules annotated with proofs.
The `:` separator has to be read as _is a proof of_, in the spirit
of the Curry-Howard isomorphism.

                  f  :  A1 → … → An → B    ?1 : A1 … ?n  :  An 
    napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
                           (f ?1 … ?n )  :  B
 
foo  

                               [x : T]
                                  ⋮  
                               ?  :  P(x) 
    #x;         ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
                            λx:T.?  :  ∀x:T.P(x)

baz
                       
                 (?1 args1)  :  P(k1 args1)  …  (?n argsn)  :  P(kn argsn)         
    ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
                   match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n  :  P(x)                    

bar

                                             [ IH  :  P(t) ]
                                                   ⋮
                 x  :  T      ?1  :  P(k1)  …  ?n  :  P(kn t)         
    nelim x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
                   (T_rect_CProp0 ?1 … ?n)  :  P(x)                    

Where `T_rect_CProp0` is the induction principle for the 
inductive type `T`.

                           ?  :  Q     Q ≡ P          
    nchange with Q;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
                           ?  :  P                    

Where the equivalence relation between types `≡` keeps into account
β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
definition unfolding), ι-reduction (pattern matching simplification),
μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
computation).

D*)


(*D

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

*)