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 aesthetic
+this is a important part of every formalization, not only from 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
- ∀ 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
--------------------------------------------
-...
+CIC is a full and functional Pure Type System (all products do exist,
+and their sort is is determined by the target) with an impedicative sort
+Prop and a predicative sort Type. The environment can be populated with
+well typed definitions or theorems, (co)inductive types validating positivity
+conditions and recursive functions provably total by simple syntactical
+analysis (recursive call on structurally smaller subterms). Co-recursive
+functions can be defined as well, and must satisfy a dual condition, that is
+performing the recursive call only after having generated a constructor (a piece
+of output).
+
+The λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment that combined with the definable total
+structural recursive functions allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly types
+local definitions (let in) that in the degenerate case work as casts (i.e.
+the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).
-Type is a set equipped with the Id equality (i.e. an intensional,
+Since we are going to formalize constructive and predicative mathematics
+in an intensional type theory like CIC, we try to establish some terminology.
+Type is the sort of sets 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,
+attach the infix = symbol only to the equality of a setoid,
not to Id.
-...
-
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.
For every Type[i] there is a corresponding level of predicative
propositions CProp[i].
-CIC is also equipped with an impredicative sort Prop that we will not
-use in this tutorial.
The standard library and the `include` command
----------------------------------------------
These notions come with some standard 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`
+- A ∪ B can be typed with `A \cup B`
+- A ∩ B can be typed with `A \cap B`
+- A ≬ B can be typed with `A \between B`
+- x ∈ A can be typed with `x \in A`
+- Ω^A, that is the type of the subsets of A, can be typed with `\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:
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.
-
-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
Some basic results that we will use are also part of the sets library:
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". *)
+ (** 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". *)
+ napply H1; (** screenshot "def-fish-rec-3". *)
nassumption;
-##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
+##| #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". *)
+ @; (** screenshot "def-fish-rec-6". *)
##[ napply x
- ##| @; (** screenshot "def-fish-rec-7". *)
+ ##| @; (** screenshot "def-fish-rec-7". *)
##[ napply xC;
- ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
+ ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
nassumption;
##]
##]
ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
#A; #U; #a; @; #H;
-##[ nelim H; #b; (* manca clear *)
+##[ nelim H; #b;
##[ #bU; @1; nassumption;
##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
##[ #E; @; napply E;
> Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
-but this cannot be ..... MAIL
+but this not so formal notation poses some problems. The image is
+often used as the left hand side of the ⊆ predicate
> Im[d(a,i)] ⊆ V
-Allora ha una comoda interpretazione (che voi usate liberamente)
+Of course this writing is interpreted by the authors as follows
> ∀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
+If we need to use the image to define 𝐂 (a subset of S) we are obliged to
+form a subset, i.e. to place a single variable `{ here | … }`.
+
+> Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
-> Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
+This poses no theoretical problems, since `S` is a setoid and thus equipped
+with an equality.
-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
+Unless we difene two different images, one for stating the image is ⊆ of
+something and another one to define 𝐂, we end up using always the latter.
+Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
> ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
+That up to rewriting with the equation defining `x` is what we mean. The
+technical problem arises when `V` is a complex construction that has to
+be proved extensional (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
D*)
(*D
-
+Thanks to our definition of image, we ca trivially a function mapping a
+new axiom set to an old one and viceversa. Note that in the second
+definition, when defining 𝐝, the projection of the Σ type is inlined
+(constructed on the fly by `*;`) while in the paper it was named `fst`.
D*)
(*D
+The dfinition of `U_x` is by recursion over the ordinal `x`.
+We thus define a recursive function. The `on x` directive tells
+the system on which argument the function is (structurally) recursive.
+
+In the `oS` case we use a local definition to name the recursive call
+since it is used twice.
+
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
- | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
+ | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n}
| 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 }.
D*)
-nlemma ord_subset:
- ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
+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.
(*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
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.
+ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
#A; #U; #a; #H; @ (0); napply H;
nqed.
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 "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 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
+is 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:
(*D
-bla bla
+The notion `F⎽x` is again defined by recursion over the ordinal `x`.
D*)
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 }
+ | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o }
| oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
].
(*D
The proof of compatibility uses this little result, that we
-factored out.
+proved outside the mail proof.
D*)
-nlemma co_ord_subset:
- ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
+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.
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.
+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
+Proving the anti-reflexivity property is simple, 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.
+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
+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:qpowerclass_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;
##| #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