← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/ring/Setoid_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/Setoid_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: Setoid_ring_normalize.v 9370 2006-11-13 09:21:31Z herbelin $ *)
 
10
 
 
11
Require Import Setoid_ring_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
  simple induction n; simple induction m; simpl in |- *;
 
20
   try reflexivity || contradiction.
 
21
  intros; rewrite (H i0); trivial.
 
22
  intros; rewrite (H i0); trivial.
 
23
Qed.
 
24
 
 
25
Section setoid.
 
26
 
 
27
Variable A : Type.
 
28
Variable Aequiv : A -> A -> Prop.
 
29
Variable Aplus : A -> A -> A.
 
30
Variable Amult : A -> A -> A.
 
31
Variable Aone : A.
 
32
Variable Azero : A.
 
33
Variable Aopp : A -> A.
 
34
Variable Aeq : A -> A -> bool.
 
35
 
 
36
Variable S : Setoid_Theory A Aequiv.
 
37
 
 
38
Add Setoid A Aequiv S as Asetoid.
 
39
 
 
40
Variable plus_morph :
 
41
 forall a a0:A, Aequiv a a0 ->
 
42
   forall a1 a2:A, Aequiv a1 a2 ->
 
43
     Aequiv (Aplus a a1)  (Aplus a0 a2).
 
44
Variable mult_morph :
 
45
 forall a a0:A, Aequiv a a0 ->
 
46
   forall a1 a2:A, Aequiv a1 a2 ->
 
47
     Aequiv (Amult a a1) (Amult a0 a2).
 
48
Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0).
 
49
 
 
50
Add Morphism Aplus : Aplus_ext.
 
51
intros; apply plus_morph; assumption.
 
52
Qed.
 
53
 
 
54
Add Morphism Amult : Amult_ext.
 
55
intros; apply mult_morph; assumption.
 
56
Qed.
 
57
 
 
58
Add Morphism Aopp : Aopp_ext.
 
59
exact opp_morph.
 
60
Qed.
 
61
 
 
62
Let equiv_refl := Seq_refl A Aequiv S.
 
63
Let equiv_sym := Seq_sym A Aequiv S.
 
64
Let equiv_trans := Seq_trans A Aequiv S.
 
65
 
 
66
Hint Resolve equiv_refl equiv_trans.
 
67
Hint Immediate equiv_sym.
 
68
 
 
69
Section semi_setoid_rings.
 
70
 
 
71
(* Section definitions. *)
 
72
 
 
73
 
 
74
(******************************************)
 
75
(* Normal abtract Polynomials             *)
 
76
(******************************************)
 
77
(* DEFINITIONS :
 
78
- A varlist is a sorted product of one or more variables : x, x*y*z 
 
79
- A monom is a constant, a varlist or the product of a constant by a varlist
 
80
  variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT.
 
81
- A canonical sum is either a monom or an ordered sum of monoms 
 
82
  (the order on monoms is defined later) 
 
83
- A normal polynomial it either a constant or a canonical sum or a constant
 
84
  plus a canonical sum
 
85
*)
 
86
 
 
87
(* varlist is isomorphic to (list var), but we built a special inductive
 
88
   for efficiency *)
 
89
Inductive varlist : Type :=
 
90
  | Nil_var : varlist
 
91
  | Cons_var : index -> varlist -> varlist.
 
92
 
 
93
Inductive canonical_sum : Type :=
 
94
  | Nil_monom : canonical_sum
 
95
  | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum
 
96
  | Cons_varlist : varlist -> canonical_sum -> canonical_sum.
 
97
 
 
98
(* Order on monoms *)
 
99
 
 
100
(* That's the lexicographic order on varlist, extended by : 
 
101
  - A constant is less than every monom 
 
102
  - The relation between two varlist is preserved by multiplication by a
 
103
  constant.
 
104
 
 
105
  Examples : 
 
106
  3 < x < y
 
107
  x*y < x*y*y*z 
 
108
  2*x*y < x*y*y*z
 
109
  x*y < 54*x*y*y*z
 
110
  4*x*y < 59*x*y*y*z
 
111
*)
 
112
 
 
113
Fixpoint varlist_eq (x y:varlist) {struct y} : bool :=
 
114
  match x, y with
 
115
  | Nil_var, Nil_var => true
 
116
  | Cons_var i xrest, Cons_var j yrest =>
 
117
      andb (index_eq i j) (varlist_eq xrest yrest)
 
118
  | _, _ => false
 
119
  end.
 
120
 
 
121
Fixpoint varlist_lt (x y:varlist) {struct y} : bool :=
 
122
  match x, y with
 
123
  | Nil_var, Cons_var _ _ => true
 
124
  | Cons_var i xrest, Cons_var j yrest =>
 
125
      if index_lt i j
 
126
      then true
 
127
      else andb (index_eq i j) (varlist_lt xrest yrest)
 
128
  | _, _ => false
 
129
  end.
 
130
 
 
131
(* merges two variables lists *)
 
132
Fixpoint varlist_merge (l1:varlist) : varlist -> varlist :=
 
133
  match l1 with
 
134
  | Cons_var v1 t1 =>
 
135
      (fix vm_aux (l2:varlist) : varlist :=
 
136
         match l2 with
 
137
         | Cons_var v2 t2 =>
 
138
             if index_lt v1 v2
 
139
             then Cons_var v1 (varlist_merge t1 l2)
 
140
             else Cons_var v2 (vm_aux t2)
 
141
         | Nil_var => l1
 
142
         end)
 
143
  | Nil_var => fun l2 => l2
 
144
  end.
 
145
 
 
146
(* returns the sum of two canonical sums  *)
 
147
Fixpoint canonical_sum_merge (s1:canonical_sum) :
 
148
 canonical_sum -> canonical_sum :=
 
149
  match s1 with
 
150
  | Cons_monom c1 l1 t1 =>
 
151
      (fix csm_aux (s2:canonical_sum) : canonical_sum :=
 
152
         match s2 with
 
153
         | Cons_monom c2 l2 t2 =>
 
154
             if varlist_eq l1 l2
 
155
             then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2)
 
156
             else
 
157
              if varlist_lt l1 l2
 
158
              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
 
159
              else Cons_monom c2 l2 (csm_aux t2)
 
160
         | Cons_varlist l2 t2 =>
 
161
             if varlist_eq l1 l2
 
162
             then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2)
 
163
             else
 
164
              if varlist_lt l1 l2
 
165
              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
 
166
              else Cons_varlist l2 (csm_aux t2)
 
167
         | Nil_monom => s1
 
168
         end)
 
169
  | Cons_varlist l1 t1 =>
 
