CODEWITHSUNDEEP
logiccoqtheorem-proving
user1791452
user1791452

Reputation: 31

Proving (p->q)->(~q->~p) using Coq Proof Assistant

I am fairly new to Coq and am trying out sample lemmas from Ruth and Ryan. The proof using natural deduction is pretty trivial, and this is what I want to prove using Coq.

assume p -> q.
  assume ~q.
    assume p.
      q.
      False.
    therefore ~p.
  therefore ~q -> ~p.
therefore (p -> q) => ~q => ~p.

I am stuck at the line 3 assume p.

Can someone please tell me if there is an one-to-one mapping from natural deduction to Coq keywords?

Upvotes: 2

Views: 3668

Answers (4)

illusory0x0
illusory0x0

Reputation: 21

An example of a proof with a Gallina.

Definition PQ_NQNP : 
  forall P : Prop,
  forall Q : Prop,
  (P -> Q) -> (~Q -> ~P)
:= 
  fun P Q pq =>
  fun nq => fun p => nq (pq p)
  .

Definition NQNP_PQ :
  forall P : Prop,
  forall Q : Prop,
  (~Q -> ~P) -> P -> Q 
:= 
fun 
  (P : Prop) 
  (Q : Prop) 
  (H : ~Q -> ~P) 
  (p : P) => 
  let nnq : ~ ~ Q := (fun (e : ~Q) => H e p) in 
  let H' :  ~ ~ Q -> Q := NNPP Q in 
  (H' nnq) 
.

Upvotes: 0

STyx
STyx

Reputation: 41

NNPP is useless !

Theorem easy : forall p q:Prop, (p->q)->(~q->~p).
Proof. intros. intro. apply H0. apply H. exact H1. Qed.

Upvotes: 4

user1791452
user1791452

Reputation: 31

Not that difficult, actually.

Just played around, introduced a double negation, and things fell flat automatically. This is how the proof looks like.

Theorem T1 : (~q->~p)->(p->q).
Proof.
intros.
apply NNPP.
intro.
apply H in H1.
contradiction.
Qed.

Ta daaaa!

Upvotes: 1

Ptival
Ptival

Reputation: 9447

You can start your proof like this:

Section CONTRA.
Variables P Q : Prop.

Hypothesis PimpQ : P -> Q.
Hypothesis notQ  : ~Q.
Hypothesis Ptrue : P.

Theorem contra : False.
Proof.

Here is the environment at that point:

1 subgoal

  P : Prop
  Q : Prop
  PimpQ : P -> Q
  notQ : ~ Q
  Ptrue : P
  ============================
   False

You should be able to continue the proof. It will be a bit more verbose than your proof (on line 4 you just wrote q, here you will have to prove it by combining PimpQ and Ptrue. It should be fairly trivial though... :)

Upvotes: 2

Related Questions