How to prove forall (p q:Prop), ~p->~((p ->q) ->p)

问题:

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

Theorem PeirceContra: forall (p q:Prop), ~p->~((p ->q) ->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.

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

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

回答1:

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. *)