MPRI PRFA — Proof Assistants

Leibniz equality

Leibniz proposed the followiing definition for equality: Two objects are equal when they have exactly the same properties.

Formally, we can define u = v as P u <-> P v for all predicates P. It is in fact enough to define it using an implication instead of equivalence, i.e. as forall P. P u -> P v. Indeed, the two definitions are equivalent:

Lemma leib_equiv A (u v : A) :
  (forall P : A -> Prop, P u <-> P v) <-> (forall P, P u -> P v).
Proof.
  split.
  - firstorder.
  - intros e P. split.
    + apply e.
    + apply e. auto.
Qed.

The magic operates above with the second apply e. It turns P v -> P u into P u -> P u. That's because it applied e with a predicate Q x := P u -> P x. Indeed e Q now has type (P u -> P u) -> (P u -> P v).

Module Leibniz.

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

  Definition leib_eq {A} (u v : A) : Prop :=
    forall (P : A -> Prop), P u -> P v.

We pick a nice notation for it.

  Notation "u == v" := (leib_eq u v) (at level 80).

We can prove various properties of this equality, in particular that it is an equivalence and a congruence.

We'll start with reflexivity. Proving a == a is the same as proving forall 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.

  Definition refl {A} (a : A) : a == a :=
    fun P (h : P a) => h.

The proof of symmetry is the same as showing that the definition of equality can be given with both <-> and ->.

  Definition sym {A} (u v : A) (e : u == v) : v == u :=
    fun P => e (fun x => P x -> P u) (refl u P).

Transitivity is composition:

  Lemma trans {A} (u v w : A) (e : u == v) (e' : v == w) : u == w.
  Proof.
    intro P.
    apply e'. apply e.
  Defined.

  Print trans.

We saw the tactic f_equal in the first lecture. It allows proving f x = f y from x = y, i.e. it lets us apply a function to both sides of an equality. When u == v, 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.

  Lemma f_equal {A B} (f : A -> B) {u v} (e : u == v) : f u == f v.
  Proof.
    intro P.
    apply e. apply refl.
  Defined.

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.

  Lemma n_plus_0 n : n + 0 == n.
  Proof.
    induction n as [ | n ih ].
    - apply refl.
    - simpl. apply f_equal. assumption.
  Qed.

We can also discriminate between 0 and S n this way. We just have to instantiate S n == 0 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.

  Lemma nat_discr n : S n == 0 -> False.
  Proof.
    intros e.
    specialize (e (fun x => match x with 0 => False | _ => True end)).
    simpl in e. apply e. constructor.
  Qed.

The standard equality of Rocq, the one you've been using since lesson 1, is not defined using Leibniz's principle. Instead it is defined as an inductive type. We will see however that the two notions are equivalent, even though the inductive one has serious advantages.

  Module EqDef.

Below is how Rocq's equality is defined (Print "=" would have yielded the same result).

    Inductive eq {A} (u : A) : A -> Prop :=
    | eq_refl : eq u u.

Let us analyse this inductive type a bit. It has two uniform parameters A : Type and u : A, and one index of type A. In the end it produces a proposition (Prop). Crucially it has only one constructor which takes no non-parameter arguments, meaning it satisfies the subsingleton criterion. This alone provides a serious advantage over Leibniz equality because it lets us eliminates equality into Type.

Now see how close the induction principle is to Leibniz equality.

    Check eq_ind.

As we were saying, we also get one in Type.

    Check eq_rect.

Let us now prove the equivalence.

    Lemma eq_to_Leibniz A (u v : A) : eq u v -> u == v.
    Proof.
      intros e.
      induction e.
      apply refl.
    Qed.

    Lemma Leibniz_to_eq A (u v : A) : u == v -> eq u v.
    Proof.
      intros e.
      apply e.
      apply eq_refl.
    Qed.

  End EqDef.

End Leibniz.

We go back to using eq with Notation = from the standard library.

We first prove symmetry and transitivity using eq_ind. They are essentially the same proofs as for Leibniz equality.

Definition eq_sym {A} {u v : A} (e : u = v) : v = u :=
  eq_ind _ (fun x => x = u) eq_refl _ e.

Definition eq_trans {A} {u v w : A} (e : u = v) (e' : v = w) : u = w :=
  eq_ind _ (fun x => u = x) e _ e'.

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.

Definition eq_sym' {A} {u v : A} (e : u = v) : v = u :=
  match e with
  | eq_refl => eq_refl
  end.

Now we prove transitivity, that is u = v -> v = w -> u = w. For this, we match on e : u = v, 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.

Fail Definition eq_trans' {A} {u v w : A} (e : u = v) (e' : v = w) : u = w :=
  match e with
  | eq_refl => e'
  end.

Definition eq_trans' {A} {u v w : A} (e : u = v) (e' : v = w) : u = w :=
  match e with
  | eq_refl => fun e' => e'
  end e'.

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.

