Нужно найти правильную тактику над 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

Надеюсь это поможет.