2

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?

user4035
  • 22,508
  • 11
  • 59
  • 94

2 Answers2

4

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.
Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
2
Theorem eqb_trans : forall n m p,
    n =? m = true ->
    m =? p = true ->
    n =? p = true.
Proof.
  intros n m p.
  repeat rewrite  Nat.eqb_eq.
  intros.
  rewrite H.
  exact H0.
Qed.

-- Check Nat.eqb_eq.

Nat.eqb_eq                                                                                          
 : forall n m : nat, (n =? m) = true <-> n = m
xingfe123
  • 79
  • 3