170
      (fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
 
171
         match s2 with
 
172
         | Cons_monom c2 l2 t2 =>
 
173
             if varlist_eq l1 l2
 
174
             then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2)
 
175
             else
 
176
              if varlist_lt l1 l2
 
177
              then Cons_varlist l1 (canonical_sum_merge t1 s2)
 
178
              else Cons_monom c2 l2 (csm_aux2 t2)
 
179
         | Cons_varlist l2 t2 =>
 
180
             if varlist_eq l1 l2
 
181
             then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2)
 
182
             else
 
183
              if varlist_lt l1 l2
 
184
              then Cons_varlist l1 (canonical_sum_merge t1 s2)
 
185
              else Cons_varlist l2 (csm_aux2 t2)
 
186
         | Nil_monom => s1
 
187
         end)
 
188
  | Nil_monom => fun s2 => s2
 
189
  end.
 
190
 
 
191
(* Insertion of a monom in a canonical sum *)
 
192
Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} :
 
193
 canonical_sum :=
 
194
  match s2 with
 
195
  | Cons_monom c2 l2 t2 =>
 
196
      if varlist_eq l1 l2
 
197
      then Cons_monom (Aplus c1 c2) l1 t2
 
198
      else
 
199
       if varlist_lt l1 l2
 
200
       then Cons_monom c1 l1 s2
 
201
       else Cons_monom c2 l2 (monom_insert c1 l1 t2)
 
202
  | Cons_varlist l2 t2 =>
 
203
      if varlist_eq l1 l2
 
204
      then Cons_monom (Aplus c1 Aone) l1 t2
 
205
      else
 
206
       if varlist_lt l1 l2
 
207
       then Cons_monom c1 l1 s2
 
208
       else Cons_varlist l2 (monom_insert c1 l1 t2)
 
209
  | Nil_monom => Cons_monom c1 l1 Nil_monom
 
210
  end.
 
211
 
 
212
Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} :
 
213
 canonical_sum :=
 
214
  match s2 with
 
215
  | Cons_monom c2 l2 t2 =>
 
216
      if varlist_eq l1 l2
 
217
      then Cons_monom (Aplus Aone c2) l1 t2
 
218
      else
 
219
       if varlist_lt l1 l2
 
220
       then Cons_varlist l1 s2
 
221
       else Cons_monom c2 l2 (varlist_insert l1 t2)
 
222
  | Cons_varlist l2 t2 =>
 
223
      if varlist_eq l1 l2
 
224
      then Cons_monom (Aplus Aone Aone) l1 t2
 
225
      else
 
226
       if varlist_lt l1 l2
 
227
       then Cons_varlist l1 s2
 
228
       else Cons_varlist l2 (varlist_insert l1 t2)
 
229
  | Nil_monom => Cons_varlist l1 Nil_monom
 
230
  end.
 
231
 
 
232
(* Computes c0*s *)
 
233
Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} :
 
234
 canonical_sum :=
 
235
  match s with
 
236
  | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t)
 
237
  | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t)
 
238
  | Nil_monom => Nil_monom
 
239
  end.
 
240
 
 
241
(* Computes l0*s  *)
 
242
Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} :
 
243
 canonical_sum :=
 
244
  match s with
 
245
  | Cons_monom c l t =>
 
246
      monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
 
247
  | Cons_varlist l t =>
 
248
      varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
 
249
  | Nil_monom => Nil_monom
 
250
  end.
 
251
 
 
252
(* Computes c0*l0*s  *)
 
253
Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist) 
 
254
 (s:canonical_sum) {struct s} : canonical_sum :=
 
255
  match s with
 
256
  | Cons_monom c l t =>
 
257
      monom_insert (Amult c0 c) (varlist_merge l0 l)
 
258
        (canonical_sum_scalar3 c0 l0 t)
 
259
  | Cons_varlist l t =>
 
260
      monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t)
 
261
  | Nil_monom => Nil_monom
 
262
  end.
 
263
 
 
264
(* returns the product of two canonical sums *) 
 
265
Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} :
 
266
 canonical_sum :=
 
267
  match s1 with
 
268
  | Cons_monom c1 l1 t1 =>
 
269
      canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2)
 
270
        (canonical_sum_prod t1 s2)
 
271
  | Cons_varlist l1 t1 =>
 
272
      canonical_sum_merge (canonical_sum_scalar2 l1 s2)
 
273
        (canonical_sum_prod t1 s2)
 
274
  | Nil_monom => Nil_monom
 
275
  end.
 
276
 
 
277
(* The type to represent concrete semi-setoid-ring polynomials *)
 
278
 
 
279
Inductive setspolynomial : Type :=
 
280
  | SetSPvar : index -> setspolynomial
 
281
  | SetSPconst : A -> setspolynomial
 
282
  | SetSPplus : setspolynomial -> setspolynomial -> setspolynomial
 
283
  | SetSPmult : setspolynomial -> setspolynomial -> setspolynomial.
 
284
 
 
285
Fixpoint setspolynomial_normalize (p:setspolynomial) : canonical_sum :=
 
286
  match p with
 
287
  | SetSPplus l r =>
 
288
      canonical_sum_merge (setspolynomial_normalize l)
 
289
        (setspolynomial_normalize r)
 
290
  | SetSPmult l r =>
 
291
      canonical_sum_prod (setspolynomial_normalize l)
 
292
        (setspolynomial_normalize r)
 
293
  | SetSPconst c => Cons_monom c Nil_var Nil_monom
 
294
  | SetSPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom
 
295
  end.
 
296
 
 
297
Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum :=
 
298
  match s with
 
299
  | Cons_monom c l t =>
 
300
      if Aeq c Azero
 
301
      then canonical_sum_simplify t
 
302
      else
 
303
       if Aeq c Aone
 
304
       then Cons_varlist l (canonical_sum_simplify t)
 
305
       else Cons_monom c l (canonical_sum_simplify t)
 
306
  | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t)
 
307
  | Nil_monom => Nil_monom
 
308
  end.
 
309
 
 
310
Definition setspolynomial_simplify (x:setspolynomial) :=
 
311
  canonical_sum_simplify (setspolynomial_normalize x).
 
312
 
 
313
Variable vm : varmap A.
 
314
 
 
315
Definition interp_var (i:index) := varmap_find Azero i vm.
 
316
 
 
317
Definition ivl_aux :=
 
318
  (fix ivl_aux (x:index) (t:varlist) {struct t} : A :=
 
319
     match t with
 
320
     | Nil_var => interp_var x
 
321
     | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t')
 
322
     end).
 
323
 
 
324
Definition interp_vl (l:varlist) :=
 
325
  match l with
 
326
  | Nil_var => Aone
 
327
  | Cons_var x t => ivl_aux x t
 
328
  end.
 
