我如何证明所有的P q:支柱，(P -> Q ) -> P) -> P) -> Q) ->Q)？

Question

我对coq很陌生，所以如果你只说自我介绍的话。我不知道该介绍什么。所以要有针对性，比如。(简介p. q.)会很有帮助的。

Answer 1

幸运的是，您的目标可以通过auto策略自动解决。如果使用它的变体info_auto，Coq将告诉您解决方案的步骤。

Goal  forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) -> Q.
  info_auto.

然后，您可以自己重放这个证明，并在intros策略中添加注释和显式变量名称，您将了解auto使用的策略(当结论是forall、含义或原子命题时该怎么办)。

 Restart. 
  intros P Q H.
  apply H (* no-choice ! *).
  intro H0.         
  apply H0.  (* no other possibility ! *)
  intro p. 
  apply H. (* no alternative ! *)
  intros _. 
  assumption. 
Qed.