Coq 中的 Prop 和 bool

Question

如何在 if 语句中使用有理数的比较？

if 1 = 2 then 1 else 2

1 = 2当然Prop不是bool。

Answer 1

我不明白 dfan 的回答与问题有什么关系......

当然1 = 2是 a Prop，是 1 等于 2 的陈述。希望你没有这个陈述的证明......

你想要的是一个函数，给定两个自然数1和2，true如果它们相等false则返回，否则返回。

该库Coq.Arith.EqNat为您提供了一个名为beq_nat.

事实上，您可能想要更好的东西，一个返回相等证明或差异证明的函数：

(* In Coq.Arith.Peano_dec *)
Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
                              (* ^ a proof that n = m
                                           ^ or a proof that n <> m *)

if 被重载以处理这些事情，所以你甚至可以写：

if eq_nat_dec 2 3 then ... else ...