Search code examples
coqcompcert

comparing two unequal values in coq

I'm proving this lemma:

Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.

Lemma test: forall (val1 val2: int), ((Vint val1) <> (Vint val2)) -> (Some (Val.cmp Ceq (Vint val1) (Vint val2)) = Some Vfalse).
Proof.

Admitted.

I've tried unfolding not, Val.cmp, ... and using rewrite over H but didn't go anywhere. Any help is appreciated.

Thanks

Solution

  • The original theorem that you had was false, unfortunately. The problem was that Val.cmp returns Vundef if one of the compared values is not an integer. Check the definition of cmp and cmp_bool here.

    The new theorem that you have is true, but is not stated in a very useful form. It is better to state it like this:

    forall val1 val2, val1 <> val2 -> Val.cmp Ceq (Vint val1) (Vint val2) = Vfalse

    Having the Vint and Some constructors around the equalities does not change the truth value of your theorem, but makes it harder to apply in most concrete settings. This result should follow by unfolding Val.cmp, Val.cmp_bool, and Int.cmp, and rewriting with Int.eq_false.