329
 
 
330
Definition interp_m (c:A) (l:varlist) :=
 
331
  match l with
 
332
  | Nil_var => c
 
333
  | Cons_var x t => Amult c (ivl_aux x t)
 
334
  end.
 
335
 
 
336
Definition ics_aux :=
 
337
  (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A :=
 
338
     match s with
 
339
     | Nil_monom => a
 
340
     | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t)
 
341
     | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t)
 
342
     end).
 
343
 
 
344
Definition interp_setcs (s:canonical_sum) : A :=
 
345
  match s with
 
346
  | Nil_monom => Azero
 
347
  | Cons_varlist l t => ics_aux (interp_vl l) t
 
348
  | Cons_monom c l t => ics_aux (interp_m c l) t
 
349
  end.
 
350
 
 
351
Fixpoint interp_setsp (p:setspolynomial) : A :=
 
352
  match p with
 
353
  | SetSPconst c => c
 
354
  | SetSPvar i => interp_var i
 
355
  | SetSPplus p1 p2 => Aplus (interp_setsp p1) (interp_setsp p2)
 
356
  | SetSPmult p1 p2 => Amult (interp_setsp p1) (interp_setsp p2)
 
357
  end.
 
358
 
 
359
(* End interpretation. *)
 
360
 
 
361
Unset Implicit Arguments.
 
362
 
 
363
(* Section properties. *)
 
364
 
 
365
Variable T : Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq.
 
366
 
 
367
Hint Resolve (SSR_plus_comm T).
 
368
Hint Resolve (SSR_plus_assoc T).
 
369
Hint Resolve (SSR_plus_assoc2 S T).
 
370
Hint Resolve (SSR_mult_comm T).
 
371
Hint Resolve (SSR_mult_assoc T).
 
372
Hint Resolve (SSR_mult_assoc2 S T).
 
373
Hint Resolve (SSR_plus_zero_left T).
 
374
Hint Resolve (SSR_plus_zero_left2 S T).
 
375
Hint Resolve (SSR_mult_one_left T).
 
376
Hint Resolve (SSR_mult_one_left2 S T).
 
377
Hint Resolve (SSR_mult_zero_left T).
 
378
Hint Resolve (SSR_mult_zero_left2 S T).
 
379
Hint Resolve (SSR_distr_left T).
 
380
Hint Resolve (SSR_distr_left2 S T).
 
381
Hint Resolve (SSR_plus_reg_left T).
 
382
Hint Resolve (SSR_plus_permute S plus_morph T).
 
383
Hint Resolve (SSR_mult_permute S mult_morph T).
 
384
Hint Resolve (SSR_distr_right S plus_morph T).
 
385
Hint Resolve (SSR_distr_right2 S plus_morph T).
 
386
Hint Resolve (SSR_mult_zero_right S T).
 
387
Hint Resolve (SSR_mult_zero_right2 S T).
 
388
Hint Resolve (SSR_plus_zero_right S T).
 
389
Hint Resolve (SSR_plus_zero_right2 S T).
 
390
Hint Resolve (SSR_mult_one_right S T).
 
391
Hint Resolve (SSR_mult_one_right2 S T).
 
392
Hint Resolve (SSR_plus_reg_right S T).
 
393
Hint Resolve refl_equal sym_equal trans_equal.
 
394
(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 
395
Hint Immediate T.
 
396
 
 
397
Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y.
 
398
Proof.
 
399
  simple induction x; simple induction y; contradiction || (try reflexivity).
 
400
  simpl in |- *; intros.
 
401
  generalize (andb_prop2 _ _ H1); intros; elim H2; intros.
 
402
  rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity.
 
403
Qed.
 
404
 
 
405
Remark ivl_aux_ok :
 
406
 forall (v:varlist) (i:index),
 
407
   Aequiv (ivl_aux i v) (Amult (interp_var i) (interp_vl v)).
 
408
Proof.
 
409
  simple induction v; simpl in |- *; intros.
 
410
  trivial.
 
411
  rewrite (H i); trivial.
 
412
Qed.
 
413
 
 
414
Lemma varlist_merge_ok :
 
415
 forall x y:varlist,
 
416
   Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y)).
 
417
Proof.
 
418
  simple induction x.
 
419
  simpl in |- *; trivial.
 
420
  simple induction y.
 
421
  simpl in |- *; trivial.
 
422
  simpl in |- *; intros.
 
423
  elim (index_lt i i0); simpl in |- *; intros.
 
424
 
 
425
  rewrite (ivl_aux_ok v i).
 
426
  rewrite (ivl_aux_ok v0 i0).
 
427
  rewrite (ivl_aux_ok (varlist_merge v (Cons_var i0 v0)) i).
 
428
  rewrite (H (Cons_var i0 v0)).
 
429
  simpl in |- *.
 
430
  rewrite (ivl_aux_ok v0 i0).
 
431
  eauto.
 
432
 
 
433
  rewrite (ivl_aux_ok v i).
 
434
  rewrite (ivl_aux_ok v0 i0).
 
435
  rewrite
 
436
   (ivl_aux_ok
 
437
      ((fix vm_aux (l2:varlist) : varlist :=
 
438
          match l2 with
 
439
          | Nil_var => Cons_var i v
 
440
          | Cons_var v2 t2 =>
 
441
              if index_lt i v2
 
442
              then Cons_var i (varlist_merge v l2)
 
443
              else Cons_var v2 (vm_aux t2)
 
444
          end) v0) i0).
 
445
  rewrite H0.
 
446
  rewrite (ivl_aux_ok v i).
 
447
  eauto.
 
448
Qed.
 
449
 
 
450
Remark ics_aux_ok :
 
451
 forall (x:A) (s:canonical_sum),
 
452
   Aequiv (ics_aux x s) (Aplus x (interp_setcs s)).
 
453
Proof.
 
454
 simple induction s; simpl in |- *; intros; trivial.
 
455
Qed.
 
456
 
 
457
Remark interp_m_ok :
 
458
 forall (x:A) (l:varlist), Aequiv (interp_m x l) (Amult x (interp_vl l)).
 
459
Proof.
 
460
  destruct l as [| i v]; trivial.
 
461
Qed.
 
462
 
 
463
Hint Resolve ivl_aux_ok.
 
464
Hint Resolve ics_aux_ok.
 
465
Hint Resolve interp_m_ok.
 
466
 
 
467
(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *)
 
468
 
 
469
Lemma canonical_sum_merge_ok :
 
470
 forall x y:canonical_sum,
 
471
   Aequiv (interp_setcs (canonical_sum_merge x y))
 
472
     (Aplus (interp_setcs x) (interp_setcs y)).
 
473
Proof.
 
474
simple induction x; simpl in |- *.
 
475
trivial.
 
