如何证明 forall (p q:Prop), ~p->~((p ->q) ->p)。使用 coq答案

【问题标题】：How to prove forall (p q:Prop), ~p->~((p ->q) ->p). using coq如何证明 forall (p q:Prop), ~p->~((p ->q) ->p)。使用 coq
【发布时间】：2019-04-14 17:00:25
【问题描述】：

我对 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 as 后获取子目标

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

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

【问题讨论】：

您在证明过程中究竟遇到了哪些困难？您是否尝试过展开否定的定义（unfold "~".）？
我试过这种方式
我试过这种方式。 PeirceContra 定理：forall (p q:Prop), ~ p -> ~((p -> q) -> p)。证明。展开不。介绍。将 H. destruct (classic p) 应用为 [ p_true | p_not_true]。 - 应用 p_true。 - elimtype 假。申请 H. Qed。

标签： coq

【解决方案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. *)

【讨论】：