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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Export List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Export Morphisms Setoid Bool.
Require Import ZArith_base.
Require Export Algebra_syntax.
Require Export Ncring.
Require Export Ncring_initial.
Require Export Ncring_tac.
Class Cring {R:Type}`{Rr:Ring R} :=
cring_mul_comm: forall x y:R, x * y == y * x.
Ltac reify_goal lvar lexpr lterm:=
(*idtac lvar; idtac lexpr; idtac lterm;*)
match lexpr with
nil => idtac
| ?e1::?e2::_ =>
match goal with
|- (?op ?u1 ?u2) =>
change (op
(@Ring_polynom.PEeval
_ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication) lvar e1)
(@Ring_polynom.PEeval
_ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication) lvar e2))
end
end.
Section cring.
Context {R:Type}`{Rr:Cring R}.
Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.
Proof.
intros. apply mk_reqe; solve_proper.
Defined.
Lemma cring_almost_ring_theory:
almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.
intros. apply mk_art ;intros.
rewrite ring_add_0_l; reflexivity.
rewrite ring_add_comm; reflexivity.
rewrite ring_add_assoc; reflexivity.
rewrite ring_mul_1_l; reflexivity.
apply ring_mul_0_l.
rewrite cring_mul_comm; reflexivity.
rewrite ring_mul_assoc; reflexivity.
rewrite ring_distr_l; reflexivity.
rewrite ring_opp_mul_l; reflexivity.
apply ring_opp_add.
rewrite ring_sub_def ; reflexivity. Defined.
Lemma cring_morph:
ring_morph zero one _+_ _*_ _-_ -_ _==_
0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
Ncring_initial.gen_phiZ.
intros. apply mkmorph ; intros; simpl; try reflexivity.
rewrite Ncring_initial.gen_phiZ_add; reflexivity.
rewrite ring_sub_def. unfold Z.sub. rewrite Ncring_initial.gen_phiZ_add.
rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
rewrite Ncring_initial.gen_phiZ_mul; reflexivity.
rewrite Ncring_initial.gen_phiZ_opp; reflexivity.
rewrite (Zeqb_ok x y H). reflexivity. Defined.
Lemma cring_power_theory :
@Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication).
intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
Lemma cring_div_theory:
div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem.
intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
simpl. apply ring_setoid. Defined.
End cring.
Ltac cring_gen :=
match goal with
|- ?g => let lterm := lterm_goal g in
match eval red in (list_reifyl (lterm:=lterm)) with
| (?fv, ?lexpr) =>
(*idtac "variables:";idtac fv;
idtac "terms:"; idtac lterm;
idtac "reifications:"; idtac lexpr; *)
reify_goal fv lexpr lterm;
match goal with
|- ?g =>
generalize
(@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_
ring_setoid
cring_eq_ext
cring_almost_ring_theory
Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
Ncring_initial.gen_phiZ
cring_morph
N
(fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication)
cring_power_theory
Z.quotrem
cring_div_theory
O fv nil);
let rc := fresh "rc"in
intro rc; apply rc
end
end
end.
Ltac cring_compute:= vm_compute; reflexivity.
Ltac cring:=
intros;
cring_gen;
cring_compute.
Instance Zcri: (Cring (Rr:=Zr)).
red. exact Z.mul_comm. Defined.
(* Cring_simplify *)
Ltac cring_simplify_aux lterm fv lexpr hyp :=
match lterm with
| ?t0::?lterm =>
match lexpr with
| ?e::?le =>
let t := constr:(@Ring_polynom.norm_subst
Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.quotrem O nil e) in
let te :=
constr:(@Ring_polynom.Pphi_dev
_ 0 1 _+_ _*_ _-_ -_
Z 0%Z 1%Z Zeq_bool
Ncring_initial.gen_phiZ
get_signZ fv t) in
let eq1 := fresh "ring" in
let nft := eval vm_compute in t in
let t':= fresh "t" in
pose (t' := nft);
assert (eq1 : t = t');
[vm_cast_no_check (eq_refl t')|
let eq2 := fresh "ring" in
assert (eq2:(@Ring_polynom.PEeval
_ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
[let eq3 := fresh "ring" in
generalize (@ring_rw_correct _ 0 1 _+_ _*_ _-_ -_ _==_
ring_setoid
cring_eq_ext
cring_almost_ring_theory
Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool
Ncring_initial.gen_phiZ
cring_morph
N
(fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication)
cring_power_theory
Z.quotrem
cring_div_theory
get_signZ get_signZ_th
O nil fv I nil (eq_refl nil) );
intro eq3; apply eq3; reflexivity|
match hyp with
| 1%nat => rewrite eq2
| ?H => try rewrite eq2 in H
end];
let P:= fresh "P" in
match hyp with
| 1%nat =>
rewrite eq1;
pattern (@Ring_polynom.Pphi_dev
_ 0 1 _+_ _*_ _-_ -_
Z 0%Z 1%Z Zeq_bool
Ncring_initial.gen_phiZ
get_signZ fv t');
match goal with
|- (?p ?t) => set (P:=p)
end;
unfold t' in *; clear t' eq1 eq2;
unfold Pphi_dev, Pphi_avoid; simpl;
repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
mkpow;simpl)
| ?H =>
rewrite eq1 in H;
pattern (@Ring_polynom.Pphi_dev
_ 0 1 _+_ _*_ _-_ -_
Z 0%Z 1%Z Zeq_bool
Ncring_initial.gen_phiZ
get_signZ fv t') in H;
match type of H with
| (?p ?t) => set (P:=p) in H
end;
unfold t' in *; clear t' eq1 eq2;
unfold Pphi_dev, Pphi_avoid in H; simpl in H;
repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
mkpow in H;simpl in H)
end; unfold P in *; clear P
]; cring_simplify_aux lterm fv le hyp
| nil => idtac
end
| nil => idtac
end.
Ltac set_variables fv :=
match fv with
| nil => idtac
| ?t::?fv =>
let v := fresh "X" in
set (v:=t) in *; set_variables fv
end.
Ltac deset n:=
match n with
| 0%nat => idtac
| S ?n1 =>
match goal with
| h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1
end
end.
(* a est soit un terme de l'anneau, soit une liste de termes.
J'ai pas réussi à un décomposer les Vlists obtenues avec ne_constr_list
dans Tactic Notation *)
Ltac cring_simplify_gen a hyp :=
let lterm :=
match a with
| _::_ => a
| _ => constr:(a::nil)
end in
match eval red in (list_reifyl (lterm:=lterm)) with
| (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
let n := eval compute in (length fv) in
idtac n;
let lt:=fresh "lt" in
set (lt:= lterm);
let lv:=fresh "fv" in
set (lv:= fv);
(* les termes de fv sont remplacés par des variables
pour pouvoir utiliser simpl ensuite sans risquer
des simplifications indésirables *)
set_variables fv;
let lterm1 := eval unfold lt in lt in
let lv1 := eval unfold lv in lv in
idtac lterm1; idtac lv1;
cring_simplify_aux lterm1 lv1 lexpr hyp;
clear lt lv;
(* on remet les termes de fv *)
deset n
end.
Tactic Notation "cring_simplify" constr(lterm):=
cring_simplify_gen lterm 1%nat.
Tactic Notation "cring_simplify" constr(lterm) "in" ident(H):=
cring_simplify_gen lterm H.
|
