CODEWITHSUNDEEP
coq
Lepticed
Lepticed

Reputation: 381

Add an assertion and its negation to Coq

I want to prove the following theorem:

Theorem T1 : forall s x,
  Ps s x -> PPs s x /\ ~IPs s x \/ ~PPs s x /\ IPs s x.

where Ps is a primitive and PPs and IPs are defined as follow (F is also a primitive):

Definition PPs x y := Ps x y /\ ~ F y x.
Definition IPs x y := Ps x y /\ F y x.

So I want a theorem that states that if Ps s x then we have either PPs s x xor IPs s x (I don’t how to write the XOR operator in Coq, so I decomposed it).

Now, I would like to introduce an assumption in my proof about the proposition F x s. I would like to have it and its negation (not at the same time), this way, I could easily prove my theorem. However, I don’t how to do this. So my question is how to prove something assuming a new proposition, then its negation?

(Do not hesitate to change the title if necessary. I had no idea.)

Upvotes: 0

Views: 71

Answers (1)

Ana Borges
Ana Borges

Reputation: 1376

If I understand correctly, you are looking for the law of excluded middle. So you want to assume F x s \/ ~ F x s and reason differently in each case.

If you know that F x s is decidable, for example if F x s : bool, then the disjunction is provable and one way you can get it into your context is as follows.

Lemma name : ... .
Proof.
  ...
  destruct (F x s) eqn:eF.
  - (* assume F x s = true *)  admit.
  - (* assume F x s = false *) admit.

If you don't know that F x s is decidable, which is the standard if F x s : Prop and you have no other assumptions, then you can make do by assuming the law of excluded middle. This is not part of the base theory of Coq, but it is admissible:

Require Import Classical.
Check classic.
(* classic : forall P : Prop, P \/ ~ P *)

So your development could look like this:

Require Import Classical.

Lemma name : ... .
Proof.
  ...
  destruct (classic (F x s)) as [yesF|notF].
  - (* assume F x s *) admit.
  - (* assume ~ F x s *) admit.

Upvotes: 1

Related Questions