MPRI 2-7-2 / 2024 / Live coding session 7

In this session we are looking at the definition of equality (u = v) in Coq. You have already used equality with rewrite, subst, reflexivity, etc., but we have until now avoided spelling out the definition.

Leibniz equality There is more than one potential definition of equality. One classical definition of equality on paper is that of Leibniz, saying that two objects are equal when they have the exactly same properties. We could say u = v is the same as P u ↔ P v for all predicates P☐. In fact, is is enough to define u = v as P u → P v for all P because one can recover the other direction as we shall see:

Let us now play with this notion of equality. We define it as follows.

We pick a nice notation for it.

We now define reflexivity. To prove a == a is the same as proving ∀ P, P a → P a. Seen that way, it should be easy to see what one is supposed to do. We assume P and some h : P a and we have to prove P a. That we do using h. In a sense we are just defining a particular case of the identity function.

Symmetry. The proof of symmetry is the same as showing that the definition of equality can be given with both ↔ and →.

Transitivity. Transitivity is composition:

Congruence. We saw the tactic f_equal in the first lecture. It allows proving f x = f y from x = y, i.e. lets us apply a function to both sides of an equality. We have P u → P v for all P, so in particular, by taking P x := Q (f x) we have Q (f u) → Q (f v) for all Q. This is how we get f u == f v from u == v.

We can still prove equalities like we did before with this definition. The main difference is that instead of tactics like f_equal, we have to apply the lemmas manually.

We can also discriminate between 0 and S n this way. From S n == 0 we just have to instantiate it with the right P. We're going to get P (S n) → P 0 so we want P 0 to be False and P (S n) to be provable, so we pick True.

Coq's standard library does not use Leibniz equality, but an equivalent definition. Namely, Coq uses an inductive definition stating that equality is the smallest reflexive relation. In the end, this is equivalent to Leibniz equality, but has some advantages as we will see.

We can see that u is a (uniform) parameter of the definition, whereas v is an index instantiated to exactly and only u in the (only) constructor. As we know, this leads to the following induction principle -- see how close it is to Leibniz equality?

We go back to using eq with Notation = from the standard library. We first prove symmetry and transitivity using eq_ind, meaning they have the essentially same proofs as for Leibniz equality. We then go into details why eq is defined inductively.

Since eq is an inductive type we can also use pattern matching to reason about it. When matching on an equality e : u = v, the only constructor is eq_refl forcing v to be exactly u in the eq_refl branch. This is why, for symmetry, we don't need to prove v = u but actually u = u and so eq_refl is a valid proof.

For transitivity, we match on e, so v is "unified" with u, meaning we only need to prove u = w → u = w which is easy. Note that to do it, we abstract over e' inside and apply it again outside: This is because the change of v to u only applies to everything *in* the branch. In other words, we first write a proof of v = w → u = w using equality e : u = v, and then we apply it to e' : v = w.

As for all other inductive types, we can also use the destruct tactic on equalities. It does the same as pattern matching. If you destruct e : u = v it will unify v with u in the goal, so that f u = f v becomes f u = f u which is provable by reflexivity.

So why is eq defined inductively and not as Leibniz equality? The reason is that Leibniz equality only quantifies over predicates P : X → Prop, because otherwise it would not live in Prop. However, this means that Leibniz equality cannot (directly) be used to do rewrites in *types*:

If we re-examine the definition of equality, we see that it is a sub-singleton:

• It has one constructor eq_refl.
• This constructor has two parameters A and u and *no* other arguments, meaning in particular all other arguments are proofs.

Of course, since Leibniz equality is equivalent to eq it could still be used as definition, but every rewrite in types would require using the equivalence. Thus, we use eq directly, because it allows both pattern matching and Leibniz-like reasoning through eq_ind. The property we just proved is called transport. We prove it again, this time with a proof term and using eq_rect:

We now turn to working with dependent functions. We prove f_equal for dependent functions:

This definition doesn't work because f u : B u and f v : B v and B u and B v are not a priori the same type. Instead, we need to transport f u from B u to B v. And we know how to do that: we simply use eq_rect on e : u = v to prove B u → B v.

Notice how eq_rect computes!

Equality can be useful when performing induction.

With this destruct, Coq will simply forget the index (S (S n)) of even and only consider the cases 0 and S (S n), even though we know S (S n) can't be 0. The remember tactic lets us replace S (S n) by some variable as index, together with equality e : m = S (S n). Now destruct or induction will work because it can unify m with 0 or S (S k) easily as it is a variable. We still get the case m = 0, but now we have equality 0 = S (S n) that we can discriminate to close the goal.

Let's do it with a proof term directly. Here we use a more advanced pattern matching notation that lets us give a name to the index of the thing we match on: we write h in even m to give a name m to the index. We write a return clause that depends on this m that says m = S (S n) → even n. So since h : even (S (S n)), the type of the whole match expression is going to be m = S (S n) → even n where m is replaced by S (S n), in other words by S (S n) = S (S n) → even n. This is why we apply the whole match to eq_refl : S (S n) = S (S n) and it then has type even n. Now we get two branches, one in which m is replaced by 0 and one in which it is replaced by S (S m). In the 0 branch, we thus have to show 0 = S (S n) → even n. We use eq_ind to go from P 0 to P (S (S n)) such that P 0 is True and P (S (S n)) is even n. In the S (S m) branch, we have S (S m) = S (S n) so we first prove that m = n by applying pred on both sides twice and use that equality to go from even m to even n.

Function extensionality We can write the following map function such that map f l applies f to every element of list l. In other words it turns [ a1 ; a2 ; a3 ; a4 ] into [ f a1 ; f a2 ; f a3 ; f a4 ]. We can thus show that map (fun x ⇒ x) l = l. However, we cannot show map (fun (x : A) ⇒ x) = (fun l ⇒ l). For this we need an extra principle that is often assumed on paper: function extensionality (FunExt). It says that two functions are equal if and only iff they yield equal results on all inputs. It already appeared in some exercises, but a reminder won't hurt.

Discriminating types. We've seen before how to show true ≠ false or 0 ≠ S n. We can also distinguish types. We cannot do it the same way as before by matching on them because we cannot match on types. Instead we have to exploit properties that hold for one and not the other. For instance, we can show that unit and bool are different by first showing that all elements of unit are equal. Then if unit = bool, then all elements of bool must be equal. But we already know two different elements of type bool: true and false.

Another independent principle: proposition extensionality. It states that two propositions are equal if and only iff they are logically equivalent, ie that they imply one another. Using this principle, we can show that propositions with a proof are equal to the True proposition.

Proof irrelevance. Proof irrelevance is another property that doesn't hold by default but that is safe to assume (like PropExt or FunExt). It says that any two proofs of the same proposition are equal. We can show that PropExt implies proof irrelevance.

This handy command let us see which axioms were used in the proof.

Uniqueness of identity proofs (UIP). Another principle that is similar to proof irrelevance is the fact that all proofs of the same equality are equal.

Boolean equality again. We recall boolean equality for natural numbers. Then we show that we can decide wether two natural numbers are equal of not. This is expressed by the type { n = m } + { n ≠ m } which either contains a proof of n = m or a proof of the opposite: n ≠ m. This can be read as a function that computes either a proof that the two numbers are equal, or disproves it. In other words, it is a decision procedure for natural number equality.

The eqn below also remembers that eq_nat n m = true or false depending on the branch we're in.