blob: fad36e5713cd46cd3610c619389a7fe216940af2 (
plain)
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
|
(************************************************************************)
(* 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 Export Morphisms Setoid Bool.
Require Import ZArith.
Require Import Algebra_syntax.
Require Export Ring2.
Require Import Ring2_polynom.
Require Import Ring2_initial.
Set Implicit Arguments.
Class nth (R:Type) (t:R) (l:list R) (i:nat).
Instance Ifind0 (R:Type) (t:R) l
: nth t(t::l) 0.
Instance IfindS (R:Type) (t2 t1:R) l i
{_:nth t1 l i}
: nth t1 (t2::l) (S i) | 1.
Class closed (T:Type) (l:list T).
Instance Iclosed_nil T
: closed (T:=T) nil.
Instance Iclosed_cons T t (l:list T)
{_:closed l}
: closed (t::l).
Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R).
Instance reify_zero (R:Type) lvar op
`{Ring (T:=R)(ring0:=op)}
: reify (ring0:=op)(PEc 0%Z) lvar op.
Instance reify_one (R:Type) lvar op
`{Ring (T:=R)(ring1:=op)}
: reify (ring1:=op) (PEc 1%Z) lvar op.
Instance reify_add (R:Type)
e1 lvar t1 e2 t2 op
`{Ring (T:=R)(add:=op)}
{_:reify (add:=op) e1 lvar t1}
{_:reify (add:=op) e2 lvar t2}
: reify (add:=op) (PEadd e1 e2) lvar (op t1 t2).
Instance reify_mul (R:Type)
e1 lvar t1 e2 t2 op
`{Ring (T:=R)(mul:=op)}
{_:reify (mul:=op) e1 lvar t1}
{_:reify (mul:=op) e2 lvar t2}
: reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2).
Instance reify_mul_ext (R:Type) `{Ring R}
lvar z e2 t2
`{Ring (T:=R)}
{_:reify e2 lvar t2}
: reify (PEmul (PEc z) e2) lvar
(@multiplication Z _ _ z t2)|9.
Instance reify_sub (R:Type)
e1 lvar t1 e2 t2 op
`{Ring (T:=R)(sub:=op)}
{_:reify (sub:=op) e1 lvar t1}
{_:reify (sub:=op) e2 lvar t2}
: reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2).
Instance reify_opp (R:Type)
e1 lvar t1 op
`{Ring (T:=R)(opp:=op)}
{_:reify (opp:=op) e1 lvar t1}
: reify (opp:=op) (PEopp e1) lvar (op t1).
Instance reify_pow (R:Type) `{Ring R}
e1 lvar t1 n
`{Ring (T:=R)}
{_:reify e1 lvar t1}
: reify (PEpow e1 n) lvar (pow_N t1 n)|1.
Instance reify_var (R:Type) t lvar i
`{nth R t lvar i}
`{Rr: Ring (T:=R)}
: reify (Rr:= Rr) (PEX Z (P_of_succ_nat i))lvar t
| 100.
Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R)
(lterm:list R).
Instance reify_nil (R:Type) lvar
`{Rr: Ring (T:=R)}
: reifylist (Rr:= Rr) nil lvar (@nil R).
Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2
`{Rr: Ring (T:=R)}
{_:reify (Rr:= Rr) e1 lvar t1}
{_:reifylist (Rr:= Rr) lexpr2 lvar lterm2}
: reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2).
Definition list_reifyl (R:Type) lexpr lvar lterm
`{Rr: Ring (T:=R)}
{_:reifylist (Rr:= Rr) lexpr lvar lterm}
`{closed (T:=R) lvar} := (lvar,lexpr).
Unset Implicit Arguments.
Ltac lterm_goal g :=
match g with
| ?t1 == ?t2 => constr:(t1::t2::nil)
| ?t1 = ?t2 => constr:(t1::t2::nil)
end.
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). reflexivity. Qed.
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
(@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
(fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
lvar e1)
(@PEeval Z _ _ _ _ _ _ _ _ _ (@gen_phiZ _ _ _ _ _ _ _ _ _) N
(fun n:N => n) (@pow_N _ _ _ _ _ _ _ _ _)
lvar e2))
end
end.
Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R),
x * (gen_phiZ c) == (gen_phiZ c) * x.
induction c. intros. simpl. gen_rewrite. simpl. intros.
rewrite <- same_gen.
induction p. simpl. gen_rewrite. rewrite IHp. reflexivity.
simpl. gen_rewrite. rewrite IHp. reflexivity.
simpl. gen_rewrite.
simpl. intros. rewrite <- same_gen.
induction p. simpl. generalize IHp. clear IHp.
gen_rewrite. intro IHp. rewrite IHp. reflexivity.
simpl. generalize IHp. clear IHp.
gen_rewrite. intro IHp. rewrite IHp. reflexivity.
simpl. gen_rewrite. Qed.
Ltac ring_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 =>
apply (@ring_correct Z _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
(@gen_phiZ _ _ _ _ _ _ _ _ _) _
(@comm _ _ _ _ _ _ _ _ _ _) Zeq_bool Zeqb_ok N (fun n:N => n)
(@pow_N _ _ _ _ _ _ _ _ _));
[apply mkpow_th; reflexivity
|vm_compute; reflexivity]
end
end
end.
Ltac ring2:=
intros;
ring_gen.
|
