← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/ring/Ring_normalize.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/ring/Ring_normalize.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: Ring_normalize.v 10913 2008-05-09 14:40:04Z herbelin $ *)
 
10
 
 
11
Require Import LegacyRing_theory.
 
12
Require Import Quote.
 
13
 
 
14
Set Implicit Arguments.
 
15
Unset Boxed Definitions.
 
16
 
 
17
Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 
18
Proof.
 
19
  intros.
 
20
  apply index_eq_prop.
 
21
  generalize H.
 
22
  case (index_eq n m); simpl in |- *; trivial; intros.
 
23
  contradiction.
 
24
Qed.
 
25
 
 
26
Section semi_rings.
 
27
 
 
28
Variable A : Type.
 
29
Variable Aplus : A -> A -> A.
 
30
Variable Amult : A -> A -> A.
 
31
Variable Aone : A.
 
32
Variable Azero : A.
 
33
Variable Aeq : A -> A -> bool.
 
34
 
 
35
(* Section definitions. *)
 
36
 
 
37
 
 
38
(******************************************)
 
39
(* Normal abtract Polynomials             *)
 
40
(******************************************)
 
41
(* DEFINITIONS :
 
42
- A varlist is a sorted product of one or more variables : x, x*y*z 
 
43
- A monom is a constant, a varlist or the product of a constant by a varlist
 
44
  variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT.
 
45
- A canonical sum is either a monom or an ordered sum of monoms 
 
46
  (the order on monoms is defined later) 
 
47
- A normal polynomial it either a constant or a canonical sum or a constant
 
48
  plus a canonical sum
 
49
*)
 
50
 
 
51
(* varlist is isomorphic to (list var), but we built a special inductive
 
52
   for efficiency *)
 
53
Inductive varlist : Type :=
 
54
  | Nil_var : varlist
 
55
  | Cons_var : index -> varlist -> varlist.
 
56
 
 
57
Inductive canonical_sum : Type :=
 
58
  | Nil_monom : canonical_sum
 
59
  | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum
 
60
  | Cons_varlist : varlist -> canonical_sum -> canonical_sum.
 
61
 
 
62
(* Order on monoms *)
 
63
 
 
64
(* That's the lexicographic order on varlist, extended by : 
 
65
  - A constant is less than every monom 
 
66
  - The relation between two varlist is preserved by multiplication by a
 
67
  constant.
 
68
 
 
69
  Examples : 
 
70
  3 < x < y
 
71
  x*y < x*y*y*z 
 
72
  2*x*y < x*y*y*z
 
73
  x*y < 54*x*y*y*z
 
74
  4*x*y < 59*x*y*y*z
 
75
*)
 
76
 
 
77
Fixpoint varlist_eq (x y:varlist) {struct y} : bool :=
 
78
  match x, y with
 
79
  | Nil_var, Nil_var => true
 
80
  | Cons_var i xrest, Cons_var j yrest =>
 
81
      andb (index_eq i j) (varlist_eq xrest yrest)
 
82
  | _, _ => false
 
83
  end.
 
84
 
 
85
Fixpoint varlist_lt (x y:varlist) {struct y} : bool :=
 
86
  match x, y with
 
87
  | Nil_var, Cons_var _ _ => true
 
88
  | Cons_var i xrest, Cons_var j yrest =>
 
89
      if index_lt i j
 
90
      then true
 
91
      else andb (index_eq i j) (varlist_lt xrest yrest)
 
92
  | _, _ => false
 
93
  end.
 
94
 
 
95
(* merges two variables lists *)
 
96
Fixpoint varlist_merge (l1:varlist) : varlist -> varlist :=
 
97
  match l1 with
 
98
  | Cons_var v1 t1 =>
 
99
      (fix vm_aux (l2:varlist) : varlist :=
 
100
         match l2 with
 
101
         | Cons_var v2 t2 =>
 
102
             if index_lt v1 v2
 
103
             then Cons_var v1 (varlist_merge t1 l2)
 
104
             else Cons_var v2 (vm_aux t2)
 
105
         | Nil_var => l1
 
106
         end)
 
107
  | Nil_var => fun l2 => l2
 
108
  end.
 
109
 
 
110
(* returns the sum of two canonical sums  *)
 
111
Fixpoint canonical_sum_merge (s1:canonical_sum) :
 
112
 canonical_sum -> canonical_sum :=
 
113
  match s1 with
 
114
  | Cons_monom c1 l1 t1 =>
 
115
      (fix csm_aux (s2:canonical_sum) : canonical_sum :=
 
116
         match s2 with
 
117
         | Cons_monom c2 l2 t2 =>
 
118
             if varlist_eq l1 l2
 
119
             then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2)
 
120
             else
 
121
              if varlist_lt l1 l2
 
122
              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
 
123
              else Cons_monom c2 l2 (csm_aux t2)
 
