Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line.
Use ALT-(right-arrow) to go to the cursor.
You can
save your edits
inside your browser and
load them back.
Finally, you can
download
your working copy of the file, e.g., for sending it to teachers.

Today:

- Automating the synthesis of statements
- Automating proofs by enhanced unification
- Mathematical structures in dependent type theory

Remember, from Lesson 2, the definition of the (polymorphic) type of lists, of which we make an isomorphic copy here:

Except that our copy is not (yet) configured: it
behaves as on a black board

.
In fact, a well-typed term of type `list A` features many copies of the polymorphic parameter `A`:

Yet the proof assistant is able to infer the value of this parameter, from the type of elements stored in the list:

Therefore, we can configure the definition, so that we do not even have to mention the holes:

In Lesson 3, we have seen that tactics use information from the goal, to compute relevant instances of lemmas.

This is typically the case with the `apply:` tactic:

Although it cannot guess arbitrary information, as balance has to be maintained between automation and efficiency:

So far, the information inferred by the proof assistant was based on constraints coming from typing rules and matching.

But the user can also add extra inference features, based on the content of the libraries.

This is what we have done in Lecture 2 and 3 when discussing how terms of type `bool` could be promoted to the status of statement, i.e., terms of type `Prop`.

Caveat: use with care, as it can obfuscate statements...

In Lesson 3, we have discussed the extension of a dependently typed lambda calculus with inductive types, so as to better represent constructions, e.g. natural numbers, booleans, etc.

Here is an important example of extension, introducing dependent pairs. Let us start with the introduction (typing) rule:

$$\frac{\Gamma \vdash T\ :\ Set \quad \Gamma \vdash P\ :\ T \rightarrow Prop}{\Gamma \vdash \Sigma x\ :\ T, p\ x : Set} $$

Using Coq's inductive types, this becomes:

And here are the projections of a pair onto its components:

Coq provides a specific syntax to define a dependent pair and its projections in one go:

Dependent pairs can be used to define a sub-type, i.e., a type for a sub-collection of elements in a given type. Here is a type for strictly positive natural numbers:

And here is a way to build terms of type `pos_nat`:

Still, this is a sub-type, and not a sub-set: functions expecting
arguments in `nat` do not apply:

But we can correct this using a coercion.

And we can use this lemma to define a new term of type `pos_nat`,
from two existing ones:

As you may have noticed, we have been stating lemmas using chains of implications rather than conjunctions.

This is because a conjunction is a pair of facts, and most of the time we will have to break this pair, in order to use each hypothesis.

Dependent pairs also allow to phrase statements in a curry- or uncurry-style.

For instance, consider a predicate (a property) P on natural numbers, which holds for any strictly positive number.

We can phrase this property on P in two different style:

Now, let us prove a toy corollary of this property, using the two
different variants. First using `posP1`:

The proof possibly requires using one step per symbol used in the
expression, provided the symbol refers to an operation preserving
strict positivity, like `+`.

This calls for some automation, implemented as a dedicated tactic.

Let us now see how things work with the second version of the hypothesis. In fact, it stops quite soon:

The problem here is that unifying `P ((S x) + 3` with the conclusion
of `posP2` does not work, as it requires guessing the value of a pair
from the sole value of its first component:

P ((S x) + 3) ~ P (val ?) ? : pos_nat

which is an instance of the following problem:

n + m ~ val ? ? : pos_nat

Now if `n` and `m` are not arbitrary terms, but themselves
projections of terms in `pos_nat`, we have a candidate solution
at hand:

We just need to inform Coq that we want this solution to be used to solve this otherwise unsolvable problem:

This worked because Coq was able to infer a solution of the form:

(val x) + (val y) ~ val (pos_nat_add x y)

Now the problem has been turned into:

P ((S x) + 3) ~ P (val (pos_nat_add ?1 ?2) ?1, ?2 : pos_nat S x ~ val ?1 3 ~ val ?2

But once again, these problems do not have intrinsic solutions: we
have to inform the unification algorithm of the lemma `pos_nat_S`.

Dependent pairs generalize to dependent tuples:

$$ \Sigma x_1\ :\ T_1 \Sigma x_2\ :\ T_2\ x_1 \dots \Sigma x_{n+1}\ :\ T_{n +1} x_1\ \dots\ x_n $$

Just like sequences \( (x_1, x_2 \dots, x_n) \) flatten nested pairs \( (x_1, (x_2, (\dots, x_n)) \), dependent tuples flatten dependent pairs.

Dependent tuples are represented by inductive types with a single constructor, and \(n\) arguments. Here is an example:

Dependent tuples can indeed model mathematical structures, which bundle a carrier set (here a type) with subsets, operations, and prescribed properties on these data.

(notes)

Dependent tuples ressemble contexts, i.e., sequences of variables paired with types, with dependencies coming in order. Such a sequence is sometimes also refered to as a *telescope*, a terminology introduced by de Bruijn in
this paper.

In Lesson 2, we defined an infix notation `==` for equality on type `nat`.
More generally, we can make this notation available on instances of the
`eqType` structure, for types endowed with an effective equality test.

Instances of a same structure share a *theory*, i.e., a corpus of results that follow from the axioms of the structure.

Some of these results are about the preservation of the structure.

We can define base case instances of the structure, for instance using the lemmas proved in Lesson 4.

But this is not enough.

This is a similar problem to the one of inferring positivity proofs, and it can be solved the same way.

(notes)

For more about these hints for unification, and the way they can be used to implement hierarchies of structures, you might refer to: this tutorial.