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.

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.