476
 
 
477
simple induction y; simpl in |- *; intros.
 
478
eauto.
 
479
 
 
480
generalize (varlist_eq_prop v v0).
 
481
elim (varlist_eq v v0).
 
482
intros; rewrite (H1 I).
 
483
simpl in |- *.
 
484
rewrite (ics_aux_ok (interp_m a v0) c).
 
485
rewrite (ics_aux_ok (interp_m a0 v0) c0).
 
486
rewrite (ics_aux_ok (interp_m (Aplus a a0) v0) (canonical_sum_merge c c0)).
 
487
rewrite (H c0).
 
488
rewrite (interp_m_ok (Aplus a a0) v0).
 
489
rewrite (interp_m_ok a v0).
 
490
rewrite (interp_m_ok a0 v0).
 
491
setoid_replace (Amult (Aplus a a0) (interp_vl v0)) with
 
492
 (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)));
 
493
 [ idtac | trivial ].
 
494
setoid_replace
 
495
 (Aplus (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)))
 
496
    (Aplus (interp_setcs c) (interp_setcs c0))) with
 
497
 (Aplus (Amult a (interp_vl v0))
 
498
    (Aplus (Amult a0 (interp_vl v0))
 
499
       (Aplus (interp_setcs c) (interp_setcs c0))));
 
500
 [ idtac | trivial ].
 
501
setoid_replace
 
502
 (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
 
503
    (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))) with
 
504
 (Aplus (Amult a (interp_vl v0))
 
505
    (Aplus (interp_setcs c)
 
506
       (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))));
 
507
 [ idtac | trivial ].
 
508
auto.
 
509
 
 
510
elim (varlist_lt v v0); simpl in |- *.
 
511
intro.
 
512
rewrite
 
513
 (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_monom a0 v0 c0)))
 
514
 .
 
515
rewrite (ics_aux_ok (interp_m a v) c).
 
516
rewrite (ics_aux_ok (interp_m a0 v0) c0).
 
517
rewrite (H (Cons_monom a0 v0 c0)); simpl in |- *.
 
518
rewrite (ics_aux_ok (interp_m a0 v0) c0); auto.
 
519
 
 
520
intro.
 
521
rewrite
 
522
 (ics_aux_ok (interp_m a0 v0)
 
523
    ((fix csm_aux (s2:canonical_sum) : canonical_sum :=
 
524
        match s2 with
 
525
        | Nil_monom => Cons_monom a v c
 
526
        | Cons_monom c2 l2 t2 =>
 
527
            if varlist_eq v l2
 
528
            then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2)
 
529
            else
 
530
             if varlist_lt v l2
 
531
             then Cons_monom a v (canonical_sum_merge c s2)
 
532
             else Cons_monom c2 l2 (csm_aux t2)
 
533
        | Cons_varlist l2 t2 =>
 
534
            if varlist_eq v l2
 
535
            then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2)
 
536
            else
 
537
             if varlist_lt v l2
 
538
             then Cons_monom a v (canonical_sum_merge c s2)
 
539
             else Cons_varlist l2 (csm_aux t2)
 
540
        end) c0)).
 
541
rewrite H0.
 
542
rewrite (ics_aux_ok (interp_m a v) c);
 
543
 rewrite (ics_aux_ok (interp_m a0 v0) c0); simpl in |- *; 
 
544
 auto.
 
545
 
 
546
generalize (varlist_eq_prop v v0).
 
547
elim (varlist_eq v v0).
 
548
intros; rewrite (H1 I).
 
549
simpl in |- *.
 
550
rewrite (ics_aux_ok (interp_m (Aplus a Aone) v0) (canonical_sum_merge c c0));
 
551
 rewrite (ics_aux_ok (interp_m a v0) c);
 
552
 rewrite (ics_aux_ok (interp_vl v0) c0).
 
553
rewrite (H c0).
 
554
rewrite (interp_m_ok (Aplus a Aone) v0).
 
555
rewrite (interp_m_ok a v0).
 
556
setoid_replace (Amult (Aplus a Aone) (interp_vl v0)) with
 
557
 (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)));
 
558
 [ idtac | trivial ].
 
559
setoid_replace
 
560
 (Aplus (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)))
 
561
    (Aplus (interp_setcs c) (interp_setcs c0))) with
 
562
 (Aplus (Amult a (interp_vl v0))
 
563
    (Aplus (Amult Aone (interp_vl v0))
 
564
       (Aplus (interp_setcs c) (interp_setcs c0))));
 
565
 [ idtac | trivial ].
 
566
setoid_replace
 
567
 (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
 
568
    (Aplus (interp_vl v0) (interp_setcs c0))) with
 
569
 (Aplus (Amult a (interp_vl v0))
 
570
    (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
 
571
 [ idtac | trivial ].
 
572
setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0);
 
573
 [ idtac | trivial ].
 
574
auto.
 
575
 
 
576
elim (varlist_lt v v0); simpl in |- *.
 
577
intro.
 
578
rewrite
 
579
 (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_varlist v0 c0)))
 
580
 ; rewrite (ics_aux_ok (interp_m a v) c);
 
581
 rewrite (ics_aux_ok (interp_vl v0) c0).
 
582
rewrite (H (Cons_varlist v0 c0)); simpl in |- *.
 
583
rewrite (ics_aux_ok (interp_vl v0) c0).
 
584
auto.
 
585
 
 
586
intro.
 
587
rewrite
 
588
 (ics_aux_ok (interp_vl v0)
 
589
    ((fix csm_aux (s2:canonical_sum) : canonical_sum :=
 
590
        match s2 with
 
591
        | Nil_monom => Cons_monom a v c
 
592
        | Cons_monom c2 l2 t2 =>
 
593
            if varlist_eq v l2
 
594
            then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2)
 
595
            else
 
596
             if varlist_lt v l2
 
597
             then Cons_monom a v (canonical_sum_merge c s2)
 
598
             else Cons_monom c2 l2 (csm_aux t2)
 
599
        | Cons_varlist l2 t2 =>
 
600
            if varlist_eq v l2
 
601
            then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2)
 
602
            else
 
603
             if varlist_lt v l2
 
604
             then Cons_monom a v (canonical_sum_merge c s2)
 
605
             else Cons_varlist l2 (csm_aux t2)
 
606
        end) c0)); rewrite H0.
 
607
rewrite (ics_aux_ok (interp_m a v) c); rewrite (ics_aux_ok (interp_vl v0) c0);
 
608
 simpl in |- *.
 
609
auto.
 
610
 
 
611
simple induction y; simpl in |- *; intros.
 
612
trivial.
 
613
 
 
614
generalize (varlist_eq_prop v v0).
 
615
elim (varlist_eq v v0).
 
