aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4132.v
blob: 806ffb771ffeaac1d9121e610b226c3ab10c3c2e (plain)
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 Omega.
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.
omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
Qed.

Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
omega. (* 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.
omega. (* Pierre L: according to a comment of bug report #4132,
          this might have triggered "Failure(occurence 2)" in the past,
          but I never managed to reproduce that. *)
Qed.