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,

4

1 に答える 1

3

この補題は偽なので証明できません。そして、これがビットの場合の反例ですwordsize = 8(一般化はあなたに任せます)。

i = 256とを取りましょうt = 255。明らかに、補題の前提は真です ( t < i)。次に、(Int.repr i) = 0整数のラップアラウンドのため。(Int.repr t) = 255、この場合オーバーフローがないためですが、補題が述べているようではなく、前述の値に対してltu返されます。truefalse

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

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

定理 については、 と はではなくに属しているため、eq_false補題とは大きく異なります。xyintZ

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

お役に立てれば。

于 2016-08-23T08:30:35.190 に答える