如何在Coq中证明逻辑等价？

Question

我想在Coq中证明以下逻辑等价。

（对 - > Q） - >（〜Q->〜p）的

这是我的尝试。我怎样才能解决这个问题？

Lemma work : (forall p q : Prop, (p->q)->(~q->~p)).
Proof.
intros p q.
intros p_implies_q not_q_implies_not_p.
refine (not_q_implies_not_p).
refine (p_implies_q).
Qed.

Answer 1

两件事可能会有所帮助。

首先，在你的第二个intros，第二个假设不是not_q_implies_not_p，而是简单地not_q。这是因为目标是（在intros p_implies_q之后）~q -> ~p，所以intros的另一个调用只引入了这个目标的假设：~q，并留下~p作为新的目标。

其次，请记住，~p只是意味着p -> False，它允许我们从~p的目标引入另一个假设。这也意味着你可以使用像~p这样的前提来证明False，假设你知道p是真的。

所以你的证据应该从类似的东西开始

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