- ∀ can be typed with `\Forall`
- λ can be typed with `\lambda`
- ≝ can be typed with `\def` or `:=`
- - → can be typed with `to` or `->`
+ - → can be typed with `\to` or `->`
- some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
The user can cycle between variants typing one of them and then
example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
Variants are listed in the aforementioned TeX/UTF-8 table.
+Pressing `F1` opens the Matita manual.
+
CIC (as implemented in Matita) in a nutshell
--------------------------------------------
(*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:
+It is clearly possible to show that U⎽x is an extensional set:
-> a = b → a ∈ U_x → b ∈ U_x
+> 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
D*)
-naxiom setoidification: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
+naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
(*D
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 "n-cov-inf-1". *)
@ (Λ 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';
+napply (U_x_is_ext … Hd); napply Hf';
nqed.
(*D
D[n-cov-inf-4]
Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
-its property.
+its property. Note that the axiom `AC` was abstracted over `A,a,i,U` before
+assuming `(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x)`. Thus the term that can be eliminated
+is `AC ???? H'` where the system is able to infer every `?`. Matita provides
+a facility to specify a number of `?` in a compact way, i.e. `…`. The system
+expand `…` first to zero, then one, then two, three and finally four question
+marks, "guessing" how may of them are needed.
D[n-cov-inf-5]
The paper proof does now a forward reasoning step, deriving (by the ord_subset
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
+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 notion `F_x` is again defined by recursion over the ordinal `x`.
+The notion `F⎽x` is again defined by recursion over the ordinal `x`.
D*)
(*D
-bar
+We now prove the compatibility property for the new fish relation.
D*)
ntheorem new_fish_compatible:
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); (** screenshot "n-f-compat-5". *)
- *; #j; #Hj; @j; napply Hj;##] #aLf'; (** screenshot "n-f-compat-6". *)
-napply aLf';
+ncases aLf; #_; #H; nlapply (H i); (** screenshot "n-f-compat-5". *)
+*; #j; #Hj; @j; (** screenshot "n-f-compat-6". *)
+napply (co_ord_subset … Hj);
nqed.
(*D
D[n-f-compat-1]
+After reducing to normal form the goal, we obseve it is exactly the conlusion of
+the dual axiom of choice we just assumed. We thus apply it ad introduce the
+fcuntion `f`.
+
D[n-f-compat-2]
+The hypothesis `aF` states that `a⋉F⎽x` for every `x`, and we choose `Λf+1`.
+
D[n-f-compat-3]
+Since F_(Λf+1) is defined by recursion and we actually have a concrete input
+`Λf+1` for that recursive function, it can compute. Anyway, using the `nnormalize`
+tactic would reduce too much (both the `+1` and the `Λf` steps would be prformed);
+we thus explicitly give a convertible type for that hypothesis, corresponding
+the computation of the `+1` step, plus the unfolding of `∩`.
+
D[n-f-compat-4]
+We are interested in the right hand side of `aLf`, an in particular to
+its intance where the generic index in `𝐈 a` is `i`.
+
D[n-f-compat-5]
+We then eliminate the existential, obtaining `j` and its property `Hj`. We provide
+the same witness
+
D[n-f-compat-6]
+What is left to prove is exactly the `co_ord_subset` lemma we factored out
+of the main proof.
D*)
minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o`
before doing the induction over `o`.
+Note that `G` is assumed to be of type `𝛀^A`, that means an extensional
+subset of `S`, while `Ω^A` means just a subset (note that the former is bold).
+
D*)
ntheorem max_new_fished:
- ∀A:nAx.∀G:ext_powerclass_setoid A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
+ ∀A:nAx.∀G:𝛀^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);
##[ napply GF;
##| #p; #IH; napply (subseteq_intersection_r … IH);
#x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
- @d; napply IH;
+ @d; napply IH; (** screenshot "n-f-max-1". *)
alias symbol "prop2" = "prop21".
-napply (. Ed^-1‡#); napply cG;
+ 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;
##]
nqed.
+(*D
+D[n-f-max-1]
+Here the situacion look really similar to the one of the dual proof where
+we had to apply the assumption `U_x_is_ext`, but here the set is just `G`
+not `F_x`. Since we assumed `G` to be extensional we can employ the facilities
+Matita provides to perform rewriting in the general setting of setoids.
+
+The lemma `.` simply triggers the mechanism, and the given argument has to
+mimick the context under which the rewriting has to happen. In that case
+we want to rewrite to the left of the binary morphism `∈`. The infix notation
+to represent the context of a binary morphism is `‡`. The right hand side
+has to be left untouched, and the identity rewriting step is represented with
+`#` (actually a reflexivity proof for the subterm identified by the context).
+
+We want to rewrite the left hand side using `Ed` right-to-left (the default
+is left-to-right). We thus write `Ed^-1`, that is a proof that `𝐝 x i d = c`.
+
+The complete command is `napply (. Ed^-1‡#)` that has to be read like:
+
+> perform some rewritings under a binary morphism,
+> on the right do nothing,
+> on the left rewrite with Ed right-to-left.
+
+After the rewriting step the goal is exactly the `cG` assumption.
+
+D*)
+
(*D
<div id="appendix" class="anchor"></div>
Where `T_rect_CProp0` is the induction principle for the
inductive type `T`.
+
Γ ⊢ ? : Q Q ≡ P
nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
Γ ⊢ ? : P
Γ; H : P; Δ ⊢ ? : G
+ Γ; H : Q; Δ ⊢ ? : G P →* Q
+ nnormalize in H; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ; H : P; Δ ⊢ ? : G
+
+Where `Q` is the normal form of `P` considering βδζιμν-reduction steps.
+
+
+ Γ ⊢ ? : Q P →* Q
+ nnormalize; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ Γ ⊢ ? : P
+
Γ ⊢ ?_2 : T → G Γ ⊢ ?_1 : T
ncut T; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
projects / helm.git / blobdiff