How to convert "Zneq_bool a b = true" to a witness of "a <> b" in Coq?

Question

I'm trying to prove the following theorem:

Theorem Zeq_to_eq: forall (a b : Z), Zneq_bool a b = true -> a <> b.
Proof.
  intros a b.
  intros neq.
  rewrite  Zeq_bool_neq.
 Admitted.

I get the following error:

Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X22==[a b neq |- Relation_Definitions.relation Prop] (internal placeholder) {?r}
 ?X23==[a b neq |- Relation_Definitions.relation Z] (internal placeholder) {?r0}
 ?X24==[a b neq (do_subrelation:=Morphisms.do_subrelation)
         |- Morphisms.Proper
              (Morphisms.respectful (fun x y : Z => x <> y)
                 (Morphisms.respectful ?X23@{__:=a; __:=b; __:=neq}
                    ?X22@{__:=a; __:=b; __:=neq})) eq] (internal placeholder) {?p}
 ?X25==[a b neq |- Morphisms.ProperProxy ?X23@{__:=a; __:=b; __:=neq} b]
         (internal placeholder) {?p0}
 ?X26==[a b neq (do_subrelation:=Morphisms.do_subrelation)
         |- Morphisms.Proper
              (Morphisms.respectful ?X22@{__:=a; __:=b; __:=neq}
                 (Basics.flip Basics.impl)) not] (internal placeholder) {?p1}

I assume that something "deep" is going wrong, but I have no idea how to debug it. Help would be appreciated.

Answer 1

Check Zeq_bool_neq.
(*
Zeq_bool_neq
     : forall x y : Z, Zeq_bool x y = false -> x <> y
*)

In general, you can apply an implication like the above, and you can rewrite if you have a logical equivalence (<->), which you can find like so:

Search (Zeq_bool) (_ <-> _).
(* Zeq_is_eq_bool: forall x y : Z, x = y <-> Zeq_bool x y = true *)

Here is how we can use it:

From Coq Require Import Bool ZArith.
Open Scope Z.

Lemma Zneq_bool_Zeq_bool (a b : Z) : Zneq_bool a b = negb (Zeq_bool a b).
Proof. now unfold Zeq_bool, Zneq_bool; destruct (a ?= b). Qed.

Theorem Zneq_to_neq (a b : Z) : Zneq_bool a b = true -> a <> b.
Proof.
  rewrite Zeq_is_eq_bool,Zneq_bool_Zeq_bool, not_true_iff_false, negb_true_iff.
  trivial.
Qed.

Incidentally, Zeq_bool / Zneq_bool functions are deprecated (see the comments in Coq.ZArith.Zbool file):

We now provide a direct Z.eqb that doesn't refer to Z.compare. The old Zeq_bool is kept for compatibility.