616
intros; rewrite (H1 I).
 
617
simpl in |- *.
 
618
rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0) (canonical_sum_merge c c0));
 
619
 rewrite (ics_aux_ok (interp_vl v0) c);
 
620
 rewrite (ics_aux_ok (interp_m a v0) c0); rewrite (H c0).
 
621
rewrite (interp_m_ok (Aplus Aone a) v0); rewrite (interp_m_ok a v0).
 
622
setoid_replace (Amult (Aplus Aone a) (interp_vl v0)) with
 
623
 (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)));
 
624
 [ idtac | trivial ].
 
625
setoid_replace
 
626
 (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)))
 
627
    (Aplus (interp_setcs c) (interp_setcs c0))) with
 
628
 (Aplus (Amult Aone (interp_vl v0))
 
629
    (Aplus (Amult a (interp_vl v0))
 
630
       (Aplus (interp_setcs c) (interp_setcs c0))));
 
631
 [ idtac | trivial ].
 
632
setoid_replace
 
633
 (Aplus (Aplus (interp_vl v0) (interp_setcs c))
 
634
    (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))) with
 
635
 (Aplus (interp_vl v0)
 
636
    (Aplus (interp_setcs c)
 
637
       (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))));
 
638
 [ idtac | trivial ].
 
639
auto.
 
640
 
 
641
elim (varlist_lt v v0); simpl in |- *; intros.
 
642
rewrite
 
643
 (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_monom a v0 c0)))
 
644
 ; rewrite (ics_aux_ok (interp_vl v) c);
 
645
 rewrite (ics_aux_ok (interp_m a v0) c0).
 
646
rewrite (H (Cons_monom a v0 c0)); simpl in |- *.
 
647
rewrite (ics_aux_ok (interp_m a v0) c0); auto.
 
648
 
 
649
rewrite
 
650
 (ics_aux_ok (interp_m a v0)
 
651
    ((fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
 
652
        match s2 with
 
653
        | Nil_monom => Cons_varlist v c
 
654
        | Cons_monom c2 l2 t2 =>
 
655
            if varlist_eq v l2
 
656
            then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2)
 
657
            else
 
658
             if varlist_lt v l2
 
659
             then Cons_varlist v (canonical_sum_merge c s2)
 
660
             else Cons_monom c2 l2 (csm_aux2 t2)
 
661
        | Cons_varlist l2 t2 =>
 
662
            if varlist_eq v l2
 
663
            then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2)
 
664
            else
 
665
             if varlist_lt v l2
 
666
             then Cons_varlist v (canonical_sum_merge c s2)
 
667
             else Cons_varlist l2 (csm_aux2 t2)
 
668
        end) c0)); rewrite H0.
 
669
rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_m a v0) c0);
 
670
 simpl in |- *; auto.
 
671
 
 
672
generalize (varlist_eq_prop v v0).
 
673
elim (varlist_eq v v0); intros.
 
674
rewrite (H1 I); simpl in |- *.
 
675
rewrite
 
676
 (ics_aux_ok (interp_m (Aplus Aone Aone) v0) (canonical_sum_merge c c0))
 
677
 ; rewrite (ics_aux_ok (interp_vl v0) c);
 
678
 rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H c0).
 
679
rewrite (interp_m_ok (Aplus Aone Aone) v0).
 
680
setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0)) with
 
681
 (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)));
 
682
 [ idtac | trivial ].
 
683
setoid_replace
 
684
 (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)))
 
685
    (Aplus (interp_setcs c) (interp_setcs c0))) with
 
686
 (Aplus (Amult Aone (interp_vl v0))
 
687
    (Aplus (Amult Aone (interp_vl v0))
 
688
       (Aplus (interp_setcs c) (interp_setcs c0))));
 
689
 [ idtac | trivial ].
 
690
setoid_replace
 
691
 (Aplus (Aplus (interp_vl v0) (interp_setcs c))
 
692
    (Aplus (interp_vl v0) (interp_setcs c0))) with
 
693
 (Aplus (interp_vl v0)
 
694
    (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
 
695
[ idtac | trivial ].
 
696
setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); auto.
 
697
 
 
698
elim (varlist_lt v v0); simpl in |- *.
 
699
rewrite
 
700
 (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_varlist v0 c0)))
 
701
 ; rewrite (ics_aux_ok (interp_vl v) c);
 
702
 rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H (Cons_varlist v0 c0));
 
703
 simpl in |- *.
 
704
rewrite (ics_aux_ok (interp_vl v0) c0); auto.
 
705
 
 
706
rewrite
 
707
 (ics_aux_ok (interp_vl v0)
 
708
    ((fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
 
709
        match s2 with
 
710
        | Nil_monom => Cons_varlist v c
 
711
        | Cons_monom c2 l2 t2 =>
 
712
            if varlist_eq v l2
 
713
            then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2)
 
714
            else
 
715
             if varlist_lt v l2
 
716
             then Cons_varlist v (canonical_sum_merge c s2)
 
717
             else Cons_monom c2 l2 (csm_aux2 t2)
 
718
        | Cons_varlist l2 t2 =>
 
719
            if varlist_eq v l2
 
720
            then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2)
 
721
            else
 
722
             if varlist_lt v l2
 
723
             then Cons_varlist v (canonical_sum_merge c s2)
 
724
             else Cons_varlist l2 (csm_aux2 t2)
 
725
        end) c0)); rewrite H0.
 
726
rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_vl v0) c0);
 
727
 simpl in |- *; auto.
 
728
Qed.
 
729
 
 
730
Lemma monom_insert_ok :
 
731
 forall (a:A) (l:varlist) (s:canonical_sum),
 
732
   Aequiv (interp_setcs (monom_insert a l s))
 
733
     (Aplus (Amult a (interp_vl l)) (interp_setcs s)).
 
734
Proof.
 
735
simple induction s; intros.
 
736
simpl in |- *; rewrite (interp_m_ok a l); trivial.
 
737
 
 
738
simpl in |- *; generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
739
intro Hr; rewrite (Hr I); simpl in |- *.
 
740
rewrite (ics_aux_ok (interp_m (Aplus a a0) v) c);
 
741
 rewrite (ics_aux_ok (interp_m a0 v) c).
 
742
rewrite (interp_m_ok (Aplus a a0) v); rewrite (interp_m_ok a0 v).
 
743
setoid_replace (Amult (Aplus a a0) (interp_vl v)) with
 
744
 (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v)));
 
745
 [ idtac | trivial ].
 
746
auto.
 
747
 
 
748
elim (varlist_lt l v); simpl in |- *; intros.
 
749
rewrite (ics_aux_ok (interp_m a0 v) c).
 
