Search code examples
logiccoqtheorem-proving

How to prove A \/ False -> A in Coq?

I am learning Coq and trying to prove "A \/ False -> A" but I am not sure what am I doing wrong.

I tried the following code:

Goal forall A False : Prop, A \/ False -> A.

Proof.

intros A False H.

destruct H as [HP | HQ].

apply HP.

exfalso.

apply HQ.

And expected to establish the premise for exfalso by applying the assumption HQ but it did not work and I got the following message: "Unable to unify "False" with "Logic.False"."

What am I missing?

Solution

  • In your statement you quantify over a proposition that you name False. There is a clash with the False that is defined in Logic. So in your environment you have two False your proposition and the one in Logic and they differ.

    The statement you want to prove is equivalent to forall A B : Prop, A \/ B -> A