by Stefano Berardi and Silvio Valentini.
-The tutorial is by Enrico Tassi.
+The tutorial and the formalization are by Enrico Tassi.
The reader should be familiar with inductively generated
formal topologies and have some basic knowledge of type theory and λ-calculus.
The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
types defined in the environment. This construct, together with the possibility to
definable total recursive functions, allows to define eliminators (or constructors)
-for (co)inductive types. The λ-calculus is also equipped with explicitly typed
-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`).
+for (co)inductive types.
Types are compare up to conversion. Since types may depend on terms, conversion
involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
> Type[0] < Type[1] < Type[2]
+Matita implements a variant of CIC in which constructive and predicative proposition
+are distinguished from predicative data types.
+
<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]` (the C initial is due to historical reasons, and
-stands for constructive, `PProp` would be more appropriate).
+stands for constructive).
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 distinction between predicative propositions and predicative data types
-is a peculirity of Matita (for example in CIC as implemented by Coq they are the
+is a peculiarity 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"/>
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="600px"/>
Theorems proved in CIC as implemented in Matita can be reused in a classical
and impredicative framework (i.e. forcing Matita to collapse the hierarchy of
constructive propositions and assuming the excluded middle on them).
Alternatively, one can decide to collapse predicative propositions and
-datatypes recovering the Axiom of Choice in the sense of Martin Löf
+predicative data types recovering the Axiom of Choice in the sense of Martin Löf
(i.e. ∃ really holds a witness and can be eliminated to inhabit a type).
This implementation of CIC is the result of the collaboration with Maietti M.,
---------------------
There are many different ways of formalizing the same piece of mathematics
-in CIC, depending on what our interests are. There is usually a tradeoff
+in CIC, depending on what our interests are. There is usually a trade-off
between the possibility of reuse the formalization we did and its complexity.
In this work, our decisions mainly regarded the following two areas
-- Equality: Id or not
- Axiom of Choice: controlled use or not
-
-### Equality
-
-TODO
-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.
+- Equality: Id or not
### Axiom of Choice
of Choice, thus choosing to identify ∃ and Σ (i.e. working in the
leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision
(that is, the author of the paper would not complain we formalized something
-diffrent from what he had in mind).
+different from what he had in mind).
Anyway, we may benefit from the minimality of CIC as implemented in Matita,
-"asking" the type system to ensure we do no use the Axiom of Choice elswhere
+"asking" the type system to ensure we do no use the Axiom of Choice elsewhere
in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
-very beginnig, the system will not complain if we use the Axiom of Choice at all.
+very beginning, the system will not complain if we use the Axiom of Choice at all.
Moreover, the elimination of an inductive type (like ∃) is a so common operation
that the syntax chosen for the elimination command is very compact and non
informative, hard to spot for a human being
existential). This is possible only thanks to the minimality of CIC as implemented
in Matita.
+### Equality
+
+What we have to decide here is which models we admit. The paper does not
+mention quotiented sets, thus using an intensional equality is enough
+to capture the intended content of the paper. Nevertheless, the formalization
+cannot be reused in a concrete example where the (families of) sets
+that will build the axiom set are quotiented.
+
+Matita gives support for setoid rewriting under a context built with
+non dependent morphisms. As we will detail later, if we assume a generic
+equality over the carrier of our axiom set, a non trivial inductive
+construction over the ordinals has to be proved to respect extensionality
+(i.e. if the input is an extensional set, also the output is).
+The proof requires to rewrite under the context formed by the family of sets
+`I` and `D`, that have a dependent type. Declaring them as dependently typed
+morphisms is possible, but Matita does not provide an adequate support for them,
+and would thus need more effort than formalizing the whole paper.
+
+Anyway, in a preliminary attempt of formalization, we tried the setoid approach,
+reaching the end of the formalization, but we had to assume the proof
+of the extensionality of the `U_x` construction (while there is no
+need to assume the same property for `F_x`!).
+
+The current version of the formalization uses `Id`.
+
The standard library and the `include` command
----------------------------------------------
Defining Axiom set
------------------
-A set of axioms is made of a set(oid) `S`, a family of sets `I` and a
+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 elements of `I(a)`.
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 (dependent) 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 "cast" function the system automatically inserts when it is needed.
cover relation between two subsets, while the inductive predicate
we are going to define relates an element and a subset.
+ a ∈ U i ∈ I(a) C(a,i) ◃ U
+ (reflexivity) ⎼⎼⎼⎼⎼⎼⎼⎼⎼ (infinity) ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ a ◃ U a ◃ U
+
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).
had side of the predicate changes, thus it has to be abstracted (in the arity
of the inductive predicate) on the right of `:`.
+The intuition Valentini suggests is that we are defining the unary predicate
+"being covered by U" (i.e. `_ ◃ U`) and not "being covered" (i.e. `_ ◃ _`).
+Unluckily, the syntax of Matita forces us to abstract `U` first, and
+we will make it the second argument of the predicate using
+the notational support Matita offers.
+
D*)
(** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
Introduction rule for fish
---------------------------
-Matita is able to generate elimination rules for inductive types,
-but not introduction rules for the coinductive case.
-
+Matita is able to generate elimination rules for inductive types
D*)
(** ncheck cover_rect_CProp0. *)
(*D
+but not introduction rules for the coinductive case.
+
+ P ⊆ U (∀x,j.x ∈ P → C(x,j) ≬ P) a ∈ P
+ (fish intro) ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+ a ⋉ U
+
We thus have to define the introduction rule for fish by co-recursion.
Here we again use the proof mode of Matita to exhibit the body of the
corecursive function.
one constructor (one introduction rule) holding the witness and the proof
that the witness satisfies a proposition.
-> ncheck Ex.
+> 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
> Im[d(a,i)] = { y | ∃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.
+This poses no theoretical problems, since `S` is a Type and thus
+equipped with the `Id` equality. If `S` was a setoid, here the equality
+would have been the one of the setoid.
Unless we define two different images, one for stating that the image is ⊆ of
something and another one to define `𝐂`, we end up using always the latter.
> ∀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 later, when `V` will be a complex
-construction that has to be proved extensional
-(i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
+That, up to rewriting with the equation defining `x`, is what we mean.
+Since we decided to use `Id` the rewriting always work (the elimination
+principle for `Id` is Leibnitz's equality, that is quantified over
+the context.
+
+The problem that arises if we decide to make `S` a setoid is that
+`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic
+functional proposition has to quotient its input with a relation bigger
+than the one of `S`.
+
+> ∀x,y:S. x = y → x ∈ V → y ∈ V
+
+If `V` is a complex construction, the proof may not be trivial.
D*)
##]
nqed.
+(*D
+
+We now prove that the two function above form a retraction pair for
+the `C` component of the axiom set. To prove that we face a little
+problem since CIC is not equipped with η-conversion. This means that
+the followin does not hold (where `A` is an axiom set).
+
+> A = (S A, I A, C A)
+
+This can be proved only under a pattern mach over `A`, that means
+that the resulting computation content of the proof is a program
+that computes something only if `A` is a concrete axiom set.
+
+To state the lemma we have to drop notation, and explicitly
+give the axiom set in input to the `C` projection.
+
+D*)
+
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;
+#A; #a; #i; @; #b; #H; (** screenshot "retr-1". *)
+##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;(** screenshot "retr-2". *)
+ nchange in a with S; nwhd in H; (** screenshot "retr-3". *)
+ ncases H; #x; #E; nrewrite > E; nwhd in x; (** screenshot "retr-4". *)
+ ncases x; #b; #Hb; nnormalize; nassumption;
##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
##[ @ b; nassumption;
##| nnormalize; @; ##]
##]
nqed.
+(*D
+D[retr-1]
+Look for example the type of `a`. The command `nchange in a with A`
+would fail because of the missing η-conversion rule. We have thus
+to pattern match over `A` and introduce its pieces.
+
+D[retr-2]
+Now the system accepts that the type of `a` is the fist component
+of the axiom set, now called `S`. Unfolding definitions in `H` we discover
+there is still some work to do.
+
+D[retr-3]
+To use the equation defining `b` we have to eliminate `H`. Unfolding
+definitions in `x` tell us there is still something to do. The `nrewrite`
+tactic is a shortcut for the elimination principle of the equality.
+It accepts an additional argument `<` or `>` to rewrite left-to-right
+or right-to-left.
+
+D[retr-4]
+We defined `𝐝` to be the first projection of `x`, thus we have to
+eliminate `x` to actually compute `𝐝`.
+
+The remaining part of the proof it not interesting and poses no
+new problems.
+
+D*)
+
(*D
We then define the inductive type of ordinals, parametrized over an axiom
D*)
-nlemma AC_fake : ∀A,a,i,U.
+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
+
+Note that, if we will decide later to identify ∃ and Σ, `AC` is
+trivially provable
+
+D*)
+
+nlemma AC_exists_is_sigma : ∀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
-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:
+In case we made `S` a setoid, the following property has to be proved
-> a = b → a ∈ U⎽x → b ∈ U⎽x
+> nlemma U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
Anyway this proof is a non trivial induction over x, that requires `𝐈` and `𝐃` to be
-declared as morphisms. This poses no problem, but goes out of the scope of the
-tutorial, since dependent morphisms are hard to manipulate, and we thus assume it.
+declared as morphisms.
D*)
-naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
(*D
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".
-alias symbol "covers" = "new covers".
+alias symbol "covers" (instance 3) = "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; @; ##] #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". *)
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:Ω^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
##]
nqed.
-(*D
-D[n-f-max-1]
-Here the situation looks 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
-exploit the facilities
-Matita provides to perform rewriting in the general setting of setoids.
-
-The `.` notation simply triggers the mechanism, while the given argument has to
-mimic the context under which the rewriting has to happen. In that case
-we want to rewrite the left hand side 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
+D[n-f-max-1]
+Note that here the right hand side of `∈` is `G` and not `F⎽p` as
+in the dual proof. If `S` was declare to be a setoid, to finish this proof
+would be enough to assume `G` extensional, and no proof of the
+extensionality of `F⎽p` is required.
-(*D
<div id="appendix" class="anchor"></div>
Appendix: tactics explanation
-----------------------------
projects / helm.git / blobdiff