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?

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.

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

Is there any disadvantage in using classical reasoning?

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.

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?

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: Jun 18 2024 at 20:02 UTC