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

Question

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

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

通常，如何证明简单的命题，例如 false->P、P/~P 等？

Answer 1

您缺少的策略是contrast ，用于证明包含矛盾假设的目标。因为你不允许使用矛盾，我相信你打算应用的引理是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.

Answer 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.

Answer 3

为了证明所有这些简单的事情，您拥有一系列策略tauto,rtauto和。intuitionfirstorder

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

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

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

Answer 4

请记住，这~P意味着P->False，并且反转False假设完成了目标（因为False没有构造函数）。所以你真的只需要applyand 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.