Tactics: stuck in eqb_trans

Trying to solve eqb_trans I became stuck:

Theorem eqb_trans : forall n m p,
  n =? m = true ->
  m =? p = true ->
  n =? p = true.

Obviously, we should use eqb_true to solve it:

Theorem eqb_true : forall n m,
    n =? m = true -> n = m.
--------------------------------------------
Proof.
  intros n m p H1 H2. apply eqb_true in H1.
  apply eqb_true with (n:=m)(m:=p) in H2.

At this point we have:

n, m, p : nat
H1 : n = m
H2 : m = p
============================
(n =? p) = true

Now I wanted to use eqb_true upon the goal:

apply eqb_true with (m:=p).

But here we get an error:

Unable to unify "?M1056 = p" with "(n =? p) = true".

Why doesn't it work? How to fix?

Solution

When you apply a lemma to the goal, it is the conclusion of the lemma that must unify with the goal rather than its premise. The conclusion of this lemma is of the form _ = _, while your goal is (_ =? _) = true. These two cannot be unified, which leads to the error you see.

To prove eqb_trans, you need the converse of eqb_true, namely

forall n m, n = m -> (n =? m) = true,

which, after some simplification, is equivalent to

forall n, (n =? n) = true.