## Stream: Coq users

### Topic: Way to solve a pattern of goal

#### Julin S (Jun 08 2022 at 06:26):

If we got a goal like this:

``````A : Set
a b : A
P : A -> A -> Prop
H : P a a
H0 : a <> b -> ~ P a a

========================= (1 / 1)

a = b
``````

Since `H` is considered true, we can say that `H0`'s right part (`~ P a a`) is `False`.

That means, `H0`'s left part (don't know the right term for the left and right parts),
ie, `a <> b` is also `False`, right?

From this we can say that `a = b`.

Which tactics can be used to get this?

#### Olivier Laurent (Jun 08 2022 at 06:38):

You can indeed deduce `~ a <>b` from `H` and `H0`.
But moving from it to `a = b` requires classical logic, so it depends if you want to use classical reasoning or not.

#### Julin S (Jun 08 2022 at 06:50):

Does using classical logic (also) mean importing something? In the source file?

Is there any disadvantage in using classical reasoning?

#### Olivier Laurent (Jun 08 2022 at 06:56):

In order to use classical reasoning, you can add an axiom `forall P : Prop, P \/ ~P` or `forall P : Prop, ~~P -> P`.
You can find them in the standard library: `From Coq Require Import Classical.` (in your case you can them move from `~ a <> b` to `a = b` by using `Classical_Prop.NNPP`).
Concerning disadvantages, a short answer is that you loose constructiveness of your proofs and thus the ability of extracting computational content.

#### Julin S (Jun 08 2022 at 07:27):

Okay, so does classical logic mean adding law of excluded middle?

Could there be a way to solve this goal with just the available hypotheses without classical logic?

#### Olivier Laurent (Jun 08 2022 at 07:33):

Julin S said:

Okay, so does classical logic mean adding law of excluded middle?

Yes for predicates in `Prop` (or double negation elimination for example).

Could there be a way to solve this goal with just the available hypotheses without classical logic?

I don't think so. However a weaker hypothesis is decidability of equality in `A`: `forall a b : A, a = b \/ a <> b` (which is provable in Coq for `A = nat` for example).

Last updated: Sep 23 2023 at 06:01 UTC