Take the 2-minute tour ×

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


a is Term -> Term -> Term

b and c are both Term

How can I do it? Thanks!

share|improve this question

2 Answers 2

up vote 3 down vote accepted

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

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.

share|improve this answer
Hi Ptival, I've simplified the overall problem, but overall it can be solved just by solving what I've posted above. Didn't realize it requires NNPP. Thanks! And apologies for the really late reply. –  yanhan Mar 23 '13 at 0:36

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.
    destruct (T_eq_dec x y); auto.
    unfold not in *.
    assert False.
    apply (H n).
End S.
share|improve this answer

Your Answer


