Skip to content

Commit 9936c90

Browse files
fajbfajb
committed
Adapt to PR tify
This is the companion of https://github.com/fajb/coq/tree/tify - Update the reflexive proof verifier for lia,lra etc. - Define instances for the [rify] tactic (Require Import Rify)
1 parent 4546804 commit 9936c90

27 files changed

+4782
-1910
lines changed

‎test-suite/micromega/milp.v

Lines changed: 190 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,190 @@
1+
Require Import Rbase Rify isZ Lra Zfloor.
2+
Local Open Scope R_scope.
3+
4+
Lemma up0 : up 0%R = 1%Z.
5+
Proof. intros. rify. lra. Qed.
6+
7+
Lemma up_succ r : up (r + 1)%R = (up r + 1)%Z.
8+
Proof. intros. rify. lra. Qed.
9+
10+
Lemma up_IZR z : up (IZR z) = (z + 1)%Z.
11+
Proof.
12+
rify. lra.
13+
Qed.
14+
15+
Lemma up_shiftz r z : up (r + IZR z)%R = (up r + z)%Z.
16+
Proof.
17+
rify. lra.
18+
Qed.
19+
20+
21+
Lemma up_succ2 r n : Zfloor (r + IZR n) = (Zfloor r + n)%Z.
22+
Proof.
23+
rify. lra.
24+
Qed.
25+
26+
Goal forall x1 x2 x3 x5 x6
27+
(H: -x2 > 0)
28+
(H0: x3 >= 0)
29+
(H1: -x1 + x5 + x6 = 0)
30+
(H2: x1 + -x5 + x6 = 0)
31+
(H4: -x1 > 0)
32+
(H6: x2 + -x3 = 0)
33+
(H7: 3 + 3*x1 = 0),
34+
False.
35+
Proof.
36+
intros.
37+
lra.
38+
Qed.
39+
40+
41+
Lemma spurious_isZ : forall
42+
(x l X : R)
43+
(delta : R)
44+
(iZ1 : isZ x)
45+
(H13 : - (X - l) <= 0)
46+
(iZ2 : isZ X)
47+
(H4 : l > 0)
48+
(iZ2 : isZ X)
49+
(H9 : delta / 2 <> 0)
50+
(iZ2 : isZ X)
51+
(H11 : 0 < delta / 2)
52+
(iZ1 : isZ x)
53+
(H10 : (X <= 0)),
54+
False.
55+
Proof.
56+
intros.
57+
lra.
58+
Qed.
59+
60+
Goal forall (k x:R) (P:Prop)
61+
(Hyp : 0 <= k < 1)
62+
(H2 : k < x < 1 /\ P)
63+
(H3 : k < x < 1),
64+
0 < x.
65+
Proof.
66+
intros.
67+
lra.
68+
Qed.
69+
70+
71+
Ltac cnf := match goal with
72+
| |- Tauto.cnf_checker _ ?F _ = true =>
73+
let f:= fresh "f" in
74+
set(f:=F); compute in f; unfold f;clear f
75+
end.
76+
77+
Ltac collect :=
78+
match goal with
79+
| |- context [ RMicromega.xcollect_isZ ?A ?B ?F] =>
80+
let f := fresh "f" in
81+
set (f:= RMicromega.xcollect_isZ A B F) ; compute in f ; unfold f; clear f
82+
end.
83+
84+
85+
Goal forall (x y:R)
86+
(H : x <= y)
87+
(Hlt : x < y),
88+
y - x = 0 -> False.
89+
Proof.
90+
intros.
91+
lra.
92+
Qed.
93+
94+
Lemma two_x_1 : forall (x:R)
95+
(IZ : isZ x)
96+
(H : 2 * x + 1 = 0),
97+
False.
98+
Proof.
99+
intros.
100+
lra.
101+
Qed.
102+
103+
Goal forall x1 x2 x3 x4,
104+
isZ x1 ->
105+
isZ x2 ->
106+
isZ x3 ->
107+
isZ x4 ->
108+
- x1 + x2 - x3 + x4 >= 0 ->
109+
x1 - x2 + x3 - x4 + 1 > 0 ->
110+
- x1 + x2 - x3 + x4 > 0 ->
111+
False.
112+
Proof.
113+
intros. lra.
114+
Qed.
115+
116+
117+
118+
Goal forall z1 z2 z3, Zfloor (IZR z1 - IZR z2 + IZR z3)%R = (z1 - z2 + z3)%Z.
119+
Proof.
120+
intros.
121+
rify.
122+
(** Now, some work over isZ *)
123+
lra.
124+
Qed.
125+
126+
Goal forall (z : Z) x, IZR z <= x -> (z <= Zfloor x)%Z.
127+
Proof.
128+
rify.
129+
lra.
130+
Qed.
131+
132+
133+
134+
Goal forall (z : Z) x, IZR z <= x < IZR z + 1 -> Zfloor x = z.
135+
Proof.
136+
intros.
137+
rify.
138+
lra.
139+
Qed.
140+
141+
142+
Goal R1 + (R1 + R1) = 3.
143+
Proof.
144+
intros.
145+
rify.
146+
reflexivity.
147+
Qed.
148+
149+
Goal forall x,
150+
x * 3 = 1 ->
151+
False.
152+
Proof.
153+
intros.
154+
Fail lra.
155+
Abort.
156+
157+
Goal forall x,
158+
isZ x ->
159+
x * 3 = 1 ->
160+
False.
161+
Proof.
162+
intros.
163+
lra.
164+
Qed.
165+
166+
167+
168+
Require Import Rfunctions R_sqrt.
169+
170+
Goal forall e x
171+
(He : 0 < e)
172+
(ef := Rmin (e / (3 * (Rabs (x) + 1))) (sqrt (e / 3)) : R)
173+
(H : sqrt (e / 3) > 0)
174+
(H0 : 3 * (Rabs ( x) + 1) >= 1),
175+
0 < ef.
176+
Proof.
177+
intros.
178+
rify. nra.
179+
Qed.
180+
181+
182+
Goal forall x v,
183+
v * (3 * x) = 1 ->
184+
x >= 1 ->
185+
v = 1 / (3 * x).
186+
Proof.
187+
intros.
188+
rify. nra.
189+
Qed.
190+

