# Library Coq.micromega.EnvRing

Require Import Setoid.
Require Import BinList.
Require Import Env.
Require Import BinPos.
Require Import BinNat.
Require Import BinInt.
Require Export Ring_theory.
Open Local Scope positive_scope.
Import RingSyntax.
Section MakeRingPol.
Variable R:Type.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
Variable req : R -> R -> Prop.
Variable Rsth : Setoid_Theory R req.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
Variable C: Type.
Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
Variable ceqb : C->C->bool.
Variable phi : C -> R.
Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
Variable Cpow : Set.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
Notation "0" := rO. Notation "1" := rI.
Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y).
Notation "x -! y " := (csub x y). Notation "-! x" := (copp x).
Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
Add Setoid R req Rsth as R_set1.
Ltac rrefl := gen_reflexivity Rsth.
Add Morphism radd : radd_ext.
Add Morphism rmul : rmul_ext.
Add Morphism ropp : ropp_ext.
Add Morphism rsub : rsub_ext.
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.
Inductive Pol : Type :=
| Pc : C -> Pol
| Pinj : positive -> Pol -> Pol
| PX : Pol -> positive -> Pol -> Pol.
Definition P0 := Pc cO.
Definition P1 := Pc cI.
Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
match P, P' with
| Pc c, Pc c' => c ?=! c'
| Pinj j Q, Pinj j' Q' =>
match Pcompare j j' Eq with
| Eq => Peq Q Q'
| _ => false
end
| PX P i Q, PX P' i' Q' =>
match Pcompare i i' Eq with
| Eq => if Peq P P' then Peq Q Q' else false
| _ => false
end
| _, _ => false
end.
Notation " P ?== P' " := (Peq P P').
Definition mkPinj j P :=
match P with
| Pc _ => P
| Pinj j' Q => Pinj ((j + j'):positive) Q
| _ => Pinj j P
end.
Definition mkPinj_pred j P:=
match j with
| xH => P
| xO j => Pinj (Pdouble_minus_one j) P
| xI j => Pinj (xO j) P
end.
Definition mkPX P i Q :=
match P with
| Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q
| Pinj _ _ => PX P i Q
| PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q
end.
Definition mkXi i := PX P1 i P0.
Definition mkX := mkXi 1.
Opposite of addition
Fixpoint Popp (P:Pol) : Pol :=
match P with
| Pc c => Pc (-! c)
| Pinj j Q => Pinj j (Popp Q)
| PX P i Q => PX (Popp P) i (Popp Q)
end.
Notation "-- P" := (Popp P).
Addition et subtraction
Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol :=
match P with
| Pc c1 => Pc (c1 +! c)
| Pinj j Q => Pinj j (PaddC Q c)
| PX P i Q => PX P i (PaddC Q c)
end.
Fixpoint PsubC (P:Pol) (c:C) {struct P} : Pol :=
match P with
| Pc c1 => Pc (c1 -! c)
| Pinj j Q => Pinj j (PsubC Q c)
| PX P i Q => PX P i (PsubC Q c)
end.
Section PopI.
Variable Pop : Pol -> Pol -> Pol.
Variable Q : Pol.
Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol :=
match P with
| Pc c => mkPinj j (PaddC Q c)
| Pinj j' Q' =>
match ZPminus j' j with
| Zpos k => mkPinj j (Pop (Pinj k Q') Q)
| Z0 => mkPinj j (Pop Q' Q)
| Zneg k => mkPinj j' (PaddI k Q')
end
| PX P i Q' =>
match j with
| xH => PX P i (Pop Q' Q)
| xO j => PX P i (PaddI (Pdouble_minus_one j) Q')
| xI j => PX P i (PaddI (xO j) Q')
end
end.
Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol :=
match P with
| Pc c => mkPinj j (PaddC (-- Q) c)
| Pinj j' Q' =>
match ZPminus j' j with
| Zpos k => mkPinj j (Pop (Pinj k Q') Q)
| Z0 => mkPinj j (Pop Q' Q)
| Zneg k => mkPinj j' (PsubI k Q')
end
| PX P i Q' =>
match j with
| xH => PX P i (Pop Q' Q)
| xO j => PX P i (PsubI (Pdouble_minus_one j) Q')
| xI j => PX P i (PsubI (xO j) Q')
end
end.
Variable P' : Pol.
Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol :=
match P with
| Pc c => PX P' i' P
| Pinj j Q' =>
match j with
| xH => PX P' i' Q'
| xO j => PX P' i' (Pinj (Pdouble_minus_one j) Q')
| xI j => PX P' i' (Pinj (xO j) Q')
end
| PX P i Q' =>
match ZPminus i i' with
| Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
| Z0 => mkPX (Pop P P') i Q'
| Zneg k => mkPX (PaddX k P) i Q'
end
end.
Fixpoint PsubX (i':positive) (P:Pol) {struct P} : Pol :=
match P with
| Pc c => PX (-- P') i' P
| Pinj j Q' =>
match j with
| xH => PX (-- P') i' Q'
| xO j => PX (-- P') i' (Pinj (Pdouble_minus_one j) Q')
| xI j => PX (-- P') i' (Pinj (xO j) Q')
end
| PX P i Q' =>
match ZPminus i i' with
| Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
| Z0 => mkPX (Pop P P') i Q'
| Zneg k => mkPX (PsubX k P) i Q'
end
end.
End PopI.
Fixpoint Padd (P P': Pol) {struct P'} : Pol :=
match P' with
| Pc c' => PaddC P c'
| Pinj j' Q' => PaddI Padd Q' j' P
| PX P' i' Q' =>
match P with
| Pc c => PX P' i' (PaddC Q' c)
| Pinj j Q =>
match j with
| xH => PX P' i' (Padd Q Q')
| xO j => PX P' i' (Padd (Pinj (Pdouble_minus_one j) Q) Q')
| xI j => PX P' i' (Padd (Pinj (xO j) Q) Q')
end
| PX P i Q =>
match ZPminus i i' with
| Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q')
| Z0 => mkPX (Padd P P') i (Padd Q Q')
| Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q')
end
end
end.
Notation "P ++ P'" := (Padd P P').
Fixpoint Psub (P P': Pol) {struct P'} : Pol :=
match P' with
| Pc c' => PsubC P c'
| Pinj j' Q' => PsubI Psub Q' j' P
| PX P' i' Q' =>
match P with
| Pc c => PX (-- P') i' (PaddC (-- Q') c)
| Pinj j Q =>
match j with
| xH => PX (-- P') i' (Psub Q Q')
| xO j => PX (-- P') i' (Psub (Pinj (Pdouble_minus_one j) Q) Q')
| xI j => PX (-- P') i' (Psub (Pinj (xO j) Q) Q')
end
| PX P i Q =>
match ZPminus i i' with
| Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q')
| Z0 => mkPX (Psub P P') i (Psub Q Q')
| Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q')
end
end
end.
Notation "P -- P'" := (Psub P P').
Multiplication
Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol :=
match P with
| Pc c' => Pc (c' *! c)
| Pinj j Q => mkPinj j (PmulC_aux Q c)
| PX P i Q => mkPX (PmulC_aux P c) i (PmulC_aux Q c)
end.
Definition PmulC P c :=
if c ?=! cO then P0 else
if c ?=! cI then P else PmulC_aux P c.
Section PmulI.
Variable Pmul : Pol -> Pol -> Pol.
Variable Q : Pol.
Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol :=
match P with
| Pc c => mkPinj j (PmulC Q c)
| Pinj j' Q' =>
match ZPminus j' j with
| Zpos k => mkPinj j (Pmul (Pinj k Q') Q)
| Z0 => mkPinj j (Pmul Q' Q)
| Zneg k => mkPinj j' (PmulI k Q')
end
| PX P' i' Q' =>
match j with
| xH => mkPX (PmulI xH P') i' (Pmul Q' Q)
| xO j' => mkPX (PmulI j P') i' (PmulI (Pdouble_minus_one j') Q')
| xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q')
end
end.
End PmulI.
Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol :=
match P'' with
| Pc c => PmulC P c
| Pinj j' Q' => PmulI Pmul Q' j' P
| PX P' i' Q' =>
match P with
| Pc c => PmulC P'' c
| Pinj j Q =>
let QQ' :=
match j with
| xH => Pmul Q Q'
| xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q'
| xI j => Pmul (Pinj (xO j) Q) Q'
end in
mkPX (Pmul P P') i' QQ'
| PX P i Q=>
let QQ' := Pmul Q Q' in
let PQ' := PmulI Pmul Q' xH P in
let QP' := Pmul (mkPinj xH Q) P' in
let PP' := Pmul P P' in
( mkPX (mkPX PP' i P0 ++ QP') i' P0 ) ++ mkPX PQ' i QQ'
end
end.
Notation "P ** P'" := (Pmul P P').
Fixpoint Psquare (P:Pol) : Pol :=
match P with
| Pc c => Pc (c *! c)
| Pinj j Q => Pinj j (Psquare Q)
| PX P i Q =>
let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in
let Q2 := Psquare Q in
let P2 := Psquare P in
mkPX (mkPX P2 i P0 ++ twoPQ) i Q2
end.
Monomial
Inductive Mon: Set :=
mon0: Mon
| zmon: positive -> Mon -> Mon
| vmon: positive -> Mon -> Mon.
Fixpoint Mphi(l:Env R) (M: Mon) {struct M} : R :=
match M with
mon0 => rI
| zmon j M1 => Mphi (jump j l) M1
| vmon i M1 =>
let x := hd 0 l in
let xi := pow_pos rmul x i in
( Mphi (tail l) M1 ) * xi
end.
Definition mkZmon j M :=
match M with mon0 => mon0 | _ => zmon j M end.
Definition zmon_pred j M :=
match j with xH => M | _ => mkZmon (Ppred j) M end.
Definition mkVmon i M :=
match M with
| mon0 => vmon i mon0
| zmon j m => vmon i (zmon_pred j m)
| vmon i' m => vmon (i + i') m
end.
Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol :=
match P, M with
_, mon0 => ( Pc cO , P )
| Pc _, _ => ( P , Pc cO )
| Pinj j1 P1, zmon j2 M1 =>
match (j1 ?= j2) Eq with
Eq => let (R,S) := MFactor P1 M1 in
( mkPinj j1 R , mkPinj j1 S )
| Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in
( mkPinj j1 R , mkPinj j1 S )
| Gt => ( P , Pc cO )
end
| Pinj _ _, vmon _ _ => ( P , Pc cO )
| PX P1 i Q1, zmon j M1 =>
let M2 := zmon_pred j M1 in
let (R1, S1) := MFactor P1 M in
let (R2, S2) := MFactor Q1 M2 in
( mkPX R1 i R2 , mkPX S1 i S2 )
| PX P1 i Q1, vmon j M1 =>
match (i ?= j) Eq with
Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
( mkPX R1 i Q1 , S1 )
| Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in
( mkPX R1 i Q1 , S1 )
| Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
( mkPX R1 i Q1 , mkPX S1 (i - j) (Pc cO))
end
end.
Definition POneSubst (P1: Pol) (M1: Mon) (P2: Pol): option Pol :=
let (Q1,R1) := MFactor P1 M1 in
match R1 with
(Pc c) => if c ?=! cO then None
else Some (Padd Q1 (Pmul P2 R1))
| _ => Some (Padd Q1 (Pmul P2 R1))
end.
Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
match POneSubst P1 M1 P2 with
Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end
| _ => P1
end.
Definition PNSubst (P1: Pol) (M1: Mon) (P2: Pol) (n: nat): option Pol :=
match POneSubst P1 M1 P2 with
Some P3 => match n with S n1 => Some (PNSubst1 P3 M1 P2 n1) | _ => None end
| _ => None
end.
Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}:
Pol :=
match LM1 with
cons ( M1 , P2 ) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n
| _ => P1
end.
Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol :=
match LM1 with
cons ( M1 , P2 ) LM2 =>
match PNSubst P1 M1 P2 n with
Some P3 => Some (PSubstL1 P3 LM2 n)
| None => PSubstL P1 LM2 n
end
| _ => None
end.
Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol :=
match PSubstL P1 LM1 n with
Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end
| _ => P1
end.
Evaluation of a polynomial towards R
Fixpoint Pphi(l:Env R) (P:Pol) {struct P} : R :=
match P with
| Pc c => [ c ]
| Pinj j Q => Pphi (jump j l) Q
| PX P i Q =>
let x := hd 0 l in
let xi := pow_pos rmul x i in
( Pphi l P ) * xi + ( Pphi (tail l) Q )
end.
Reserved Notation "P @ l " (at level 10, no associativity).
Notation "P @ l " := (Pphi l P).
Proofs
Lemma ZPminus_spec : forall x y,
match ZPminus x y with
| Z0 => x = y
| Zpos k => x = (y + k)%positive
| Zneg k => y = (x + k)%positive
end.
Lemma Peq_ok : forall P P',
( P ?== P' ) = true -> forall l, P@l == P'@ l.
Lemma Pphi0 : forall l, P0@l == 0.
Lemma env_morph : forall p e1 e2, (forall x, e1 x = e2 x) ->
p @ e1 = p @ e2.
Lemma Pjump_Pplus : forall P i j l, P @ ( jump (i + j) l ) = P @ ( jump j (jump i l)).
Lemma Pjump_xO_tail : forall P p l,
P @ ( jump (xO p) (tail l)) = P @ ( jump (xI p) l ).
Lemma Pjump_Pdouble_minus_one : forall P p l,
P @ ( jump (Pdouble_minus_one p) (tail l)) = P @ ( jump (xO p) l ).
Lemma Pphi1 : forall l, P1@l == 1.
Lemma mkPinj_ok : forall j l P, ( mkPinj j P )@ l == P@ ( jump j l ).
Let pow_pos_Pplus :=
pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).
Lemma mkPX_ok : forall l P i Q,
( mkPX P i Q )@ l == P@l *( pow_pos rmul (hd 0 l) i ) + Q@ ( tail l ).
Ltac Esimpl :=
repeat (progress (
match goal with
| |- context [P0@ ? l] => rewrite (Pphi0 l)
| |- context [P1@ ? l] => rewrite (Pphi1 l)
| |- context [( mkPinj ?j ?P )@? l] => rewrite (mkPinj_ok j l P)
| |- context [( mkPX ?P ?i ?Q )@? l] => rewrite (mkPX_ok l P i Q)
| |- context [[ cO ]] => rewrite (morph0 CRmorph)
| |- context [[ cI ]] => rewrite (morph1 CRmorph)
| |- context [[? x +! ? y ]] => rewrite ((morph_add CRmorph) x y)
| |- context [[? x *! ? y ]] => rewrite ((morph_mul CRmorph) x y)
| |- context [[? x -! ? y ]] => rewrite ((morph_sub CRmorph) x y)
| |- context [[ -! ? x ]] => rewrite ((morph_opp CRmorph) x)
end));
rsimpl; simpl.
Lemma PaddC_ok : forall c P l, ( PaddC P c )@ l == P@l + [ c ].
Lemma PsubC_ok : forall c P l, ( PsubC P c )@ l == P@l - [ c ].
Lemma PmulC_aux_ok : forall c P l, ( PmulC_aux P c )@ l == P@l * [ c ].
Lemma PmulC_ok : forall c P l, ( PmulC P c )@ l == P@l * [ c ].
Lemma Popp_ok : forall P l, ( -- P )@ l == - P@l.
Ltac Esimpl2 :=
Esimpl;
repeat (progress (
match goal with
| |- context [( PaddC ?P ?c )@? l] => rewrite (PaddC_ok c P l)
| |- context [( PsubC ?P ?c )@? l] => rewrite (PsubC_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 Padd_ok : forall P' P l, ( P ++ P' )@ l == P@l + P'@l.
Lemma Psub_ok : forall P' P l, ( P -- P' )@ l == P@l - P'@l.
Lemma PmulI_ok :
forall P',
(forall (P : Pol) (l : Env R), ( Pmul P P' ) @ l == P @ l * P' @ l) ->
forall (P : Pol) (p : positive) (l : Env R),
( PmulI Pmul P' p P ) @ l == P @ l * P' @ ( jump p l ).
Lemma Pmul_ok : forall P P' l, ( P ** P' )@ l == P@l * P'@l.
Lemma Psquare_ok : forall P l, ( Psquare P )@ l == P@l * P@l.
Lemma Mphi_morph : forall P env env', (forall x, env x = env' x ) ->
Mphi env P = Mphi env' P.
Lemma Mjump_xO_tail : forall M p l,
Mphi (jump (xO p) (tail l)) M = Mphi (jump (xI p) l) M.
Lemma Mjump_Pdouble_minus_one : forall M p l,
Mphi (jump (Pdouble_minus_one p) (tail l)) M = Mphi (jump (xO p) l) M.
Lemma Mjump_Pplus : forall M i j l, Mphi (jump (i + j) l ) M = Mphi (jump j (jump i l)) M.
Lemma mkZmon_ok: forall M j l,
Mphi l (mkZmon j M) == Mphi l (zmon j M).
Lemma zmon_pred_ok : forall M j l,
Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M).
Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M * pow_pos rmul (hd 0 l) i.
Lemma Mphi_ok: forall P M l,
let (Q,R) := MFactor P M in
P@l == Q@l + ( Mphi l M ) * ( R@l ).
Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
Lemma PNSubst1_ok: forall n P1 M1 P2 l,
Mphi l M1 == P2@l -> P1@l == ( PNSubst1 P1 M1 P2 n )@ l.
Lemma PNSubst_ok: forall n P1 M1 P2 l P3,
PNSubst P1 M1 P2 n = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
Fixpoint MPcond (LM1: list (Mon * Pol)) (l: Env R) {struct LM1} : Prop :=
match LM1 with
cons ( M1 , P2 ) LM2 => ( Mphi l M1 == P2@l ) /\ ( MPcond LM2 l )
| _ => True
end.
Lemma PSubstL1_ok: forall n LM1 P1 l,
MPcond LM1 l -> P1@l == ( PSubstL1 P1 LM1 n )@ l.
Lemma PSubstL_ok: forall n LM1 P1 P2 l,
PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l.
Lemma PNSubstL_ok: forall m n LM1 P1 l,
MPcond LM1 l -> P1@l == ( PNSubstL P1 LM1 m n )@ l.
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.
evaluation of polynomial expressions towards R
Definition mk_X j := mkPinj_pred j mkX.
evaluation of polynomial expressions towards R
Fixpoint PEeval (l:Env R) (pe:PExpr) {struct pe} : R :=
match pe with
| PEc c => phi c
| PEX j => nth 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.
Correctness proofs
Lemma mkX_ok : forall p l, nth p l == ( mk_X p ) @ l.
Ltac Esimpl3 :=
repeat match goal with
| |- context [(? P1 ++ ? P2 )@? l] => rewrite (Padd_ok P2 P1 l)
| |- context [(? P1 -- ? P2 )@? l] => rewrite (Psub_ok P2 P1 l)
end;Esimpl2;try rrefl;try apply (ARadd_comm ARth).
Section POWER.
Variable subst_l : Pol -> Pol.
Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
match p with
| xH => subst_l (Pmul res P)
| xO p => Ppow_pos (Ppow_pos res P p) P p
| xI p => subst_l (Pmul (Ppow_pos (Ppow_pos res P p) P p) P)
end.
Definition Ppow_N P n :=
match n with
| N0 => P1
| Npos p => Ppow_pos P1 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 == res@l * ( pow_pos Pmul P p )@ l.
Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) ->
forall P n, ( Ppow_N P n )@ l == ( pow_N P1 Pmul P n )@ l.
End POWER.
Normalization and rewriting
Section NORM_SUBST_REC.
Variable n : nat.
Variable lmp:list (Mon * Pol).
Let subst_l P := PNSubstL P lmp n n.
Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
Let Ppow_subst := Ppow_N subst_l.
Fixpoint norm_aux (pe:PExpr) : Pol :=
match pe with
| PEc c => Pc c
| PEX j => mk_X j
| PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1)
| 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.
End NORM_SUBST_REC.
End MakeRingPol.