124
         | Cons_varlist l2 t2 =>
 
125
             if varlist_eq l1 l2
 
126
             then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2)
 
127
             else
 
128
              if varlist_lt l1 l2
 
129
              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
 
130
              else Cons_varlist l2 (csm_aux t2)
 
131
         | Nil_monom => s1
 
132
         end)
 
133
  | Cons_varlist l1 t1 =>
 
134
      (fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
 
135
         match s2 with
 
136
         | Cons_monom c2 l2 t2 =>
 
137
             if varlist_eq l1 l2
 
138
             then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2)
 
139
             else
 
140
              if varlist_lt l1 l2
 
141
              then Cons_varlist l1 (canonical_sum_merge t1 s2)
 
142
              else Cons_monom c2 l2 (csm_aux2 t2)
 
143
         | Cons_varlist l2 t2 =>
 
144
             if varlist_eq l1 l2
 
145
             then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2)
 
146
             else
 
147
              if varlist_lt l1 l2
 
148
              then Cons_varlist l1 (canonical_sum_merge t1 s2)
 
149
              else Cons_varlist l2 (csm_aux2 t2)
 
150
         | Nil_monom => s1
 
151
         end)
 
152
  | Nil_monom => fun s2 => s2
 
153
  end.
 
154
 
 
155
(* Insertion of a monom in a canonical sum *)
 
156
Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} :
 
157
 canonical_sum :=
 
158
  match s2 with
 
159
  | Cons_monom c2 l2 t2 =>
 
160
      if varlist_eq l1 l2
 
161
      then Cons_monom (Aplus c1 c2) l1 t2
 
162
      else
 
163
       if varlist_lt l1 l2
 
164
       then Cons_monom c1 l1 s2
 
165
       else Cons_monom c2 l2 (monom_insert c1 l1 t2)
 
166
  | Cons_varlist l2 t2 =>
 
167
      if varlist_eq l1 l2
 
168
      then Cons_monom (Aplus c1 Aone) l1 t2
 
169
      else
 
170
       if varlist_lt l1 l2
 
171
       then Cons_monom c1 l1 s2
 
172
       else Cons_varlist l2 (monom_insert c1 l1 t2)
 
173
  | Nil_monom => Cons_monom c1 l1 Nil_monom
 
174
  end.
 
175
 
 
176
Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} :
 
177
 canonical_sum :=
 
178
  match s2 with
 
179
  | Cons_monom c2 l2 t2 =>
 
180
      if varlist_eq l1 l2
 
181
      then Cons_monom (Aplus Aone c2) l1 t2
 
182
      else
 
183
       if varlist_lt l1 l2
 
184
       then Cons_varlist l1 s2
 
185
       else Cons_monom c2 l2 (varlist_insert l1 t2)
 
186
  | Cons_varlist l2 t2 =>
 
187
      if varlist_eq l1 l2
 
188
      then Cons_monom (Aplus Aone Aone) l1 t2
 
189
      else
 
190
       if varlist_lt l1 l2
 
191
       then Cons_varlist l1 s2
 
192
       else Cons_varlist l2 (varlist_insert l1 t2)
 
193
  | Nil_monom => Cons_varlist l1 Nil_monom
 
194
  end.
 
195
 
 
196
(* Computes c0*s *)
 
197
Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} :
 
198
 canonical_sum :=
 
199
  match s with
 
200
  | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t)
 
201
  | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t)
 
202
  | Nil_monom => Nil_monom
 
203
  end.
 
204
 
 
205
(* Computes l0*s  *)
 
206
Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} :
 
207
 canonical_sum :=
 
208
  match s with
 
209
  | Cons_monom c l t =>
 
210
      monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
 
211
  | Cons_varlist l t =>
 
212
      varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
 
213
  | Nil_monom => Nil_monom
 
214
  end.
 
215
 
 
216
(* Computes c0*l0*s  *)
 
217
Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) 
 
218
 (s:canonical_sum) {struct s} : canonical_sum :=
 
219
  match s with
 
220
  | Cons_monom c l t =>
 
221
      monom_insert (Amult c0 c) (varlist_merge l0 l)
 
222
        (canonical_sum_scalar3 c0 l0 t)
 
223
  | Cons_varlist l t =>
 
224
      monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t)
 
225
  | Nil_monom => Nil_monom
 
226
  end.
 
227
 
 
228
(* returns the product of two canonical sums *) 
 
229
Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} :
 
230
 canonical_sum :=
 
231
  match s1 with
 
232
  | Cons_monom c1 l1 t1 =>
 
233
      canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2)
 
234
        (canonical_sum_prod t1 s2)
 
235
  | Cons_varlist l1 t1 =>
 
236
      canonical_sum_merge (canonical_sum_scalar2 l1 s2)
 
237
        (canonical_sum_prod t1 s2)
 
