CODEWITHSUNDEEP
coqlogical-foundations
user4035
user4035

Reputation: 23729

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?

Upvotes: 2

Views: 598

Answers (2)

xingfe123
xingfe123

Reputation: 79

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

Upvotes: 2

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

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.

Upvotes: 4

Related Questions