Functional equality

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 used to neatly 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 n' 0).

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, as illustrated in the resource file.

Alternatively, one can apply eq_S to make the goal coincide with the induction hypothesis, as also illustrated in the resource file.

The point of the present chapter is to present a third alternative that uses 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').

Postlude

Pablito: Wait a second.

Bong-sun: Sure. OK, we have waited a second.

Pablito (heedless): <clickety clickety click>:

Check (f_equal S).

Bong-sun (helpful): The *response* window reads:

f_equal S
     : forall x y : nat, x = y -> S x = S y

Pablito (muttering to himself): Right. And now:

Check eq_S.

Bong-sun (helpful): The *response* window reads:

eq_S: forall x y : nat, x = y -> S x = S y

Pablito: Ha!

Halcyon: Ah?

Bong-sun: You are right, Pablito, it’s the same elephant.

Pablito (reflectively): So eq_S is a specialized version of f_equal...

Bong-sun: Tis.

Mimer: Good find, Pablito.

Resources

• The .v file for the present lecture note (latest version: 07 Mar 2025).

Version

Created [07 Mar 2025]