Lemma f_equal' A B (f : A -> B) u v :
  u = v ->
  f u = f v.
Proof.
  intros e.
  destruct e. reflexivity.
Qed.

Definition f_equal'' A B (f : A -> B) u v (e : u = v) : f u = f v :=
  match e with
  | eq_refl => eq_refl
  end.

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 perfom rewriting in types:

Goal forall {A} (u v : A),
  Leibniz.leib_eq u v -> forall P : A -> Type, P u -> P v.
Proof.
  intros A u v e P.
  Fail specialize (e P).
Abort.

As we mentioned above, eq on the other hand satisfies the subsingleton criterion, which is why rewriting is allowed.

Goal forall {A} (u v : A), u = v -> forall P : A -> Type, P u -> P v.
Proof.
  intros A u v e P.
  rewrite e. auto. Show Proof.
Qed.

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:

Definition transport {A u v} (e : u = v :> A) (P : A -> Type) : P u -> P v :=
  match e with
  | eq_refl => fun a => a
  end.

Definition transport' {A u v} (e : u = v :> A) (P : A -> Type) : P u -> P v :=
  eq_rect u (fun v : A => P u -> P v) (fun a => a) v e.

We've now seen essentially all the definitions we've been using until now. Let us have a look at more complicated things. We're first going to look at dependent functions and try to adapt f_equal to them.

Fail Lemma dep_f_equal A B (f : forall (x : A), B x) u v :
  u = v ->
  f u = f v.

Even just stating the lemma fails. That's because f u : B u and f v : B v and B u and B v are not a priori the same type. They are equal, assuming u = v, however! Thankfully we have just seen how to go from B u to B v: we just use transport.

We'll provide a nice notation for it, to make things more readable.

Notation "e # t" := (transport e _ t) (t at next level, at level 19).

Lemma dep_f_equal A B (f : forall (x : A), B x) u v (e : u = v) :
  e # f u = f v.
Proof.
  destruct e.

Notice how transport computes!

  simpl.
  reflexivity.
Qed.

If you remember, we've been using equality through the remember tactic to help when induction (or destruct) was forgetting information. Like so:

Inductive even : nat -> Prop :=
| even0 : even 0
| evenS : forall n, even n -> even (S (S n)).

Lemma evenSS_inv n :
  even (S (S n)) ->
  even n.
Proof.
  intros h.
  destruct h.
Abort.

Lemma evenSS_inv n :
  even (S (S n)) ->
  even n.
Proof.
  intros h.
  remember (S (S n)) as m eqn: e.
  destruct h.
  - discriminate.
  - inversion e. subst. assumption.
Qed.

This you already knew. Let's now 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 it will have type 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 discriminate the equality using transport to go from P 0 to P (S (S n)) such that P 0 is True and P (S (S n)) is even n (no need to go through False).

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.

Definition evenSS_inv_alt n (h : even (S (S n))) : even n :=
  match h in even m return m = S (S n) -> even n
  with
  | even0 =>
    fun (e : 0 = S (S n)) =>
      transport e (fun x => match x with 0 => True | _ => even n end) I
  | evenS m h' =>
    fun (e : S (S m) = S (S n)) =>
      (f_equal (fun x => pred (pred x)) e) # h'
  end eq_refl.

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.

Definition all_equal A := forall (x y : A), x = y.

Lemma unit_neq_bool :
  unit <> bool.
Proof.
  intro e.
  assert (h : all_equal unit).
  { intros [] []. reflexivity. }
  rewrite e in h.
  specialize (h true false). discriminate.
Qed.