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 inside your browser and . Finally, you can your working copy of the file, e.g., for sending it to teachers.

## Type-inference Based Automation

Today:

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

## Redundant annotations: polymorphism

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:

## Matching and unification

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:

## Coercions

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...

## Dependent pairs

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:

## Currying

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.

## Uncurry

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.

## Augmenting unification

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.

## Structures as dependent tuples

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.

## Sharing notations and theory

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.