coq中两种不相等值的比较

Question

我在证明这个引理：

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.

我尝试过展开not, Val.cmp, ...，并在H上使用rewrite，但没有去任何地方。任何帮助都是非常感谢的。

谢谢

Answer 1

不幸的是，你原来的定理是错误的。问题是，如果比较值之一不是整数，Val.cmp返回Vundef。检查cmp和cmp_bool 这里的定义。

你所拥有的新定理是正确的，但不是以一种非常有用的形式表述的。最好这样说：

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

在等式附近使用Vint和Some构造函数并不会改变定理的真值，但会使其更难在大多数具体设置中应用。这个结果应该是展开Val.cmp、Val.cmp_bool和Int.cmp，然后用Int.eq_false重写。