238
  | Nil_monom => Nil_monom
 
239
  end.
 
240
 
 
241
(* The type to represent concrete semi-ring polynomials *)
 
242
Inductive spolynomial : Type :=
 
243
  | SPvar : index -> spolynomial
 
244
  | SPconst : A -> spolynomial
 
245
  | SPplus : spolynomial -> spolynomial -> spolynomial
 
246
  | SPmult : spolynomial -> spolynomial -> spolynomial.
 
247
 
 
248
Fixpoint spolynomial_normalize (p:spolynomial) : canonical_sum :=
 
249
  match p with
 
250
  | SPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom
 
251
  | SPconst c => Cons_monom c Nil_var Nil_monom
 
252
  | SPplus l r =>
 
253
      canonical_sum_merge (spolynomial_normalize l) (spolynomial_normalize r)
 
254
  | SPmult l r =>
 
255
      canonical_sum_prod (spolynomial_normalize l) (spolynomial_normalize r)
 
256
  end.
 
257
 
 
258
(* Deletion of useless 0 and 1 in canonical sums *)
 
259
Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum :=
 
260
  match s with
 
261
  | Cons_monom c l t =>
 
262
      if Aeq c Azero
 
263
      then canonical_sum_simplify t
 
264
      else
 
265
       if Aeq c Aone
 
266
       then Cons_varlist l (canonical_sum_simplify t)
 
267
       else Cons_monom c l (canonical_sum_simplify t)
 
268
  | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t)
 
269
  | Nil_monom => Nil_monom
 
270
  end.
 
271
 
 
272
Definition spolynomial_simplify (x:spolynomial) :=
 
273
  canonical_sum_simplify (spolynomial_normalize x).
 
274
 
 
275
(* End definitions. *)
 
276
 
 
277
(* Section interpretation. *)
 
278
 
 
279
(*** Here a variable map is defined and the interpetation of a spolynom
 
280
  acording to a certain variables map. Once again the choosen definition
 
281
  is generic and could be changed ****)
 
282
 
 
283
Variable vm : varmap A.
 
284
 
 
285
(* Interpretation of list of variables 
 
286
 * [x1; ... ; xn ] is interpreted as (find v x1)* ... *(find v xn)
 
287
 * The unbound variables are mapped to 0. Normally this case sould
 
288
 * never occur. Since we want only to prove correctness theorems, which form
 
289
 * is : for any varmap and any spolynom ... this is a safe and pain-saving
 
290
 * choice *)
 
291
Definition interp_var (i:index) := varmap_find Azero i vm.
 
292
 
 
293
(* Local *) Definition ivl_aux :=
 
294
              (fix ivl_aux (x:index) (t:varlist) {struct t} : A :=
 
295
                 match t with
 
296
                 | Nil_var => interp_var x
 
297
                 | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t')
 
298
                 end).
 
299
 
 
300
Definition interp_vl (l:varlist) :=
 
301
  match l with
 
302
  | Nil_var => Aone
 
303
  | Cons_var x t => ivl_aux x t
 
304
  end.
 
305
 
 
306
(* Local *) Definition interp_m (c:A) (l:varlist) :=
 
307
              match l with
 
308
              | Nil_var => c
 
309
              | Cons_var x t => Amult c (ivl_aux x t)
 
310
              end.
 
311
 
 
312
(* Local *) Definition ics_aux :=
 
313
              (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A :=
 
314
                 match s with
 
315
                 | Nil_monom => a
 
316
                 | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t)
 
317
                 | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t)
 
318
                 end).
 
319
 
 
320
(* Interpretation of a canonical sum *)
 
321
Definition interp_cs (s:canonical_sum) : A :=
 
322
  match s with
 
323
  | Nil_monom => Azero
 
324
  | Cons_varlist l t => ics_aux (interp_vl l) t
 
325
  | Cons_monom c l t => ics_aux (interp_m c l) t
 
326
  end.
 
327
 
 
328
Fixpoint interp_sp (p:spolynomial) : A :=
 
329
  match p with
 
330
  | SPconst c => c
 
331
  | SPvar i => interp_var i
 
332
  | SPplus p1 p2 => Aplus (interp_sp p1) (interp_sp p2)
 
333
  | SPmult p1 p2 => Amult (interp_sp p1) (interp_sp p2)
 
334
  end.
 
335
 
 
336
 
 
337
(* End interpretation. *)
 
338
 
 
339
Unset Implicit Arguments.
 
340
 
 
341
(* Section properties. *)
 
342
 
 
343
Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
 
344
 
 
345
Hint Resolve (SR_plus_comm T).
 
346
Hint Resolve (SR_plus_assoc T).
 
347
Hint Resolve (SR_plus_assoc2 T).
 
348
Hint Resolve (SR_mult_comm T).
 
349
Hint Resolve (SR_mult_assoc T).
 
