如何在 Coq 中证明一个荒谬的规则
How to prove an absurd rule in Coq
我必须证明以下陈述，但是在尝试使用 inversion 陈述时出现错误 The type of H is not inductive.：
我怎样才能正确地做到这一点？
Variables phi: Prop.
Section absurd_rule.
Hypothesis H1: phi -> true = false.
Lemma absurd_rule: ~phi.
Proof.
intro H.
inversion H.
End absurd_rule.
inversion 不是这里使用的正确规则，因为 H : phi.
没有什么可反转的
让我们在你intro H:
之后暂停一下
H1 : phi -> true = false
H : phi
______________________________________(1/1)
False
首先注意H1 H : true = false（简单应用）。让我们通过编写 apply H1 in H:
来利用它
H : true = false
______________________________________(1/1)
False
快到了！现在，true = false 必然是矛盾的，这是因为构造函数冲突。
有专门的规则来处理这种情况，命名为 discriminate H.
没有更多的子目标，我们就在那里。完整的证明 session 如下所示：
Variables phi: Prop.
Section absurd_rule.
Hypothesis H1 : phi -> true = false.
Lemma absurd_rule : ~phi.
Proof.
intro H.
apply H1 in H.
discriminate H.
Qed.
此外，值得注意的是，您可以使用 False 来描述底部（小写 false 是不同的东西——归纳布尔值，而不是空的 Prop）。
你的证明的一个更简单的版本就是
Variables phi: Prop.
Section absurd_rule.
Hypothesis H1 : phi -> False.
Lemma absurd_rule : ~phi.
Proof.
assumption.
Qed.
...这不是什么大发现，因为您只是假设 phi 是错误的。
经过一秒钟的思考...
你不能“证明规则”。规则是语言的语义，是您用来从假设中得出结论的法则。它们不是要证明的“定理”，而是一种你用来操纵句子的先验推理。它们甚至与公理不同，它是元级别的东西。你可以证明一个蕴涵，但不能证明一个演绎规则。
因此，您的问题的“解决方案”只是一个身份。您的 absurd_rule 只是 not phi 蕴含 not phi 的引理，这是平凡的事实——请记住，在直觉逻辑中，否定通常 定义为 暗示错误。
我必须证明以下陈述，但是在尝试使用 inversion 陈述时出现错误 The type of H is not inductive.：
我怎样才能正确地做到这一点？
Variables phi: Prop.
Section absurd_rule.
Hypothesis H1: phi -> true = false.
Lemma absurd_rule: ~phi.
Proof.
intro H.
inversion H.
End absurd_rule.
inversion 不是这里使用的正确规则，因为 H : phi.
让我们在你intro H:
H1 : phi -> true = false
H : phi
______________________________________(1/1)
False
首先注意H1 H : true = false（简单应用）。让我们通过编写 apply H1 in H:
H : true = false
______________________________________(1/1)
False
快到了！现在，true = false 必然是矛盾的，这是因为构造函数冲突。
有专门的规则来处理这种情况，命名为 discriminate H.
没有更多的子目标，我们就在那里。完整的证明 session 如下所示：
Variables phi: Prop.
Section absurd_rule.
Hypothesis H1 : phi -> true = false.
Lemma absurd_rule : ~phi.
Proof.
intro H.
apply H1 in H.
discriminate H.
Qed.
此外，值得注意的是，您可以使用 False 来描述底部（小写 false 是不同的东西——归纳布尔值，而不是空的 Prop）。
你的证明的一个更简单的版本就是
Variables phi: Prop.
Section absurd_rule.
Hypothesis H1 : phi -> False.
Lemma absurd_rule : ~phi.
Proof.
assumption.
Qed.
...这不是什么大发现，因为您只是假设 phi 是错误的。
经过一秒钟的思考...
你不能“证明规则”。规则是语言的语义，是您用来从假设中得出结论的法则。它们不是要证明的“定理”，而是一种你用来操纵句子的先验推理。它们甚至与公理不同，它是元级别的东西。你可以证明一个蕴涵，但不能证明一个演绎规则。
因此，您的问题的“解决方案”只是一个身份。您的 absurd_rule 只是 not phi 蕴含 not phi 的引理，这是平凡的事实——请记住，在直觉逻辑中，否定通常 定义为 暗示错误。