Library Coq.micromega.EnvRing
Opposite of addition
Addition et subtraction
Multiplication
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
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
evaluation of polynomial expressions towards R
evaluation of polynomial expressions towards R
Correctness proofs
Normalization and rewriting