如何证明引理“(P \/ Q) /\ ~P -> Q.”在coq？答案

【问题标题】：How to prove the lemma "(P \/ Q) /\ ~P -> Q." in coq?如何证明引理“(P \/ Q) /\ ~P -> Q.”在coq？
【发布时间】：2012-10-03 09:50:36
【问题描述】：

我试图用 tatics [intro]、[apply]、[assumption]、[destruct]、[left]、[right]、[split] 来证明这个引理，但失败了。谁能教我怎么证明？

Lemma a : (P \/ Q) /\ ~P -> Q.
proof.

以及一般情况下如何证明false->P、P/~P等简单命题？

【问题讨论】：

另见How to do cases with an inductive type in Coq，它讨论了一个不同但相关的引理
@cachuanhu 请注意，虽然这不是必需的，但这是习惯性的，如果您将一个对您来说足够好的答案标记为“已接受”，您将获得几个声望点。您的评论表明您找到了克服困难的方法。如果此处没有任何答案符合您的要求，您可以随意编写自己的答案并将其标记为“已接受”。一个公认的答案将有助于像我这样仍在学习这些 Coq 策略的人。
对不起。我投票赞成接受的答案。还有什么我应该做的吗？

标签： coq

【解决方案1】：

您缺少的策略是矛盾，用于证明包含矛盾假设的目标。因为你不允许使用矛盾，我相信你打算应用的引理是False的归纳原则。这样做之后，您可以应用否定命题并通过假设关闭分支。请注意，您可以做得比您的教练要求的更好，并使用没有列出的策略！析取三段论的证明项比较容易写：

Definition dis_syllogism (P Q : Prop) (H : (P ∨ Q) ∧ ¬P) : Q :=
  match H with
    | conj H₁ H₂ =>
      match H₁ with
      | or_introl H₃ => False_ind Q (H₂ H₃)
      | or_intror H₃ => H₃
      end
  end.

【讨论】：

或者，也可以使用策略证明定理，然后简单地“打印”它以找出它是什么。
那么策略是apply (False_ind Q (H₂ H₃))，所以它是一回事；但是如果你想很好地开始使用依赖类型，你最终需要弄清楚如何编写证明术语，所以命题逻辑是一个很好的起点。
是的，“矛盾”等等，我相信也会建立同样的术语。（值得注意的是，即使您使用看起来“更简单”的策略，您可以看到 apply False 是低级别的，它仍然会在幕后构建相同的证明项。）
好吧contradiction 是最简单的方法，并且您已经给出了一个没有使用内置决策程序的标准证明；但操作人员希望仅使用列出的策略进行证明，因此我将 contradiction 的使用转换为“低级”构造。
我一点也不反对你！我认为看到联系很重要，仅此而已。拥有这两种解决方案真是太好了，而且你的解决方案比我的更适合机器！抱歉，如果我似乎不同意您的观点，我只是认为重要的是要看到这两种方法是一回事！

【解决方案2】：

Section Example.

  (* Introduce some hypotheses.. *)
  Hypothesis P Q : Prop.

  Lemma a : (P \/ Q) /\ ~P -> Q.
    intros.
    inversion H.
    destruct H0.
      contradiction.
      assumption.
  Qed.

End Example.

【讨论】：

这个例子可以稍微解释一下！

【解决方案3】：

为了证明所有这些简单的事情，你有一系列策略 tauto、rtauto、intuition 和 firstorder。

我相信它们都比 tauto 强，后者是直觉命题逻辑的完整决策程序。

然后，intuition 允许您输入一些提示和引理以供使用，一阶可以推理一阶归纳法。

doc 中当然有更多详细信息，但这些是您想在此类目标上使用的策略。

【讨论】：

Tks。我找到了解决办法。

【解决方案4】：

请记住，~P 表示P->False，反转False 假设即可完成目标（因为False 没有构造函数）。所以你真的只需要apply 和inversion。

Lemma a : forall (P Q:Prop), (P \/ Q) /\ ~P -> Q.
Proof.
  intros. 
  inversion H.
  inversion H0.
  - apply H1 in H2.  (* applying ~P on P gives H2: False *)
    inversion H2.
  - apply H2.
Qed.

【讨论】：