350
Hint Resolve (SR_mult_assoc2 T).
 
351
Hint Resolve (SR_plus_zero_left T).
 
352
Hint Resolve (SR_plus_zero_left2 T).
 
353
Hint Resolve (SR_mult_one_left T).
 
354
Hint Resolve (SR_mult_one_left2 T).
 
355
Hint Resolve (SR_mult_zero_left T).
 
356
Hint Resolve (SR_mult_zero_left2 T).
 
357
Hint Resolve (SR_distr_left T).
 
358
Hint Resolve (SR_distr_left2 T).
 
359
(*Hint Resolve (SR_plus_reg_left T).*)
 
360
Hint Resolve (SR_plus_permute T).
 
361
Hint Resolve (SR_mult_permute T).
 
362
Hint Resolve (SR_distr_right T).
 
363
Hint Resolve (SR_distr_right2 T).
 
364
Hint Resolve (SR_mult_zero_right T).
 
365
Hint Resolve (SR_mult_zero_right2 T).
 
366
Hint Resolve (SR_plus_zero_right T).
 
367
Hint Resolve (SR_plus_zero_right2 T).
 
368
Hint Resolve (SR_mult_one_right T).
 
369
Hint Resolve (SR_mult_one_right2 T).
 
370
(*Hint Resolve (SR_plus_reg_right T).*)
 
371
Hint Resolve refl_equal sym_equal trans_equal.
 
372
(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
 
373
Hint Immediate T.
 
374
 
 
375
Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y.
 
376
Proof.
 
377
  simple induction x; simple induction y; contradiction || (try reflexivity).
 
378
  simpl in |- *; intros.
 
379
  generalize (andb_prop2 _ _ H1); intros; elim H2; intros.
 
380
  rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity.
 
381
Qed.
 
382
 
 
383
Remark ivl_aux_ok :
 
384
 forall (v:varlist) (i:index),
 
385
   ivl_aux i v = Amult (interp_var i) (interp_vl v).
 
386
Proof.
 
387
  simple induction v; simpl in |- *; intros.
 
388
  trivial.
 
389
  rewrite H; trivial.
 
390
Qed.
 
391
 
 
392
Lemma varlist_merge_ok :
 
393
 forall x y:varlist,
 
394
   interp_vl (varlist_merge x y) = Amult (interp_vl x) (interp_vl y).
 
395
Proof.
 
396
  simple induction x.
 
397
  simpl in |- *; trivial.
 
398
  simple induction y.
 
399
  simpl in |- *; trivial.
 
400
  simpl in |- *; intros.
 
401
  elim (index_lt i i0); simpl in |- *; intros.
 
402
 
 
403
  repeat rewrite ivl_aux_ok.
 
404
  rewrite H. simpl in |- *.
 
405
  rewrite ivl_aux_ok.
 
406
  eauto.
 
407
 
 
408
  repeat rewrite ivl_aux_ok.
 
409
  rewrite H0.
 
410
  rewrite ivl_aux_ok.
 
411
  eauto.
 
412
Qed.
 
413
 
 
414
Remark ics_aux_ok :
 
415
 forall (x:A) (s:canonical_sum), ics_aux x s = Aplus x (interp_cs s).
 
416
Proof.
 
417
  simple induction s; simpl in |- *; intros.
 
418
  trivial.
 
419
  reflexivity.
 
420
  reflexivity.
 
421
Qed.
 
422
 
 
423
Remark interp_m_ok :
 
424
 forall (x:A) (l:varlist), interp_m x l = Amult x (interp_vl l).
 
425
Proof.
 
426
  destruct l as [| i v].
 
427
  simpl in |- *; trivial.
 
428
  reflexivity.
 
429
Qed.
 
430
 
 
431
Lemma canonical_sum_merge_ok :
 
432
 forall x y:canonical_sum,
 
433
   interp_cs (canonical_sum_merge x y) = Aplus (interp_cs x) (interp_cs y).
 
434
 
 
435
simple induction x; simpl in |- *.
 
436
trivial.
 
437
 
 
438
simple induction y; simpl in |- *; intros.
 
439
(* monom and nil *)
 
440
eauto.
 
441
 
 
442
(* monom and monom *)
 
443
generalize (varlist_eq_prop v v0).
 
444
elim (varlist_eq v v0).
 
445
intros; rewrite (H1 I).
 
446
simpl in |- *; repeat rewrite ics_aux_ok; rewrite H.
 
447
repeat rewrite interp_m_ok.
 
448
rewrite (SR_distr_left T).
 
449
repeat rewrite <- (SR_plus_assoc T).
 
450
apply f_equal with (f := Aplus (Amult a (interp_vl v0))).
 
451
trivial.
 
452
 
 
453
elim (varlist_lt v v0); simpl in |- *.
 
454
repeat rewrite ics_aux_ok.
 
455
rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
 
456
 
 
457
rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
 
458
 eauto.
 
459
 
 
460
(* monom and varlist *)
 
461
generalize (varlist_eq_prop v v0).
 
462
elim (varlist_eq v v0).
 
463
intros; rewrite (H1 I).
 
464
simpl in |- *; repeat rewrite ics_aux_ok; rewrite H.
 
465
repeat rewrite interp_m_ok.
 
466
rewrite (SR_distr_left T).
 
467
repeat rewrite <- (SR_plus_assoc T).
 
468
apply f_equal with (f := Aplus (Amult a (interp_vl v0))).
 
469
rewrite (SR_mult_one_left T).
 
470
trivial.
 
471
 
 
472
elim (varlist_lt v v0); simpl in |- *.
 
473
repeat rewrite ics_aux_ok.
 
474
rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
 
475
rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
 
476
 eauto.
 
477
 
 
478
simple induction y; simpl in |- *; intros.
 
479
(* varlist and nil *)
 
480
trivial.
 
481
 
 
482
(* varlist and monom *)
 
483
generalize (varlist_eq_prop v v0).
 
484
elim (varlist_eq v v0).
 
485
intros; rewrite (H1 I).
 
486
simpl in |- *; repeat rewrite ics_aux_ok; rewrite H.
 
487
repeat rewrite interp_m_ok.
 
488
rewrite (SR_distr_left T).
 
489
repeat rewrite <- (SR_plus_assoc T).
 
490
rewrite (SR_mult_one_left T).
 
491
apply f_equal with (f := Aplus (interp_vl v0)).
 
492
trivial.
 
493
 
 
494
elim (varlist_lt v v0); simpl in |- *.
 
495
repeat rewrite ics_aux_ok.
 
496
rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
 
497
rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
 
498
 eauto.
 
499
 
 
500
(* varlist and varlist *)
 
501
generalize (varlist_eq_prop v v0).
 
502
elim (varlist_eq v v0).
 
503
intros; rewrite (H1 I).
 
504
simpl in |- *; repeat rewrite ics_aux_ok; rewrite H.
 
505
repeat rewrite interp_m_ok.
 
506
rewrite (SR_distr_left T).
 
507
repeat rewrite <- (SR_plus_assoc T).
 
508
rewrite (SR_mult_one_left T).
 
509
apply f_equal with (f := Aplus (interp_vl v0)).
 
510
trivial.
 
511
 
 
512
elim (varlist_lt v v0); simpl in |- *.
 
513
repeat rewrite ics_aux_ok.
 
514
rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
 
515
rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
 
516
 eauto.
 
517
Qed.
 
518
 
 
519
Lemma monom_insert_ok :
 
520
 forall (a:A) (l:varlist) (s:canonical_sum),
 
521
   interp_cs (monom_insert a l s) =
 
522
   Aplus (Amult a (interp_vl l)) (interp_cs s).
 
523
intros; generalize s; simple induction s0.
 
524
 
 
525
simpl in |- *; rewrite interp_m_ok; trivial.
 
526
 
 
527
simpl in |- *; intros.
 
528
generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
529
intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
 
530
 repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T);
 
