Skip to content

Commit 034067d

Browse files
lyonel2017thery
lyonel2017
and
thery
committed
Add support for existentiel quantifier in nsatz
Co-authored-by: Laurent Thery <[email protected]>
1 parent 94590a1 commit 034067d

File tree

5 files changed

+728
-0
lines changed

5 files changed

+728
-0
lines changed

‎doc/stdlib/hidden-files

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ theories/micromega/ZifyComparison.v
5959
theories/micromega/ZifyClasses.v
6060
theories/micromega/ZifyPow.v
6161
theories/micromega/Zify.v
62+
theories/nsatz/ENsatzTactic.v
6263
theories/nsatz/NsatzTactic.v
6364
theories/omega/OmegaLemmas.v
6465
theories/omega/PreOmega.v

‎test-suite/success/ENsatz.v

Lines changed: 204 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
1+
From Stdlib Require Import Znumtheory.
2+
From Stdlib Require Import ZArith.
3+
From Stdlib Require Import ENsatzTactic.
4+
5+
Lemma modulo1 a b c: (a mod b = c -> exists k, a - c = k*b)%Z.
6+
Proof.
7+
intros.
8+
destruct (Z.eq_dec b 0) as [H1 | H1].
9+
- subst.
10+
exists 0%Z.
11+
rewrite Zmod_0_r.
12+
rewrite Z.sub_diag.
13+
rewrite Z.mul_0_l.
14+
trivial.
15+
- specialize (Zmod_divides (a -c)%Z b H1).
16+
rewrite Zminus_mod.
17+
rewrite H.
18+
rewrite Zminus_mod_idemp_r.
19+
rewrite Z.sub_diag.
20+
rewrite Zmod_0_l.
21+
intros [H2 _].
22+
destruct (H2 eq_refl).
23+
exists x.
24+
rewrite Z.mul_comm.
25+
trivial.
26+
Qed.
27+
28+
Lemma modulo2 a b c: ((exists k, a - c = k*b) -> a mod b = c mod b)%Z.
29+
Proof.
30+
intros. destruct H.
31+
rewrite Z.sub_move_r in H.
32+
subst.
33+
rewrite Z.add_comm.
34+
rewrite Z_mod_plus_full.
35+
reflexivity.
36+
Qed.
37+
38+
Lemma div1 a b : ((a | b) -> exists k, b = k*a)%Z.
39+
Proof.
40+
intros.
41+
destruct (Z.eq_dec a 0) as [H1 | H1].
42+
- subst.
43+
exists 0%Z.
44+
apply Z.divide_0_l in H.
45+
subst. reflexivity.
46+
- apply Zdivide_mod in H.
47+
apply (Zmod_divides _ _ H1 ) in H.
48+
destruct H.
49+
rewrite Z.mul_comm in H.
50+
exists x. trivial.
51+
Qed.
52+
53+
Lemma div2 a b : ((exists k, b = k*a) -> (a | b))%Z.
54+
Proof.
55+
intros.
56+
destruct (Z.eq_dec a 0) as [H1 | H1].
57+
- subst.
58+
destruct H.
59+
rewrite Z.mul_0_r in H.
60+
subst.
61+
apply Z.divide_0_r.
62+
- assert (H': exists k:Z, b = a * k).
63+
destruct H. exists x. rewrite Z.mul_comm. trivial.
64+
apply (Zmod_divides _ _ H1) in H'.
65+
apply (Zmod_divide _ _ H1 H').
66+
Qed.
67+
68+
Ltac div_to_equality H x y := try (apply (div1 x y) in H).
69+
70+
Ltac divs_to_equalities :=
71+
lazymatch goal with
72+
| H: (?x | ?y)%Z |- _ => div_to_equality H x y
73+
end.
74+
75+
Ltac mod_to_equality H x y z:= try (apply (modulo1 x y z) in H).
76+
77+
Ltac mods_to_equalities :=
78+
lazymatch goal with
79+
| H: (?z = ?x mod ?y)%Z |- _ => apply symmetry in H; mods_to_equalities
80+
| H: (?x mod ?y = ?z)%Z |- _ => mod_to_equality H x y z
81+
end.
82+
83+
Ltac exists_to_equalities :=
84+
lazymatch goal with
85+
| H: (exists e: ?A, ?b1) |- _ => destruct H
86+
end.
87+
88+
Ltac get_mods_aux a :=
89+
match a with
90+
| context [?a mod ?b] =>
91+
first [get_mods_aux a | get_mods_aux b |
92+
let j := fresh "j" in
93+
let Hj := fresh "Hj" in
94+
remember (a mod b) as j eqn: Hj]
95+
end.
96+
97+
Ltac get_mods :=
98+
match goal with
99+
|- context [?a mod ?b] =>
100+
let t := constr:(a mod b) in
101+
get_mods_aux t
102+
end.
103+
104+
Ltac preprocess :=
105+
intros;
106+
repeat mods_to_equalities;
107+
repeat divs_to_equalities;
108+
repeat exists_to_equalities;
109+
match goal with
110+
| |- (?x mod ?n)%Z = (?y mod ?n)%Z => apply modulo2
111+
| |- (?x | ?y)%Z => apply div2
112+
| |- ?g => idtac
113+
end;
114+
repeat (get_mods; mods_to_equalities; exists_to_equalities).
115+
116+
(*
117+
Examples of the Stdlib.
118+
*)
119+
120+
Example mod_mod_divide: forall a b c : Z, (c | b) -> (a mod b) mod c = a mod c.
121+
Proof.
122+
preprocess.
123+
Time ensatz.
124+
Qed.
125+
126+
Example mod_mod_divide2: forall a b c : Z, (c | b) -> ((a mod b) mod b) mod c = a mod c.
127+
preprocess.
128+
Time ensatz.
129+
Qed.
130+
131+
Example Zmult_mod_idemp_l : forall a b n : Z, (a mod n * b) mod n = (a * b) mod n.
132+
Proof.
133+
preprocess.
134+
Time ensatz.
135+
Qed.
136+
137+
Example Zplus_mod_idemp_l: forall a b n : Z, (a mod n + b) mod n = (a + b) mod n.
138+
Proof.
139+
preprocess.
140+
Time ensatz.
141+
Qed.
142+
143+
Example Zplus_mod: forall a b n : Z, (a + b) mod n = (a mod n + b mod n) mod n.
144+
Proof.
145+
preprocess.
146+
Time ensatz.
147+
Qed.
148+
149+
Example Zmult_mod: forall a b n : Z, (a * b) mod n = (a mod n * (b mod n)) mod n.
150+
Proof.
151+
preprocess.
152+
Time ensatz.
153+
Qed.
154+
155+
Example mod_mod_opp_r: forall a b : Z, (a mod - b) mod b = a mod b.
156+
Proof.
157+
preprocess.
158+
Time ensatz.
159+
Qed.
160+
161+
Example cong: forall a b m : Z, (a - b) mod m = 0%Z -> a mod m = b mod m.
162+
Proof.
163+
preprocess.
164+
Time ensatz.
165+
Qed.
166+
167+
(*
168+
Example of the paper "Automating elementary number-theoretic proofs
169+
using Gröbner bases" by John Harrison.
170+
*)
171+
Example cancellation_congruence a n x y:
172+
(a * x = (a * y) mod n -> (exists e1 e2, a * e1 + n * e2 = 1) -> y mod n = x mod n)%Z.
173+
Proof.
174+
preprocess.
175+
Time ensatz.
176+
Qed.
177+
178+
(*
179+
Examples of the paper "Connecting Gröbner bases programs with Coq to
180+
do proofs in algebra, geometry and arithmetics" by Loïc Pottier.
181+
*)
182+
Definition divides(a b:Z):= exists c:Z, b=c*a.
183+
Definition modulo(a b p:Z):= exists k:Z, a - b = k*p.
184+
Definition ideal(x a b:Z):= exists u:Z, exists v:Z, x = u*a+v*b.
185+
Definition gcd(g a b:Z):= divides g a /\ divides g b /\ ideal g a b.
186+
Definition coprime(a b:Z):= exists u:Z, exists v:Z, 1 = u*a+v*b.
187+
188+
Goal forall a b c:Z, divides a (b*c) -> coprime a b -> divides a c.
189+
unfold divides, modulo, coprime, ideal, gcd.
190+
preprocess.
191+
Time ensatz.
192+
Qed.
193+
194+
Goal forall m n r:Z, divides m r -> divides n r -> coprime m n -> divides (m*n) r.
195+
unfold divides, modulo, coprime, ideal, gcd.
196+
preprocess.
197+
Time ensatz.
198+
Qed.
199+
200+
Goal forall x y a n:Z, modulo (x*x) a n -> modulo (y*y) a n -> divides n ((x+y)*(x-y)).
201+
unfold divides, modulo, coprime, ideal, gcd.
202+
preprocess.
203+
Time ensatz.
204+
Qed.

‎theories/All/All.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ From Stdlib Require Export rtauto.Rtauto.
3636
From Stdlib Require Export omega.OmegaLemmas.
3737
From Stdlib Require Export omega.PreOmega.
3838
From Stdlib Require Export nsatz.NsatzTactic.
39+
From Stdlib Require Export nsatz.ENsatzTactic.
3940
From Stdlib Require Export micromega.DeclConstant.
4041
From Stdlib Require Export micromega.DeclConstantZ.
4142
From Stdlib Require Export micromega.Env.

‎theories/Make.nsatz

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
nsatz/NsatzTactic.v
2+
nsatz/ENsatzTactic.v
23

34
-Q nsatz Stdlib.nsatz

0 commit comments

Comments
 (0)