CODEWITHSUNDEEP
coq
yanhan
yanhan

Reputation: 3537

coq change premise 'negation of not equal' to 'equal'

Suppose I have a premise like this:

H2: ~ a b c <> a b c

And I wish to change it to:

a b c = a b c

Where

a is Term -> Term -> Term

b and c are both Term

How can I do it? Thanks!

Upvotes: 1

Views: 1988

Answers (2)

t0yv0
t0yv0

Reputation: 4724

Just a little thought to add to Ptival's answer - if your desired goal was not trivially solved by reflexivity, you could still make progress provided you had decidable equality on your Term, for example by applying this little lemma:

Section S.
  Parameter T : Type.
  Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}.

  Lemma not_ne : forall (x y : T), ~ (x <> y) -> x = y.
  Proof.
    intros.
    destruct (T_eq_dec x y); auto.
    unfold not in *.
    assert False.
    apply (H n).
    contradiction.
  Qed.
End S.

Upvotes: 1

Ptival
Ptival

Reputation: 9437

If you unfold the definitions of ~ and <>, you hypothesis has the following type:

H2: (a b c = a b c -> False) -> False

Therefore, what you wish to achieve is what logicians usually call "double negation elimination". It is not an intuitionistically-provable theorem, and is therefore defined in the Classical module of Coq (see http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Logic.Classical_Prop.html for details):

Classical.NNPP : forall (p : Prop), ~ ~ p -> p

I assume your actual problem is more involved than a b c = a b c, but for the sake of mentioning it, if you really care about obtaining that particular hypothesis, you can safely prove it without even looking at H2:

assert (abc_refl : a b c = a b c) by reflexivity.

If your actual example is not immediately reflexive and the equality is actually false, maybe you want to turn your goal into showing that H2 is absurd. You can do so by eliminating H2 (elim H2., which is basically doing a cut on the False type), and you will end up in the context:

H2 : ~ a b c <> a b c
EQ : a b c = a b c
=====================
False

I'm not sure whether all of this helps, but you might have oversimplified your problem so that I cannot provide more insight on what your real problem is.

Upvotes: 3

Related Questions