← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/micromega/EnvRing.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/micromega/EnvRing.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
(* F. Besson: to evaluate polynomials, the original code is using a list.
 
9
   For big polynomials, this is inefficient -- linear access.
 
10
   I have modified the code to use binary trees -- logarithmic access.  *)
 
11
 
 
12
 
 
13
Set Implicit Arguments.
 
14
Require Import Setoid.
 
15
Require Import BinList.
 
16
Require Import Env.
 
17
Require Import BinPos.
 
18
Require Import BinNat.
 
19
Require Import BinInt.
 
20
Require Export Ring_theory.
 
21
 
 
22
Open Local Scope positive_scope.
 
23
Import RingSyntax.
 
24
 
 
25
Section MakeRingPol.
 
26
 
 
27
 (* Ring elements *)
 
28
 Variable R:Type.
 
29
 Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
 
30
 Variable req : R -> R -> Prop.
 
31
 
 
32
 (* Ring properties *)
 
33
 Variable Rsth : Setoid_Theory R req.
 
34
 Variable Reqe : ring_eq_ext radd rmul ropp req.
 
35
 Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
 
36
 
 
37
 (* Coefficients *)
 
38
 Variable C: Type.
 
39
 Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
 
40
 Variable ceqb : C->C->bool.
 
41
 Variable phi : C -> R.
 
42
 Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
 
43
                                cO cI cadd cmul csub copp ceqb phi.
 
44
 
 
45
  (* Power coefficients *)
 
46
 Variable Cpow : Set.
 
47
 Variable Cp_phi : N -> Cpow.
 
48
 Variable rpow : R -> Cpow -> R.
 
49
 Variable pow_th : power_theory rI rmul req Cp_phi rpow.
 
50
 
 
51
 
 
52
 (* R notations *)
 
53
 Notation "0" := rO. Notation "1" := rI.
 
54
 Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
 
55
 Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
 
56
 Notation "x == y" := (req x y).
 
57
 
 
58
 (* C notations *)              
 
59
 Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y).
 
60
 Notation "x -! y " := (csub x y). Notation "-! x" := (copp x).
 
61
 Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
 
62
 
 
63
 (* Usefull tactics *)          
 
64
  Add Setoid R req Rsth as R_set1.
 
65
 Ltac rrefl := gen_reflexivity Rsth.
 
66
  Add Morphism radd : radd_ext.  exact (Radd_ext Reqe). Qed.
 
67
  Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
 
68
  Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
 
69
  Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
 
70
 Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
 
71
 Ltac add_push := gen_add_push radd Rsth Reqe ARth.
 
72
 Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.
 
73
 
 
74
 (* Definition of multivariable polynomials with coefficients in C :
 
75
    Type [Pol] represents [X1 ... Xn].
 
76
    The representation is Horner's where a [n] variable polynomial
 
77
    (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients
 
78
    are polynomials with [n-1] variables (C[X2..Xn]).
 
79
    There are several optimisations to make the repr compacter:
 
80
    - [Pc c] is the constant polynomial of value c
 
81
       == c*X1^0*..*Xn^0
 
82
    - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables.
 
83
        variable indices are shifted of j in Q.
 
84
       == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn}
 
85
    - [PX P i Q] is an optimised Horner form of P*X^i + Q
 
86
        with P not the null polynomial
 
87
       == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn}
 
88
 
 
89
    In addition:
 
90
    - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden
 
91
      since they can be represented by the simpler form (PX P (i+j) Q)
 
92
    - (Pinj i (Pinj j P)) is (Pinj (i+j) P)
 
93
    - (Pinj i (Pc c)) is (Pc c)
 
94
 *)
 
95
 
 
96
 Inductive Pol : Type :=
 
97
  | Pc : C -> Pol
 
98
  | Pinj : positive -> Pol -> Pol
 
99
  | PX : Pol -> positive -> Pol -> Pol.
 
100
 
 
101
 Definition P0 := Pc cO.
 
102
 Definition P1 := Pc cI.
 
103
 
 
104
 Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
 
105
  match P, P' with
 
106
  | Pc c, Pc c' => c ?=! c'
 
107
  | Pinj j Q, Pinj j' Q' =>
 
108
    match Pcompare j j' Eq with
 
109
    | Eq => Peq Q Q'
 
110
    | _ => false
 
111
    end
 
112
  | PX P i Q, PX P' i' Q' =>
 
113
    match Pcompare i i' Eq with
 
114
    | Eq => if Peq P P' then Peq Q Q' else false
 
115
    | _ => false
 
116
    end
 
117
  | _, _ => false
 
118
  end.
 
119
 
 
120
 Notation " P ?== P' " := (Peq P P').
 
121
 
 
122
 Definition mkPinj j P :=
 
123
  match P with
 
124
  | Pc _ => P
 
125
  | Pinj j' Q => Pinj ((j + j'):positive) Q
 
126
  | _ => Pinj j P
 
127
  end.
 
128
 
 
129
 Definition mkPinj_pred j P:=
 
130
  match j with
 
131
  | xH => P
 
132
  | xO j => Pinj (Pdouble_minus_one j) P
 
133
  | xI j => Pinj (xO j) P
 
134
  end.
 
135
 
 
136
 Definition mkPX P i Q :=
 
137
  match P with
 
138
  | Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q
 
139
  | Pinj _ _ => PX P i Q
 
140
  | PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q
 
141
  end.
 
142
 
 
143
 Definition mkXi i := PX P1 i P0.
 
144
 
 
145
 Definition mkX := mkXi 1.
 
146
 
 
147
 (** Opposite of addition *)
 
148
 
 
149
 Fixpoint Popp (P:Pol) : Pol :=
 
150
  match P with
 
151
  | Pc c => Pc (-! c)
 
152
  | Pinj j Q => Pinj j (Popp Q)
 
153
  | PX P i Q => PX (Popp P) i (Popp Q)
 
154
  end.
 
155
 
 
156
 Notation "-- P" := (Popp P).
 
157
 
 
158
 (** Addition et subtraction *)
 
159
 
 
160
 Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol :=
 
161
  match P with
 
162
  | Pc c1 => Pc (c1 +! c)
 
163
  | Pinj j Q => Pinj j (PaddC Q c)
 
164
  | PX P i Q => PX P i (PaddC Q c)
 
165
  end.
 
166
 
 
167
 Fixpoint PsubC (P:Pol) (c:C) {struct P} : Pol :=
 
168
  match P with
 
169
  | Pc c1 => Pc (c1 -! c)
 
170
  | Pinj j Q => Pinj j (PsubC Q c)
 
171
  | PX P i Q => PX P i (PsubC Q c)
 
172
  end.
 
173
 
 
174
 Section PopI.
 
175
 
 
176
  Variable Pop : Pol -> Pol -> Pol.
 
177
  Variable Q : Pol.
 
178
 
 
179
  Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol :=
 
180
   match P with
 
181
   | Pc c => mkPinj j (PaddC Q c)
 
182
   | Pinj j' Q' =>
 
183
     match ZPminus j' j with
 
