(*D
-Matita Tutorial: inductively generated formal topologies
-========================================================
+Inductively generated formal topologies in Matita
+=================================================
-This is a not so short introduction to Matita, based on
+This is a not so short introduction to [Matita][2], based on
the formalization of the paper
> Between formal topology and game theory: an
> explicit solution for the conditions for an
> inductive generation of formal topologies
-by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
+by Stefano Berardi and Silvio Valentini.
-The tutorial spends a considerable amount of effort in defining
+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.
+
+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 "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 all development release
+(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
------------
window on the top right is where the system shows you the ongoing proof;
the error window, on the bottom right, is where the system complains.
On the top of the script window five buttons drive the processing of
-the proof script. From left to right the requesting the system to:
+the proof script. From left to right they request the system to:
- go back to the beginning of the script
- go back one step
When the system processes a command, it locks the part of the script
corresponding to the command, such that you cannot edit it anymore
-(without to go back). Locked parts are coloured in blue.
+(without going back). Locked parts are coloured in blue.
The sequent window is hyper textual, i.e. you can click on symbols
-to jump to their definition, or switch between different notation
+to jump to their definition, or switch between different notations
for the same expression (for example, equality has two notations,
one of them makes the type of the arguments explicit).
Everywhere in the script you can use the `ncheck (term).` command to
-ask for the type a given term. If you that in the middle of a proof,
+ask for the type a given term. If you do that in the middle of a proof,
the term is assumed to live in the current proof context (i.e. can use
variables introduced so far).
to mean double or single arrows.
Here we recall some of these "shortcuts":
- - ∀ can be typed with `\Forall`
+ - ∀ can be typed with `\forall`
- λ can be typed with `\lambda`
- ≝ can be typed with `\def` or `:=`
- → can be typed with `\to` or `->`
example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
Variants are listed in the aforementioned TeX/UTF-8 table.
+The syntax of terms (and types) is the one of the λ-calculus CIC
+on which Matita is based. The main syntactical difference w.r.t.
+the usual mathematical notation is the function application, written
+`(f x y)` in place of `f(x,y)`.
+
Pressing `F1` opens the Matita manual.
-CIC (as implemented in Matita) in a nutshell
---------------------------------------------
+CIC (as [implemented in Matita][3]) 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
+and their sort is is determined by the target) with an impredicative sort
+Prop and a predicative sort Type. It features both dependent types and
+polymorphism like the [Calculus of Constructions][4]. Proofs and terms share
+the same syntax, and they can occur in types.
+
+The environment used for in the typing judgement 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
+analysis (recursive calls are allowed only on structurally smaller subterms).
+Co-recursive
+functions can be defined as well, and must satisfy the dual condition, i.e.
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`).
+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.
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 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 = 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].
-
+Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
+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,
+and `Type[1]` for classes. The index `i` is just a label: constraints among
+universes are declared by the user. The standard library defines
+
+> 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).
+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 S, a family of sets I and a
-family C of subsets of S indexed by elements a of S and I(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)`.
It is desirable to state theorems like "for every set of axioms, …"
without explicitly mentioning S, I and C. To do that, the three
components have to be grouped into a record (essentially a dependently
typed tuple). The system is able to generate the projections
-of the record for free, and they are named as the fields of
-the record. So, given a axiom set `A` we can obtain the set
+of the record automatically, and they are named as the fields of
+the record. So, given an axiom set `A` we can obtain the set
with `S A`, the family of sets with `I A` and the family of subsets
with `C A`.
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
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 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 function case the system automatically inserts when it is needed.
+a "cast" function the system automatically inserts when it is needed.
In that case, the projection `S` has type `Ax → setoid`, and whenever
the expected type of a term is `setoid` while its type is `Ax`, the
-system inserts the coercion around it, to make the whole term well types.
+system inserts the coercion around it, to make the whole term well typed.
When formalizing an algebraic structure, declaring the carrier as a
coercion is a common practice, since it allows to write statements like
The quantification over `x` of type `G` is ill-typed, since `G` is a term
(of type `Group`) and thus not a type. Since the carrier projection
-`carr` of `G` is a coercion, that maps a `Group` into the type of
+`carr` is a coercion, that maps a `Group` into the type of
its elements, the system automatically inserts `carr` around `G`,
-obtaining `…∀x: carr G.…`. Coercions are also hidden by the system
-when it displays a term.
+obtaining `…∀x: carr G.…`.
-In this particular case, the coercion `S` allows to write
+Coercions are hidden by the system when it displays a term.
+In this particular case, the coercion `S` allows to write (and read):
∀A:Ax.∀a:A.…
D*)
-(* ncheck I. *)
-(* ncheck C. *)
+(** ncheck I. *) (* shows: ∀A:Ax.A → Type[0] *)
+(** ncheck C. *) (* shows: ∀A:Ax.∀a:A.A → I A a → Ω^A *)
(*D
`A` is an axiom set and `a` has type `S A` (or thanks to the coercion
mechanism simply `A`). In Matita, a question mark represents an implicit
argument, i.e. a missing piece of information the system is asked to
-infer. Matita performs some sort of type inference, thus writing
+infer. Matita performs Hindley-Milner-style type inference, thus writing
`I ? a` is enough: since the second argument of `I` is typed by the
-first one, the first one can be inferred just computing the type of `a`.
+first one, the first (omitted) argument can be inferred just
+computing the type of `a` (that is `A`).
D*)
-(* ncheck (∀A:Ax.∀a:A.I ? a). *)
+(** ncheck (∀A:Ax.∀a:A.I ? a). *) (* shows: ∀A:Ax.∀a:A.I A a *)
(*D
-This is still not completely satisfactory, since you have always type
+This is still not completely satisfactory, since you have always to type
`?`; to fix this minor issue we have to introduce the notational
support built in Matita.
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).
The syntax separates with `:` abstractions that are fixed for every
constructor (introduction rule) and abstractions that can change. In that
-case the parameter `U` is abstracted once and forall in front of every
+case the parameter `U` is abstracted once and for all in front of every
constructor, and every occurrence of the inductive predicate is applied to
`U` in a consistent way. Arguments abstracted on the right of `:` are not
constant, for example the xcinfinity constructor introduces `a ◃ U`,
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. *)
+(** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *)
(*D
type is the arity of the inductive `xcover` predicate just defined).
Then it has to be abstracted over the arguments of that cover relation,
-i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`)
+i.e. the axiom set and the set `U`, and the subset (in that case `𝐂 a i`)
sitting on the left hand side of `◃`.
D*)
We now define the notation `a ◃ b`. Here the keywork `hvbox`
and `break` tell the system how to wrap text when it does not
-fit the screen (they can be safely ignore for the scope of
+fit the screen (they can be safely ignored for the scope of
this tutorial). We also add an interpretation for that notation,
where the (abstracted) cover relation is implicit. The system
will not be able to infer it from the other arguments `C` and `U`
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.
ends a definition or proof.
We can now define the interpretation for the cover relation between an
-element and a subset fist, then between two subsets (but this time
-we fixed the relation `cover_set` is abstracted on).
+element and a subset first, then between two subsets (but this time
+we fix the relation `cover_set` is abstracted on).
D*)
We will proceed similarly for the fish relation, but before going
on it is better to give a short introduction to the proof mode of Matita.
-We define again the `cover_set` term, but this time we will build
+We define again the `cover_set` term, but this time we build
its body interactively. In the λ-calculus Matita is based on, CIC, proofs
and terms share the same syntax, and it is thus possible to use the
-commands devoted to build proof term to build regular definitions.
+commands devoted to build proof term also to build regular definitions.
A tentative semantics for the proof mode commands (called tactics)
in terms of sequent calculus rules are given in the
<a href="#appendix">appendix</a>.
D[xcover-set-2]
We have now to provide a proposition, and we exhibit it. We left
a part of it implicit; since the system cannot infer it it will
-ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition
-whenever `?` is.
+ask for it later.
+Note that the type of `∀y:A.y ∈ C → ?` is a proposition
+whenever `?` is a proposition.
D[xcover-set-3]
The proposition we want to provide is an application of the
The system will now ask in turn the three implicit arguments
passed to cover. The syntax `##[` allows to start a branching
to tackle every sub proof individually, otherwise every command
-is applied to every subrpoof. The command `##|` switches to the next
+is applied to every subproof. The command `##|` switches to the next
subproof and `##]` ends the branching.
D*)
(*D
-Introction rule for fish
-------------------------
-
-Matita is able to generate elimination rules for inductive types,
-but not introduction rules for the coinductive case.
+Introduction rule for fish
+---------------------------
+Matita is able to generate elimination rules for inductive types
D*)
-(* ncheck cover_rect_CProp0. *)
+(** ncheck cover_rect_CProp0. *)
(*D
-We thus have to define the introduction rule for fish by corecursion.
+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.
(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[def-fish-rec-5]
We then introduce `x`, break the conjunction (the `*;` command is the
equivalent of `ncases` but operates on the first hypothesis that can
-be introduced. We then introduce the two sides of the conjunction.
+be introduced). We then introduce the two sides of the conjunction.
D[def-fish-rec-5-1]
-The goal is now the existence of an a point in `𝐂 a i` fished by `U`.
+The goal is now the existence of a point in `𝐂 a i` fished by `U`.
We thus need to use the introduction rule for the existential quantifier.
In CIC it is a defined notion, that is an inductive type with just
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
the co-recursive call.
D[def-fish-rec-9]
-The co-recursive call needs some arguments, but all of them live
+The co-recursive call needs some arguments, but all of them are
in the context. Instead of explicitly mention them, we use the
`nassumption` tactic, that simply tries to apply every context item.
We now have to define the subset of `S` of points covered by `U`.
We also define a prefix notation for it. Remember that the precedence
-of the prefix form of a symbol has to be lower than the precedence
+of the prefix form of a symbol has to be higher than the precedence
of its infix form.
D*)
(*D
Here we define the equation characterizing the cover relation.
-In the igft.ma file we proved that `◃U` is the minimum solution for
+Even if it is not part of the paper, we proved that `◃(U)` is
+the minimum solution for
such equation, the interested reader should be able to reply the proof
with Matita.
(*D
-We similarly define the subset of point fished by `F`, the
-equation characterizing `⋉F` and prove that fish is
+We similarly define the subset of points "fished" by `F`, the
+equation characterizing `⋉(F)` and prove that fish is
the biggest solution for such equation.
D*)
Part 2, the new set of axioms
-----------------------------
-Since the name of objects (record included) has to unique
-within the same script, we prefix every field name
+Since the name of defined objects (record included) has to be unique
+within the same file, we prefix every field name
in the new definition of the axiom set with `n`.
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
We again define a notation for the projections, making the
-projected record an implicit argument. Note that since we already have
-a notation for `𝐈` we just add another interpretation for it. The
-system, looking at the argument of `𝐈`, will be able to use
+projected record an implicit argument. Note that, since we already have
+a notation for `𝐈`, we just add another interpretation for it. The
+system, looking at the argument of `𝐈`, will be able to choose
the correct interpretation.
D*)
(*D
+The first result the paper presents to motivate the new formulation
+of the axiom set is the possibility to define and old axiom set
+starting from a new one and vice versa. The key definition for
+such construction is the image of d(a,i).
The paper defines the image as
> Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
> ∀j:D(a,i). d(a,i,j) ∈ V
-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 | … }`.
+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 | … }` of type `S`.
> 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 difene two different images, one for stating the image is ⊆ of
-something and another one to define 𝐂, we end up using always the latter.
+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.
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).
+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*)
+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 }.
-notation "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
+notation < "𝐈𝐦 [𝐝 \sub ( ❨a,\emsp i❩ )]" non associative with precedence 70 for @{ 'Im $a $i }.
interpretation "image" 'Im a i = (image ? a i).
(*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`.
+Thanks to our definition of image, we can define a function mapping a
+new axiom set to an old one and vice versa. Note that in the second
+definition, when we give the `𝐝` component, the projection of the
+Σ-type is inlined (constructed on the fly by `*;`)
+while in the paper it was named `fst`.
D*)
(*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; (** 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
set. We also attach some notations to the constructors.
| oL : ∀a:A.∀i.∀f:𝐃 a i → Ord A. Ord A.
notation "0" non associative with precedence 90 for @{ 'oO }.
-notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
notation "x+1" non associative with precedence 50 for @{'oS $x }.
+notation "Λ term 90 f" non associative with precedence 50 for @{ 'oL $f }.
interpretation "ordinals Zero" 'oO = (oO ?).
-interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
interpretation "ordinals Succ" 'oS x = (oS ? x).
+interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
(*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 definition of `U⎽x` is by recursion over the ordinal `x`.
+We thus define a recursive function using the `nlet rec` command.
+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
not. The symbol `⎽` can act as a separator, and can be typed as an alternative
for `_` (i.e. pressing ALT-L after `_`).
-The notion ◃(U) has to be defined as the subset of of y
-belonging to U_x for some x. Moreover, we have to define the notion
+The notion ◃(U) has to be defined as the subset of elements `y`
+belonging to `U⎽x` for some `x`. Moreover, we have to define the notion
of cover between sets again, since the one defined at the beginning
-of the tutorial works only for the old axiom set definition.
+of the tutorial works only for the old axiom set.
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
-The proof of infinity uses the following form of the Axiom of choice,
-that cannot be prove inside Matita, since the existential quantifier
+The proof of infinity uses the following form of the Axiom of Choice,
+that cannot be proved inside Matita, since the existential quantifier
lives in the sort of predicative propositions while the sigma in the conclusion
lives in the sort of data types, and thus the former cannot be eliminated
-to provide the second.
+to provide the witness for the second.
D*)
(*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:
+Note that, if we will decide later to identify ∃ and Σ, `AC` is
+trivially provable
+
+D*)
-> a = b → a ∈ U⎽x → b ∈ U⎽x
+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.
+
+(*D
-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
-tutorial and we thus assume it.
+In case we made `S` a setoid, the following property has to be proved
+
+> 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.
D*)
-naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
(*D
-The reflexivity proof is trivial, it is enough to provide the ordinal 0
-as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
+The reflexivity proof is trivial, it is enough to provide the ordinal `0`
+as a witness, then `◃(U)` reduces to `U` by definition,
+hence the conclusion. Note that `0` is between `(` and `)` to
+make it clear that it is a term (an ordinal) and not the number
+of the constructor we want to apply (that is the first and only one
+of the existential inductive type).
D*)
ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
D*)
-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".
+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; 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-1]
We eliminate the existential, obtaining an `i` and a proof that the
-image of d(a,i) is covered by U. The `nnormalize` tactic computes the normal
+image of `𝐝 a i` is covered by U. The `nnormalize` tactic computes the normal
form of `H`, thus expands the definition of cover between sets.
D[n-cov-inf-2]
-The paper proof considers `H` implicitly substitutes the equation assumed
-by `H` in its conclusion. In Matita this step is not completely trivia.
-We thus assert (`ncut`) the nicer form of `H`.
+When the paper proof considers `H`, it implicitly substitutes assumed
+equation defining `y` in its conclusion.
+In Matita this step is not completely trivial.
+We thus assert (`ncut`) the nicer form of `H` and prove it.
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 is `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
D[n-cov-inf-7]
The definition of `U⎽(…+1)` expands to the union of two sets, and proving
-that `a ∈ X ∪ Y` is defined as proving that `a` is in `X` or `Y`. Applying
-the second constructor `@2;` of the disjunction, we are left to prove that `a`
-belongs to the right hand side.
+that `a ∈ X ∪ Y` is, by definition, equivalent to prove that `a` is in `X` or `Y`.
+Applying the second constructor `@2;` of the disjunction,
+we are left to prove that `a` belongs to the right hand side of the union.
D[n-cov-inf-8]
-We thus provide `i`, introduce the element being in the image and we are
-left to prove that it belongs to `U_(Λf)`. In the meanwhile, since belonging
-to the image means that there exists an object in the domain… we eliminate the
+We thus provide `i` as the witness of the existential, introduce the
+element being in the image and we are
+left to prove that it belongs to `U⎽(Λf)`. In the meanwhile, since belonging
+to the image means that there exists an object in the domain …, we eliminate the
existential, obtaining `d` (of type `𝐃 a i`) and the equation defining `x`.
D[n-cov-inf-9]
(*D
-The next proof is that ◃(U) is mininal. The hardest part of the proof
+The next proof is that ◃(U) is minimal. The hardest part of the proof
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:
*; #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
The proof of compatibility uses this little result, that we
-proved outside the mail proof.
+proved outside the main proof.
D*)
nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
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
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.
+`a ∈ F⎽x`. If `x` is choose to be `0`, we obtain the thesis.
D*)
ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
(*D
D[n-f-compat-1]
-After reducing to normal form the goal, we obseve it is exactly the conlusion of
+After reducing to normal form the goal, we observe it is exactly the conclusion of
the dual axiom of choice we just assumed. We thus apply it ad introduce the
fcuntion `f`.
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);
+`Λf+1` for that recursive function, it can be computed.
+Anyway, using the `nnormalize`
+tactic would reduce too much (both the `+1` and the `Λf` steps would be performed);
we thus explicitly give a convertible type for that hypothesis, corresponding
-the computation of the `+1` step, plus the unfolding of `∩`.
+the computation of the `+1` step, plus the unfolding the definition of
+the intersection.
D[n-f-compat-4]
We are interested in the right hand side of `aLf`, an in particular to
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.
+ ∀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;
##]
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
+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
-----------------------------
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; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
(*D
+<date>
Last updated: $Date$
+</date>
[1]: http://upsilon.cc/~zack/research/publications/notation.pdf
+[2]: http://matita.cs.unibo.it
+[3]: http://www.cs.unibo.it/~tassi/smallcc.pdf
+[4]: http://www.inria.fr/rrrt/rr-0530.html
D*)
projects / helm.git / blobdiff