如何在Coq中证明以下内容？

Question

如何在Coq中证明以下内容？

(p->q)->(~q->~p)

这是我开始的。

Lemma work : (forall p q : Prop, (p->q)->(~q->~p)).
Proof.
  intros p q.
  intros p_implies_q not_q.
  intros p_true.

Answer 1

Lemma work : (forall p q : Prop, (p->q)->(~q->~p)).
Proof.
  intros p q.
  intros p_implies_q not_q.
  intros p_true.
  apply not_q.
  apply p_implies_q.
  auto.
Qed.

一些评论:

• 每当你有一个目标的形式 A -> B，您可以使用 intros H 命令添加 H: A 到你的前提列表中，并留下一个目标。B.

• ~P 是一个句法糖，用于 P -> False. 因此，如果你的目标是 ~P那么 intros H 会加 H: P 到您的处所列表，并将目标减少到 False

• 如果你的目标是 Q 而你有一个前提 H: P -> Q，执行命令 apply H 将改变你的目标为 P

• 连续 intros 命令可以合二为一，所以证明可以缩短为

  Proof.
    intros p q p_implies_q not_q p_true.
    apply not_q.
    apply p_implies_q.
    auto.
  Qed.