Stream: Coq users

Topic: Way to solve a pattern of goal


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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: 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.

view this post on Zulip 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?

view this post on Zulip 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: Feb 06 2023 at 11:03 UTC