531
 eauto.
 
532
elim (varlist_lt l v); simpl in |- *;
 
533
 [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
 
534
 | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
 
535
    rewrite ics_aux_ok; eauto ].
 
536
 
 
537
simpl in |- *; intros.
 
538
generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
539
intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
 
540
 repeat rewrite ics_aux_ok; rewrite (SR_distr_left T);
 
541
 rewrite (SR_mult_one_left T); eauto.
 
542
elim (varlist_lt l v); simpl in |- *;
 
543
 [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
 
544
 | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
 
545
    rewrite ics_aux_ok; eauto ].
 
546
Qed.
 
547
 
 
548
Lemma varlist_insert_ok :
 
549
 forall (l:varlist) (s:canonical_sum),
 
550
   interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s).
 
551
intros; generalize s; simple induction s0.
 
552
 
 
553
simpl in |- *; trivial.
 
554
 
 
555
simpl in |- *; intros.
 
556
generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
557
intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
 
558
 repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T);
 
559
 rewrite (SR_mult_one_left T); eauto.
 
560
elim (varlist_lt l v); simpl in |- *;
 
561
 [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
 
562
 | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
 
563
    rewrite ics_aux_ok; eauto ].
 
564
 
 
565
simpl in |- *; intros.
 
566
generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
567
intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
 
568
 repeat rewrite ics_aux_ok; rewrite (SR_distr_left T);
 
569
 rewrite (SR_mult_one_left T); eauto.
 
570
elim (varlist_lt l v); simpl in |- *;
 
571
 [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
 
572
 | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
 
573
    rewrite ics_aux_ok; eauto ].
 
574
Qed.
 
