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
The original theorem that you had was false, unfortunately. The problem was that
Val.cmp
returnsVundef
if one of the compared values is not an integer. Check the definition ofcmp
andcmp_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:
Having the
Vint
andSome
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 unfoldingVal.cmp
,Val.cmp_bool
, andInt.cmp
, and rewriting withInt.eq_false
.