Как доказать (p q: Prop), ~ p-> ~ ((p -> q) -> p). используя coq

Question

Я совершенно новичок в программировании coq и не могу доказать теорему ниже. Мне нужна помощь по шагам, как решить ниже построить?

Теорема PeirceContra: forall (p q: Prop), ~ p-> ~ ((p -> q) -> p).

Я попробовал доказательства ниже. Приведенная аксиома как 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 как

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

Но теперь я застрял здесь, потому что не могу доказать P, используя конструкцию p_not_true данной аксиомы ...... Пожалуйста, предложите некоторую помощь ...... Мне не ясно, как использовать данную аксиому для доказательства логики ................

Answer 1

Эта лемма может быть доказана конструктивно.Если вы думаете о том, что можно сделать на каждом этапе, чтобы добиться прогресса, лемма доказывает себя:

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