184
     | Zpos k =>  mkPinj j (Pop (Pinj k Q') Q)
 
185
     | Z0 => mkPinj j (Pop Q' Q)
 
186
     | Zneg k => mkPinj j' (PaddI k Q')
 
187
     end
 
188
   | PX P i Q' =>
 
189
     match j with
 
190
     | xH => PX P i (Pop Q' Q)
 
191
     | xO j => PX P i (PaddI (Pdouble_minus_one j) Q')
 
192
     | xI j => PX P i (PaddI (xO j) Q')
 
193
     end
 
194
   end.
 
195
 
 
196
  Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol :=
 
197
   match P with
 
198
   | Pc c => mkPinj j (PaddC (--Q) c)
 
199
   | Pinj j' Q' =>
 
200
     match ZPminus j' j with
 
201
     | Zpos k =>  mkPinj j (Pop (Pinj k Q') Q)
 
202
     | Z0 => mkPinj j (Pop Q' Q)
 
203
     | Zneg k => mkPinj j' (PsubI k Q')
 
204
     end
 
205
   | PX P i Q' =>
 
206
     match j with
 
207
     | xH => PX P i (Pop Q' Q)
 
208
     | xO j => PX P i (PsubI (Pdouble_minus_one j) Q')
 
209
     | xI j => PX P i (PsubI (xO j) Q')
 
210
     end
 
211
   end.
 
212
 
 
213
 Variable P' : Pol.
 
214
 
 
215
 Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol :=
 
216
  match P with
 
217
  | Pc c => PX P' i' P
 
218
  | Pinj j Q' =>
 
219
    match j with
 
220
    | xH =>  PX P' i' Q'
 
221
    | xO j => PX P' i' (Pinj (Pdouble_minus_one j) Q')
 
222
    | xI j => PX P' i' (Pinj (xO j) Q')
 
223
    end
 
224
  | PX P i Q' =>
 
225
    match ZPminus i i' with
 
226
    | Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
 
227
    | Z0 => mkPX (Pop P P') i Q'
 
228
    | Zneg k => mkPX (PaddX k P) i Q'
 
229
    end
 
230
  end.
 
231
 
 
232
 Fixpoint PsubX (i':positive) (P:Pol) {struct P} : Pol :=
 
233
  match P with
 
234
  | Pc c => PX (--P') i' P
 
235
  | Pinj j Q' =>
 
236
    match j with
 
237
    | xH =>  PX (--P') i' Q'
 
238
    | xO j => PX (--P') i' (Pinj (Pdouble_minus_one j) Q')
 
239
    | xI j => PX (--P') i' (Pinj (xO j) Q')
 
240
    end
 
241
  | PX P i Q' =>
 
242
    match ZPminus i i' with
 
243
    | Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
 
244
    | Z0 => mkPX (Pop P P') i Q'
 
245
    | Zneg k => mkPX (PsubX k P) i Q'
 
246
    end
 
247
  end.
 
248
 
 
249
 
 
250
 End PopI.
 
251
 
 
252
 Fixpoint Padd (P P': Pol) {struct P'} : Pol :=
 
253
  match P' with
 
254
  | Pc c' => PaddC P c'
 
255
  | Pinj j' Q' => PaddI Padd Q' j' P
 
256
  | PX P' i' Q' =>
 
257
    match P with
 
258
    | Pc c => PX P' i' (PaddC Q' c)
 
259
    | Pinj j Q =>
 
260
      match j with
 
261
      | xH => PX P' i' (Padd Q Q')
 
262
      | xO j => PX P' i' (Padd (Pinj (Pdouble_minus_one j) Q) Q')
 
263
      | xI j => PX P' i' (Padd (Pinj (xO j) Q) Q')
 
264
      end
 
265
    | PX P i Q =>
 
266
      match ZPminus i i' with
 
267
      | Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q')
 
268
      | Z0 => mkPX (Padd P P') i (Padd Q Q')
 
269
      | Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q')
 
270
      end
 
271
    end
 
272
  end.
 
273
 Notation "P ++ P'" := (Padd P P').
 
274
 
 
275
 Fixpoint Psub (P P': Pol) {struct P'} : Pol :=
 
276
  match P' with
 
277
  | Pc c' => PsubC P c'
 
278
  | Pinj j' Q' => PsubI Psub Q' j' P
 
279
  | PX P' i' Q' =>
 
280
    match P with
 
281
    | Pc c => PX (--P') i' (*(--(PsubC Q' c))*) (PaddC (--Q') c)
 
282
    | Pinj j Q =>
 
283
      match j with
 
284
      | xH => PX (--P') i' (Psub Q Q')
 
285
      | xO j => PX (--P') i' (Psub (Pinj (Pdouble_minus_one j) Q) Q')
 
286
      | xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q')
 
287
      end
 
288
    | PX P i Q =>
 
289
      match ZPminus i i' with
 
290
      | Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q')
 
291
      | Z0 => mkPX (Psub P P') i (Psub Q Q')
 
292
      | Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q')
 
293
      end
 
294
    end
 
295
  end.
 
296
 Notation "P -- P'" := (Psub P P').
 
297
 
 
298
 (** Multiplication *)
 
299
 
 
300
 Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol :=
 
301
  match P with
 
302
  | Pc c' => Pc (c' *! c)
 
303
  | Pinj j Q => mkPinj j (PmulC_aux Q c)
 
304
  | PX P i Q => mkPX (PmulC_aux P c) i (PmulC_aux Q c)
 
305
  end.
 
306
 
 
307
 Definition PmulC P c :=
 
308
  if c ?=! cO then P0 else
 
309
  if c ?=! cI then P else PmulC_aux P c.
 
310
 
 
311
 Section PmulI.
 
312
  Variable Pmul : Pol -> Pol -> Pol.
 
313
  Variable Q : Pol.
 
314
  Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol :=
 
315
   match P with
 
316
   | Pc c => mkPinj j (PmulC Q c)
 
317
   | Pinj j' Q' =>
 
318
     match ZPminus j' j with
 
319
     | Zpos k => mkPinj j (Pmul (Pinj k Q') Q)
 
320
     | Z0 => mkPinj j (Pmul Q' Q)
 
321
     | Zneg k => mkPinj j' (PmulI k Q')
 
322
     end
 
323
   | PX P' i' Q' =>
 
324
     match j with
 
325
     | xH => mkPX (PmulI xH P') i' (Pmul Q' Q)
 
326
     | xO j' => mkPX (PmulI j P') i' (PmulI (Pdouble_minus_one j') Q')
 
327
     | xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q')
 
328
     end
 
329
   end.
 
330
 
 
331
 End PmulI.
 
332
(* A symmetric version of the multiplication *)
 
333
 
 
334
 Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol :=
 
335
   match P'' with
 
336
   | Pc c => PmulC P c
 
337
   | Pinj j' Q' => PmulI Pmul Q' j' P
 
338
   | PX P' i' Q' =>
 
339
     match P with
 
340
     | Pc c => PmulC P'' c
 
341
     | Pinj j Q =>
 
342
       let QQ' :=
 
343
         match j with
 
344
         | xH => Pmul Q Q'
 
345
         | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q'
 
346
         | xI j => Pmul (Pinj (xO j) Q) Q'
 
347
         end in
 
348
       mkPX (Pmul P P') i' QQ'
 
349
     | PX P i Q=>
 
350
       let QQ' := Pmul Q Q' in
 
351
       let PQ' := PmulI Pmul Q' xH P in
 
352
       let QP' := Pmul (mkPinj xH Q) P' in
 
353
       let PP' := Pmul P P' in
 
354
       (mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ'
 
355
     end
 
356
  end.
 
357
 
 
358
(* Non symmetric *)
 
359
(*
 
360
 Fixpoint Pmul_aux (P P' : Pol) {struct P'} : Pol :=
 
361
  match P' with
 
362
  | Pc c' => PmulC P c'
 
363
  | Pinj j' Q' => PmulI Pmul_aux Q' j' P
 
364
  | PX P' i' Q' =>
 
365
     (mkPX (Pmul_aux P P') i' P0) ++ (PmulI Pmul_aux Q' xH P)
 
366
  end.
 
367
 
 
368
 Definition Pmul P P' :=
 
369
  match P with
 
370
  | Pc c => PmulC P' c
 
371
  | Pinj j Q => PmulI Pmul_aux Q j P'
 
372
  | PX P i Q =>
 
373
    (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P')
 
374
  end.
 
375
*)
 
376
 Notation "P ** P'" := (Pmul P P').
 
377
 
 
378
 Fixpoint Psquare (P:Pol) : Pol :=
 
379
   match P with
 
380
   | Pc c => Pc (c *! c)
 
381
   | Pinj j Q => Pinj j (Psquare Q)
 
382
   | PX P i Q =>
 
383
     let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in
 
384
     let Q2 := Psquare Q in
 
385
     let P2 := Psquare P in
 
386
     mkPX (mkPX P2 i P0 ++ twoPQ) i Q2
 
387
   end.
 
388
 
 
389
 (** Monomial **)
 
390
 
 
391
  Inductive Mon: Set :=
 
392
    mon0: Mon
 
393
  | zmon: positive -> Mon -> Mon
 
394
  | vmon: positive -> Mon -> Mon.
 
395
 
 
396
 Fixpoint Mphi(l:Env R) (M: Mon) {struct M} : R :=
 
397
  match M with
 
398
     mon0 => rI
 
399
  | zmon j M1  => Mphi (jump j l) M1
 
400
  | vmon i M1 =>
 
401
     let x := hd 0 l in
 
402
     let xi := pow_pos rmul x i in
 
403
    (Mphi (tail l) M1) * xi
 
404
  end.
 
405
 
 
406
 Definition mkZmon j M :=
 
407
   match M with mon0 => mon0 | _ => zmon j M end.
 
408
 
 
409
 Definition zmon_pred j M :=
 
410
   match j with xH => M | _ => mkZmon (Ppred j) M end.
 
411
 
 
412
 Definition mkVmon i M :=
 
413
   match M with
 
414
   | mon0 => vmon i mon0
 
415
   | zmon j m => vmon i (zmon_pred j m)
 
416
   | vmon i' m => vmon (i+i') m
 
417
   end.
 
418
 
 
419
 Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol :=
 
420
   match P, M with
 
421
        _, mon0 => (Pc cO, P)
 
422
   | Pc _, _    => (P, Pc cO)
 
423
   | Pinj j1 P1, zmon j2 M1 =>
 
424
      match (j1 ?= j2) Eq with
 
425
        Eq => let (R,S) := MFactor P1 M1 in
 
426
                 (mkPinj j1 R, mkPinj j1 S)
 
427
      | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in
 
428
                 (mkPinj j1 R, mkPinj j1 S)
 
429
      | Gt => (P, Pc cO)
 
430
      end
 
431
  | Pinj _ _, vmon _ _ => (P, Pc cO)
 
432
  | PX P1 i Q1, zmon j M1 =>
 
433
             let M2 := zmon_pred j M1 in
 
434
             let (R1, S1) := MFactor P1 M in
 
435
             let (R2, S2) := MFactor Q1 M2 in
 
436
               (mkPX R1 i R2, mkPX S1 i S2)
 
437
  | PX P1 i Q1, vmon j M1 =>
 
438
      match (i ?= j) Eq with
 
439
        Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
 
440
                 (mkPX R1 i Q1, S1)
 
441
      | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in
 
442
                 (mkPX R1 i Q1, S1)
 
443
      | Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
 
444
                 (mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO))
 
445
      end
 
446
   end.
 
447
 
 
448
  Definition POneSubst (P1: Pol) (M1: Mon) (P2: Pol): option Pol :=
 
449
    let (Q1,R1) := MFactor P1 M1 in
 
450
    match R1 with
 
451
     (Pc c) => if c ?=! cO then None
 
452
               else Some (Padd Q1 (Pmul P2 R1))
 
453
    | _ => Some (Padd Q1 (Pmul P2 R1))
 
454
    end.
 
455
 
 
456
  Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
 
457
    match POneSubst P1 M1 P2 with
 
458
     Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end
 
459
    | _ => P1
 
460
    end.
 
461
 
 
462
  Definition PNSubst (P1: Pol) (M1: Mon) (P2: Pol) (n: nat): option Pol :=
 
463
    match POneSubst P1 M1 P2 with
 
464
     Some P3 => match n with S n1 => Some (PNSubst1 P3 M1 P2 n1) | _ => None end
 
465
    | _ => None
 
466
    end.
 
467
 
 
468
  Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}:
 
469
     Pol :=
 
470
    match LM1 with
 
471
     cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n
 
472
    | _ => P1
 
473
    end.
 
474
 
 
475
  Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol :=
 
476
    match LM1 with
 
477
     cons (M1,P2) LM2 =>
 
478
      match PNSubst P1 M1 P2 n with
 
479
        Some P3 => Some (PSubstL1 P3 LM2 n)
 
480
     |  None => PSubstL P1 LM2 n
 
481
     end
 
482
    | _ => None
 
483
    end.
 
484
 
 
485
  Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol :=
 
486
    match PSubstL P1 LM1 n with
 
487
     Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end
 
488
    | _ => P1
 
489
    end.
 
490
 
 
491
 (** Evaluation of a polynomial towards R *)
 
492
 
 
493
 Fixpoint Pphi(l:Env R) (P:Pol) {struct P} : R :=
 
494
  match P with
 
495
  | Pc c => [c]
 
496
  | Pinj j Q => Pphi (jump j l) Q
 
497
  | PX P i Q =>
 
498
     let x := hd 0 l in
 
499
     let xi := pow_pos rmul x i in
 
500
    (Pphi l P) * xi + (Pphi (tail l) Q)
 
501
  end.
 
502
 
 
503
 Reserved Notation "P @ l " (at level 10, no associativity).
 
504
 Notation "P @ l " := (Pphi l P).
 
505
 (** Proofs *)
 
506
 Lemma ZPminus_spec : forall x y,
 
507
  match ZPminus x y with
 
508
  | Z0 => x = y
 
509
  | Zpos k => x = (y + k)%positive
 
510
  | Zneg k => y = (x + k)%positive
 
511
  end.
 
512
 Proof.
 
513
  induction x;destruct y.
 
514
  replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial.
 
515
  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
 
516
  replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial.
 
517
  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;trivial.
 
518
  apply Pplus_xI_double_minus_one.
 
519
  simpl;trivial.
 
520
  replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));trivial.
 
521
  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;trivial.
 
522
  apply Pplus_xI_double_minus_one.
 
523
  replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial.
 
524
  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
 
525
  replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial.
 
526
  rewrite <- Pplus_one_succ_l.
 
527
  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
 
528
  replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial.
 
529
  replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial.
 
530
  rewrite <- Pplus_one_succ_l.
 
531
  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
 
532
  simpl;trivial.
 
533
 Qed.
 
534
 
 
535
 Lemma Peq_ok : forall P P',
 
536
    (P ?== P') = true -> forall l, P@l == P'@ l.
 
537
 Proof.
 
538
  induction P;destruct P';simpl;intros;try discriminate;trivial.
 
539
  apply (morph_eq CRmorph);trivial.
 
540
  assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
 
541
   try discriminate H.
 
542
  rewrite (IHP P' H); rewrite H1;trivial;rrefl.
 
543
  assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
 
544
   try discriminate H.
 
545
  rewrite H1;trivial. clear H1.
 
546
  assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2);
 
547
   destruct (P2 ?== P'1);[destruct (P3 ?== P'2); [idtac|discriminate H]
 
548
                         |discriminate H].
 
549
  rewrite (H1 H);rewrite (H2 H);rrefl.
 
550
 Qed.
 
551
 
 
552
 Lemma Pphi0 : forall l, P0@l == 0.
 
553
 Proof.
 
554
  intros;simpl;apply (morph0 CRmorph).
 
555
 Qed.
 
556
 
 
557
Lemma env_morph : forall p e1 e2, (forall x, e1 x = e2 x) -> 
 
558
 p @ e1 = p @ e2.
 
559
Proof.
 
560
  induction p ; simpl.
 
561
  reflexivity.
 
562
  intros.
 
563
  apply IHp.
 
564
  intros.
 
565
  unfold jump.
 
566
  apply H.
 
567
  intros.
 
568
  rewrite (IHp1 e1 e2) ; auto.
 
569
  rewrite (IHp2 (tail e1) (tail e2)) ; auto.
 
570
  unfold hd. unfold nth.  rewrite H.  reflexivity.
 
571
  unfold tail.  unfold jump. intros ; apply H.
 
572
Qed.
 
573
 
 
574
Lemma Pjump_Pplus : forall P i j l, P @ (jump (i + j) l ) = P @ (jump j (jump i l)).
 
575
Proof.
 
576
  intros. apply env_morph. intros. rewrite <- jump_Pplus.
 
577
  rewrite Pplus_comm.
 
578
  reflexivity.
 
579
Qed.
 
580
 
 
581
Lemma Pjump_xO_tail : forall P p l, 
 
582
  P @ (jump (xO p) (tail l)) = P @ (jump (xI p) l).
 
583
Proof.
 
584
  intros.
 
585
  apply env_morph.
 
586
  intros.
 
587
  rewrite (@jump_simpl R (xI p)).
 
588
  rewrite (@jump_simpl R (xO p)).
 
589
  reflexivity.
 
590
Qed.
 
591
 
 
592
Lemma Pjump_Pdouble_minus_one : forall P p l,
 
593
  P @ (jump (Pdouble_minus_one p) (tail l)) = P @ (jump (xO p) l).
 
594
Proof.
 
595
  intros.
 
596
  apply env_morph.
 
597
  intros.
 
598
  rewrite jump_Pdouble_minus_one.
 
599
  rewrite (@jump_simpl R (xO p)).
 
600
  reflexivity.
 
601
Qed.
 
602
 
 
603
 
 
604
 
 
605
 Lemma Pphi1 : forall l,  P1@l == 1.
 
606
 Proof.
 
607
  intros;simpl;apply (morph1 CRmorph).
 
608
 Qed.
 
609
 
 
610
 Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l).
 
611
 Proof.
 
612
  intros j l p;destruct p;simpl;rsimpl.
 
613
  rewrite Pjump_Pplus.
 
614
  reflexivity.
 
615
 Qed.
 
616
 
 
617
 Let pow_pos_Pplus :=
 
618
    pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).
 
619
 
 
620
 Lemma mkPX_ok : forall l P i Q,
 
621
  (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l).
 
622
 Proof.
 
623
  intros l P i Q;unfold mkPX.
 
624
  destruct P;try (simpl;rrefl).
 
625
  assert (H := morph_eq CRmorph c cO);destruct (c ?=! cO);simpl;try rrefl.
 
626
  rewrite (H (refl_equal true));rewrite (morph0 CRmorph).
 
627
  rewrite mkPinj_ok;rsimpl;simpl;rrefl.
 
628
  assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl.
 
629
  rewrite (H (refl_equal true));trivial.
 
630
  rewrite Pphi0.  rewrite pow_pos_Pplus;rsimpl.
 
631
 Qed.
 
632
 
 
633
 
 
634
 Ltac Esimpl :=
 
635
  repeat (progress (
 
636
   match goal with
 
637
   | |- context [P0@?l] => rewrite (Pphi0 l)
 
638
   | |- context [P1@?l] => rewrite (Pphi1 l)
 
639
   | |- context [(mkPinj ?j ?P)@?l] => rewrite (mkPinj_ok j l P)
 
640
   | |- context [(mkPX ?P ?i ?Q)@?l] => rewrite (mkPX_ok l P i Q)
 
641
   | |- context [[cO]] => rewrite (morph0 CRmorph)
 
642
   | |- context [[cI]] => rewrite (morph1 CRmorph)
 
643
   | |- context [[?x +! ?y]] => rewrite ((morph_add CRmorph) x y)
 
644
   | |- context [[?x *! ?y]] => rewrite ((morph_mul CRmorph) x y)
 
645
   | |- context [[?x -! ?y]] => rewrite ((morph_sub CRmorph) x y)
 
646
   | |- context [[-! ?x]] => rewrite ((morph_opp CRmorph) x)
 
647
   end));
 
648
  rsimpl; simpl.
 
649
 
 
650
 Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c].
 
651
 Proof.
 
652
  induction P;simpl;intros;Esimpl;trivial.
 
653
  rewrite IHP2;rsimpl.
 
654
 Qed.
 
655
 
 
656
 Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c].
 
657
 Proof.
 
658
  induction P;simpl;intros.
 
659
  Esimpl.
 
660
  rewrite IHP;rsimpl.
 
661
  rewrite IHP2;rsimpl.
 
662
 Qed.
 
663
 
 
664
 Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c].
 
665
 Proof.
 
666
  induction P;simpl;intros;Esimpl;trivial.
 
667
  rewrite IHP1;rewrite IHP2;rsimpl.
 
668
  mul_push ([c]);rrefl.
 
669
 Qed.
 
670
 
 
671
 Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].
 
672
 Proof.
 
673
  intros c P l; unfold PmulC.
 
674
  assert (H:= morph_eq CRmorph c cO);destruct (c ?=! cO).
 
675
  rewrite (H (refl_equal true));Esimpl.
 
676
  assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
 
677
  rewrite (H1 (refl_equal true));Esimpl.
 
678
  apply PmulC_aux_ok.
 
679
 Qed.
 
680
 
 
681
 Lemma Popp_ok : forall P l, (--P)@l == - P@l.
 
682
 Proof.
 
683
  induction P;simpl;intros.
 
684
  Esimpl.
 
685
  apply IHP.
 
686
  rewrite IHP1;rewrite IHP2;rsimpl.
 
687
 Qed.
 
688
 
 
689
 Ltac Esimpl2 :=
 
690
  Esimpl;
 
691
  repeat (progress (
 
692
   match goal with
 
693
   | |- context [(PaddC ?P ?c)@?l] => rewrite (PaddC_ok c P l)
 
694
   | |- context [(PsubC ?P ?c)@?l] => rewrite (PsubC_ok c P l)
 
695
   | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l)
 
696
   | |- context [(--?P)@?l] => rewrite (Popp_ok P l)
 
697
   end)); Esimpl.
 
698
 
 
699
 
 
700
 
 
701
 
 
702
 Lemma Padd_ok : forall P' P l, (P ++ P')@l == P@l + P'@l.
 
703
 Proof.
 
704
  induction P';simpl;intros;Esimpl2.
 
705
  generalize P p l;clear P p l.
 
706
  induction P;simpl;intros.
 
707
  Esimpl2;apply (ARadd_comm ARth).
 
708
  assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
 
709
  rewrite H;Esimpl. rewrite IHP';rrefl.
 
710
  rewrite H;Esimpl. rewrite IHP';Esimpl.
 
711
  rewrite Pjump_Pplus. rrefl.
 
712
  rewrite H;Esimpl. rewrite IHP.
 
713
  rewrite Pjump_Pplus. rrefl.
 
714
  destruct p0;simpl.
 
715
  rewrite IHP2;simpl. rsimpl.
 
716
  rewrite Pjump_xO_tail. Esimpl.
 
717
  rewrite IHP2;simpl.
 
718
  rewrite Pjump_Pdouble_minus_one.
 
719
  rsimpl.
 
720
  rewrite IHP'.
 
721
  rsimpl.
 
722
  destruct P;simpl.
 
723
  Esimpl2;add_push [c];rrefl.
 
724
  destruct p0;simpl;Esimpl2.
 
725
  rewrite IHP'2;simpl.
 
726
  rewrite Pjump_xO_tail.
 
727
  rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
 
728
  rewrite IHP'2;simpl.
 
729
  rewrite Pjump_Pdouble_minus_one. rsimpl.
 
730
  add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
 
731
  rewrite IHP'2;rsimpl.
 
732
  unfold tail.
 
733
  add_push (P @ (jump 1 l));rrefl.
 
734
  assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
 
735
  rewrite IHP'1;rewrite IHP'2;rsimpl.
 
736
  add_push (P3 @ (tail l));rewrite H;rrefl.
 
737
  rewrite IHP'1;rewrite IHP'2;simpl;Esimpl.
 
738
  rewrite H;rewrite Pplus_comm.
 
739
  rewrite pow_pos_Pplus;rsimpl.
 
740
  add_push (P3 @ (tail l));rrefl.
 
741
  assert (forall P k l,
 
742
           (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k).
 
743
   induction P;simpl;intros;try apply (ARadd_comm ARth).
 
744
   destruct p2; simpl; try apply (ARadd_comm ARth).
 
745
   rewrite Pjump_xO_tail.
 
746
   apply (ARadd_comm ARth).   
 
747
   rewrite Pjump_Pdouble_minus_one.
 
748
   apply (ARadd_comm ARth).   
 
749
    assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2.
 
750
    rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl.
 
751
    rewrite IHP'1;simpl;Esimpl.
 
752
    rewrite H1;rewrite Pplus_comm.
 
753
    rewrite pow_pos_Pplus;simpl;Esimpl.
 
754
    add_push (P5 @ (tail l0));rrefl.
 
755
    rewrite IHP1;rewrite H1;rewrite Pplus_comm.
 
756
    rewrite pow_pos_Pplus;simpl;rsimpl.
 
757
    add_push (P5 @ (tail l0));rrefl.
 
758
  rewrite H0;rsimpl.
 
759
  add_push (P3 @ (tail l)).
 
760
  rewrite H;rewrite Pplus_comm.
 
761
  rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl.
 
762
  add_push (P3 @ (tail l));rrefl.
 
763
 Qed.
 
764
 
 
765
 Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
 
766
 Proof.
 
767
  induction P';simpl;intros;Esimpl2;trivial.
 
768
  generalize P p l;clear P p l.
 
769
  induction P;simpl;intros.
 
770
  Esimpl2;apply (ARadd_comm ARth).
 
771
  assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
 
772
  rewrite H;Esimpl. rewrite IHP';rsimpl.
 
773
  rewrite H;Esimpl. rewrite IHP';Esimpl.
 
774
  rewrite <- Pjump_Pplus;rewrite Pplus_comm;rrefl.
 
775
  rewrite H;Esimpl. rewrite IHP.
 
776
  rewrite <- Pjump_Pplus;rewrite Pplus_comm;rrefl.
 
777
  destruct p0;simpl.
 
778
  rewrite IHP2;simpl; try   rewrite Pjump_xO_tail ; rsimpl.
 
779
  rewrite IHP2;simpl.
 
780
  rewrite Pjump_Pdouble_minus_one;rsimpl.
 
781
  unfold tail ; rsimpl.
 
782
  rewrite IHP';rsimpl.
 
783
  destruct P;simpl.
 
784
  repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl.
 
785
  destruct p0;simpl;Esimpl2.
 
786
  rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial.
 
787
  rewrite Pjump_xO_tail.
 
788
  add_push (P @ ((jump (xI p0) l)));rrefl.  
 
789
  rewrite IHP'2;simpl;rewrite Pjump_Pdouble_minus_one;rsimpl.
 
790
  add_push (- (P'1 @ l * pow_pos  rmul (hd 0 l) p));rrefl.
 
791
  unfold tail.
 
792
  rewrite IHP'2;rsimpl;add_push (P @ (jump 1 l));rrefl.
 
793
  assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
 
794
  rewrite IHP'1; rewrite IHP'2;rsimpl.
 
795
  add_push (P3 @ (tail l));rewrite H;rrefl.
 
796
   rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl.
 
797
  rewrite H;rewrite Pplus_comm.
 
798
  rewrite pow_pos_Pplus;rsimpl.
 
799
  add_push (P3 @ (tail l));rrefl.
 
800
  assert (forall P k l,
 
801
           (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k).
 
802
   induction P;simpl;intros.
 
803
   rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial.
 
804
   destruct p2;simpl; rewrite Popp_ok;rsimpl.
 
805
   rewrite Pjump_xO_tail.
 
806
   apply (ARadd_comm ARth);trivial.
 
807
   rewrite Pjump_Pdouble_minus_one.
 
808
   apply (ARadd_comm ARth);trivial.
 
809
   apply (ARadd_comm ARth);trivial.
 
810
    assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl.
 
811
    rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl.
 
812
    rewrite IHP'1;rewrite H1;rewrite Pplus_comm.
 
813
    rewrite pow_pos_Pplus;simpl;Esimpl.
 
814
    add_push (P5 @ (tail l0));rrefl.
 
815
    rewrite IHP1;rewrite H1;rewrite Pplus_comm.
 
816
    rewrite pow_pos_Pplus;simpl;rsimpl.
 
817
    add_push (P5 @ (tail l0));rrefl.
 
818
  rewrite H0;rsimpl.
 
819
  rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)).
 
820
  rewrite H;rewrite Pplus_comm.
 
821
  rewrite pow_pos_Pplus;rsimpl.
 
822
 Qed.
 
823
(* Proof for the symmetric version *)
 
824
 
 
825
 Lemma PmulI_ok :
 
826
  forall P',
 
827
   (forall (P : Pol) (l : Env  R), (Pmul P P') @ l == P @ l * P' @ l) ->
 
828
   forall (P : Pol) (p : positive) (l : Env R),
 
829
    (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
 
830
 Proof.
 
831
  induction P;simpl;intros.
 
832
  Esimpl2;apply (ARmul_comm ARth).
 
833
  assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
 
834
  rewrite H1; rewrite H;rrefl.
 
835
  rewrite H1; rewrite H.
 
836
  rewrite Pjump_Pplus;simpl;rrefl.
 
837
  rewrite H1.
 
838
  rewrite Pjump_Pplus;rewrite IHP;rrefl.
 
839
  destruct p0;Esimpl2.
 
840
  rewrite IHP1;rewrite IHP2;rsimpl.
 
841
  rewrite Pjump_xO_tail.
 
842
  mul_push (pow_pos rmul (hd 0 l) p);rrefl.
 
843
  rewrite IHP1;rewrite IHP2;simpl;rsimpl.
 
844
  mul_push (pow_pos rmul (hd 0 l) p); rewrite Pjump_Pdouble_minus_one.
 
845
  rrefl.
 
846
  rewrite IHP1;simpl;rsimpl.
 
847
  mul_push (pow_pos rmul (hd 0 l) p).
 
848
  rewrite H;rrefl.
 
849
 Qed.
 
850
 
 
851
(*
 
852
 Lemma PmulI_ok :
 
853
  forall P',
 
854
   (forall (P : Pol) (l : list R), (Pmul_aux P P') @ l == P @ l * P' @ l) ->
 
855
   forall (P : Pol) (p : positive) (l : list R),
 
856
    (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l).
 
857
 Proof.
 
858
  induction P;simpl;intros.
 
859
  Esimpl2;apply (ARmul_comm ARth).
 
860
  assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
 
861
  rewrite H1; rewrite H;rrefl.
 
862
  rewrite H1; rewrite H.
 
863
  rewrite Pplus_comm.
 
864
  rewrite jump_Pplus;simpl;rrefl.
 
865
  rewrite H1;rewrite Pplus_comm.
 
866
  rewrite jump_Pplus;rewrite IHP;rrefl.
 
867
  destruct p0;Esimpl2.
 
868
  rewrite IHP1;rewrite IHP2;simpl;rsimpl.
 
869
  mul_push (pow_pos rmul (hd 0 l) p);rrefl.
 
870
  rewrite IHP1;rewrite IHP2;simpl;rsimpl.
 
871
  mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl.
 
872
  rewrite IHP1;simpl;rsimpl.
 
873
  mul_push (pow_pos rmul (hd 0 l) p).
 
874
  rewrite H;rrefl.
 
875
 Qed.
 
876
 
 
877
 Lemma Pmul_aux_ok : forall P' P l,(Pmul_aux P P')@l == P@l * P'@l.
 
878
 Proof.
 
879
  induction P';simpl;intros.
 
880
  Esimpl2;trivial.
 
881
  apply PmulI_ok;trivial.
 
882
  rewrite Padd_ok;Esimpl2.
 
883
  rewrite (PmulI_ok P'2 IHP'2). rewrite IHP'1. rrefl.
 
884
 Qed.
 
885
*)
 
886
 
 
887
(* Proof for the symmetric version *)
 
888
 Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
 
889
 Proof.
 
890
  intros P P';generalize P;clear P;induction P';simpl;intros.
 
891
  apply PmulC_ok. apply PmulI_ok;trivial.
 
892
  destruct P.
 
893
  rewrite (ARmul_comm ARth);Esimpl2;Esimpl2.
 
894
  Esimpl2. rewrite IHP'1;Esimpl2.
 
895
   assert (match p0 with
 
896
           | xI j => Pinj (xO j) P ** P'2
 
897
           | xO j => Pinj (Pdouble_minus_one j) P ** P'2
 
898
           | 1 => P ** P'2
 
899
           end @ (tail l) == P @ (jump p0 l) * P'2 @ (tail l)).
 
900
   destruct p0;rewrite IHP'2;Esimpl.
 
901
   rewrite Pjump_xO_tail. reflexivity.
 
902
   rewrite Pjump_Pdouble_minus_one;Esimpl.
 
903
   rewrite H;Esimpl.
 
904
   rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2.
 
905
   repeat (rewrite IHP'1 || rewrite IHP'2);simpl.
 
906
   rewrite PmulI_ok;trivial.
 
907
   unfold tail.
 
908
   mul_push (P'1@l). simpl. mul_push (P'2 @ (jump 1 l)). Esimpl.
 
909
 Qed.
 
910
 
 
911
(*
 
912
Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
 
913
 Proof.
 
914
  destruct P;simpl;intros.
 
915
  Esimpl2;apply (ARmul_comm ARth).
 
916
  rewrite (PmulI_ok P (Pmul_aux_ok P)).
 
917
  apply (ARmul_comm ARth).
 
918
  rewrite Padd_ok; Esimpl2.
 
919
  rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial.
 
920
  rewrite Pmul_aux_ok;mul_push (P' @ l).
 
921
  rewrite (ARmul_comm ARth (P' @ l));rrefl.
 
922
 Qed.
 
923
*)
 
924
 
 
925
 Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
 
926
 Proof.
 
927
  induction P;simpl;intros;Esimpl2.
 
928
  apply IHP. rewrite Padd_ok. rewrite Pmul_ok;Esimpl2.
 
929
  rewrite IHP1;rewrite IHP2.
 
930
  mul_push (pow_pos rmul (hd 0 l) p). mul_push (P2@l).
 
931
  rrefl.
 
932
 Qed.
 
933
 
 
934
 Lemma Mphi_morph : forall P env env', (forall x, env x = env' x ) -> 
 
935
   Mphi env P = Mphi env' P.
 
936
 Proof.
 
937
   induction P ; simpl.
 
938
   reflexivity.
 
939
   intros.
 
940
   apply IHP.
 
941
   intros.
 
942
   unfold jump.
 
943
   apply H.
 
944
   (**)
 
945
   intros.
 
946
   replace (Mphi (tail env) P) with (Mphi (tail env') P).
 
947
   unfold hd. unfold nth.
 
948
   rewrite H.
 
949
   reflexivity.
 
950
   apply IHP.
 
951
   unfold tail,jump.
 
952
   intros. symmetry. apply H.
 
953
 Qed.
 
954
 
 
955
Lemma Mjump_xO_tail : forall M p l, 
 
956
  Mphi  (jump (xO p) (tail l)) M = Mphi (jump (xI p) l) M.
 
957
Proof.
 
958
  intros.
 
959
  apply Mphi_morph.
 
960
  intros.
 
961
  rewrite (@jump_simpl R (xI p)).
 
962
  rewrite (@jump_simpl R (xO p)).
 
963
  reflexivity.
 
964
Qed.
 
965
 
 
966
Lemma Mjump_Pdouble_minus_one : forall M p l,
 
967
  Mphi (jump (Pdouble_minus_one p) (tail l)) M = Mphi (jump (xO p) l) M.
 
968
Proof.
 
969
  intros.
 
970
  apply Mphi_morph.
 
971
  intros.
 
972
  rewrite jump_Pdouble_minus_one.
 
973
  rewrite (@jump_simpl R (xO p)).
 
974
  reflexivity.
 
975
Qed.
 
976
 
 
977
Lemma Mjump_Pplus : forall M i j l, Mphi (jump (i + j) l ) M = Mphi (jump j (jump i l)) M.
 
978
Proof.
 
979
  intros. apply Mphi_morph. intros. rewrite <- jump_Pplus.
 
980
  rewrite Pplus_comm.
 
981
  reflexivity.
 
982
Qed.
 
983
 
 
984
 
 
985
 
 
986
 Lemma mkZmon_ok: forall M j l,
 
987
   Mphi l (mkZmon j M) == Mphi l (zmon j M).
 
988
 intros M j l; case M; simpl; intros; rsimpl.
 
989
 Qed.
 
990
 
 
991
 Lemma zmon_pred_ok : forall M j l,
 
992
    Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M).
 
993
 Proof.
 
994
   destruct j; simpl;intros l; rsimpl.
 
995
   rewrite mkZmon_ok;rsimpl.
 
996
   simpl.
 
997
   rewrite Mjump_xO_tail.
 
998
   reflexivity.
 
999
   rewrite mkZmon_ok;simpl.
 
1000
   rewrite Mjump_Pdouble_minus_one; rsimpl.
 
1001
 Qed.
 
1002
 
 
1003
 Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i.
 
1004
 Proof.
 
1005
  destruct M;simpl;intros;rsimpl.
 
1006
   rewrite zmon_pred_ok;simpl;rsimpl.
 
1007
  rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl.
 
1008
 Qed.
 
1009
 
 
1010
 
 
1011
 Lemma Mphi_ok: forall P M l,
 
1012
    let (Q,R) := MFactor P M in
 
1013
      P@l == Q@l + (Mphi l M) * (R@l).
 
1014
 Proof.
 
1015
 intros P; elim P; simpl; auto; clear P.
 
1016
   intros c M l; case M; simpl; auto; try intro p; try intro m;
 
1017
   try rewrite (morph0 CRmorph); rsimpl.
 
1018
 
 
1019
   intros i P Hrec M l; case M; simpl; clear M.
 
1020
     rewrite (morph0 CRmorph); rsimpl.
 
1021
     intros j M.
 
1022
     case_eq ((i ?= j) Eq); intros He; simpl.
 
1023
       rewrite (Pcompare_Eq_eq _ _ He).
 
1024
       generalize (Hrec M (jump j l)); case (MFactor P M);
 
1025
        simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
 
1026
       generalize (Hrec (zmon (j -i) M) (jump i l));
 
1027
       case (MFactor P (zmon (j -i) M)); simpl.
 
1028
       intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
 
1029
       rewrite  <- (Pplus_minus _ _ (ZC2 _ _ He)).
 
1030
       rewrite Mjump_Pplus; auto.
 
1031
       rewrite (morph0 CRmorph); rsimpl.
 
1032
       intros P2 m; rewrite (morph0 CRmorph); rsimpl.
 
1033
 
 
1034
   intros P2 Hrec1 i Q2 Hrec2 M l; case M; simpl; auto.
 
1035
   rewrite (morph0 CRmorph); rsimpl.
 
1036
   intros j M1.
 
1037
     generalize (Hrec1 (zmon j M1) l);
 
1038
     case (MFactor P2 (zmon j M1)).
 
1039
     intros R1 S1 H1.
 
1040
     generalize (Hrec2 (zmon_pred j M1) (tail l));
 
1041
     case (MFactor Q2 (zmon_pred j M1)); simpl.
 
1042
     intros R2 S2 H2; rewrite H1; rewrite H2.
 
1043
     repeat rewrite mkPX_ok; simpl.
 
1044
     rsimpl.
 
1045
     apply radd_ext; rsimpl.
 
1046
     rewrite (ARadd_comm ARth); rsimpl.
 
1047
     apply radd_ext; rsimpl.
 
1048
     rewrite (ARadd_comm ARth); rsimpl.
 
1049
     rewrite zmon_pred_ok;rsimpl.
 
1050
   intros j M1.
 
1051
     case_eq ((i ?= j) Eq); intros He; simpl.
 
1052
       rewrite (Pcompare_Eq_eq _ _ He).
 
1053
       generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1));
 
1054
        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
 
1055
       rewrite H; rewrite mkPX_ok; rsimpl.
 
1056
       repeat (rewrite <-(ARadd_assoc ARth)).
 
1057
       apply radd_ext; rsimpl.
 
1058
       rewrite (ARadd_comm ARth); rsimpl.
 
1059
       apply radd_ext; rsimpl.
 
1060
       repeat (rewrite <-(ARmul_assoc ARth)).
 
1061
       rewrite mkZmon_ok.
 
1062
       apply rmul_ext; rsimpl.
 
1063
       rewrite (ARmul_comm ARth); rsimpl.
 
1064
       generalize (Hrec1 (vmon (j - i) M1) l);
 
1065
             case (MFactor P2 (vmon (j - i) M1));
 
1066
        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
 
1067
       rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto.
 
1068
       rewrite mkPX_ok; rsimpl.
 
1069
       repeat (rewrite <-(ARadd_assoc ARth)).
 
1070
       apply radd_ext; rsimpl.
 
1071
       rewrite (ARadd_comm ARth); rsimpl.
 
1072
       apply radd_ext; rsimpl.
 
1073
       repeat (rewrite <-(ARmul_assoc ARth)).
 
1074
       apply rmul_ext; rsimpl.
 
1075
       rewrite (ARmul_comm ARth); rsimpl.
 
1076
       apply rmul_ext; rsimpl.
 
1077
       rewrite <- pow_pos_Pplus.
 
1078
       rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl.
 
1079
       generalize (Hrec1 (mkZmon 1 M1) l);
 
1080
             case (MFactor P2 (mkZmon 1 M1));
 
1081
        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
 
1082
       rewrite H; rsimpl.
 
1083
       rewrite mkPX_ok; rsimpl.
 
1084
       repeat (rewrite <-(ARadd_assoc ARth)).
 
1085
       apply radd_ext; rsimpl.
 
1086
       rewrite (ARadd_comm ARth); rsimpl.
 
1087
       apply radd_ext; rsimpl.
 
1088
       rewrite mkZmon_ok.
 
1089
       repeat (rewrite <-(ARmul_assoc ARth)).
 
1090
       apply rmul_ext; rsimpl.
 
1091
       rewrite (ARmul_comm ARth); rsimpl.
 
1092
       rewrite mkPX_ok; simpl; rsimpl.
 
1093
       rewrite (morph0 CRmorph); rsimpl.
 
1094
       repeat (rewrite <-(ARmul_assoc ARth)).
 
1095
       rewrite (ARmul_comm ARth (Q3@l)); rsimpl.
 
1096
       apply rmul_ext; rsimpl.
 
1097
       rewrite <- pow_pos_Pplus.
 
1098
       rewrite (Pplus_minus _ _ He); rsimpl.
 
1099
 Qed.
 
1100
 
 
1101
(* Proof for the symmetric version *)
 
1102
 
 
1103
 Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
 
1104
    POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
 
1105
 Proof.
 
1106
 intros P2 M1 P3 P4 l; unfold POneSubst.
 
1107
 generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto.
 
1108
 intros Q1 R1; case R1.
 
1109
   intros c H; rewrite H.
 
1110
   generalize (morph_eq CRmorph c cO);
 
1111
        case (c ?=! cO); simpl; auto.
 
1112
   intros H1 H2; rewrite H1; auto; rsimpl.
 
1113
   discriminate.
 
1114
   intros _ H1 H2; injection H1; intros; subst.
 
1115
   rewrite H2; rsimpl.
 
1116
 (* new version *)
 
1117
   rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
 
1118
 intros i P5 H; rewrite H.
 
1119
   intros HH H1; injection HH; intros; subst; rsimpl.
 
1120
   rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. 
 
1121
 intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
 
1122
   assert (P4 = Q1 ++ P3 ** PX i P5 P6).
 
1123
   injection H2; intros; subst;trivial.
 
1124
  rewrite H;rewrite Padd_ok;rewrite Pmul_ok;rsimpl.
 
1125
Qed.
 
1126
(*
 
1127
  Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
 
1128
    POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
 
1129
Proof.
 
1130
 intros P2 M1 P3 P4 l; unfold POneSubst.
 
1131
 generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto.
 
1132
 intros Q1 R1; case R1.
 
1133
   intros c H; rewrite H.
 
1134
   generalize (morph_eq CRmorph c cO);
 
1135
        case (c ?=! cO); simpl; auto.
 
1136
   intros H1 H2; rewrite H1; auto; rsimpl.
 
1137
   discriminate.
 
1138
   intros _ H1 H2; injection H1; intros; subst.
 
1139
   rewrite H2; rsimpl.
 
1140
  rewrite Padd_ok; rewrite Pmul_ok; rsimpl.
 
1141
  intros i P5 H; rewrite H.
 
1142
   intros HH H1; injection HH; intros; subst; rsimpl.
 
1143
   rewrite Padd_ok; rewrite Pmul_ok. rewrite H1; rsimpl.
 
1144
   intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
 
1145
   injection H2; intros; subst; rsimpl.
 
1146
   rewrite Padd_ok.
 
1147
   rewrite Pmul_ok; rsimpl.
 
1148
 Qed.
 
1149
*)
 
1150
 Lemma PNSubst1_ok: forall n P1 M1 P2 l,
 
1151
    Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
 
1152
 Proof.
 
1153
 intros n; elim n; simpl; auto.
 
1154
   intros P2 M1 P3 l H.
 
1155
   generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l);
 
1156
   case (POneSubst P2 M1 P3); [idtac | intros; rsimpl].
 
1157
   intros P4 Hrec; rewrite (Hrec P4); auto; rsimpl.
 
1158
 intros n1 Hrec P2 M1 P3 l H.
 
1159
   generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l);
 
1160
   case (POneSubst P2 M1 P3); [idtac | intros; rsimpl].
 
1161
   intros P4 Hrec1; rewrite (Hrec1 P4); auto; rsimpl.
 
1162
 Qed.
 
1163
 
 
1164
 Lemma PNSubst_ok: forall n P1 M1 P2 l P3,
 
1165
    PNSubst P1 M1 P2 n = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
 
1166
 Proof.
 
1167
 intros n P2 M1 P3 l P4; unfold PNSubst.
 
1168
 generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l);
 
1169
 case (POneSubst P2 M1 P3); [idtac | intros; discriminate].
 
1170
 intros P5 H1; case n; try (intros; discriminate).
 
1171
 intros n1 H2; injection H2; intros; subst.
 
1172
 rewrite <- PNSubst1_ok; auto.
 
1173
 Qed.
 
1174
 
 
1175
 Fixpoint MPcond (LM1: list (Mon * Pol)) (l: Env R) {struct LM1} : Prop :=
 
1176
    match LM1 with
 
1177
     cons (M1,P2) LM2 =>  (Mphi l M1 == P2@l) /\ (MPcond LM2 l)
 
1178
    | _ => True
 
1179
    end.
 
1180
 
 
1181
 Lemma PSubstL1_ok: forall n LM1 P1 l,
 
1182
    MPcond LM1 l ->  P1@l == (PSubstL1 P1 LM1 n)@l.
 
1183
 Proof.
 
1184
 intros n LM1; elim LM1; simpl; auto.
 
1185
   intros; rsimpl.
 
1186
 intros (M2,P2) LM2 Hrec P3 l [H H1].
 
1187
 rewrite <- Hrec; auto.
 
1188
 apply PNSubst1_ok; auto.
 
1189
 Qed.
 
1190
 
 
1191
 Lemma PSubstL_ok: forall n LM1 P1 P2 l,
 
1192
   PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l ->  P1@l == P2@l.
 
1193
 Proof.
 
1194
 intros n LM1; elim LM1; simpl; auto.
 
1195
   intros; discriminate.
 
1196
 intros (M2,P2) LM2 Hrec P3 P4 l.
 
1197
 generalize (PNSubst_ok n P3 M2 P2); case (PNSubst P3 M2 P2 n).
 
1198
   intros P5 H0 H1 [H2 H3]; injection H1; intros; subst.
 
1199
   rewrite <- PSubstL1_ok; auto.
 
1200
 intros l1 H [H1 H2]; auto.
 
1201
 Qed.
 
1202
 
 
1203
 Lemma PNSubstL_ok: forall m n LM1 P1 l,
 
1204
    MPcond LM1 l ->  P1@l == (PNSubstL P1 LM1 m n)@l.
 
1205
 Proof.
 
1206
 intros m; elim m; simpl; auto.
 
1207
   intros n LM1 P2 l H; generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l);
 
1208
     case (PSubstL P2 LM1 n); intros; rsimpl; auto.
 
1209
 intros m1 Hrec n LM1 P2 l H.
 
1210
 generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l);
 
1211
     case (PSubstL P2 LM1 n); intros; rsimpl; auto.
 
1212
 rewrite <- Hrec; auto.
 
1213
 Qed.
 
1214
 
 
1215
 (** Definition of polynomial expressions *)
 
1216
 
 
1217
 Inductive PExpr : Type :=
 
1218
  | PEc : C -> PExpr
 
1219
  | PEX : positive -> PExpr
 
1220
  | PEadd : PExpr -> PExpr -> PExpr
 
1221
  | PEsub : PExpr -> PExpr -> PExpr
 
1222
  | PEmul : PExpr -> PExpr -> PExpr
 
1223
  | PEopp : PExpr -> PExpr
 
1224
  | PEpow : PExpr -> N -> PExpr.
 
1225
 
 
1226
 (** evaluation of polynomial expressions towards R *)
 
1227
 Definition mk_X j := mkPinj_pred j mkX.
 
1228
 
 
1229
 (** evaluation of polynomial expressions towards R *)
 
1230
 
 
1231
 Fixpoint PEeval (l:Env R) (pe:PExpr) {struct pe} : R :=
 
1232
   match pe with
 
1233
   | PEc c => phi c
 
1234
   | PEX j => nth j l
 
1235
   | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
 
1236
   | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
 
1237
   | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
 
1238
   | PEopp pe1 => - (PEeval l pe1)
 
1239
   | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
 
1240
   end.
 
1241
 
 
1242
 (** Correctness proofs *)
 
1243
 
 
1244
 Lemma mkX_ok : forall p l, nth  p l == (mk_X p) @ l.
 
1245
 Proof.
 
1246
  destruct p;simpl;intros;Esimpl;trivial.
 
1247
  rewrite nth_spec ; auto.
 
1248
  unfold hd.
 
1249
  rewrite <- nth_Pdouble_minus_one.
 
1250
  rewrite (nth_jump (Pdouble_minus_one p) l 1).
 
1251
  reflexivity.
 
1252
 Qed.
 
1253
 
 
1254
 Ltac Esimpl3 :=
 
1255
  repeat match goal with
 
1256
  | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l)
 
1257
  | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l)
 
1258
  end;Esimpl2;try rrefl;try apply (ARadd_comm ARth).
 
1259
 
 
1260
(* Power using the chinise algorithm *)
 
1261
(*Section POWER.
 
1262
  Variable subst_l : Pol -> Pol.
 
1263
  Fixpoint Ppow_pos (P:Pol) (p:positive){struct p} : Pol :=
 
1264
   match p with
 
1265
   | xH => P
 
1266
   | xO p => subst_l (Psquare (Ppow_pos P p))
 
1267
   | xI p => subst_l (Pmul P (Psquare (Ppow_pos P p)))
 
1268
   end.
 
1269
 
 
1270
  Definition Ppow_N P n :=
 
1271
   match n with
 
1272
   | N0 => P1
 
1273
   | Npos p => Ppow_pos P p
 
1274
   end.
 
1275
 
 
1276
  Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
 
1277
         forall P p, (Ppow_pos P p)@l == (pow_pos Pmul P p)@l.
 
1278
  Proof.
 
1279
   intros l subst_l_ok P.
 
1280
   induction p;simpl;intros;try rrefl;try rewrite subst_l_ok.
 
1281
   repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl.
 
1282
   repeat rewrite Pmul_ok;rewrite Psquare_ok;rewrite IHp;rrefl.
 
1283
  Qed.
 
1284
 
 
1285
  Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
 
1286
         forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
 
1287
  Proof.  destruct n;simpl. rrefl. apply Ppow_pos_ok. trivial.  Qed.
 
1288
 
 
1289
 End POWER. *)
 
1290
 
 
1291
Section POWER.
 
1292
  Variable subst_l : Pol -> Pol.
 
1293
  Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
 
1294
   match p with
 
1295
   | xH => subst_l (Pmul res P)
 
1296
   | xO p => Ppow_pos (Ppow_pos res P p) P p
 
1297
   | xI p => subst_l (Pmul  (Ppow_pos (Ppow_pos res P p) P p) P)
 
1298
   end.
 
1299
 
 
1300
  Definition Ppow_N P n :=
 
1301
   match n with
 
1302
   | N0 => P1
 
1303
   | Npos p => Ppow_pos P1 P p
 
1304
   end.
 
1305
 
 
1306
  Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
 
1307
         forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l.
 
1308
  Proof.
 
1309
   intros l subst_l_ok res P p. generalize res;clear res.
 
1310
   induction p;simpl;intros;try rewrite subst_l_ok; repeat rewrite Pmul_ok;repeat rewrite IHp.
 
1311
   rsimpl. mul_push (P@l);rsimpl. rsimpl. rrefl.
 
1312
  Qed.
 
1313
 
 
1314
  Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
 
1315
         forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
 
1316
  Proof.  destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl.  auto. Qed.
 
1317
 
 
1318
 End POWER.
 
1319
 
 
1320
 (** Normalization and rewriting *)
 
1321
 
 
1322
 Section NORM_SUBST_REC.
 
1323
  Variable n : nat.
 
1324
  Variable lmp:list (Mon*Pol).
 
1325
  Let subst_l P := PNSubstL P lmp n n.
 
1326
  Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
 
1327
  Let Ppow_subst := Ppow_N subst_l.
 
1328
 
 
1329
  Fixpoint norm_aux (pe:PExpr) : Pol :=
 
1330
   match pe with
 
1331
   | PEc c => Pc c
 
1332
   | PEX j => mk_X j
 
1333
   | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1)
 
1334
   | PEadd pe1 (PEopp pe2) =>
 
1335
     Psub (norm_aux pe1) (norm_aux pe2)
 
1336
   | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
 
1337
   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
 
1338
   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
 
1339
   | PEopp pe1 => Popp (norm_aux pe1)
 
1340
   | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
 
1341
   end.
 
1342
 
 
1343
  Definition norm_subst pe := subst_l (norm_aux pe).
 
1344
 
 
1345
 (*
 
1346
  Fixpoint norm_subst (pe:PExpr) : Pol :=
 
1347
   match pe with
 
1348
   | PEc c => Pc c
 
1349
   | PEX j => subst_l (mk_X j)
 
1350
   | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1)
 
1351
   | PEadd pe1 (PEopp pe2) =>
 
1352
     Psub (norm_subst pe1) (norm_subst pe2)
 
1353
   | PEadd pe1 pe2 => Padd (norm_subst  pe1) (norm_subst pe2)
 
1354
   | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2)
 
1355
   | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2)
 
1356
   | PEopp pe1 => Popp (norm_subst pe1)
 
1357
   | PEpow pe1 n => Ppow_subst (norm_subst pe1) n
 
1358
   end.
 
1359
 
 
1360
  Lemma norm_subst_spec :
 
1361
     forall l pe, MPcond lmp l ->
 
1362
       PEeval l pe == (norm_subst pe)@l.
 
1363
  Proof.
 
1364
   intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l).
 
1365
      unfold subst_l;intros.
 
1366
      rewrite <- PNSubstL_ok;trivial. rrefl.
 
1367
   assert (Pms_ok:forall P1 P2, (Pmul_subst P1 P2)@l == P1@l*P2@l).
 
1368
    intros;unfold Pmul_subst;rewrite subst_l_ok;rewrite Pmul_ok;rrefl.
 
1369
   induction pe;simpl;Esimpl3.
 
1370
   rewrite subst_l_ok;apply mkX_ok.
 
1371
   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3.
 
1372
   rewrite IHpe1;rewrite IHpe2;rrefl.
 
1373
   rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl.
 
1374
   rewrite IHpe;rrefl.
 
1375
   unfold Ppow_subst. rewrite Ppow_N_ok. trivial.
 
1376
   rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
 
1377
   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;
 
1378
      repeat rewrite Pmul_ok;rrefl.
 
1379
  Qed.
 
1380
*)
 
1381
 Lemma norm_aux_spec :
 
1382
     forall l pe, (*MPcond lmp l ->*)
 
1383
       PEeval l pe == (norm_aux pe)@l.
 
1384
  Proof.
 
1385
   intros.
 
1386
   induction pe;simpl;Esimpl3.
 
1387
   apply mkX_ok.
 
1388
   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. 
 
1389
   rewrite IHpe1;rewrite IHpe2;rrefl.
 
1390
   rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
 
1391
   rewrite IHpe;rrefl.
 
1392
   rewrite Ppow_N_ok by reflexivity. 
 
1393
   rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
 
1394
   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
 
1395
      repeat rewrite Pmul_ok;rrefl.
 
1396
  Qed.
 
1397
 
 
1398
 
 
1399
 End NORM_SUBST_REC.
 
1400
 
 
1401
 
 
1402
End MakeRingPol.
 
1403