Unable to correctly use the 'apply' tactic

Using Coq
1

I am trying to solve the 1 star exercise in the ‘Logic’ chapter from ‘Logical Foundations’.

Theorem eqb_neq : ∀ x y : nat,
x =? y = false ↔ x ≠ y.

My attempt is to try to do this:
Proof.
intros x y. split.

  • apply not_true_iff_false with (b := (x=?y)).

But I am not able to use the ‘apply’ tactic.

PS.
Lemma not_true_iff_false : forall b,
b <> true ↔ b = false.

Can someone help me out? Thanks!

2

Try

Theorem eqb_neq : ∀ x y : nat, x =? y = false ↔ x ≠ y.
Proof.
  intros x y.
  split.
  - intros H.
    apply not_true_iff_false in H.
3

Hi!

Thank you so much for your suggestion! I was able to complete the proof but it is not an elegant and short one. I introduce H1 and use eqb_refl. Is there an easier way that I’m overlooking?

4

I’m not sure how much you are allowed to assume. I mean the simplest proof is just

Theorem eqb_neq : ∀ x y : nat, x =? y = false ↔ x ≠ y.
Proof.
  apply Nat.eqb_neq.
Qed.