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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Import Zdiv_def.
Require Export Morphisms Setoid Bool.
Require Import ZArith.
Open Scope Z_scope.
Require Import Algebra_syntax.
Require Import Ring_polynom.
Require Export Cring.
Require Import Cring_initial.
Set Implicit Arguments.
Class is_closed_list T (l:list T) := {}.
Instance Iclosed_nil T
: is_closed_list (T:=T) nil.
Instance Iclosed_cons T t l
`{is_closed_list (T:=T) l}
: is_closed_list (T:=T) (t::l).
Class is_in_list_at (R:Type) (t:R) (l:list R) (i:nat) := {}.
Instance Ifind0 (R:Type) (t:R) l
: is_in_list_at t (t::l) 0.
Instance IfindS (R:Type) (t2 t1:R) l i
`{is_in_list_at R t1 l i}
: is_in_list_at t1 (t2::l) (S i) | 1.
Class reifyPE (R:Type) (e:PExpr Z) (lvar:list R) (t:R) := {}.
Instance reify_zero (R:Type) (RR:Cring R) lvar
: reifyPE (PEc 0%Z) lvar cring0.
Instance reify_one (R:Type) (RR:Cring R) lvar
: reifyPE (PEc 1%Z) lvar cring1.
Instance reify_plus (R:Type) (RR:Cring R)
e1 lvar t1 e2 t2
`{reifyPE R e1 lvar t1}
`{reifyPE R e2 lvar t2}
: reifyPE (PEadd e1 e2) lvar (cring_plus t1 t2).
Instance reify_mult (R:Type) (RR:Cring R)
e1 lvar t1 e2 t2
`{reifyPE R e1 lvar t1}
`{reifyPE R e2 lvar t2}
: reifyPE (PEmul e1 e2) lvar (cring_mult t1 t2).
Instance reify_sub (R:Type) (RR:Cring R)
e1 lvar t1 e2 t2
`{reifyPE R e1 lvar t1}
`{reifyPE R e2 lvar t2}
: reifyPE (PEsub e1 e2) lvar (cring_sub t1 t2).
Instance reify_opp (R:Type) (RR:Cring R)
e1 lvar t1
`{reifyPE R e1 lvar t1}
: reifyPE (PEopp e1) lvar (cring_opp t1).
Instance reify_pow (R:Type) (RR:Cring R)
e1 lvar t1 n
`{reifyPE R e1 lvar t1}
: reifyPE (PEpow e1 n) lvar (@Ring_theory.pow_N _ cring1 cring_mult t1 n).
Instance reify_var (R:Type) t lvar i
`{is_in_list_at R t lvar i}
: reifyPE (PEX Z (P_of_succ_nat i)) lvar t
| 100.
Class reifyPElist (R:Type) (lexpr:list (PExpr Z)) (lvar:list R)
(lterm:list R) := {}.
Instance reifyPE_nil (R:Type) lvar
: @reifyPElist R nil lvar (@nil R).
Instance reifyPE_cons (R:Type) e1 lvar t1 lexpr2 lterm2
`{reifyPE R e1 lvar t1} `{reifyPElist R lexpr2 lvar lterm2}
: reifyPElist (e1::lexpr2) lvar (t1::lterm2).
Definition list_reifyl (R:Type) lexpr lvar lterm
`{reifyPElist R lexpr lvar lterm}
`{is_closed_list (T:=R) lvar} := (lvar,lexpr).
Unset Implicit Arguments.
Instance multiplication_phi_cring{R:Type}{Rr:Cring R} : Multiplication :=
{multiplication x y := cring_mult
(@gen_phiZ R Rr x) y}.
(*
Print HintDb typeclass_instances.
*)
(* Reification *)
Ltac lterm_goal g :=
match g with
cring_eq ?t1 ?t2 => constr:(t1::t2::nil)
| cring_eq ?t1 ?t2 -> ?g => let lvar := lterm_goal g in constr:(t1::t2::lvar)
end.
Ltac reify_goal lvar lexpr lterm:=
(* idtac lvar; idtac lexpr; idtac lterm;*)
match lexpr with
nil => idtac
| ?e::?lexpr1 =>
match lterm with
?t::?lterm1 => (* idtac "t="; idtac t;*)
let x := fresh "T" in
set (x:= t);
change x with
(@PEeval _ 0 addition multiplication subtraction opposite Z
(@gen_phiZ _ _)
N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e);
clear x;
reify_goal lvar lexpr1 lterm1
end
end.
Existing Instance gen_phiZ_morph.
Existing Instance Zr.
Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
intros x y H. rewrite (Zeq_bool_eq x y H). rrefl. Qed.
Lemma cring_eq_ext: forall (R:Type)(Rr:Cring R),
ring_eq_ext addition multiplication opposite cring_eq.
intros. apply mk_reqe; set_cring_notations;intros.
cring_rewrite H0. cring_rewrite H. rrefl.
cring_rewrite H0. cring_rewrite H. rrefl.
cring_rewrite H. rrefl. Defined.
Lemma cring_almost_ring_theory: forall (R:Type)(Rr:Cring R),
almost_ring_theory 0 1 addition multiplication subtraction opposite cring_eq.
intros. apply mk_art ; set_cring_notations;intros.
cring_rewrite cring_add_0_l; rrefl.
cring_rewrite cring_add_comm; rrefl.
cring_rewrite cring_add_assoc; rrefl.
cring_rewrite cring_mul_1_l; rrefl.
apply cring_mul_0_l.
cring_rewrite cring_mul_comm; rrefl.
cring_rewrite cring_mul_assoc; rrefl.
cring_rewrite cring_distr_l; rrefl.
cring_rewrite cring_opp_mul_l; rrefl.
apply cring_opp_add.
cring_rewrite cring_sub_def ; rrefl. Defined.
Lemma cring_morph: forall (R:Type)(Rr:Cring R),
ring_morph 0 1 addition multiplication subtraction opposite cring_eq
0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
(@gen_phiZ _ _).
intros. apply mkmorph ; intros; simpl; try rrefl; set_cring_notations.
cring_rewrite gen_phiZ_add; rrefl.
cring_rewrite cring_sub_def. unfold Zminus. cring_rewrite gen_phiZ_add.
cring_rewrite gen_phiZ_opp; rrefl.
cring_rewrite gen_phiZ_mul; rrefl.
cring_rewrite gen_phiZ_opp; rrefl.
rewrite (Zeqb_ok x y H). rrefl. Defined.
Lemma cring_power_theory : forall (R:Type)(Rr:Cring R),
power_theory 1 (@multiplication _ _ (@multiplication_cring R Rr)) cring_eq (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication).
intros; apply mkpow_th; set_cring_notations. rrefl. Defined.
Lemma cring_div_theory: forall (R:Type)(Rr:Cring R),
div_theory cring_eq Zplus Zmult (gen_phiZ Rr) Zquotrem.
intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
simpl. apply (@cring_setoid R Rr). Defined.
Ltac cring_gen :=
match goal with
|- ?g => let lterm := lterm_goal g in (* les variables *)
match eval red in (list_reifyl (lterm:=lterm)) with
| (?fv, ?lexpr) =>
(* idtac "variables:";idtac fv;
idtac "terms:"; idtac lterm;
idtac "reifications:"; idtac lexpr;
*)
let lv := fresh "lvar" in
set (lv := fv);
reify_goal lv lexpr lterm;
match goal with
|- ?g =>
set_cring_notations ; unfold lv;
generalize (@ring_correct _ 0 1 addition multiplication subtraction opposite
cring_eq
cring_setoid (@cring_eq_ext _ _) (@cring_almost_ring_theory _ _)
Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
(@gen_phiZ _ _) (@cring_morph _ _) N (fun n:N => n)
(@Ring_theory.pow_N _ 1 multiplication)
(@cring_power_theory _ _) Zquotrem (@cring_div_theory _ _) O fv nil);
set_cring_notations;
let rc := fresh "rc"in
intro rc; apply rc
end
end
end.
Ltac cring_compute:= vm_compute; reflexivity.
Ltac cring:=
unset_cring_notations; intros;
unfold multiplication_phi_cring; simpl gen_phiZ;
match goal with
|- (@cring_eq ?r ?rd _ _ ) =>
cring_gen; cring_compute
end.
(* Tests *)
Variable R: Type.
Variable Rr: Cring R.
Existing Instance Rr.
Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z.
cring.
Qed.
(* reification: 0,7s
sinon, le reste de la tactique donne le même temps que ring
*)
Goal forall x y z t u :R, (x + y + z + t + u)^13 == (u + t + z + y + x) ^13.
Time cring. (*Finished transaction in 0. secs (0.410938u,0.s)*)
Qed.
(*
Goal forall x y z t u :R, (x + y + z + t + u)^16 == (u + t + z + y + x) ^16.
Time cring.(*Finished transaction in 1. secs (0.968852u,0.001s)*)
Qed.
*)
(*
Require Export Ring.
Open Scope Z_scope.
Goal forall x y z t u :Z, (x + y + z + t + u)^13 = (u + t + z + y + x) ^13.
intros.
Time ring.(*Finished transaction in 0. secs (0.371944u,0.s)*)
Qed.
Goal forall x y z t u :Z, (x + y + z + t + u)^16 = (u + t + z + y + x) ^16.
intros.
Time ring.(*Finished transaction in 1. secs (0.914861u,0.s)*)
Qed.
*)
Goal forall x y z:R, 6*x^2 + y == y + 3*2*x^2 + 0 .
cring.
Qed.
(*
Goal forall x y z:R, x + y == y + x + 0 .
cring.
Qed.
Goal forall x y z:R, x * y * z == x * (y * z).
cring.
Qed.
Goal forall x y z:R, 3 * x * (2%Z * y * z) == 6 * (x * y) * z.
cring.
Qed.
Goal forall x y z:R, x ^ 2%N == x * x.
cring.
Qed.
*)
|
