coq - 需要在 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

希望这可以帮助。