750
rewrite (interp_m_ok a0 v); rewrite (interp_m_ok a l).
 
751
auto.
 
752
 
 
753
rewrite (ics_aux_ok (interp_m a0 v) (monom_insert a l c));
 
754
 rewrite (ics_aux_ok (interp_m a0 v) c); rewrite H.
 
755
auto.
 
756
 
 
757
simpl in |- *.
 
758
generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
759
intro Hr; rewrite (Hr I); simpl in |- *.
 
760
rewrite (ics_aux_ok (interp_m (Aplus a Aone) v) c);
 
761
 rewrite (ics_aux_ok (interp_vl v) c).
 
762
rewrite (interp_m_ok (Aplus a Aone) v).
 
763
setoid_replace (Amult (Aplus a Aone) (interp_vl v)) with
 
764
 (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v)));
 
765
 [ idtac | trivial ].
 
766
setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v);
 
767
 [ idtac | trivial ].
 
768
auto.
 
769
 
 
770
elim (varlist_lt l v); simpl in |- *; intros; auto.
 
771
rewrite (ics_aux_ok (interp_vl v) (monom_insert a l c)); rewrite H.
 
772
rewrite (ics_aux_ok (interp_vl v) c); auto.
 
773
Qed.
 
774
 
 
775
Lemma varlist_insert_ok :
 
776
 forall (l:varlist) (s:canonical_sum),
 
777
   Aequiv (interp_setcs (varlist_insert l s))
 
778
     (Aplus (interp_vl l) (interp_setcs s)).
 
779
Proof.
 
780
simple induction s; simpl in |- *; intros.
 
781
trivial.
 
782
 
 
783
generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
784
intro Hr; rewrite (Hr I); simpl in |- *.
 
785
rewrite (ics_aux_ok (interp_m (Aplus Aone a) v) c);
 
786
 rewrite (ics_aux_ok (interp_m a v) c).
 
787
rewrite (interp_m_ok (Aplus Aone a) v); rewrite (interp_m_ok a v).
 
788
setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with
 
789
 (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v)));
 
790
 [ idtac | trivial ].
 
791
setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
 
792
 
 
793
elim (varlist_lt l v); simpl in |- *; intros; auto.
 
794
rewrite (ics_aux_ok (interp_m a v) (varlist_insert l c));
 
795
 rewrite (ics_aux_ok (interp_m a v) c).
 
796
rewrite (interp_m_ok a v).
 
797
rewrite H; auto.
 
798
 
 
799
generalize (varlist_eq_prop l v); elim (varlist_eq l v).
 
800
intro Hr; rewrite (Hr I); simpl in |- *.
 
801
rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v) c);
 
802
 rewrite (ics_aux_ok (interp_vl v) c).
 
803
rewrite (interp_m_ok (Aplus Aone Aone) v).
 
804
setoid_replace (Amult (Aplus Aone Aone) (interp_vl v)) with
 
805
 (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v)));
 
806
 [ idtac | trivial ].
 
807
setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
 
808
 
 
809
elim (varlist_lt l v); simpl in |- *; intros; auto.
 
810
rewrite (ics_aux_ok (interp_vl v) (varlist_insert l c)).
 
811
rewrite H.
 
812
rewrite (ics_aux_ok (interp_vl v) c); auto.
 
813
Qed.
 
814
 
 
815
Lemma canonical_sum_scalar_ok :
 
816
 forall (a:A) (s:canonical_sum),
 
817
   Aequiv (interp_setcs (canonical_sum_scalar a s))
 
818
     (Amult a (interp_setcs s)).
 
819
Proof.
 
820
simple induction s; simpl in |- *; intros.
 
821
trivial.
 
822
 
 
823
rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c));
 
824
 rewrite (ics_aux_ok (interp_m a0 v) c).
 
825
rewrite (interp_m_ok (Amult a a0) v); rewrite (interp_m_ok a0 v).
 
826
rewrite H.
 
827
setoid_replace (Amult a (Aplus (Amult a0 (interp_vl v)) (interp_setcs c)))
 
828
 with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c)));
 
829
 [ idtac | trivial ].
 
830
auto.
 
831
 
 
832
rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c));
 
833
 rewrite (ics_aux_ok (interp_vl v) c); rewrite H.
 
834
rewrite (interp_m_ok a v).
 
835
auto.
 
836
Qed.
 
837
 
 
838
Lemma canonical_sum_scalar2_ok :
 
839
 forall (l:varlist) (s:canonical_sum),
 
840
   Aequiv (interp_setcs (canonical_sum_scalar2 l s))
 
841
     (Amult (interp_vl l) (interp_setcs s)).
 
842
Proof.
 
843
simple induction s; simpl in |- *; intros; auto.
 
844
rewrite (monom_insert_ok a (varlist_merge l v) (canonical_sum_scalar2 l c)).
 
845
rewrite (ics_aux_ok (interp_m a v) c).
 
846
rewrite (interp_m_ok a v).
 
847
rewrite H.
 
848
rewrite (varlist_merge_ok l v).
 
849
setoid_replace
 
850
 (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c))) with
 
851
 (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
 
852
    (Amult (interp_vl l) (interp_setcs c)));
 
853
 [ idtac | trivial ].
 
854
auto.
 
855
 
 
856
rewrite (varlist_insert_ok (varlist_merge l v) (canonical_sum_scalar2 l c)).
 
857
rewrite (ics_aux_ok (interp_vl v) c).
 
858
rewrite H.
 
859
rewrite (varlist_merge_ok l v).
 
860
auto.
 
861
Qed.
 
862
 
 
863
Lemma canonical_sum_scalar3_ok :
 
864
 forall (c:A) (l:varlist) (s:canonical_sum),
 
865
   Aequiv (interp_setcs (canonical_sum_scalar3 c l s))
 
866
     (Amult c (Amult (interp_vl l) (interp_setcs s))).
 
867
Proof.
 
868
simple induction s; simpl in |- *; intros.
 
869
rewrite (SSR_mult_zero_right S T (interp_vl l)).
 
870
auto.
 
871
 
 
872
rewrite
 
873
 (monom_insert_ok (Amult c a) (varlist_merge l v)
 
874
    (canonical_sum_scalar3 c l c0)).
 
875
rewrite (ics_aux_ok (interp_m a v) c0).
 
876
rewrite (interp_m_ok a v).
 
877
rewrite H.
 
878
rewrite (varlist_merge_ok l v).
 
879
setoid_replace
 
880
 (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c0))) with
 
881
 (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
 
882
    (Amult (interp_vl l) (interp_setcs c0)));
 
883
 [ idtac | trivial ].
 
884
setoid_replace
 
885
 (Amult c
 
886
    (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
 
887
       (Amult (interp_vl l) (interp_setcs c0)))) with
 
