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

Question

我试图用tatics [intros],[apply],[assume],[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.