coq - 比较 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, ...和使用rewrite，H但没有去任何地方。任何帮助表示赞赏。

谢谢

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。