575
 
 
576
Lemma canonical_sum_scalar_ok :
 
577
 forall (a:A) (s:canonical_sum),
 
578
   interp_cs (canonical_sum_scalar a s) = Amult a (interp_cs s).
 
579
simple induction s.
 
580
simpl in |- *; eauto.
 
581
 
 
582
simpl in |- *; intros.
 
583
repeat rewrite ics_aux_ok.
 
584
repeat rewrite interp_m_ok.
 
585
rewrite H.
 
586
rewrite (SR_distr_right T).
 
587
repeat rewrite <- (SR_mult_assoc T).
 
588
reflexivity.
 
589
 
 
590
simpl in |- *; intros.
 
591
repeat rewrite ics_aux_ok.
 
592
repeat rewrite interp_m_ok.
 
593
rewrite H.
 
594
rewrite (SR_distr_right T).
 
595
repeat rewrite <- (SR_mult_assoc T).
 
596
reflexivity.
 
597
Qed.
 
598
 
 
599
Lemma canonical_sum_scalar2_ok :
 
600
 forall (l:varlist) (s:canonical_sum),
 
601
   interp_cs (canonical_sum_scalar2 l s) = Amult (interp_vl l) (interp_cs s).
 
602
simple induction s.
 
603
simpl in |- *; trivial.
 
604
 
 
605
simpl in |- *; intros.
 
606
rewrite monom_insert_ok.
 
607
repeat rewrite ics_aux_ok.
 
608
repeat rewrite interp_m_ok.
 
609
rewrite H.
 
610
rewrite varlist_merge_ok.
 
611
repeat rewrite (SR_distr_right T). 
 
612
repeat rewrite <- (SR_mult_assoc T).
 
613
repeat rewrite <- (SR_plus_assoc T).
 
614
rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
 
615
reflexivity.
 
616
 
 
617
simpl in |- *; intros.
 
618
rewrite varlist_insert_ok.
 
619
repeat rewrite ics_aux_ok.
 
620
repeat rewrite interp_m_ok.
 
621
rewrite H.
 
622
rewrite varlist_merge_ok.
 
623
repeat rewrite (SR_distr_right T). 
 
624
repeat rewrite <- (SR_mult_assoc T).
 
625
repeat rewrite <- (SR_plus_assoc T).
 
626
reflexivity.
 
627
Qed.
 
628
 
 
629
Lemma canonical_sum_scalar3_ok :
 
630
 forall (c:A) (l:varlist) (s:canonical_sum),
 
631
   interp_cs (canonical_sum_scalar3 c l s) =
 
632
   Amult c (Amult (interp_vl l) (interp_cs s)).
 
633
simple induction s.
 
634
simpl in |- *; repeat rewrite (SR_mult_zero_right T); reflexivity.
 
635
 
 
636
simpl in |- *; intros.
 
637
rewrite monom_insert_ok.
 
638
repeat rewrite ics_aux_ok.
 
639
repeat rewrite interp_m_ok.
 
640
rewrite H.
 
641
rewrite varlist_merge_ok.
 
642
repeat rewrite (SR_distr_right T). 
 
643
repeat rewrite <- (SR_mult_assoc T).
 
644
repeat rewrite <- (SR_plus_assoc T).
 
645
rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
 
646
reflexivity.
 
647
 
 
648
simpl in |- *; intros.
 
649
rewrite monom_insert_ok.
 
650
repeat rewrite ics_aux_ok.
 
651
repeat rewrite interp_m_ok.
 
652
rewrite H.
 
653
rewrite varlist_merge_ok.
 
654
repeat rewrite (SR_distr_right T). 
 
655
repeat rewrite <- (SR_mult_assoc T).
 
656
repeat rewrite <- (SR_plus_assoc T).
 
657
rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)).
 
658
reflexivity.
 
659
Qed.
 
660
 
 
661
Lemma canonical_sum_prod_ok :
 
662
 forall x y:canonical_sum,
 
663
   interp_cs (canonical_sum_prod x y) = Amult (interp_cs x) (interp_cs y).
 
664
simple induction x; simpl in |- *; intros.
 
665
trivial.
 
666
 
 
667
rewrite canonical_sum_merge_ok.
 
668
rewrite canonical_sum_scalar3_ok.
 
669
rewrite ics_aux_ok.
 
670
rewrite interp_m_ok.
 
671
rewrite H.
 
672
rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)).
 
673
symmetry  in |- *.
 
674
eauto.
 
675
 
 
676
rewrite canonical_sum_merge_ok.
 
677
rewrite canonical_sum_scalar2_ok.
 
678
rewrite ics_aux_ok.
 
679
rewrite H.
 
680
trivial.
 
681
Qed.
 
682
 
 
683
Theorem spolynomial_normalize_ok :
 
684
 forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p.
 
685
simple induction p; simpl in |- *; intros.
 
