Search code examples
coqcompcert

Need finding the right tactic over Int.lt

I have the following Lemma but couldn't prove it:

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

I found the tactic for equality (link) but can't find the one for lt/ltu or gt/gtu:

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

Any help will be appreciated!

Thanks,

Solution

  • This lemma cannot be proved because it is false. And here is a counterexample for the case where wordsize = 8 bits (I'll leave the generalization to you).

    Let's take i = 256 and t = 255. Clearly, the premise of the lemma is true (t < i). Then, (Int.repr i) = 0 because of the integer wrap around. (Int.repr t) = 255, since there is no overflow in this case, but ltu will return true for the aforementioned values, not false as the lemma states.

    Definition i := 256.
Definition t := 255.

Eval compute in ltu (repr i) (repr t).  (* returns true *)

    As for the theorem eq_false, it differs significantly from your lemma, since x and y belong to int, not Z:

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

    Hope this helps.