如何证明所有人（p q：Prop），〜p->〜（（p-> q）-> p）。使用coq

问题描述

我对coq编程完全陌生，无法在定理下证明。我需要有关如何解决以下构造问题的步骤的帮助吗？

I am completely new to coq programming and unable to prove below theorem. I need help on steps how to solve below construct?

我尝试了以下方式的证明。
公理为公理经典：forall P：Prop，P \ /〜P。

I tried the proof below way.Given axiom as Axiom classic : forall P:Prop, P \/ ~ P.

Theorem PeirceContra: forall (p q:Prop), ~ p -> ~((p  -> q)  -> p).
Proof.
  unfold not.
  intros.
  apply H.
  destruct (classic p) as [ p_true | p_not_true].
  - apply p_true.
  - elimtype False. apply H.
Qed.

使用elimtype后获得子目标并将H用作

Getting subgoal after using elimtype and apply H as

1 subgoal
p, q : Prop
H : p -> False
H0 : (p -> q) -> p
p_not_true : ~ p
______________________________________(1/1)
p

但是现在我被困在这里，因为我无法使用给定公理的p_not_true构造来证明P……请提出一些帮助……
我不清楚如何使用给定证明逻辑的公理。......

But now I am stuck here because I am unable to prove P using p_not_true construct of given axiom......Please suggest some help......I am not clear how to use the given axiom to prove logic................

推荐答案

这个引理可以证明建设性地。如果您考虑可以采取哪些步骤来取得进步，引理就证明了自己：

This lemma can be proved constructively. If you think about what can be done at each step to make progress the lemma proves itself:

Lemma PeirceContra :
  forall P Q, ~P -> ~((P -> Q) -> P).
Proof.
  intros P Q np.
  unfold "~".
  intros pq_p.
  apply np.     (* this is pretty much the only thing we can do at this point *)
  apply pq_p.   (* this is almost inevitable too *)

  (* the rest should be easy *)
(* Qed. *)

这篇关于如何证明所有人（p q：Prop），〜p->〜（（p-> q）-> p）。使用coq的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！