Skip to content

Commit f796e05

Browse files
fajbfajb
committed
fix test-suite
1 parent dc34c3a commit f796e05

File tree

8 files changed

+476
-229
lines changed

8 files changed

+476
-229
lines changed

‎test-suite/bugs/bug_16803.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
From Stdlib Require Import Lia.
22
From Stdlib Require Import ZArith.
3-
Import ZifyClasses.
3+
Import TifyClasses.
44

55
Module Test1.
66

‎test-suite/bugs/bug_18151.v‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,25 +3,25 @@ From Stdlib Require Import Zify ZifyClasses.
33
Import Z.
44
Open Scope Z_scope.
55

6-
#[global] Instance sat_mod_le : ZifyClasses.Saturate BinIntDef.Z.modulo :=
6+
#[global] Instance sat_mod_le : Saturate BinIntDef.Z.modulo :=
77
{|
8-
ZifyClasses.PArg1 := fun a => 0 <= a;
9-
ZifyClasses.PArg2 := fun b => 0 < b;
10-
ZifyClasses.PRes := fun a b ab => ab <= a;
11-
ZifyClasses.SatOk := mod_le
8+
PArg1 := fun a => 0 <= a;
9+
PArg2 := fun b => 0 < b;
10+
PRes := fun a b ab => ab <= a;
11+
SatOk := mod_le
1212
|}.
1313
Add Zify Saturate sat_mod_le.
1414

1515
Lemma shiftr_lbound a n:
1616
0 <= a -> True -> 0 <= (Z.shiftr a n).
1717
Proof. now intros; apply Z.shiftr_nonneg. Qed.
1818

19-
#[global] Instance sat_shiftr_lbound : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
19+
#[global] Instance sat_shiftr_lbound : Saturate BinIntDef.Z.shiftr :=
2020
{|
21-
ZifyClasses.PArg1 := fun a => 0 <= a;
22-
ZifyClasses.PArg2 := fun b => True;
23-
ZifyClasses.PRes := fun a b ab => 0 <= ab;
24-
ZifyClasses.SatOk := shiftr_lbound
21+
PArg1 := fun a => 0 <= a;
22+
PArg2 := fun b => True;
23+
PRes := fun a b ab => 0 <= ab;
24+
SatOk := shiftr_lbound
2525
|}.
2626
Add Zify Saturate sat_shiftr_lbound.
2727

‎test-suite/micromega/bug_18158.v‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -40,42 +40,42 @@ Proof.
4040
intros; apply shiftr_ubound; assumption.
4141
Qed.
4242

43-
#[global] Instance sat_shiftr_lbound : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
43+
#[global] Instance sat_shiftr_lbound : TifyClasses.Saturate BinIntDef.Z.shiftr :=
4444
{|
45-
ZifyClasses.PArg1 := fun a => 0 <= a;
46-
ZifyClasses.PArg2 := fun b => True;
47-
ZifyClasses.PRes := fun a b ab => 0 <= ab;
48-
ZifyClasses.SatOk := shiftr_lbound
45+
TifyClasses.PArg1 := fun a => 0 <= a;
46+
TifyClasses.PArg2 := fun b => True;
47+
TifyClasses.PRes := fun a b ab => 0 <= ab;
48+
TifyClasses.SatOk := shiftr_lbound
4949
|}.
50-
Add Zify Saturate sat_shiftr_lbound.
50+
Add Tify Saturate sat_shiftr_lbound.
5151

52-
#[global] Instance sat_shiftr_contr_8 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
52+
#[global] Instance sat_shiftr_contr_8 : TifyClasses.Saturate BinIntDef.Z.shiftr :=
5353
{|
54-
ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 8;
55-
ZifyClasses.PArg2 := fun b => 0 <= b;
56-
ZifyClasses.PRes := fun a b ab => ab < 2 ^ 8;
57-
ZifyClasses.SatOk := shiftrContractive8
54+
TifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 8;
55+
TifyClasses.PArg2 := fun b => 0 <= b;
56+
TifyClasses.PRes := fun a b ab => ab < 2 ^ 8;
57+
TifyClasses.SatOk := shiftrContractive8
5858
|}.
59-
Add Zify Saturate sat_shiftr_contr_8.
59+
Add Tify Saturate sat_shiftr_contr_8.
6060

61-
#[global] Instance sat_shiftr_contr_16 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
61+
#[global] Instance sat_shiftr_contr_16 : TifyClasses.Saturate BinIntDef.Z.shiftr :=
6262
{|
63-
ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 16;
64-
ZifyClasses.PArg2 := fun b => 0 <= b;
65-
ZifyClasses.PRes := fun a b ab => ab < 2 ^ 16;
66-
ZifyClasses.SatOk := shiftrContractive16
63+
TifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 16;
64+
TifyClasses.PArg2 := fun b => 0 <= b;
65+
TifyClasses.PRes := fun a b ab => ab < 2 ^ 16;
66+
TifyClasses.SatOk := shiftrContractive16
6767
|}.
68-
Add Zify Saturate sat_shiftr_contr_16.
68+
Add Tify Saturate sat_shiftr_contr_16.
6969

7070

