The Leibniz equality is an equivalence relation. As such, it is reflexive, symmetric, and transitive.
When a goal is an equality where both sides are syntactically identical, it is proved using the reflexivity tactic.
And when we need an equality where both sides are syntactically identical to use as an assumption, eq_refl is our friend. If we type:
Check (eq_refl 2).
the *response* window reads:
eq_refl
: 2 = 2
For example, consider this slightly artificial proposition about negb : bool -> bool, the resident negation function:
Proposition about_negb :
forall x : bool,
(forall y : bool,
x = y -> negb (negb x) = y) ->
negb (negb (negb x)) = negb x.
Its proof starts as usual, and then we can visualize the type of the result of applying the local assumption to the given boolean:
Proof.
intros x H_x.
Check (H_x x).
The *response* window reads:
H_x x
: x = x -> negb (negb x) = x
So H_x x needs to be applied to the equality x = x, which is precisely what eq_refl provides:
Check (H_x x (eq_refl x)).
The *response* window reads:
H_x x eq_refl
: negb (negb x) = x
We can then rewrite the left-hand side of this equality in the goal. The resulting goal is an equality whose left-hand side and right-hand side are identical, which we prove using the reflexivity tactic to complete the proof:
rewrite -> (H_x x (eq_refl x)).
reflexivity.
Qed.
When the goal is an equality, we can swap its left-hand side and its right-hand side using the symmetry tactic.
And when we have an assumption that is an equality and we want to swap its left-hand side and its right-hand side, eq_sym is our friend. For example, when we type:
Check (Nat.add_0_l 2).
the *response* window reads:
Nat.add_0_l 2
: 0 + 2 = 2
and when we type:
Check (eq_sym (Nat.add_0_l 2)).
the *response* window reads:
eq_sym (Nat.add_0_l 2)
: 2 = 0 + 2
And when we have an assumption x = y and another assumption y = z, eq_trans is our friend to obtain x = z without using the rewrite tactic.
For example, assume that we are given three functions foo, bar, and baz and that we have proved the equivalence of foo and bar and the equivalence of bar and baz. We can prove the equivalence of foo and baz as a corollary:
Definition foo (n : nat) : nat :=
S n.
Definition bar (n : nat) : nat :=
1 + n.
Definition baz (n : nat) : nat :=
n + 1.
Lemma equivalence_of_foo_and_bar :
forall n : nat,
foo n = bar n.
Admitted.
Lemma equivalence_of_bar_and_baz :
forall n : nat,
bar n = baz n.
Admitted.
Corollary equivalence_of_foo_and_baz :
forall n : nat,
foo n = baz n.
Proof.
intro n.
Check (eq_trans (equivalence_of_foo_and_bar n) (equivalence_of_bar_and_baz n)).
(* eq_trans (equivalence_of_foo_and_bar n) (equivalence_of_bar_and_baz n)
: foo n = baz n *)
exact (eq_trans (equivalence_of_foo_and_bar n) (equivalence_of_bar_and_baz n)).
Qed.
The revisitation of Exercise 11 from Week 02 in Week 04 involved three definitions of the negation function. The first and the second were proved equivalent, and the second and the third were proved equivalent. So as illustrated just above with foo, bar, and baz, eq_trans would have come handy to prove the equivalence of the first and the third definitions of the negation function.