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
+this a important part of every formalization, not only for the aesthetic
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
+Orienteering
-----------
+The graphical interface of Matita is composed of three windows:
+the script window, on the left, is where you type; the sequent
+window on the top right is where the system shows you the ongoing proof;
+the error window, on the bottom right, is where the system complains.
+On the top of the script window five buttons drive the processing of
+the proof script. From left to right the requesting the system to:
+
+- go back to the beginning of the script
+- go back one step
+- go to the current cursor position
+- advance one step
+- advance to the end of the script
+
+When the system processes a command, it locks the part of the script
+corresponding to the command, such that you cannot edit it anymore
+(without to go back). Locked parts are coloured in blue.
+
+The sequent window is hyper textual, i.e. you can click on symbols
+to jump to their definition, or switch between different notation
+for the same expression (for example, equality has two notations,
+one of them makes the type of the arguments explicit).
+
+Everywhere in the script you can use the `ncheck (term).` command to
+ask for the type a given term. If you that in the middle of a proof,
+the term is assumed to live in the current proof context (i.e. can use
+variables introduced so far).
+
+To ease the typing of mathematical symbols, the script window
+implements two unusual input facilities:
+
+- some TeX symbols can be typed using their TeX names, and are
+ automatically converted to UTF-8 characters. For a list of
+ the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
+ Moreover some ASCII-art is understood as well, like `=>` and `->`
+ to mean double or single arrows.
+ Here we recall some of these "shortcuts":
+
+ - ∀ `\Forall`
+ - λ `\lambda`
+ - ≝ `\def` or `:=`
+ - → `to` or `->`
+
+- some symbols have variants, like the ≤ relation and ≲, ≼, ≰, ⋠.
+ The use can cycle between variants typing one them and then
+ pressing ALT-L. Note that also letters do have variants, for
+ example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
+ Variants are listed in the aforementioned TeX/UTF-8 table.
+
+CIC (as implemented in Matita) in a nutshell
+--------------------------------------------
+...
-TODO
+Type is a set equipped with the Id equality (i.e. an intensional,
+not quotiented set). We will avoid using Leibnitz equality Id,
+thus we will explicitly equip a set with an equality when needed.
+We will call this structure `setoid`. Note that we will
+attach the infix = symbols only to the equality of a setoid,
+not to Id.
-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):
+We write Type[i] to mention a Type in the predicative hierarchy
+of types. To ease the comprehension we will use Type[0] for sets,
+and Type[1] for classes.
-- ∀ `\Forall`
-- λ `\lambda`
-- ≝ `\def`
-- → `->`
+For every Type[i] there is a corresponding level of predicative
+propositions CProp[i].
-Virtuals, ALT-L, for example `I` changes into `𝕀`, finally `𝐈`.
+CIC is also equipped with an impredicative sort Prop that we will not
+use in this tutorial.
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:
+These notions come with some standard notation attached to them:
- A ∪ B `A \cup B`
- A ∩ B `A \cap B`
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.
+
+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).
(*UNHIDE*)
(*D
Defining Axiom set
------------------
-records, projections, types of projections..
+A set of axioms is made of a set S, a family of sets I and a
+family C of subsets of S indexed by elements a of S and I(a).
+
+It is desirable to state theorems like "for every set of axioms, …"
+without explicitly mentioning S, I and C. To do that, the three
+components have to be grouped into a record (essentially a dependently
+typed tuple). The system is able to generate the projections
+of the record for free, and they are named as the fields of
+the record. So, given a axiom set `A` we can obtain the set
+with `S A`, the family of sets with `I A` and the family of subsets
+with `C A`.
D*)
(*D
+Forget for a moment the `:>` that will be detailed later, and focus on
+the record definition. It is made of a list of pairs: a name, followed
+by `:` and the its type. It is a dependently typed tuple, thus
+already defined names (fields) can be used in the types that follow.
+
+Note that `S` is declared to be a `setoid` and not a Type. The original
+paper probably also considers I to generate setoids, and both I and C
+to be morphisms. For the sake of simplicity, we will "cheat" and use
+setoids only when strictly needed (i.e. where we want to talk about
+equality). Setoids will play a role only when we will define
+the alternative version of the axiom set.
+
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.
∀G:Group.∀x:G.x * x^-1 = 1
-The quantification over `x` of type `G` is illtyped, since `G` is a term
+The quantification over `x` of type `G` is ill-typed, 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`,
Implicit arguments
------------------
-Something that is not still satisfactory, in that the dependent type
+Something that is not still satisfactory, is 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.
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
+mechanism 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
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.
+mappings between the content 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
(*D
-The forst notation defines the writing `𝐈 a` where `a` is a generic
+The first 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
(*D
For output purposes we can define more complex notations, for example
-we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing
+we can put bold parentheses 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.
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
+Anyway, to ease the understanding of the definition of the cover relation
between subsets, we first define the inductive predicate unfolding the
definition, and we later refine it with.
`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
+had side of the predicate changes, thus it has to be abstracted (in the arity
of the inductive predicate) on the right of `:`.
D*)
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,
+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
-The orizontal line separates the hypotheses from the conclusion.
+The horizontal 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
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
+its body interactively. In the λ-calculus Matita is based on, CIC, proofs
+and terms share the same syntax, and it is thus possible to use the
commands devoted to build proof term to build regular definitions.
+A tentative semantics for the proof mode commands (called tactics)
+in terms of sequent calculus rules are given in the
+<a href="#appendix">appendix</a>.
D*)
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
+can be skipped, since the system would be able to unfold the definition
of inclusion by itself)
D[def-fish-rec-2-1]
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.
+be introduced. We then introduce the two sides of the conjunction.
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.
+We thus need to use the introduction rule 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.
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;
+ntheorem fished_fish_equation : ∀A,F. fish_equation A F (⋉F).
+#A; #F; #a; @; (* *; non genera outtype che lega a *) #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.
+ntheorem fished_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.
Part 2, the new set of axioms
-----------------------------
+Since the name of objects (record included) has to unique
+within the same script, we prefix every field name
+in the new definition of the axiom set with `n`.
+
D*)
nrecord nAx : Type[2] ≝ {
nd: ∀a:nS. ∀i:nI a. nD a i → nS
}.
-(*
-TYPE f A → B, g : B → A, f ∘ g = id, g ∘ g = id.
+(*D
-a = b → I a = I b
-*)
+We again define a notation for the projections, making the
+projected record an implicit argument. Note that since we already have
+a notation for `𝐈` we just add another interpretation for it. The
+system, looking at the argument of `𝐈`, will be able to use
+the correct interpretation.
+
+D*)
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}.
interpretation "d" 'd a i j = (nd ? a i j).
interpretation "new I" 'I a = (nI ? a).
+(*D
+
+The paper defines the image as
+
+> Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
+
+but this cannot be ..... MAIL
+
+> Im[d(a,i)] ⊆ V
+
+Allora ha una comoda interpretazione (che voi usate liberamente)
+
+> ∀j:D(a,i). d(a,i,j) ∈ V
+
+Ma se voglio usare Im per definire C, che è un subset di S, devo per
+forza (almeno credo) definire un subset, ovvero dire che
+
+> Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
+
+Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua
+uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si
+scatenano i setoidi. Ovvero Im[d(a,i)] ⊆ V diventa il seguente
+
+> ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
+
+
+D*)
+
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 }.
interpretation "image" 'Im a i = (image ? a i).
+(*D
+
+
+
+D*)
+
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);
##]
nqed.
+(*D
+
+We then define the inductive type of ordinals, parametrized over an axiom
+set. We also attach some notations to the constructors.
+
+D*)
+
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 "0" non associative with precedence 90 for @{ 'oO }.
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 Zero" 'oO = (oO ?).
interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
interpretation "ordinals Succ" 'oS x = (oS ? x).
+(*D
+
+Note that Matita does not support notation in the left hand side
+of a pattern match, and thus the names of the constructors have to
+be spelled out verbatim.
+
+BLA let rec. Bla let_in.
+
+D*)
+
nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
match x with
[ oO ⇒ U
notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
interpretation "famU" 'famU U x = (famU ? U x).
+
+(*D
+
+We attach as the input notation for U_x the similar `U⎽x` where underscore,
+that is a character valid for identifier names, has been replaced by `⎽` that is
+not. The symbol `⎽` can act as a separator, and can be typed as an alternative
+for `_` (i.e. pressing ALT-L after `_`).
+
+The notion ◃(U) has to be defined as the subset of of y
+belonging to U_x for some x. Moreover, we have to define the notion
+of cover between sets again, since the one defined at the beginning
+of the tutorial works only for the old axiom set definition.
+
+D*)
ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
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.
+(*D
+
+Before proving that this cover relation validates the reflexivity and infinity
+rules, we prove this little technical lemma that is used in the proof for the
+infinity rule.
+
+D*)
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)).
+(*D
+
+The proof of infinity uses the following form of the Axiom of choice,
+that cannot be prove inside Matita, since the existential quantifier
+lives in the sort of predicative propositions while the sigma in the conclusion
+lives in the sort of data types, and thus the former cannot be eliminated
+to provide the second.
+
+D*)
+
+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)).
+
+(*D
+
+In the proof of infinity, we have to rewrite under the ∈ predicate.
+It is clearly possible to show that U_x is an extensional set:
+
+> a=b → a ∈ U_x → b ∈ U_x
+
+Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
+declared as morphisms. This poses to problem, but goes out of the scope of the
+tutorial and we thus assume it.
+
+D*)
naxiom setoidification :
- ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
+ ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
(*D
-Bla Bla,
+The reflexivity proof is trivial, it is enough to provide the ordinal 0
+as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
+D*)
+ntheorem new_coverage_reflexive:
+ ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
+#A; #U; #a; #H; @ (0); napply H;
+nqed.
+
+(*D
+
+We now proceed with the proof of the infinity rule.
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;
+#A; #U; #a; (** screenshot "n-cov-inf-1". *)
+*; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
+ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
+ #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *)
+ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
- ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';
-@ ((Λ f)+1); @2; nwhd; @i; #x; *; #d; #Hd;
+ ##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
+@ (Λ f+1); (** screenshot "n-cov-inf-7". *)
+@2; (** screenshot "n-cov-inf-8". *)
+@i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
napply (setoidification … Hd); napply Hf';
nqed.
+(*D
+D[n-cov-inf-1]
+We eliminate the existential, obtaining an `i` and a proof that the
+image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
+form of `H`, thus expands the definition of cover between sets.
+
+D[n-cov-inf-2]
+The paper proof considers `H` implicitly substitutes the equation assumed
+by `H` in its conclusion. In Matita this step is not completely trivia.
+We thus assert (`ncut`) the nicer form of `H`.
+
+D[n-cov-inf-3]
+After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
+What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
+becomes trivial is `j` is chosen to be `z`. In the command `napply #`,
+the `#` is a standard notation for the reflexivity property of the equality.
+
+D[n-cov-inf-4]
+Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
+its property.
+
+D[n-cov-inf-5]
+The paper proof does now a forward reasoning step, deriving (by the ord_subset
+lemma we proved above) `Hf'` i.e. 𝐝 a i j ∈ U⎽(Λf).
+
+D[n-cov-inf-6]
+To prove that `a◃U` we have to exhibit the ordinal x such that `a ∈ U⎽x`.
+
+D[n-cov-inf-7]
+The definition of `U⎽(…+1)` expands to the union of two sets, and proving
+that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
+the second constructor `@2;` of the disjunction, we are left to prove that `a`
+belongs to the right hand side.
+
+D[n-cov-inf-8]
+We thus provide `i`, introduce the element being in the image and we are
+left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging
+to the image means that there exists an object in the domain… we eliminate the
+existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
+
+D[n-cov-inf-9]
+We just need to use the equational definition of `x` to obtain a conclusion
+that can be proved with `Hf'`. We assumed that `U_x` is extensional for
+every `x`, thus we are allowed to use `Hd` and close the proof.
+
+D*)
+
+(*D
+
+The next proof is that ◃(U) is mininal. The hardest part of the proof
+it to prepare the goal for the induction. The desiderata is to prove
+`U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
+unfolding all definitions:
+
+> ∀x. x ∈ { y | ∃o:Ord A.y ∈ U⎽o } → x ∈ V
+
+D*)
+
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;
+ ∀A:nAx.∀U:Ω^A.∀V.U ⊆ V → (∀a:A.∀i.𝐈𝐦[𝐝 a i] ⊆ V → a ∈ V) → ◃U ⊆ V.
+#A; #U; #V; #HUV; #Im;#b; (** screenshot "n-cov-min-2". *)
+*; #o; (** screenshot "n-cov-min-3". *)
+ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
+nelim o; (** screenshot "n-cov-min-5". *)
##[ #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.
+(*D
+D[n-cov-min-2]
+After all the introductions, event the element hidden in the ⊆ definition,
+we have to eliminate the existential quantifier, obtaining the ordinal `o`
+
+D[n-cov-min-3]
+What is left is almost right, but the element `b` is already in the
+context. We thus generalize every occurrence of `b` in
+the current goal, obtaining `∀c.c ∈ U⎽o → c ∈ V` that is `U⎽o ⊆ V`.
+
+D[n-cov-min-4]
+We then proceed by induction on `o` obtaining the following goals
+
+D[n-cov-min-5]
+All of them can be proved using simple set theoretic arguments,
+the induction hypothesis and the assumption `Im`.
+
+D*)
+
+
+(*D
+
+bla bla
+
+D*)
+
nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
match x with
[ oO ⇒ F
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.
+(*D
+
+The proof of compatibility uses this little result, that we
+factored out.
+D*)
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.
+(*D
+
+We assume the dual of the axiom of choice, as in the paper proof.
+
+D*)
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.
+(*D
+
+Proving the anti-reflexivity property is simce, since the
+assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
+`a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
+
+D*)
+ntheorem new_fish_antirefl:
+ ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
+#A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
+nqed.
+
+(*D
+
+bar
+D*)
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));
+#A; #F; #a; #aF; #i; nnormalize; (** screenshot "n-f-compat-1". *)
+napply AC_dual; #f; (** screenshot "n-f-compat-2". *)
+nlapply (aF (Λf+1)); #aLf; (** screenshot "n-f-compat-3". *)
+nchange in aLf with
+ (a ∈ F⎽(Λ f) ∧ ∀i:𝐈 a.∃j:𝐃 a i.𝐝 a i j ∈ F⎽(Λ f)); (** screenshot "n-f-compat-4". *)
ncut (∃j:𝐃 a i.𝐝 a i j ∈ F⎽(f j));##[
- ncases aLf; #_; #H; nlapply (H i); *; #j; #Hj; @j; napply Hj;##] #aLf';
+ ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
+ *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
napply aLf';
nqed.
+(*D
+D[n-f-compat-1]
+D[n-f-compat-2]
+D[n-f-compat-3]
+D[n-f-compat-4]
+D[n-f-compat-5]
+D[n-f-compat-6]
+
+D*)
+
+(*D
+
+The proof that `⋉(F)` is maximal is exactly the dual one of the
+minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
+before doing the induction over `o`.
+
+D*)
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;
+ ∀A:nAx.∀G:qpowerclass_setoid A.∀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;
+ @d; napply IH;
+ napply (. 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;
##]
(*D
-Appendix: natural deduction like tactics explanation
------------------------------------------------------
+<div id="appendix" class="anchor"></div>
+Appendix: tactics explanation
+-----------------------------
In this appendix we try to give a description of tactics
in terms of sequent calculus rules annotated with proofs.
napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
Γ ⊢ (f ?1 … ?n ) : B
-foo
+ Γ ⊢ ? : F → B Γ ⊢ f : F
+ nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ (? f) : B
- Γ; x : T ⊢ ? : P(x)
- #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- Γ ⊢ λx:T.? : ∀x:T.P(x)
-baz
+ Γ; x : T ⊢ ? : P(x)
+ #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ λx:T.? : ∀x:T.P(x)
+
- Γ; args… : Args… ⊢ ?i : P(k1 args1) … (?n argsn) : P(kn argsn)
- ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- Γ ⊢ match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n : P(x)
+ Γ ⊢ ?_i : args_i → P(k_i args_i)
+ 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)
+ Γ ⊢ ?i : ∀t. P(t) → P(k_i … t …)
nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- (T_rect_CProp0 ?1 … ?n) : P(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
+ Γ ⊢ ? : Q Q ≡ P
+ nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ ? : P
Where the equivalence relation between types `≡` keeps into account
β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
computation).
+
+ Γ; H : Q; Δ ⊢ ? : G Q ≡ P
+ nchange in H with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ; H : P; Δ ⊢ ? : G
+
+
+
+ Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
+ ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ (?_2 ?_1) : G
+
+
+ Γ ⊢ ? : ∀x.P(x)
+ ngeneralize in match t; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ (? t) : P(t)
+
D*)
[1]: http://upsilon.cc/~zack/research/publications/notation.pdf
-*)
+D*)
projects / helm.git / commitdiff