‎test-suite/output/MExtraction.v

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,11 +57,12 @@ Extract Constant Rinv => "fun x -> 1 / x".
5757
extraction is only performed as a test in the test suite. *)
5858
Recursive Extraction
5959
Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
60+
map_eFormula eFormula
6061
Tauto.abst_form
61-
ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ
62+
ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ RMicromega.cnfR
6263
List.map simpl_cone (*map_cone indexes*)
6364
denorm QArith_base.Qpower vm_add
64-
normZ normQ normQ Z.to_N N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
65+
normZ normQ (*normQ*) Z.to_N N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
6566

6667
(* Local Variables: *)
6768
(* coding: utf-8 *)

‎test-suite/success/tify.v

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
From Stdlib Require Import Reals.
2+
From Stdlib Require Import ZArith.
3+
From Stdlib Require Import ZifyClasses Tify.
4+
5+
(* Inject nat -> Z *)
6+
7+
Instance Inj_nat_Z : InjTyp nat Z.
8+
Proof.
9+
apply (mkinj _ _ Z.of_nat (fun x => (0 <= x)%Z)).
10+
apply Nat2Z.is_nonneg.
11+
Defined.
12+
Add Tify InjTyp Inj_nat_Z.
13+
14+
Instance Op_nat_add_Z : BinOp Nat.add.
15+
Proof.
16+
apply mkbop with (TBOp := Z.add).
17+
simpl. apply Nat2Z.inj_add.
18+
Defined.
19+
Add Tify BinOp Op_nat_add_Z.
20+
21+
Instance Op_eq_nat_eq_Z : BinRel (@eq nat).
22+
Proof.
23+
apply mkbrel with (TR := @eq Z).
24+
simpl. split. congruence.
25+
apply Nat2Z.inj.
26+
Defined.
27+
Add Tify BinRel Op_eq_nat_eq_Z.
28+
29+
30+
(** Inject nat -> R *)
31+
32+
Definition isZ (r:R) := IZR (Zfloor r) = r.
33+
34+
Instance Inj_nat_R : InjTyp nat R.
35+
Proof.
36+
apply (mkinj _ _ INR (fun r => isZ r /\ 0 <= r)).
37+
- intros. split. unfold isZ.
38+
rewrite INR_IZR_INZ.
39+
rewrite ZfloorZ. reflexivity.
40+
apply pos_INR.
41+
Defined.
42+
Add Tify InjTyp Inj_nat_R.
43+
44+
Instance Op_add_R : BinOp Nat.add.
45+
Proof.
46+
apply mkbop with (TBOp := Rplus).
47+
simpl. intros. apply plus_INR.
48+
Defined.
49+
Add Tify BinOp Op_add_R.
50+
51+
Instance Op_eq_nat_eq_R : BinRel (@eq nat).
52+
Proof.
53+
apply mkbrel with (TR := @eq R).
54+
simpl. split; intro. congruence.
55+
apply INR_eq; auto.
56+
Defined.
57+
Add Tify BinRel Op_eq_nat_eq_R.
58+
59+
60+
(* tify selects the right injection *)
61+
62+
Goal forall (x y:nat), (x + y = y + x)%nat.
63+
Proof.
64+
intros.
65+
tify R.
66+
apply Rplus_comm.
67+
Qed.
68+
69+
Goal forall (x y:nat), (x + y = y + x)%nat.
70+
Proof.
71+
intros.
72+
tify Z.
73+
apply Zplus_comm.
74+
Qed.
75+
76+
(* The R instances do not break lia. *)
77+
From Stdlib Require Import Lia.
78+
Goal forall (x y:nat), (x + y = y + x)%nat.
79+
Proof.
80+
intros.
81+
lia.
82+
Qed.

