如何在 Coq 中将 "Zneq_bool a b = true" 转换为 "a <> b" 的见证？

Question

我正在尝试证明以下定理：

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.

我收到以下错误：

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}

我认为 "deep" 出了问题，但我不知道如何调试它。帮助将不胜感激。

Answer 1

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

一般来说，你可以apply一个像上面那样的蕴涵，如果你有一个逻辑等价（<->），你可以rewrite，你可以这样找到：

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

下面是我们如何使用它：

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.

顺便说一句，Zeq_bool / Zneq_bool 函数 已弃用 （请参阅 Coq.ZArith.Zbool 文件中的注释）：

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

如何在 Coq 中将 "Zneq_bool a b = true" 转换为 "a <> b" 的见证？

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

coq

coq-tactic