需要找到合适的战术来对付Int.lt

Question

我有以下引理，但无法证明:

Lemma my_comp2: forall i t:Z,
t<i -> Int.ltu (Int.repr i) (Int.repr t) = false.
Proof.
....

我找到了相等的策略(链接)，但找不到lt/ltu或gt/gtu的策略:

Theorem eq_false: forall x y, x <> y -> eq x y = false.

任何帮助将不胜感激!

谢谢,

Answer 1

这个引理不能证明，因为它是假的。这里是wordsize = 8位的反例(我将把概括留给你)。

取i = 256和t = 255。显然，引理的前提为真(t < i)。然后，(Int.repr i) = 0因为整型而绕。(Int.repr t) = 255，因为在这种情况下没有溢出，但ltu将为上述值返回true，而不是引理所述的false。

Definition i := 256.
Definition t := 255.
Eval compute in ltu (repr i) (repr t).  (* returns true *)

<人力资源>

关于eq_false定理，它与你的引理有很大的不同，因为x和y属于int，而不是Z:

Check eq_false
 : forall x y : int, x <> y -> eq x y = false