The f_equal lemma captures that applying a function to two equal arguments yields equal results:
f_equal : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y
Warning
All of A, B, x, and y are implicit arguments, so f_equal is only applied to a function f and an equality x = y.
Functional equality can be neatly used to provide equality in context, as illustrated below:
Proposition add_0_r :
forall n : nat,
n + 0 = n.
Proof.
intro n.
induction n as [ | n' IHn'].
- exact (fold_unfold_add_O 0).
- rewrite -> fold_unfold_add_S.
The *goals* window reads:
n' : nat
IHn' : n' + 0 = n'
============================
S (n' + 0) = S n'
At that point, the standard thing to do is to use the induction hypothesis and then the reflexivity tactic. Instead – and this is the point of the present chapter – let us use f_equal, applying it to a function that represents the context of n' + 0 on the left-hand side and of n' on the right-hand side:
Check (f_equal S).
The *response* window reads:
f_equal S
: forall x y : nat, x = y -> S x = S y
As warned above, f_equal is defined so that several of its arguments are implicit, so that in effect, it only has two arguments, namely the function and the Leibniz equality. And here, the induction hypothesis is providing this Leibniz equality:
Check (f_equal S IHn').
The *response* window reads:
f_equal S IHn'
: S (n' + 0) = S n'
And since the resulting Leibniz equality is the goal, we can use the exact tactic to complete the proof:
exact (f_equal S IHn').
Factored out of Chapter Life after the midterm project [14 Apr 2024]