Как доказать логическую эквивалентность в 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_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.