boolean - Coq 中的 prop 和 bool

Question

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

if 1 = 2 then 1 else 2

1 = 2 当然是 Prop 而不是 bool。

Answer 1

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

当然，1 = 2 是一个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 ...