0

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,

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
saeed M
  • 21
  • 7

1 Answers1

3

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43