CODEWITHSUNDEEP
mathlogiccoqdiscrete-mathematics
user11093107
user11093107

Reputation:

How to prove logic equivalence in Coq?

I want to prove the following logic equivalence in Coq.

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

Here is what I attempted. How can I fix this?

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.

Upvotes: 0

Views: 173

Answers (1)

SCappella
SCappella

Reputation: 10424

Two things that might help.

First, in your second intros, the second hypothesis is not not_q_implies_not_p, but rather, simply not_q. This is because the goal is (after intros p_implies_q) ~q -> ~p, so another invocation of intros only brings in the hypothesis of this goal: ~q, and leaves ~p as the new goal.

Second, remember that ~p simply means p -> False, which allows us to introduce another hypothesis from the goal of ~p. This also means that you can use a premise like ~p to prove False, assuming you know that p is true.

So your proof should start out something like

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

Upvotes: 1

Related Questions