Library Coq.micromega.EnvRing
Definition of polynomial expressions
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 MFactor (
P:
Pol) (
M:
Mon) :
Pol * Pol :=
match P,
M with
_,
mon0 =>
(Pc cO, P)
|
Pc _,
_ =>
(P, Pc cO)
|
Pinj j1 P1,
zmon j2 M1 =>
match (
j1 ?= j2)
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)
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) :
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) :
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) :
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) :
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
Ltac destr_pos_sub :=
match goal with |-
context [
Z.pos_sub ?
x ?
y] =>
generalize (
Z.pos_sub_discr x y);
destruct (
Z.pos_sub x y)
end.
Lemma Peq_ok P P' :
(P ?== P') = true -> forall l,
P@l == P'@ l.
Lemma Peq_spec P P' :
BoolSpec (
forall l,
P@l == P'@l)
True (
P ?== P').
Lemma Pphi0 l :
P0@l == 0.
Lemma Pphi1 l :
P1@l == 1.
Lemma env_morph p e1 e2 :
(forall x,
e1 x = e2 x) -> p @ e1 = p @ e2.
Lemma Pjump_add P i j l :
P @ (jump (
i + j)
l) = P @ (jump j (
jump i l)
).
Lemma Pjump_xO_tail P p l :
P @ (jump (
xO p) (
tail l)
) = P @ (jump (
xI p)
l).
Lemma Pjump_pred_double P p l :
P @ (jump (
Pos.pred_double p) (
tail l)
) = P @ (jump (
xO p)
l).
Lemma mkPinj_ok j l P :
(mkPinj j P)@l == P@(jump j l).
Lemma pow_pos_add x i j :
x^(j + i) == x^i * x^j.
Lemma ceqb_spec c c' :
BoolSpec (
[c] == [c'])
True (
c ?=! c').
Lemma mkPX_ok l P i Q :
(mkPX P i Q)@l == P@l * (hd l)^i + Q@(tail l).
Hint Rewrite
Pphi0
Pphi1
mkPinj_ok
mkPX_ok
(
morph0 CRmorph)
(
morph1 CRmorph)
(
morph0 CRmorph)
(
morph_add CRmorph)
(
morph_mul CRmorph)
(
morph_sub CRmorph)
(
morph_opp CRmorph)
:
Esimpl.
Ltac Esimpl :=
try rewrite_db Esimpl;
rsimpl;
simpl.
Lemma PaddC_ok c P l :
(PaddC P c)@l == P@l + [c].
Lemma PsubC_ok c P l :
(PsubC P c)@l == P@l - [c].
Lemma PmulC_aux_ok c P l :
(PmulC_aux P c)@l == P@l * [c].
Lemma PmulC_ok c P l :
(PmulC P c)@l == P@l * [c].
Lemma Popp_ok P l :
(--P)@l == - P@l.
Hint Rewrite PaddC_ok PsubC_ok PmulC_ok Popp_ok :
Esimpl.
Lemma PaddX_ok P' P k l :
(forall P l,
(P++P')@l == P@l + P'@l) ->
(PaddX Padd P' k P) @ l == P@l + P'@l * (hd l)^k.
Lemma Padd_ok P' P l :
(P ++ P')@l == P@l + P'@l.
Lemma PsubX_ok P' P k l :
(forall P l,
(P--P')@l == P@l - P'@l) ->
(PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k.
Lemma Psub_ok P' P l :
(P -- P')@l == P@l - P'@l.
Lemma PmulI_ok P' :
(forall P l,
(Pmul P P') @ l == P @ l * P' @ l) ->
forall P p l,
(PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
Lemma Pmul_ok P P' l :
(P**P')@l == P@l * P'@l.
Lemma Psquare_ok P l :
(Psquare P)@l == P@l * P@l.
Lemma Mphi_morph M e1 e2 :
(forall x,
e1 x = e2 x) -> M @@ e1 = M @@ e2.
Lemma Mjump_xO_tail M p l :
M @@ (jump (
xO p) (
tail l)
) = M @@ (jump (
xI p)
l).
Lemma Mjump_pred_double M p l :
M @@ (jump (
Pos.pred_double p) (
tail l)
) = M @@ (jump (
xO p)
l).
Lemma Mjump_add M i j l :
M @@ (jump (
i + j)
l) = M @@ (jump j (
jump i l)
).
Lemma mkZmon_ok M j l :
(mkZmon j M) @@ l == (zmon j M) @@ l.
Lemma zmon_pred_ok M j l :
(zmon_pred j M) @@ (tail l) == (zmon j M) @@ l.
Lemma mkVmon_ok M i l :
(mkVmon i M)@@l == M@@l * (hd l)^i.
Ltac destr_mfactor R S :=
match goal with
|
H :
context [
MFactor ?
P _] |-
context [
MFactor ?
P ?
M] =>
specialize (
H M);
destruct MFactor as (
R,
S)
end.
Lemma Mphi_ok P M l :
let (
Q,
R) :=
MFactor P M in
P@l == Q@l + M@@l * R@l.
Lemma POneSubst_ok P1 M1 P2 P3 l :
POneSubst P1 M1 P2 = Some P3 -> M1@@l == P2@l ->
P1@l == P3@l.
Lemma PNSubst1_ok n P1 M1 P2 l :
M1@@l == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
Lemma PNSubst_ok n P1 M1 P2 l P3 :
PNSubst P1 M1 P2 n = Some P3 -> M1@@l == P2@l -> P1@l == P3@l.
Fixpoint MPcond (
LM1:
list (
Mon * Pol)) (
l:
Env R) :
Prop :=
match LM1 with
|
cons (M1,P2) LM2 =>
(M1@@l == P2@l) /\ MPcond LM2 l
|
_ =>
True
end.
Lemma PSubstL1_ok n LM1 P1 l :
MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l.
Lemma PSubstL_ok n LM1 P1 P2 l :
PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l.
Lemma PNSubstL_ok m n LM1 P1 l :
MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l.
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.