Как проверить равенство между двумя целыми числами в 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 в названии).

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.