coq - 如何证明coq中的引理 "(P\/Q)/\~P -> Q."？

Question

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

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

一般而言，如何证明诸如 false->P、P/~P 等简单命题？

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