686
 
 
687
reflexivity.
 
688
reflexivity.
 
689
 
 
690
rewrite canonical_sum_merge_ok.
 
691
rewrite H; rewrite H0.
 
692
reflexivity.
 
693
 
 
694
rewrite canonical_sum_prod_ok.
 
695
rewrite H; rewrite H0.
 
696
reflexivity.
 
697
Qed.
 
698
 
 
699
Lemma canonical_sum_simplify_ok :
 
700
 forall s:canonical_sum, interp_cs (canonical_sum_simplify s) = interp_cs s.
 
701
simple induction s.
 
702
 
 
703
reflexivity.
 
704
 
 
705
(* cons_monom *)
 
706
simpl in |- *; intros.
 
707
generalize (SR_eq_prop T a Azero).
 
708
elim (Aeq a Azero).
 
709
intro Heq; rewrite (Heq I).
 
710
rewrite H.
 
711
rewrite ics_aux_ok.
 
712
rewrite interp_m_ok.
 
713
rewrite (SR_mult_zero_left T).
 
714
trivial.
 
715
 
 
716
intros; simpl in |- *.
 
717
generalize (SR_eq_prop T a Aone).
 
718
elim (Aeq a Aone).
 
719
intro Heq; rewrite (Heq I).
 
720
simpl in |- *.
 
721
repeat rewrite ics_aux_ok.
 
722
rewrite interp_m_ok.
 
723
rewrite H.
 
724
rewrite (SR_mult_one_left T).
 
725
reflexivity.
 
726
 
 
727
simpl in |- *.
 
728
repeat rewrite ics_aux_ok.
 
729
rewrite interp_m_ok.
 
730
rewrite H.
 
731
reflexivity.
 
732
 
 
733
(* cons_varlist *)
 
734
simpl in |- *; intros.
 
735
repeat rewrite ics_aux_ok.
 
736
rewrite H.
 
737
reflexivity.
 
738
 
 
739
Qed.
 
740
 
 
741
Theorem spolynomial_simplify_ok :
 
742
 forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p.
 
743
intro.
 
744
unfold spolynomial_simplify in |- *.
 
745
rewrite canonical_sum_simplify_ok.
 
746
apply spolynomial_normalize_ok.
 
747
Qed.
 
748
 
 
749
(* End properties. *)
 
750
End semi_rings.
 
751
 
 
752
Implicit Arguments Cons_varlist.
 
753
Implicit Arguments Cons_monom.
 
754
Implicit Arguments SPconst.
 
755
Implicit Arguments SPplus.
 
756
Implicit Arguments SPmult.
 
757
 
 
758
Section rings.
 
759
 
 
760
(* Here the coercion between Ring and Semi-Ring will be useful *)
 
761
 
 
762
Set Implicit Arguments.
 
763
 
 
764
Variable A : Type.
 
765
Variable Aplus : A -> A -> A.
 
766
Variable Amult : A -> A -> A.
 
767
Variable Aone : A.
 
768
Variable Azero : A.
 
769
Variable Aopp : A -> A.
 
770
Variable Aeq : A -> A -> bool.
 
771
Variable vm : varmap A.
 
772
Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
 
773
 
 
774
Hint Resolve (Th_plus_comm T).
 
775
Hint Resolve (Th_plus_assoc T).
 
776
Hint Resolve (Th_plus_assoc2 T).
 
777
Hint Resolve (Th_mult_comm T).
 
778
Hint Resolve (Th_mult_assoc T).
 
779
Hint Resolve (Th_mult_assoc2 T).
 
780
Hint Resolve (Th_plus_zero_left T).
 
781
Hint Resolve (Th_plus_zero_left2 T).
 
782
Hint Resolve (Th_mult_one_left T).
 
783
Hint Resolve (Th_mult_one_left2 T).
 
784
Hint Resolve (Th_mult_zero_left T).
 
785
Hint Resolve (Th_mult_zero_left2 T).
 
786
Hint Resolve (Th_distr_left T).
 
787
Hint Resolve (Th_distr_left2 T).
 
788
(*Hint Resolve (Th_plus_reg_left T).*)
 
789
Hint Resolve (Th_plus_permute T).
 
790
Hint Resolve (Th_mult_permute T).
 
791
Hint Resolve (Th_distr_right T).
 
792
Hint Resolve (Th_distr_right2 T).
 
793
Hint Resolve (Th_mult_zero_right T).
 
794
Hint Resolve (Th_mult_zero_right2 T).
 
795
Hint Resolve (Th_plus_zero_right T).
 
796
Hint Resolve (Th_plus_zero_right2 T).
 
797
Hint Resolve (Th_mult_one_right T).
 
798
Hint Resolve (Th_mult_one_right2 T).
 
799
(*Hint Resolve (Th_plus_reg_right T).*)
 
800
Hint Resolve refl_equal sym_equal trans_equal.
 
