1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
Require Import ZArith Lia.
Open Scope Z_scope.
(** bug 4132: omega was using "simpl" either on whole equations, or on
delimited but wrong spots. This was leading to unexpected reductions
when one atom (here [b]) is an evaluable reference instead of a variable. *)
Lemma foo
(x y x' zxy zxy' z : Z)
(b := 5)
(Ry : - b <= y < b)
(Bx : x' <= b)
(H : - zxy' <= zxy)
(H' : zxy' <= x') : - b <= zxy.
Proof.
lia. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
Qed.
Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
lia. (* Pierre L: according to a comment of bug report #4132,
this might have triggered "index out of bounds" in the past,
but I never managed to reproduce that in any version,
even before my fix. *)
Qed.
Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
lia. (* Pierre L: according to a comment of bug report #4132,
this might have triggered "Failure(occurrence 2)" in the past,
but I never managed to reproduce that. *)
Qed.
|