71-
#[global] Instance sat_shiftr_contr_32 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
71+
#[global] Instance sat_shiftr_contr_32 : TifyClasses.Saturate BinIntDef.Z.shiftr :=
7272
{|
73-
ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 32;
74-
ZifyClasses.PArg2 := fun b => 0 <= b;
75-
ZifyClasses.PRes := fun a b ab => ab < 2 ^ 32;
76-
ZifyClasses.SatOk := shiftrContractive32
73+
TifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 32;
74+
TifyClasses.PArg2 := fun b => 0 <= b;
75+
TifyClasses.PRes := fun a b ab => ab < 2 ^ 32;
76+
TifyClasses.SatOk := shiftrContractive32
7777
|}.
78-
Add Zify Saturate sat_shiftr_contr_32.
78+
Add Tify Saturate sat_shiftr_contr_32.
7979

8080

8181
Goal forall x y ,
@@ -85,7 +85,7 @@ Goal forall x y ,
8585
-> Z.le (Z.shiftr y 8) 255
8686
-> Z.le (Z.shiftr x 24) 255.
8787
intros.
88-
Zify.zify_saturate.
88+
Tify.tify_saturate.
8989
(* [xlia zchecker] used to raise a [Stack overflow] error. It is supposed to fail normally. *)
9090
assert_fails (xlia zchecker).
9191
Abort.

‎test-suite/micromega/milp.v‎

Lines changed: 70 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,89 @@
11
Require Import Rbase Rify isZ Lra Zfloor.
22
Local Open Scope R_scope.
33

4+
Unset Lra Cache.
5+
46
Lemma up0 : up 0%R = 1%Z.
5-
Proof. intros. rify. lra. Qed.
7+
Proof. intros. lra. Qed.
68

79
Lemma up_succ r : up (r + 1)%R = (up r + 1)%Z.
8-
Proof. intros. rify. lra. Qed.
10+
Proof. intros. lra. Qed.
911

1012
Lemma up_IZR z : up (IZR z) = (z + 1)%Z.
1113
Proof.
12-
rify. lra.
14+
lra.
1315
Qed.
1416

1517
Lemma up_shiftz r z : up (r + IZR z)%R = (up r + z)%Z.
1618
Proof.
17-
rify. lra.
19+
lra.
20+
Qed.
21+
22+
Lemma div_inv : forall y x,
23+
1 = 1 + (y - x) / x ->
24+
(y - x) * / x = 0.
25+
Proof. intros. lra. Qed.
26+
27+
Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R) (x5 : R) (x6 : R)
28+
(H0 : -x2 + x6 = R0)
29+
(H1 : x6 + -x4 = R0)
30+
(H2 : x2*x3 + -x1*x3 = R0)
31+
(H3 : x4 + -x2*x5 = R0)
32+
(H5 : x2*x3 + -x1*x3 > R0)
33+
, False
34+
.
35+
Proof.
36+
intros.
37+
lra.
38+
Qed.
39+
40+
Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R)
41+
(H0 : x4 >= 0)
42+
(H1 : 1 + -x4 > 0)
43+
(H2 : -x4 + x1 > 0)
44+
(H3 : 1 + -x1 > 0)
45+
(H4 : x2 + -x3 = 0)
46+
(H5 : -x1 > 0)
47+
, False
48+
.
49+
Proof.
50+
intros.
51+
lra.
1852
Qed.
1953

2054

55+
Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R)
56+
(H0 : x4 >= 0)
57+
(H1 : 1 + -x4 > 0)
58+
(H2 : -x4 + x1 > 0)
59+
(H3 : 1 + -x1 > 0)
60+
(H4 : x2 + -x3 = 0)
61+
(H5 : -x1 > 0)
62+
, False
63+
.
64+
Proof.
65+
intros.
66+
lra.
67+
Qed.
68+
69+
70+
71+
72+
Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R) (x5 : R) (x6 : R)
73+
(H0 : -x2 + x6 = R0)
74+
(H1 : x6 + -x4 = R0)
75+
(H2 : x2*x3 + -x1*x3 = R0)
76+
(H3 : x4 + -x2*x5 = R0)
77+
(H5 : x2*x3 + -x1*x3 > R0)
78+
, False
79+
.
80+
Proof.
81+
lra.
82+
Qed.
83+
2184
Lemma up_succ2 r n : Zfloor (r + IZR n) = (Zfloor r + n)%Z.
2285
Proof.
23-
rify. lra.
86+
lra.
2487
Qed.
2588

2689
Goal forall x1 x2 x3 x5 x6
@@ -175,7 +238,7 @@ Goal forall e x
175238
0 < ef.
176239
Proof.
177240
intros.
178-
rify. nra.
241+
nra.
179242
Qed.
180243

181244

@@ -185,6 +248,6 @@ Goal forall x v,
185248
v = 1 / (3 * x).
186249
Proof.
187250
intros.
188-
rify. nra.
251+
nra.
189252
Qed.
190253

‎test-suite/micromega/rexample.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,11 +75,12 @@ Proof.
7575
lra.
7676
Qed.
7777

78-
Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
78+
(*Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
7979
Proof.
8080
intros.
8181
psatz R 3.
8282
Qed.
83+
*)
8384

8485
Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
8586
Proof.

‎test-suite/micromega/witness_tactics.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
From Stdlib Require Import ZArith QArith.
22
From Stdlib.micromega Require Import RingMicromega EnvRing Tauto.
3-
From Stdlib.micromega Require Import ZMicromega QMicromega.
3+
From Stdlib.micromega Require Import ZMicromega QMicromega MMicromega.
44

55
Declare ML Module "rocq-runtime.plugins.micromega".
66

0 commit comments

Comments
 (0)