801
(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 
802
Hint Immediate T.
 
803
 
 
804
(*** Definitions *)
 
805
 
 
806
Inductive polynomial : Type :=
 
807
  | Pvar : index -> polynomial
 
808
  | Pconst : A -> polynomial
 
809
  | Pplus : polynomial -> polynomial -> polynomial
 
810
  | Pmult : polynomial -> polynomial -> polynomial
 
811
  | Popp : polynomial -> polynomial.
 
812
 
 
813
Fixpoint polynomial_normalize (x:polynomial) : canonical_sum A :=
 
814
  match x with
 
815
  | Pplus l r =>
 
816
      canonical_sum_merge Aplus Aone (polynomial_normalize l)
 
817
        (polynomial_normalize r)
 
818
  | Pmult l r =>
 
819
      canonical_sum_prod Aplus Amult Aone (polynomial_normalize l)
 
820
        (polynomial_normalize r)
 
821
  | Pconst c => Cons_monom c Nil_var (Nil_monom A)
 
822
  | Pvar i => Cons_varlist (Cons_var i Nil_var) (Nil_monom A)
 
823
  | Popp p =>
 
824
      canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var
 
825
        (polynomial_normalize p)
 
826
  end.
 
827
 
 
828
Definition polynomial_simplify (x:polynomial) :=
 
829
  canonical_sum_simplify Aone Azero Aeq (polynomial_normalize x).
 
830
 
 
831
Fixpoint spolynomial_of (x:polynomial) : spolynomial A :=
 
832
  match x with
 
833
  | Pplus l r => SPplus (spolynomial_of l) (spolynomial_of r)
 
834
  | Pmult l r => SPmult (spolynomial_of l) (spolynomial_of r)
 
835
  | Pconst c => SPconst c
 
836
  | Pvar i => SPvar A i
 
837
  | Popp p => SPmult (SPconst (Aopp Aone)) (spolynomial_of p)
 
838
  end.
 
839
 
 
840
(*** Interpretation *)
 
841
 
 
842
Fixpoint interp_p (p:polynomial) : A :=
 
843
  match p with
 
844
  | Pconst c => c
 
845
  | Pvar i => varmap_find Azero i vm
 
846
  | Pplus p1 p2 => Aplus (interp_p p1) (interp_p p2)
 
847
  | Pmult p1 p2 => Amult (interp_p p1) (interp_p p2)
 
848
  | Popp p1 => Aopp (interp_p p1)
 
849
  end.
 
850
 
 
851
(*** Properties *)
 
852
 
 
853
Unset Implicit Arguments.
 
854
 
 
855
Lemma spolynomial_of_ok :
 
856
 forall p:polynomial,
 
857
   interp_p p = interp_sp Aplus Amult Azero vm (spolynomial_of p).
 
858
simple induction p; reflexivity || (simpl in |- *; intros).
 
859
rewrite H; rewrite H0; reflexivity.
 
860
rewrite H; rewrite H0; reflexivity.
 
861
rewrite H.
 
862
rewrite (Th_opp_mult_left2 T).
 
863
rewrite (Th_mult_one_left T).
 
864
reflexivity.
 
865
Qed.
 
866
 
 
867
Theorem polynomial_normalize_ok :
 
868
 forall p:polynomial,
 
869
   polynomial_normalize p =
 
870
   spolynomial_normalize Aplus Amult Aone (spolynomial_of p).
 
871
simple induction p; reflexivity || (simpl in |- *; intros).
 
872
rewrite H; rewrite H0; reflexivity.
 
873
rewrite H; rewrite H0; reflexivity.
 
874
rewrite H; simpl in |- *.
 
875
elim
 
876
 (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var
 
877
    (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0)));
 
878
 [ reflexivity
 
879
 | simpl in |- *; intros; rewrite H0; reflexivity
 
880
 | simpl in |- *; intros; rewrite H0; reflexivity ].
 
881
Qed.
 
882
 
 
883
Theorem polynomial_simplify_ok :
 
884
 forall p:polynomial,
 
885
   interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p) = interp_p p.
 
886
intro.
 
887
unfold polynomial_simplify in |- *.
 
888
rewrite spolynomial_of_ok.
 
889
rewrite polynomial_normalize_ok.
 
890
rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T).
 
891
rewrite (spolynomial_normalize_ok A Aplus Amult Aone Azero Aeq vm T).
 
892
reflexivity.
 
893
Qed.
 
894
 
 
895
End rings.
 
896
 
 
897
Infix "+" := Pplus : ring_scope.
 
898
Infix "*" := Pmult : ring_scope.
 
899
Notation "- x" := (Popp x) : ring_scope.
 
900
Notation "[ x ]" := (Pvar x) (at level 0) : ring_scope.
 
901
 
 
902
Delimit Scope ring_scope with ring.