Library Coq.setoid_ring.Ring_polynom
Opposite of addition
Addition et subtraction
Multiplication
Monomial
A monomial is X1^k1...Xi^ki. Its representation
is a simplified version of the polynomial representation:
- mon0 correspond to the polynom P1.
- (zmon j M) corresponds to (Pinj j ...),
i.e. skip j variable indices.
- (vmon i M) is X^i*M with X the current variable,
its corresponds to (PX P1 i ...)]
Inductive Mon:
Set :=
|
mon0:
Mon
|
zmon:
positive -> Mon -> Mon
|
vmon:
positive -> Mon -> Mon.
Definition mkZmon j M :=
match M with mon0 =>
mon0 |
_ =>
zmon j M end.
Definition zmon_pred j M :=
match j with xH =>
M |
_ =>
mkZmon (
Pos.pred 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 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 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) :
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) :
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) :
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) :
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
Evaluation of a monomial towards R
Proofs
Definition of polynomial expressions
evaluation of polynomial expressions towards R
evaluation of polynomial expressions towards R
Correctness proofs
Normalization and rewriting
Internally, norm_aux is expanded in a large number of cases.
To speed-up proofs, we use an alternative definition.
Definition get_PEopp pe :=
match pe with
|
PEopp pe' =>
Some pe'
|
_ =>
None
end.
Lemma norm_aux_PEadd pe1 pe2 :
norm_aux (
PEadd pe1 pe2)
=
match get_PEopp pe1,
get_PEopp pe2 with
|
Some pe1',
_ =>
(norm_aux pe2) -- (norm_aux pe1')
|
None,
Some pe2' =>
(norm_aux pe1) -- (norm_aux pe2')
|
None,
None =>
(norm_aux pe1) ++ (norm_aux pe2)
end.
Lemma norm_aux_PEopp pe :
match get_PEopp pe with
|
Some pe' =>
norm_aux pe = -- (norm_aux pe')
|
None =>
True
end.
Lemma norm_aux_spec l pe :
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 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 fv)
n lm)
|
PX P i Q =>
let rP :=
add_mult_dev rP P fv (
N.add (
Npos i)
n)
lm in
if Q ?== P0 then rP
else add_mult_dev rP Q (
tail fv)
N0 (
add_pow_list (
hd 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 fv)
n lm)
|
Pinj j Q =>
mult_dev Q (
jump j fv)
N0 (
add_pow_list (
hd fv)
n lm)
|
PX P i Q =>
let rP :=
mult_dev P fv (
N.add (
Npos i)
n)
lm in
if Q ?== P0 then rP
else
let lmq :=
add_pow_list (
hd 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 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 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 r p :
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 (
Pos.pred_double 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 (
Pos.pred_double p)
|
xI p =>
mkmult_pow (
-x)
x (
xO p)
end.
Definition Pphi_dev :=
Pphi_avoid mkpow mkopp_pow mkmult_pow.
Lemma mkmult_pow_ok p r x :
mkmult_pow r x p == r * x^p.
Lemma mkpow_ok p x :
mkpow x p == x^p.
Lemma mkopp_pow_ok p x :
mkopp_pow x p == - 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.