‎theories/All/All.v

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ From Stdlib Require Export micromega.Lqa.
4747
From Stdlib Require Export micromega.Lra.
4848
From Stdlib Require Export micromega.OrderedRing.
4949
From Stdlib Require Export micromega.Psatz.
50+
From Stdlib Require Export micromega.MMicromega.
5051
From Stdlib Require Export micromega.QMicromega.
5152
From Stdlib Require Export micromega.RMicromega.
5253
From Stdlib Require Export micromega.Refl.
@@ -57,8 +58,10 @@ From Stdlib Require Export micromega.ZArith_hints.
5758
From Stdlib Require Export micromega.ZCoeff.
5859
From Stdlib Require Export micromega.ZMicromega.
5960
From Stdlib Require Export micromega.Zify.
61+
From Stdlib Require Export micromega.Tify.
6062
From Stdlib Require Export micromega.ZifyBool.
6163
From Stdlib Require Export micromega.ZifyClasses.
64+
From Stdlib Require Export micromega.TifyClasses.
6265
From Stdlib Require Export micromega.ZifyComparison.
6366
From Stdlib Require Export micromega.ZifyInst.
6467
From Stdlib Require Export micromega.ZifyN.
@@ -67,6 +70,8 @@ From Stdlib Require Export micromega.ZifyPow.
6770
From Stdlib Require Export micromega.ZifySint63.
6871
From Stdlib Require Export micromega.ZifyUint63.
6972
From Stdlib Require Export micromega.Ztac.
73+
From Stdlib Require Export micromega.isZ.
74+
From Stdlib Require Export micromega.Rify.
7075
From Stdlib Require Export funind.FunInd.
7176
From Stdlib Require Export funind.Recdef.
7277
From Stdlib Require Export extraction.ExtrHaskellBasic.

‎theories/Reals/RIneq.v

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2522,6 +2522,9 @@ Qed.
25222522
Lemma succ_IZR : forall n:Z, IZR (Z.succ n) = IZR n + 1.
25232523
Proof. now intros n; unfold Z.succ; apply plus_IZR. Qed.
25242524

2525+
Lemma pred_IZR : forall n:Z, IZR (Z.pred n) = IZR n - 1.
2526+
Proof. now intros n; unfold Z.pred; apply plus_IZR. Qed.
2527+
25252528
Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n.
25262529
Proof.
25272530
intros [| p | p]; unfold IZR; simpl.

‎theories/Strings/PString.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,9 @@ From Stdlib Require Import ZArith.
1212
#[local] Open Scope list_scope.
1313
#[local] Arguments to_Z _/ : simpl nomatch.
1414

15-
#[local] Instance Op_max_length : ZifyClasses.CstOp max_length :=
15+
#[local] Instance Op_max_length : TifyClasses.CstOp max_length :=
1616
{ TCst := 16777211%Z ; TCstInj := eq_refl }.
17-
Add Zify CstOp Op_max_length.
17+
Add Tify CstOp Op_max_length.
1818

1919
#[local] Ltac case_if :=
2020
lazymatch goal with

‎theories/micromega/Lia.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
12
(************************************************************************)
23
(* * The Rocq Prover / The Rocq Development Team *)
34
(* v * Copyright INRIA, CNRS and contributors *)

‎theories/micromega/Lra.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Ltac rchange :=
2929
let __varmap := fresh "__varmap" in
3030
let __ff := fresh "__ff" in
3131
intros __wit __varmap __ff ;
32-
change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ;
32+
change (Tauto.eval_bf (eReval_formula (@find R 0%R __varmap)) __ff) ;
3333
apply (RTautoChecker_sound __ff __wit).
3434

3535
Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.

0 commit comments

Comments
 (0)