888
 (Aplus (Amult c (Amult (interp_vl l) (Amult a (interp_vl v))))
 
889
    (Amult c (Amult (interp_vl l) (interp_setcs c0))));
 
890
 [ idtac | trivial ].
 
891
setoid_replace (Amult (Amult c a) (Amult (interp_vl l) (interp_vl v))) with
 
892
 (Amult c (Amult a (Amult (interp_vl l) (interp_vl v))));
 
893
 [ idtac | trivial ].
 
894
auto.
 
895
 
 
896
rewrite
 
897
 (monom_insert_ok c (varlist_merge l v) (canonical_sum_scalar3 c l c0))
 
898
 .
 
899
rewrite (ics_aux_ok (interp_vl v) c0).
 
900
rewrite H.
 
901
rewrite (varlist_merge_ok l v).
 
902
setoid_replace
 
903
 (Aplus (Amult c (Amult (interp_vl l) (interp_vl v)))
 
904
    (Amult c (Amult (interp_vl l) (interp_setcs c0)))) with
 
905
 (Amult c
 
906
    (Aplus (Amult (interp_vl l) (interp_vl v))
 
907
       (Amult (interp_vl l) (interp_setcs c0))));
 
908
 [ idtac | trivial ].
 
909
auto.
 
910
Qed.
 
911
 
 
912
Lemma canonical_sum_prod_ok :
 
913
 forall x y:canonical_sum,
 
914
   Aequiv (interp_setcs (canonical_sum_prod x y))
 
915
     (Amult (interp_setcs x) (interp_setcs y)).
 
916
Proof.
 
917
simple induction x; simpl in |- *; intros.
 
918
trivial.
 
919
 
 
920
rewrite
 
921
 (canonical_sum_merge_ok (canonical_sum_scalar3 a v y)
 
922
    (canonical_sum_prod c y)).
 
923
rewrite (canonical_sum_scalar3_ok a v y).
 
924
rewrite (ics_aux_ok (interp_m a v) c).
 
925
rewrite (interp_m_ok a v).
 
926
rewrite (H y).
 
927
setoid_replace (Amult a (Amult (interp_vl v) (interp_setcs y))) with
 
928
 (Amult (Amult a (interp_vl v)) (interp_setcs y));
 
929
 [ idtac | trivial ].
 
930
setoid_replace
 
931
 (Amult (Aplus (Amult a (interp_vl v)) (interp_setcs c)) (interp_setcs y))
 
932
 with
 
933
 (Aplus (Amult (Amult a (interp_vl v)) (interp_setcs y))
 
934
    (Amult (interp_setcs c) (interp_setcs y)));
 
935
 [ idtac | trivial ].
 
936
trivial.
 
937
 
 
938
rewrite
 
939
 (canonical_sum_merge_ok (canonical_sum_scalar2 v y) (canonical_sum_prod c y))
 
940
 .
 
941
rewrite (canonical_sum_scalar2_ok v y).
 
942
rewrite (ics_aux_ok (interp_vl v) c).
 
943
rewrite (H y).
 
944
trivial.
 
945
Qed.
 
946
 
 
947
Theorem setspolynomial_normalize_ok :
 
948
 forall p:setspolynomial,
 
949
   Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p).
 
950
Proof.
 
951
simple induction p; simpl in |- *; intros; trivial.
 
952
rewrite
 
953
 (canonical_sum_merge_ok (setspolynomial_normalize s)
 
954
    (setspolynomial_normalize s0)).
 
955
rewrite H; rewrite H0; trivial.
 
956
 
 
957
rewrite
 
958
 (canonical_sum_prod_ok (setspolynomial_normalize s)
 
959
    (setspolynomial_normalize s0)).
 
960
rewrite H; rewrite H0; trivial.
 
961
Qed.
 
962
 
 
963
Lemma canonical_sum_simplify_ok :
 
964
 forall s:canonical_sum,
 
965
   Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s).
 
966
Proof.
 
967
simple induction s; simpl in |- *; intros.
 
968
trivial.
 
969
 
 
970
generalize (SSR_eq_prop T a Azero).
 
971
elim (Aeq a Azero).
 
972
simpl in |- *.
 
973
intros.
 
974
rewrite (ics_aux_ok (interp_m a v) c).
 
975
rewrite (interp_m_ok a v).
 
976
rewrite (H0 I).
 
977
setoid_replace (Amult Azero (interp_vl v)) with Azero;
 
978
 [ idtac | trivial ].
 
979
rewrite H.
 
980
trivial.
 
981
 
 
982
intros; simpl in |- *.
 
983
generalize (SSR_eq_prop T a Aone).
 
984
elim (Aeq a Aone).
 
985
intros.
 
986
rewrite (ics_aux_ok (interp_m a v) c).
 
987
rewrite (interp_m_ok a v).
 
988
rewrite (H1 I).
 
989
simpl in |- *.
 
990
rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
 
991
rewrite H.
 
992
auto.
 
993
 
 
994
simpl in |- *.
 
995
intros.
 
996
rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)).
 
997
rewrite (ics_aux_ok (interp_m a v) c).
 
998
rewrite H; trivial.
 
999
 
 
1000
rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
 
1001
rewrite H.
 
1002
auto.
 
1003
Qed.
 
1004
 
 
1005
Theorem setspolynomial_simplify_ok :
 
1006
 forall p:setspolynomial,
 
1007
   Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p).
 
1008
Proof.
 
1009
intro.
 
1010
unfold setspolynomial_simplify in |- *.
 
1011
rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)).
 
1012
exact (setspolynomial_normalize_ok p).
 
1013
Qed.
 
1014
 
 
1015
End semi_setoid_rings.
 
1016
 
 
1017
Implicit Arguments Cons_varlist.
 
1018
Implicit Arguments Cons_monom.
 
1019
Implicit Arguments SetSPconst.
 
1020
Implicit Arguments SetSPplus.
 
1021
Implicit Arguments SetSPmult.
 
1022
 
 
1023
 
 
1024
 
 
1025
Section setoid_rings.
 
1026
 
 
1027
Set Implicit Arguments.
 
1028
 
 
1029
Variable vm : varmap A.
 
1030
Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq.
 
1031
 
 
1032
Hint Resolve (STh_plus_comm T).
 
1033
Hint Resolve (STh_plus_assoc T).
 
1034
Hint Resolve (STh_plus_assoc2 S T).
 
1035
Hint Resolve (STh_mult_comm T).
 
1036
Hint Resolve (STh_mult_assoc T).
 
1037
Hint Resolve (STh_mult_assoc2 S T).
 
1038
Hint Resolve (STh_plus_zero_left T).
 
1039
Hint Resolve (STh_plus_zero_left2 S T).
 
