Julin S (Jun 08 2022 at 06:26): 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