CODEWITHSUNDEEP
coqcoq-tactic
Zazaeil
Zazaeil

Reputation: 4109

Coq: proving `P -> ~P -> Q` without `contradiction` tactic?

I am learning Coq and I just discovered that it is constructive.

That's one way I can prove that "contradiction implies everything" and it works:

Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.
Proof.
  intros P Q p not_p.
  contradiction.
  Qed.

Note that no Q was constructed, so I assume contradiction is built-in into the Coq proof engine. It seems to me that otherwise one has to show how Q is consructed, and it isn't possible for any Q, thus the theorem above can not be proved then. In particular I can not prove the theorem above in the following (pseudo) code:

intros P Q p not_p.
introduce P \/ Q. # here I have to construct Q, right?.. that's the point where Coq's "constructivity" becomes an obstruction
introduce ~P \/ Q. # same here
run case analysis on both and figure out that Q must be true.
Qed.

Am I right?

Upvotes: 1

Views: 196

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

In Coq, negation is defined as follows:

Inductive False : Prop := 
  (* An inductive proposition with no constructors *). 
Definition not (P : Prop) : Prop := P -> False.

The lemma you proved is a consequence of the following more primitive principle:

Lemma exfalso (Q : Prop) : False -> Q.
Proof. intros contra. destruct contra. Qed.

Intuitively, if we know that an inductive proposition P holds and we want to show that some other Q holds as well, all we need to do is consider all the constructors that could have been applied to establish P. This is what the destruct tactic does. But when P is False, there are no constructors, so we do not have to do anything.

I like to thing of this situation as follows: it is not the case that this process constructed a proof of Q, but rather that we showed there we do not have to construct anything.

Given exfalso, it is easy to prove your original statement in more primitive terms (I advice you to walk through this proof to see what is going on!):

Goal forall P Q : Prop, P -> ~P -> Q.
Proof.
intros P Q Hyes Hno.
apply exfalso. apply Hno. apply Hyes.
Qed.

Upvotes: 1

Josh Grosso
Josh Grosso

Reputation: 2114

contradiction isn't actually necessary here, and there are two main reasons why:

  1. ~ P is a standard library notation for P -> False, which means that if you have hypotheses P and ~ P, you can apply ~ P to P to get False.

  2. The standard library defines False like so: Inductive False : Prop :=. That means that if you destruct a hypothesis of type False, the resulting case analysis will have zero cases. That is to say, your proof will be done!

So, to summarize, you can prove your theorem like so:

Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.
Proof.
  intros P Q p not_p.
  apply not_p in p.
  destruct p.
Qed.

Upvotes: 1

Related Questions