1040
Hint Resolve (STh_mult_one_left T).
 
1041
Hint Resolve (STh_mult_one_left2 S T).
 
1042
Hint Resolve (STh_mult_zero_left S plus_morph mult_morph T).
 
1043
Hint Resolve (STh_mult_zero_left2 S plus_morph mult_morph T).
 
1044
Hint Resolve (STh_distr_left T).
 
1045
Hint Resolve (STh_distr_left2 S T).
 
1046
Hint Resolve (STh_plus_reg_left S plus_morph T).
 
1047
Hint Resolve (STh_plus_permute S plus_morph T).
 
1048
Hint Resolve (STh_mult_permute S mult_morph T).
 
1049
Hint Resolve (STh_distr_right S plus_morph T).
 
1050
Hint Resolve (STh_distr_right2 S plus_morph T).
 
1051
Hint Resolve (STh_mult_zero_right S plus_morph mult_morph T).
 
1052
Hint Resolve (STh_mult_zero_right2 S plus_morph mult_morph T).
 
1053
Hint Resolve (STh_plus_zero_right S T).
 
1054
Hint Resolve (STh_plus_zero_right2 S T).
 
1055
Hint Resolve (STh_mult_one_right S T).
 
1056
Hint Resolve (STh_mult_one_right2 S T).
 
1057
Hint Resolve (STh_plus_reg_right S plus_morph T).
 
1058
Hint Resolve refl_equal sym_equal trans_equal.
 
1059
(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
 
1060
Hint Immediate T.
 
1061
 
 
1062
 
 
1063
(*** Definitions *)
 
1064
 
 
1065
Inductive setpolynomial : Type :=
 
1066
  | SetPvar : index -> setpolynomial
 
1067
  | SetPconst : A -> setpolynomial
 
1068
  | SetPplus : setpolynomial -> setpolynomial -> setpolynomial
 
1069
  | SetPmult : setpolynomial -> setpolynomial -> setpolynomial
 
1070
  | SetPopp : setpolynomial -> setpolynomial.
 
1071
 
 
1072
Fixpoint setpolynomial_normalize (x:setpolynomial) : canonical_sum :=
 
1073
  match x with
 
1074
  | SetPplus l r =>
 
1075
      canonical_sum_merge (setpolynomial_normalize l)
 
1076
        (setpolynomial_normalize r)
 
1077
  | SetPmult l r =>
 
1078
      canonical_sum_prod (setpolynomial_normalize l)
 
1079
        (setpolynomial_normalize r)
 
1080
  | SetPconst c => Cons_monom c Nil_var Nil_monom
 
1081
  | SetPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom
 
1082
  | SetPopp p =>
 
1083
      canonical_sum_scalar3 (Aopp Aone) Nil_var (setpolynomial_normalize p)
 
1084
  end.
 
1085
 
 
1086
Definition setpolynomial_simplify (x:setpolynomial) :=
 
1087
  canonical_sum_simplify (setpolynomial_normalize x).
 
1088
 
 
1089
Fixpoint setspolynomial_of (x:setpolynomial) : setspolynomial :=
 
1090
  match x with
 
1091
  | SetPplus l r => SetSPplus (setspolynomial_of l) (setspolynomial_of r)
 
1092
  | SetPmult l r => SetSPmult (setspolynomial_of l) (setspolynomial_of r)
 
1093
  | SetPconst c => SetSPconst c
 
1094
  | SetPvar i => SetSPvar i
 
1095
  | SetPopp p => SetSPmult (SetSPconst (Aopp Aone)) (setspolynomial_of p)
 
1096
  end.
 
1097
 
 
1098
(*** Interpretation *)
 
1099
 
 
1100
Fixpoint interp_setp (p:setpolynomial) : A :=
 
1101
  match p with
 
1102
  | SetPconst c => c
 
1103
  | SetPvar i => varmap_find Azero i vm
 
1104
  | SetPplus p1 p2 => Aplus (interp_setp p1) (interp_setp p2)
 
1105
  | SetPmult p1 p2 => Amult (interp_setp p1) (interp_setp p2)
 
1106
  | SetPopp p1 => Aopp (interp_setp p1)
 
1107
  end.
 
1108
 
 
1109
(*** Properties *)
 
1110
 
 
1111
Unset Implicit Arguments.
 
1112
 
 
1113
Lemma setspolynomial_of_ok :
 
1114
 forall p:setpolynomial,
 
1115
   Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p)).
 
1116
simple induction p; trivial; simpl in |- *; intros.
 
1117
rewrite H; rewrite H0; trivial.
 
1118
rewrite H; rewrite H0; trivial.
 
1119
rewrite H.
 
1120
rewrite
 
1121
 (STh_opp_mult_left2 S plus_morph mult_morph T Aone
 
1122
    (interp_setsp vm (setspolynomial_of s))).
 
1123
rewrite (STh_mult_one_left T (interp_setsp vm (setspolynomial_of s))).
 
1124
trivial.
 
1125
Qed.
 
1126
 
 
1127
Theorem setpolynomial_normalize_ok :
 
1128
 forall p:setpolynomial,
 
1129
   setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p).
 
1130
simple induction p; trivial; simpl in |- *; intros.
 
1131
rewrite H; rewrite H0; reflexivity.
 
1132
rewrite H; rewrite H0; reflexivity.
 
1133
rewrite H; simpl in |- *.
 
1134
elim
 
1135
 (canonical_sum_scalar3 (Aopp Aone) Nil_var
 
1136
    (setspolynomial_normalize (setspolynomial_of s)));
 
1137
 [ reflexivity
 
1138
 | simpl in |- *; intros; rewrite H0; reflexivity
 
1139
 | simpl in |- *; intros; rewrite H0; reflexivity ].
 
1140
Qed.
 
1141
 
 
1142
Theorem setpolynomial_simplify_ok :
 
1143
 forall p:setpolynomial,
 
1144
   Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p).
 
1145
intro.
 
1146
unfold setpolynomial_simplify in |- *.
 
1147
rewrite (setspolynomial_of_ok p).
 
1148
rewrite setpolynomial_normalize_ok.
 
1149
rewrite
 
1150
 (canonical_sum_simplify_ok vm
 
1151
    (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq
 
1152
       plus_morph mult_morph T)
 
1153
    (setspolynomial_normalize (setspolynomial_of p)))
 
1154
 .
 
1155
rewrite
 
1156
 (setspolynomial_normalize_ok vm
 
1157
    (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq
 
1158
       plus_morph mult_morph T) (setspolynomial_of p))
 
1159
 .
 
1160
trivial.
 
1161
Qed.
 
1162
 
 
1163
End setoid_rings.
 
1164
 
 
1165
End setoid.