Library Coq.setoid_ring.Ring_polynom
Opposite of addition
Addition et subtraction
Multiplication
Monomial
Inductive Mon:
Set :=
mon0:
Mon
|
zmon:
positive ->
Mon ->
Mon
|
vmon:
positive ->
Mon ->
Mon.
Fixpoint Mphi(
l:
list 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 CFactor (
P:
Pol) (
c:
C) {
struct P}:
Pol * Pol :=
match P with
|
Pc c1 =>
let (
q,
r) :=
cdiv c1 c in (Pc r, Pc q)
|
Pinj j1 P1 =>
let (
R,
S) :=
CFactor P1 c in
(mkPinj j1 R, mkPinj j1 S)
|
PX P1 i Q1 =>
let (
R1,
S1) :=
CFactor P1 c in
let (
R2,
S2) :=
CFactor Q1 c in
(mkPX R1 i R2, mkPX S1 i S2)
end.
Fixpoint MFactor (
P:
Pol) (
c:
C) (
M:
Mon) {
struct P}:
Pol * Pol :=
match P,
M with
_,
mon0 =>
if (
ceqb c cI)
then (Pc cO, P) else
CFactor P c
|
Pc _,
_ =>
(P, Pc cO)
|
Pinj j1 P1,
zmon j2 M1 =>
match (
j1 ?= j2)
Eq with
Eq =>
let (
R,
S) :=
MFactor P1 c M1 in
(mkPinj j1 R, mkPinj j1 S)
|
Lt =>
let (
R,
S) :=
MFactor P1 c (
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 c M in
let (
R2,
S2) :=
MFactor Q1 c 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 c (
mkZmon xH M1)
in
(mkPX R1 i Q1, S1)
|
Lt =>
let (
R1,
S1) :=
MFactor P1 c (
vmon (
j - i)
M1)
in
(mkPX R1 i Q1, S1)
|
Gt =>
let (
R1,
S1) :=
MFactor P1 c (
mkZmon xH M1)
in
(mkPX R1 i Q1, mkPX S1 (
i-j) (
Pc cO)
)
end
end.
Definition POneSubst (
P1:
Pol) (
cM1:
C * Mon) (
P2:
Pol):
option Pol :=
let (
c,
M1) :=
cM1 in
let (
Q1,
R1) :=
MFactor P1 c 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) (
cM1:
C * Mon) (
P2:
Pol) (
n:
nat) {
struct n}:
Pol :=
match POneSubst P1 cM1 P2 with
Some P3 =>
match n with S n1 =>
PNSubst1 P3 cM1 P2 n1 |
_ =>
P3 end
|
_ =>
P1
end.
Definition PNSubst (
P1:
Pol) (
cM1:
C * Mon) (
P2:
Pol) (
n:
nat):
option Pol :=
match POneSubst P1 cM1 P2 with
Some P3 =>
match n with S n1 =>
Some (
PNSubst1 P3 cM1 P2 n1) |
_ =>
None end
|
_ =>
None
end.
Fixpoint PSubstL1 (
P1:
Pol) (
LM1:
list (
(C * 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 (
(C * 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 (
(C * 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
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 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 [?
P@?l] =>
match P with
|
P0 =>
rewrite (
Pphi0 l)
|
P1 =>
rewrite (
Pphi1 l)
| (
mkPinj ?
j ?
P) =>
rewrite (
mkPinj_ok j l P)
| (
mkPX ?
P ?
i ?
Q) =>
rewrite (
mkPX_ok l P i Q)
end
| |-
context [
[?c]] =>
match c with
|
cO =>
rewrite (
morph0 CRmorph)
|
cI =>
rewrite (
morph1 CRmorph)
| ?
x +! ?y =>
rewrite ((
morph_add CRmorph)
x y)
| ?
x *! ?y =>
rewrite ((
morph_mul CRmorph)
x y)
| ?
x -! ?y =>
rewrite ((
morph_sub CRmorph)
x y)
|
-! ?x =>
rewrite ((
morph_opp CRmorph)
x)
end
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 :
list R),
(Pmul P P') @ l == P @ l * P' @ l) ->
forall (
P :
Pol) (
p :
positive) (
l :
list 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 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 Mcphi_ok:
forall P c l,
let (
Q,
R) :=
CFactor P c in
P@l == Q@l + (phi c) * (R@l).
Lemma Mphi_ok:
forall P (
cM:
C * Mon)
l,
let (
c,
M) :=
cM in
let (
Q,
R) :=
MFactor P c M in
P@l == Q@l + (phi c) * (Mphi l M) * (R@l).
Lemma POneSubst_ok:
forall P1 M1 P2 P3 l,
POneSubst P1 M1 P2 = Some P3 ->
phi (
fst M1)
* Mphi l (
snd M1)
== P2@l ->
P1@l == P3@l.
Lemma PNSubst1_ok:
forall n P1 M1 P2 l,
[fst M1] * Mphi l (
snd 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 ->
[fst M1] * Mphi l (
snd M1)
== P2@l ->
P1@l == P3@l.
Fixpoint MPcond (
LM1:
list (
C * Mon * Pol)) (
l:
list R) {
struct LM1} :
Prop :=
match LM1 with
cons (M1,P2) LM2 =>
([fst M1] * Mphi l (
snd 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
evaluation of polynomial expressions towards R
evaluation of polynomial expressions towards R
Correctness proofs
Normalization and rewriting
Section NORM_SUBST_REC.
Variable n :
nat.
Variable lmp:
list (
C*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,
MPcond lmp l ->
PEeval l pe == (norm_aux pe)@l.
Lemma norm_subst_spec :
forall l pe,
MPcond lmp l ->
PEeval l pe == (norm_subst pe)@l.
End NORM_SUBST_REC.
Fixpoint interp_PElist (
l:
list R) (
lpe:
list (
PExpr*PExpr)) {
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.
Fixpoint mon_of_pol (
P:
Pol) :
option (
C * Mon) :=
match P with
|
Pc c =>
if (
c ?=! cO)
then None else Some (c, mon0)
|
Pinj j P =>
match mon_of_pol P with
|
None =>
None
|
Some (c,m) =>
Some (c, mkZmon j m)
end
|
PX P i Q =>
if Peq Q P0 then
match mon_of_pol P with
|
None =>
None
|
Some (c,m) =>
Some (c, mkVmon i m)
end
else None
end.
Fixpoint mk_monpol_list (
lpe:
list (
PExpr * PExpr)) :
list (
C*Mon*Pol) :=
match lpe with
|
nil =>
nil
|
(me,pe)::lpe =>
match mon_of_pol (
norm_subst 0
nil me)
with
|
None =>
mk_monpol_list lpe
|
Some m =>
(m,norm_subst 0
nil pe):: mk_monpol_list lpe
end
end.
Lemma mon_of_pol_ok :
forall P m,
mon_of_pol P = Some m ->
forall l,
[fst m] * Mphi l (
snd m)
== P@l.
Lemma interp_PElist_ok :
forall l lpe,
interp_PElist l lpe ->
MPcond (
mk_monpol_list lpe)
l.
Lemma norm_subst_ok :
forall n l lpe pe,
interp_PElist l lpe ->
PEeval l pe == (norm_subst n (
mk_monpol_list lpe)
pe)@l.
Lemma ring_correct :
forall n l lpe pe1 pe2,
interp_PElist l lpe ->
(let lmp :=
mk_monpol_list lpe in
norm_subst n lmp pe1 ?== norm_subst n lmp pe2) = true ->
PEeval l pe1 == PEeval l pe2.
Generic evaluation of polynomial towards R avoiding parenthesis
Variable get_sign :
C ->
option C.
Variable get_sign_spec :
sign_theory copp ceqb get_sign.
Section EVALUATION.
Variable mkpow :
R ->
positive ->
R.
Variable mkopp_pow :
R ->
positive ->
R.
Variable mkmult_pow :
R ->
R ->
positive ->
R.
Fixpoint mkmult_rec (
r:
R) (
lm:
list (
R*positive)) {
struct lm}:
R :=
match lm with
|
nil =>
r
|
cons (x,p) t =>
mkmult_rec (
mkmult_pow r x p)
t
end.
Definition mkmult1 lm :=
match lm with
|
nil => 1
|
cons (x,p) t =>
mkmult_rec (
mkpow x p)
t
end.
Definition mkmultm1 lm :=
match lm with
|
nil =>
ropp rI
|
cons (x,p) t =>
mkmult_rec (
mkopp_pow x p)
t
end.
Definition mkmult_c_pos c lm :=
if c ?=! cI then mkmult1 (
rev' lm)
else mkmult_rec [c] (
rev' lm).
Definition mkmult_c c lm :=
match get_sign c with
|
None =>
mkmult_c_pos c lm
|
Some c' =>
if c' ?=! cI then mkmultm1 (
rev' lm)
else mkmult_rec [c] (
rev' lm)
end.
Definition mkadd_mult rP c lm :=
match get_sign c with
|
None =>
rP + mkmult_c_pos c lm
|
Some c' =>
rP - mkmult_c_pos c' lm
end.
Definition add_pow_list (
r:
R)
n l :=
match n with
|
N0 =>
l
|
Npos p =>
(r,p)::l
end.
Fixpoint add_mult_dev
(
rP:
R) (
P:
Pol) (
fv:
list R) (
n:
N) (
lm:
list (
R*positive)) {
struct P} :
R :=
match P with
|
Pc c =>
let lm :=
add_pow_list (
hd 0
fv)
n lm in
mkadd_mult rP c lm
|
Pinj j Q =>
add_mult_dev rP Q (
jump j fv)
N0 (
add_pow_list (
hd 0
fv)
n lm)
|
PX P i Q =>
let rP :=
add_mult_dev rP P fv (
Nplus (
Npos i)
n)
lm in
if Q ?== P0 then rP
else add_mult_dev rP Q (
tail fv)
N0 (
add_pow_list (
hd 0
fv)
n lm)
end.
Fixpoint mult_dev (
P:
Pol) (
fv :
list R) (
n:
N)
(
lm:
list (
R*positive)) {
struct P} :
R :=
match P with
|
Pc c =>
mkmult_c c (
add_pow_list (
hd 0
fv)
n lm)
|
Pinj j Q =>
mult_dev Q (
jump j fv)
N0 (
add_pow_list (
hd 0
fv)
n lm)
|
PX P i Q =>
let rP :=
mult_dev P fv (
Nplus (
Npos i)
n)
lm in
if Q ?== P0 then rP
else
let lmq :=
add_pow_list (
hd 0
fv)
n lm in
add_mult_dev rP Q (
tail fv)
N0 lmq
end.
Definition Pphi_avoid fv P :=
mult_dev P fv N0 nil.
Fixpoint r_list_pow (
l:
list (
R*positive)) :
R :=
match l with
|
nil =>
rI
|
cons (r,p) l =>
pow_pos rmul r p * r_list_pow l
end.
Hypothesis mkpow_spec :
forall r p,
mkpow r p == pow_pos rmul r p.
Hypothesis mkopp_pow_spec :
forall r p,
mkopp_pow r p == - (pow_pos rmul r p).
Hypothesis mkmult_pow_spec :
forall r x p,
mkmult_pow r x p == r * pow_pos rmul x p.
Lemma mkmult_rec_ok :
forall lm r,
mkmult_rec r lm == r * r_list_pow lm.
Lemma mkmult1_ok :
forall lm,
mkmult1 lm == r_list_pow lm.
Lemma mkmultm1_ok :
forall lm,
mkmultm1 lm == - r_list_pow lm.
Lemma r_list_pow_rev :
forall l,
r_list_pow (
rev' l)
== r_list_pow l.
Lemma mkmult_c_pos_ok :
forall c lm,
mkmult_c_pos c lm == [c]* r_list_pow lm.
Lemma mkmult_c_ok :
forall c lm,
mkmult_c c lm == [c] * r_list_pow lm.
Lemma mkadd_mult_ok :
forall rP c lm,
mkadd_mult rP c lm == rP + [c]*r_list_pow lm.
Lemma add_pow_list_ok :
forall r n l,
r_list_pow (
add_pow_list r n l)
== pow_N rI rmul r n * r_list_pow l.
Lemma add_mult_dev_ok :
forall P rP fv n lm,
add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (
hd 0
fv)
n * r_list_pow lm.
Lemma mult_dev_ok :
forall P fv n lm,
mult_dev P fv n lm == P@fv * pow_N rI rmul (
hd 0
fv)
n * r_list_pow lm.
Lemma Pphi_avoid_ok :
forall P fv,
Pphi_avoid fv P == P@fv.
End EVALUATION.
Definition Pphi_pow :=
let mkpow x p :=
match p with xH =>
x |
_ =>
rpow x (
Cp_phi (
Npos p))
end in
let mkopp_pow x p :=
ropp (
mkpow x p)
in
let mkmult_pow r x p :=
rmul r (
mkpow x p)
in
Pphi_avoid mkpow mkopp_pow mkmult_pow.
Lemma local_mkpow_ok :
forall (
r :
R) (
p :
positive),
match p with
|
xI _ =>
rpow r (
Cp_phi (
Npos p))
|
xO _ =>
rpow r (
Cp_phi (
Npos p))
| 1 =>
r
end == pow_pos rmul r p.
Lemma Pphi_pow_ok :
forall P fv,
Pphi_pow fv P == P@fv.
Lemma ring_rw_pow_correct :
forall n lH l,
interp_PElist l lH ->
forall lmp,
mk_monpol_list lH = lmp ->
forall pe npe,
norm_subst n lmp pe = npe ->
PEeval l pe == Pphi_pow l npe.
Fixpoint mkmult_pow (
r x:
R) (
p:
positive) {
struct p} :
R :=
match p with
|
xH =>
r*x
|
xO p =>
mkmult_pow (
mkmult_pow r x p)
x p
|
xI p =>
mkmult_pow (
mkmult_pow (
r*x)
x p)
x p
end.
Definition mkpow x p :=
match p with
|
xH =>
x
|
xO p =>
mkmult_pow x x (
Pdouble_minus_one p)
|
xI p =>
mkmult_pow x x (
xO p)
end.
Definition mkopp_pow x p :=
match p with
|
xH =>
-x
|
xO p =>
mkmult_pow (
-x)
x (
Pdouble_minus_one p)
|
xI p =>
mkmult_pow (
-x)
x (
xO p)
end.
Definition Pphi_dev :=
Pphi_avoid mkpow mkopp_pow mkmult_pow.
Lemma mkmult_pow_ok :
forall p r x,
mkmult_pow r x p == r*pow_pos rmul x p.
Lemma mkpow_ok :
forall p x,
mkpow x p == pow_pos rmul x p.
Lemma mkopp_pow_ok :
forall p x,
mkopp_pow x p == - pow_pos rmul x p.
Lemma Pphi_dev_ok :
forall P fv,
Pphi_dev fv P == P@fv.
Lemma ring_rw_correct :
forall n lH l,
interp_PElist l lH ->
forall lmp,
mk_monpol_list lH = lmp ->
forall pe npe,
norm_subst n lmp pe = npe ->
PEeval l pe == Pphi_dev l npe.
End MakeRingPol.