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?
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.