Coq:prove Prop隐含自然数的算术关系

Question

我试图在 coq 中证明以下引理 --

Lemma less_than_two_equivalent: forall x, less_than_two x = true -> x < 2.

基于下面的定义。

Fixpoint less_than (a b:nat): bool:=
match a, b with
|0, 0 => false
|0, _ => true
|S a', 0 => false
|S a', S b' => less_than a' b'
end.

Fixpoint less_than_two (x:nat) : bool  := if less_than x 2 then true else false.

从数学上讲，只有 2 种情况，0 或 1。而且 destruction应该是锤子，但是没有足够的关于 S x 的信息来进一步推理。

我应该将 less_than 修改为归纳数据类型吗？如果不是，如何解决？

Answer 1

让我从重新定义 less_than_two 开始。首先，它不是递归的，所以将它定义为 Fixpoint 没有意义。接下来，if less_than x 2 then true else false 本质上与 less_than x 2 相同。在这一点上我不会费心引入一个新的定义，所以你的引理变成了

Lemma less_than_two_equivalent x: less_than x 2 = true -> x < 2. 
Proof.
  do 2 (destruct x; auto); simpl.
  destruct x; discriminate.
Qed.

我不知道你的证明究竟出了什么问题，但你可能又忘记了 destruct x 一次。当您看到 less_than x 0 = true -> S (S x) < 2 时，您仍然不能使用 discriminate 来完成您的目标，因为评估在变量上被阻止 - less_than 第一个模式匹配 a 参数然后才检查 b。 x 的破坏解除了计算的阻碍并让 Coq 看到你有 false = true 作为你的前提，因此目标变得可证明。

请注意，这取决于比较函数的特定实现。你选了这个吗

(* (!) the [struct] annotation is important here, as well as as
   the order of the parameters [b, a] in the match expression *)

Fixpoint less_than' (a b : nat) {struct b} : bool :=
  match b, a with
  | 0, _ => false
  | _, 0 => true
  | S b', S a' => less_than' a' b'
  end.

你会得到更简单的证明（少一个destruct）：

Lemma less_than_two_equivalent x: less_than' x 2 = true -> x < 2. 
Proof.
  do 2 (destruct x; auto).
  discriminate.
Qed.

Coq:prove Prop隐含自然数的算术关系

Coq:prove Prop implies arithmetic relations of natural number

math

coq

proof

prop