(named "nightly builds" in the download page of Matita)
with a version strictly greater than 0.5.7.
+To read this tutorial in HTML format, you need a decent browser
+equipped with a unicode capable font. Use the PDF format if some
+symbols are not displayed correctly.
+
Orienteering
------------
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 `Id` (Leibniz equality),
-thus we will explicitly equip a set with an equivalence relation when needed.
-We will call this structure a _setoid_. Note that we will
-attach the infix `=` symbol only to the equality of a setoid,
-not to Id.
+not quotiented set).
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,
> Type[0] < Type[1] < Type[2]
+<object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
+
For every `Type[i]` there is a corresponding level of predicative
-propositions `CProp[i]`. A predicative proposition cannot be eliminated toward
-`Type[j]` unless it holds no computational content (i.e. it is an inductive type
+propositions `CProp[i]` (the C initial is due to historical reasons, and
+stands for constructive, `PProp` would be more appropriate).
+A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
with 0 or 1 constructors with propositional arguments, like `Id` and `And`
but not like `Or`).
+The distintion between predicative propositions and predicative data types
+is a peculirity of Matita (for example in CIC as implemented by Coq they are the
+same). The additional restriction of not allowing the elimination of a CProp
+toward a Type makes the theory of Matita minimal in the following sense:
+
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
+
+Theorems proved in this setting can be reused in a classical framwork (forcing
+Matita to collapse the hierarchy of constructive propositions). Alternatively,
+one can decide to collapse predicative propositions and datatypes recovering the
+Axiom of Choice (i.e. ∃ really holds a content and can thus be eliminated to
+provide a witness for a Σ).
+
+Formalization choices
+---------------------
+
+We will avoid using `Id` (Leibniz equality),
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,
+not to Id.
+
+
The standard library and the `include` command
----------------------------------------------
D*)
nrecord Ax : Type[1] ≝ {
- S :> setoid;
+ S :> Type[0];
I : S → Type[0];
- C : ∀a:S. I a → Ω ^ S
+ C : ∀a:S. I a → Ω^S
}.
(*D
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.
+| creflexivity : ∀a. a ∈ U → cover A U a
+| cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover A U a.
(** screenshot "cover". *)
napply cover;
nqed.
(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". *)
+#a; #a_in_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". *)
+##| #i; ncases (H2 a a_in_P i); (** screenshot "def-fish-rec-5". *)
#x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
@; (** screenshot "def-fish-rec-6". *)
##[ napply x
D*)
-nrecord nAx : Type[2] ≝ {
- nS:> setoid;
+nrecord nAx : Type[1] ≝ {
+ nS:> Type[0];
nI: nS → Type[0];
nD: ∀a:nS. nI a → Type[0];
nd: ∀a:nS. ∀i:nI a. nD a i → nS
D*)
+include "logic/equality.ma".
+
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 }.
##]
nqed.
+nlemma Ax_nAx_equiv :
+ ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
+ C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.
+#A; #a; #i; @; #b; #H;
+##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;
+ nwhd in H; ncases H; #x; #E; nrewrite > E;
+ ncases x in E; #b; #Hb; #_; nnormalize; nassumption;
+##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
+ ##[ @ b; nassumption;
+ ##| nnormalize; @; ##]
+##]
+nqed.
+
(*D
We then define the inductive type of ordinals, parametrized over an axiom
D*)
-ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ 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.
D*)
+nlemma AC_fake : ∀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)).
+#A; #a; #i; #U; #H; @;
+##[ #j; ncases (H j); #x; #_; napply x;
+##| #j; ncases (H j); #x; #Hx; napply Hx; ##]
+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*)
+alias symbol "exists" (instance 1) = "exists".
+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".
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". *)
*; #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". *)
+ #z; napply H; @ z; @; ##] #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';(** 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 (U_x_is_ext … Hd); napply Hf';
+nrewrite > Hd; napply Hf';
nqed.
(*D
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 if `j` is chosen to be `z`. In the command `napply #`,
-the `#` is a standard notation for the reflexivity property of the equality.
+becomes trivial if `j` is chosen to be `z`.
D[n-cov-inf-4]
Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
*; #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;
+##[ napply HUV;
##| #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; ##]
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.
+ (∀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
D*)
ntheorem max_new_fished:
- ∀A:nAx.∀G:𝛀^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; (** screenshot "n-f-max-1". *)
- alias symbol "prop2" = "prop21".
- napply (. Ed^-1‡#); napply cG;
+ @d; napply IH; (** screenshot "n-f-max-1". *)
+ nrewrite < Ed; napply cG;
##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
#b; #Hb; #d; napply (Hf d); napply Hb;
##]
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
+ Γ ⊢ f : A_1 → … → A_n → B Γ ⊢ ?_i : A_i
napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- Γ ⊢ (f ?1 … ?n ) : B
+ Γ ⊢ (f ?_1 … ?_n ) : B
Γ ⊢ ? : F → B Γ ⊢ f : F
nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
projects / helm.git / blobdiff