aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/Ncring_polynom.v
blob: b0348f8fd6234fe718d6df33aa3d880aaf444fd6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*  A <X1,...,Xn>: non commutative polynomials on a commutative ring A *)

Set Implicit Arguments.
Require Import Setoid.
Require Import BinList.
Require Import BinPos.
Require Import BinNat.
Require Import BinInt.
Require Export Ring_polynom. (* n'utilise que PExpr *)
Require Export Ncring.

Section MakeRingPol.

Context (C R:Type) `{Rh:Ring_morphism C R}.

Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.

 Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm).
 Ltac add_push := gen_add_push .

(* Definition of non commutative multivariable polynomials 
   with coefficients in C :
 *)

 Inductive Pol : Type :=
  | Pc : C -> Pol
  | PX : Pol -> positive -> positive -> Pol -> Pol. 
    (* PX P i n Q represents P * X_i^n + Q *)
Definition cO:C . exact ring0. Defined.
Definition cI:C . exact ring1. Defined.

 Definition P0 := Pc 0.
 Definition P1 := Pc 1.

Variable Ceqb:C->C->bool.
Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
Notation "x =? y" := (equalityb x y) (at level 70, no associativity).
Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y).

Instance equalityb_coef : Equalityb C :=
  {equalityb x y := Ceqb x y}.

 Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
  match P, P' with
  | Pc c, Pc c' => c =? c'
  | PX P i n Q, PX P' i' n' Q' =>
    match Pos.compare i i', Pos.compare n n' with
    | Eq, Eq => if Peq P P' then Peq Q Q' else false
    | _,_ => false
    end
  | _, _ => false
  end.

Instance equalityb_pol : Equalityb Pol :=
  {equalityb x y := Peq x y}.

(* Q a ses variables de queue < i *)
 Definition mkPX P i n Q :=
  match P with
  | Pc c => if c =? 0 then Q else PX P i n Q 
  | PX P' i' n' Q' => 
       match Pos.compare i i' with
        | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q
        | _ => PX P i n Q
       end
  end.

 Definition mkXi i n := PX P1 i n P0.

 Definition mkX i := mkXi i 1.

 (** Opposite of addition *)

 Fixpoint Popp (P:Pol) : Pol :=
  match P with
  | Pc c => Pc (- c)
  | PX P i n Q => PX (Popp P) i n (Popp Q)
  end.

 Notation "-- P" := (Popp P)(at level 30).

 (** Addition et subtraction *)

 Fixpoint PaddCl (c:C)(P:Pol) {struct P} : Pol :=
  match P with
  | Pc c1 => Pc (c + c1)
  | PX P i n Q => PX P i n (PaddCl c Q)
  end.

(* Q quelconque *)

Section PaddX.
Variable Padd:Pol->Pol->Pol.
Variable P:Pol.

(* Xi^n * P + Q
les variables de tete de Q ne sont pas forcement < i 
mais Q est normalisé : variables de tete decroissantes *)

Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
  match Q with
  | Pc c => mkPX P i n Q
  | PX P' i' n' Q' => 
      match Pos.compare i i' with
      | (* i > i' *)
        Gt => mkPX P i n Q
      | (* i < i' *)
        Lt => mkPX P' i' n' (PaddX i n Q')
      | (* i = i' *)
        Eq => match Z.pos_sub n n' with
              | (* n > n' *) 
                Zpos k => mkPX (PaddX i k P') i' n' Q'
              | (* n = n' *)
                Z0 => mkPX (Padd P P') i n Q'
              | (* n < n' *)
                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
              end
      end
  end.

End PaddX.

Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol :=
  match P1 with
  | Pc c => PaddCl c P2
  | PX P' i' n' Q' =>
      PaddX Padd P' i' n' (Padd Q' P2)
  end.

 Notation "P ++ P'" := (Padd P P').

Definition Psub(P P':Pol):= P ++ (--P').

 Notation "P -- P'" := (Psub P P')(at level 50).

 (** Multiplication *)

 Fixpoint PmulC_aux (P:Pol) (c:C)  {struct P} : Pol :=
  match P with
  | Pc c' => Pc (c' * c)
  | PX P i n Q => mkPX (PmulC_aux P c) i n (PmulC_aux Q c)
  end.

 Definition PmulC P c :=
  if c =? 0 then P0 else
  if c =? 1 then P else PmulC_aux P c.

 Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol :=
   match P2 with
   | Pc c => PmulC P1 c
   | PX P i n Q =>
     PaddX Padd (Pmul P1 P) i n (Pmul P1 Q)
   end.

 Notation "P ** P'" := (Pmul P P')(at level 40).

 Definition Psquare (P:Pol) : Pol := P ** P.


 (** Evaluation of a polynomial towards R *)

 Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
  match P with
  | Pc c => [c]
  | PX P i n Q =>
     let x := nth 0 i l in
     let xn := pow_pos x n in
   (Pphi l P) * xn + (Pphi l Q)
  end.

 Reserved Notation "P @ l " (at level 10, no associativity).
 Notation "P @ l " := (Pphi l P).

 (** Proofs *)

 Ltac destr_pos_sub H :=
  match goal with |- context [Z.pos_sub ?x ?y] =>
   assert (H := Z.pos_sub_discr x y); destruct (Z.pos_sub x y)
  end.

 Lemma Peq_ok : forall P P',
    (P =? P') = true -> forall l, P@l == P'@ l.
 Proof.
 induction P;destruct P';simpl;intros ;try easy.
 - now apply ring_morphism_eq, Ceqb_eq.
 - specialize (IHP1 P'1). specialize (IHP2 P'2).
   simpl in IHP1, IHP2.
   destruct (Pos.compare_spec p p1); try discriminate;
   destruct (Pos.compare_spec p0 p2); try discriminate.
   destruct (Peq P2 P'1); try discriminate.
   subst; now rewrite IHP1, IHP2.
 Qed.

 Lemma Pphi0 : forall l, P0@l == 0.
 Proof.
  intros;simpl. 
 rewrite ring_morphism0. reflexivity.
 Qed.

 Lemma Pphi1 : forall l,  P1@l == 1.
 Proof.
  intros;simpl; rewrite ring_morphism1. reflexivity.
 Qed.

 Lemma mkPX_ok : forall l P i n Q,
  (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l.
 Proof.
  intros l P i n Q;unfold mkPX.
  destruct P;try (simpl;reflexivity).
  assert (Hh := ring_morphism_eq  c 0). 
  simpl; case_eq (Ceqb c 0);simpl;try reflexivity.
  intros.
  rewrite Hh. rewrite ring_morphism0.
  rsimpl. apply Ceqb_eq. trivial.
  destruct (Pos.compare_spec i p).
  assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. 
  rewrite Hh. 
  rewrite Pphi0. rsimpl. rewrite Pos.add_comm. rewrite pow_pos_add;rsimpl.
  subst;trivial. reflexivity. trivial. intros. simpl. reflexivity. simpl. reflexivity.
 simpl. reflexivity.
 Qed.

Ltac Esimpl :=
  repeat (progress (
   match goal with
   | |- context [?P@?l] =>
       match P with
       | P0 => rewrite (Pphi0 l)
       | P1 => rewrite (Pphi1 l)
       | (mkPX ?P ?i ?n ?Q) => rewrite (mkPX_ok l P i n Q)
       end
   | |- context [[?c]] =>
       match c with
       | 0 => rewrite ring_morphism0
       | 1 => rewrite ring_morphism1
       | ?x + ?y => rewrite ring_morphism_add
       | ?x * ?y => rewrite ring_morphism_mul
       | ?x - ?y => rewrite ring_morphism_sub
       | - ?x => rewrite ring_morphism_opp
       end
   end));
  simpl; rsimpl.

 Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .
 Proof.
  induction P; simpl; intros; Esimpl; try reflexivity.
 rewrite IHP2. rsimpl. 
rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0) [c]).
reflexivity.
 Qed.

 Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l ==  P@l * [c].
 Proof.
  induction P;simpl;intros.  rewrite ring_morphism_mul.
try reflexivity.
  simpl. Esimpl.  rewrite IHP1;rewrite IHP2;rsimpl. 
  Qed.

 Lemma PmulC_ok : forall c P l, (PmulC P c)@l ==  P@l * [c].
 Proof.
  intros c P l; unfold PmulC.
  assert (Hh:= ring_morphism_eq c 0);case_eq (c =? 0). intros.
  rewrite Hh;Esimpl. apply Ceqb_eq;trivial. 
  assert (H1h:= ring_morphism_eq c 1);case_eq (c =? 1);intros.
  rewrite H1h;Esimpl. apply Ceqb_eq;trivial.
  apply PmulC_aux_ok.
 Qed.

 Lemma Popp_ok : forall P l, (--P)@l == - P@l.
 Proof.
  induction P;simpl;intros.
  Esimpl.
  rewrite IHP1;rewrite IHP2;rsimpl.
 Qed.

 Ltac Esimpl2 :=
  Esimpl;
  repeat (progress (
   match goal with
   | |- context [(PaddCl ?c ?P)@?l] => rewrite (PaddCl_ok c P l)
   | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l)
   | |- context [(--?P)@?l] => rewrite (Popp_ok P l)
   end)); Esimpl.

Lemma PaddXPX: forall P i n Q,
  PaddX Padd P i n Q =
  match Q with
  | Pc c => mkPX P i n Q
  | PX P' i' n' Q' => 
      match Pos.compare i i' with
      | (* i > i' *)
        Gt => mkPX P i n Q
      | (* i < i' *)
        Lt => mkPX P' i' n' (PaddX Padd P i n Q')
      | (* i = i' *)
        Eq => match Z.pos_sub n n' with
              | (* n > n' *) 
                Zpos k => mkPX (PaddX Padd P i k P') i' n' Q'
              | (* n = n' *)
                Z0 => mkPX (Padd P P') i n Q'
              | (* n < n' *)
                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
              end
      end
  end.
induction Q; reflexivity.
Qed.

Lemma PaddX_ok2 : forall P2,
   (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l)
   /\
   (forall P k n l,
           (PaddX Padd P2 k n P) @ l == 
             P2 @ l * pow_pos (nth 0 k l) n  + P @ l).
induction P2;simpl;intros. split. intros. apply PaddCl_ok.
 induction P.  unfold PaddX. intros. rewrite mkPX_ok.
 simpl. rsimpl.
intros. simpl.
 destruct (Pos.compare_spec k p) as [Hh|Hh|Hh].
 destr_pos_sub H1h. Esimpl2.
rewrite Hh; trivial. rewrite H1h. reflexivity.
simpl. rewrite mkPX_ok. rewrite IHP1. Esimpl2.
 rewrite Pos.add_comm in H1h.
rewrite H1h. 
rewrite pow_pos_add.  Esimpl2.
rewrite Hh; trivial. reflexivity.
rewrite mkPX_ok. rewrite PaddCl_ok. Esimpl2. rewrite Pos.add_comm in H1h.
rewrite H1h.  Esimpl2. rewrite pow_pos_add. Esimpl2.
rewrite Hh; trivial. reflexivity.
rewrite mkPX_ok. rewrite IHP2. Esimpl2.
rewrite (ring_add_comm  (P2 @ l * pow_pos (nth 0 p l) p0) 
                             ([c] * pow_pos (nth 0 k l) n)).
reflexivity.  assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c  0); 
 intros; simpl.
rewrite H1h;trivial. Esimpl2. apply Ceqb_eq; trivial. reflexivity.
decompose [and] IHP2_1. decompose [and] IHP2_2. clear IHP2_1 IHP2_2.
split. intros. rewrite H0. rewrite H1.
Esimpl2.
induction P. unfold PaddX. intros. rewrite mkPX_ok. simpl. reflexivity.
intros. rewrite PaddXPX. 
destruct (Pos.compare_spec k p1) as [H3h|H3h|H3h].
destr_pos_sub H4h.
rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. Esimpl2.
rewrite H4h. rewrite H3h;trivial. reflexivity.
rewrite mkPX_ok. rewrite IHP1. Esimpl2. rewrite H3h;trivial.
rewrite Pos.add_comm in H4h.
rewrite H4h. rewrite pow_pos_add. Esimpl2.
rewrite mkPX_ok. simpl. rewrite H0. rewrite H1. 
rewrite mkPX_ok.
 Esimpl2. rewrite H3h;trivial.
 rewrite Pos.add_comm in H4h.
rewrite H4h. rewrite pow_pos_add. Esimpl2.
rewrite mkPX_ok. simpl. rewrite IHP2. Esimpl2.
gen_add_push (P2 @ l * pow_pos (nth 0 p1 l) p2). try reflexivity.
rewrite mkPX_ok. simpl. reflexivity.
Qed.

Lemma Padd_ok : forall P Q l, (P ++ Q) @ l == P @ l + Q @ l.
intro P. elim (PaddX_ok2 P); auto.
Qed.

Lemma PaddX_ok : forall P2 P k n l,
   (PaddX Padd P2 k n P) @ l ==  P2 @ l * pow_pos (nth 0 k l) n  + P @ l.
intro P2. elim (PaddX_ok2 P2); auto.
Qed.

 Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
unfold Psub. intros. rewrite Padd_ok. rewrite Popp_ok. rsimpl.
 Qed.

 Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
induction P'; simpl; intros. rewrite PmulC_ok. reflexivity.
rewrite PaddX_ok. rewrite IHP'1. rewrite IHP'2. Esimpl2.
Qed.

 Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
 Proof.
  intros. unfold Psquare. apply Pmul_ok.
 Qed.

 (** Definition of polynomial expressions *)

(*
 Inductive PExpr : Type :=
  | PEc : C -> PExpr
  | PEX : positive -> PExpr
  | PEadd : PExpr -> PExpr -> PExpr
  | PEsub : PExpr -> PExpr -> PExpr
  | PEmul : PExpr -> PExpr -> PExpr
  | PEopp : PExpr -> PExpr
  | PEpow : PExpr -> N -> PExpr.
*)

 (** Specification of the power function *)
 Section POWER.
  Variable Cpow : Set.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.

  Record power_theory : Prop := mkpow_th {
    rpow_pow_N : forall r n,  (rpow r (Cp_phi n))== (pow_N r n)
  }.

 End POWER.
 Variable Cpow : Set.
 Variable Cp_phi : N -> Cpow.
 Variable rpow : R -> Cpow -> R.
 Variable pow_th : power_theory Cp_phi rpow.

 (** evaluation of polynomial expressions towards R *)

 Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
   match pe with
   | PEO => 0
   | PEI => 1
   | PEc c => [c]
   | PEX _ j => nth 0 j l
   | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
   | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
   | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
   | PEopp pe1 => - (PEeval l pe1)
   | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
   end.

Strategy expand [PEeval].

 Definition mk_X j := mkX j.

 (** Correctness proofs *)

 Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
 Proof.
  destruct p;simpl;intros;Esimpl;trivial.
 Qed.

 Ltac Esimpl3 :=
  repeat match goal with
  | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P1 P2 l)
  | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P1 P2 l)
  end;try Esimpl2;try reflexivity;try apply ring_add_comm.

(* Power using the chinise algorithm *)

Section POWER2.
  Variable subst_l : Pol -> Pol.
  Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
   match p with
   | xH => subst_l (Pmul P res)
   | xO p => Ppow_pos (Ppow_pos res P p) P p
   | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p))
   end.

  Definition Ppow_N P n :=
   match n with
   | N0 => P1
   | Npos p => Ppow_pos P1 P p
   end.

  Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R :=
  match i with
  | xH => x
  | xO i => let p := pow_pos_gen m x i in m p p
  | xI i => let p := pow_pos_gen m x i in m x (m p p)
  end.

Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
         forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l.
  Proof.
   intros l subst_l_ok res P p. generalize res;clear res.
   induction p;simpl;intros. try rewrite subst_l_ok.
 repeat rewrite Pmul_ok. repeat rewrite IHp.
   rsimpl. repeat rewrite Pmul_ok. repeat rewrite IHp. rsimpl.
 try rewrite subst_l_ok.
 repeat rewrite Pmul_ok. reflexivity.
  Qed.

Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
  match p with
  | N0 => x1
  | Npos p => pow_pos_gen m x p
  end.

  Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
         forall P n, (Ppow_N P n)@l == (pow_N_gen P1 Pmul P n)@l.
  Proof.  destruct n;simpl. reflexivity. rewrite Ppow_pos_ok; trivial. Esimpl.  Qed.

 End POWER2.

 (** Normalization and rewriting *)

 Section NORM_SUBST_REC.
  Let subst_l (P:Pol) := P.
  Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
  Let Ppow_subst := Ppow_N subst_l.

  Fixpoint norm_aux (pe:PExpr C) : Pol :=
   match pe with
   | PEO => Pc cO
   | PEI => Pc cI
   | PEc c => Pc c
   | PEX _ j => mk_X j
   | PEadd pe1 (PEopp pe2) =>
     Psub (norm_aux pe1) (norm_aux pe2)
   | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
   | PEopp pe1 => Popp (norm_aux pe1)
   | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
   end.

  Definition norm_subst pe := subst_l (norm_aux pe).

 
 Lemma norm_aux_spec :
     forall l pe, 
       PEeval l pe == (norm_aux pe)@l.
  Proof.
   intros.
   induction pe.
   - now simpl; rewrite <- ring_morphism0.
   - now simpl; rewrite <- ring_morphism1.
   - Esimpl3. 
   - Esimpl3. 
   - simpl.
     rewrite IHpe1;rewrite IHpe2.
     destruct pe2; Esimpl3. 
     unfold Psub.
     destruct pe1; destruct pe2; rewrite Padd_ok; rewrite Popp_ok; reflexivity.
   - simpl. unfold Psub. rewrite IHpe1;rewrite IHpe2.
     now destruct pe1; 
       [destruct pe2; rewrite Padd_ok; rewrite Popp_ok; Esimpl3 | Esimpl3..]. 
   - simpl. rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. reflexivity.
   - now simpl; rewrite IHpe; Esimpl3. 
   - simpl.
     rewrite Ppow_N_ok; (intros;try reflexivity). 
     rewrite rpow_pow_N; [| now apply pow_th]. 
     induction n;simpl; [now Esimpl3|]. 
     induction p; simpl; trivial.
     + try rewrite IHp;try rewrite IHpe;
         repeat rewrite Pms_ok; repeat rewrite Pmul_ok;reflexivity.
     + rewrite Pmul_ok. 
       try rewrite IHp;try rewrite IHpe; repeat rewrite Pms_ok;
         repeat rewrite Pmul_ok;reflexivity. 
  Qed.

 Lemma norm_subst_spec :
     forall l pe, 
       PEeval l pe == (norm_subst pe)@l.
 Proof.
  intros;unfold norm_subst.
  unfold subst_l.  apply norm_aux_spec. 
 Qed.

 End NORM_SUBST_REC.

 Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {struct lpe} : Prop :=
   match lpe with
   | nil => True
   | (me,pe)::lpe =>
     match lpe with
     | nil => PEeval l me == PEeval l pe
     | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe
     end
  end.


 Lemma norm_subst_ok : forall l pe,
   PEeval l pe == (norm_subst pe)@l.
 Proof.
   intros;apply norm_subst_spec. 
  Qed.


 Lemma ring_correct : forall l pe1 pe2,
   (norm_subst pe1 =? norm_subst pe2) = true ->
   PEeval l pe1 == PEeval l pe2.
 Proof.
  simpl;intros.
  do 2 (rewrite (norm_subst_ok l);trivial).
  apply Peq_ok;trivial.
 Qed.

End MakeRingPol.