(*D
-Matita Tutorial: inductively generated formal topologies
-========================================================
+Inductively generated formal topologies in Matita
+=================================================
This is a not so short introduction to [Matita][2], based on
the formalization of the paper
by Stefano Berardi and Silvio Valentini.
-The tutorial is by Enrico Tassi.
+The tutorial and the formalization are by Enrico Tassi.
-The tutorial spends a considerable amount of effort in defining
+The reader should be familiar with inductively generated
+formal topologies and have some basic knowledge of type theory and λ-calculus.
+
+A considerable part of this tutorial is devoted to explain how to define
notations that resemble the ones used in the original paper. We believe
-this is a important part of every formalization, not only from the aesthetic
+this is an 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
statements) readable to the author of the paper.
-The formalization uses the ng (new generation) version of Matita
+The formalization uses the "new generation" version of Matita
(that will be named 1.x when finally released).
Last stable release of the "old" system is named 0.5.7; the ng system
-is coexisting with the old one in every development release
+is coexisting with the old one in all development release
(named "nightly builds" in the download page of Matita)
with a version strictly greater than 0.5.7.
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
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]
+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]`. 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).
+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 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="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
+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.,
+Sambin G. and Valentini S. of the University of Padua.
+
+Formalization choices
+---------------------
+
+There are many different ways of formalizing the same piece of mathematics
+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
+
+- Axiom of Choice: controlled use or not
+- Equality: Id or not
+
+### Axiom of Choice
+
+In this paper it is clear that the author is interested in using the Axiom
+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
+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 elsewhere
+in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the
+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
+(in fact it is just two characters long!).
+
+We decided to formalize the whole paper without identifying
+CProp and Type and assuming the Axiom of Choice as a real axiom
+(i.e. a black hole with no computational content, a function with no body).
+
+It is clear that this approach give us full control on when/where we really use
+the Axiom of Choice. But, what are we loosing? What happens to the computational
+content of the proofs if the Axiom of Choice gives no content back?
+
+It really
+depends on when we actually look at the computational content of the proof and
+we "run" that program. We can extract the content and run it before or after
+informing the system that our propositions are actually code (i.e. identifying
+∃ and Σ). If we run the program before, as soon as the computation reaches the
+Axiom of Choice it stops, giving no output. If we tell the system that CProp and
+Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection)
+and the extracted code would compute an output.
+
+Note that the computational
+content is there even if the Axiom of Choice is an axiom, the difference is
+just that we cannot use it (the typing rules inhibit the elimination of the
+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" (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