在"如果-然后-否则"条件下拆分大小写

Question

这是一个愚蠢的初学者问题，但我如何证明这个定理？

Open Scope Z.
Theorem test : forall x y:Z, (x > 0 -> y = 1) / (x <= 0 -> y = 2) -> y >= 1.
Proof.
intros.
destruct x.
destruct H.
(* stuck *)
Qed.

我真正想做的是将一个if-then-else语句建模为一个Prop，并在证明它的条件下进行案例拆分。我陷入了这样的上下文：

y: nat
H: 0 > 0 -> y = 1
-----------------
(1/3)
y >= 1
(2/3)
y >= 1
(3/3)
y >= 1

我有点明白，要摆脱不可能的情况，我需要在假设中找到矛盾，但我该怎么做呢？

欢迎就如何做得更好提出建议，例如，这是模拟if-then-else的最佳方式吗？

Answer 1

我如何证明这个定理？

Theorem test : forall x y:Z, (x > 0 -> y = 1) / (x <= 0 -> y = 2) -> y >= 1.

你的定理是不正确的。

假设H: x > 0 -> y = 1但x实际上是0，那么你没有办法证明y >= 1因为你对y一无所知。

也许你的意思是使用and(/)而不是or？ 然后这里有一个证明，它使用lia来完成繁琐的Z算术。

Require Import ZArith Lia. Open Scope Z.
Theorem test : forall x y:Z, (x > 0 -> y = 1) / (x <= 0 -> y = 2) -> y >= 1.
Proof.  intros x y [H1 H2]. enough (x>0 / x<=0) as [H|H]; lia. Qed.

Answer 2

我认为您正在寻找的是引理

Z_lt_le_dec : forall x y : Z, {x < y} + {y <= x}

的图书馆。{ … } + { … }的意思类似于/，即它是一种析取，但在这里这种析取构造了一个Set而不是Prop的类型。这意味着，虽然你不能使用/的析取来构建一个返回nat的函数(因为Coq强制认为命题应该是无关紧要的)，但你可以使用{ … } + { … }的函数。你可以写

Definition test (x : Z) := if (Z_lt_le_dec 0 x) then 1 else 2.

这是像这样的模式匹配的语法糖

Definition test (x : Z) := match (Z_lt_le_dec 0 x) with
| left _ => 1
| right _ => 2
end.

其中left和right是{ … } + { … }的两个构造函数。

要检查此test是否发挥了应有的作用，您现在可以尝试去证明

Lemma test_ge1 (x : Z) : 1 <= test x.