equality - 如何在 Coq 中检查两个整数之间的相等性？

Question

我正在尝试检查 Coq 中两个整数之间的相等性，但我收到此错误：“术语“first = second”的类型为“Prop”，它不是（共）归纳类型。”。Coq 中有没有提供相等检查的库？这是我的代码：

Definition verify_eq (first : Z) (second : Z) : Z :=
   if first = second then 0 else 1.

Answer 1

你很幸运！在Z定义的同一个模块中（我假设 ZArith 在标准库中），有一个术语Z.eqb : Z -> Z -> bool可以对整数相等进行布尔测试（从技术上讲，它在子模块中Z——这就是Z名称中有 a 的原因）。

Require Import ZArith. (* I assume you already imported this, since you're using Z *)

Definition verify_eq (first : Z) (second : Z) : Z :=
   if Z.eqb first second then 0 else 1.