Library Coq.setoid_ring.Ncring_polynom
Set Implicit Arguments.
Require Import Setoid.
Require Import BinList.
Require Import BinPos.
Require Import BinNat.
Require Import BinInt.
Require Export Ring_polynom.
Require Export Ncring.
Section MakeRingPol.
Context (
C R:
Type) `{
Rh:
Ring_morphism C R}.
Variable phiCR_comm:
forall (
c:
C)(
x:
R),
x * [c] == [c] * x.
Ltac rsimpl :=
repeat (
gen_rewrite ||
rewrite phiCR_comm).
Ltac add_push :=
gen_add_push .
Inductive Pol :
Type :=
|
Pc :
C -> Pol
|
PX :
Pol -> positive -> positive -> Pol -> Pol.
Definition cO:
C .
Definition cI:
C .
Definition P0 :=
Pc 0.
Definition P1 :=
Pc 1.
Variable Ceqb:
C->C->bool.
#[
universes(
template)]
Class Equalityb (
A :
Type):= {
equalityb :
A -> A -> bool}.
Notation "x =? y" := (
equalityb x y) (
at level 70,
no associativity).
Variable Ceqb_eq:
forall x y:
C,
Ceqb x y = true -> (x == y).
Instance equalityb_coef :
Equalityb C :=
{
equalityb x y :=
Ceqb x y}.
Fixpoint Peq (
P P' :
Pol) {
struct P'} :
bool :=
match P,
P' with
|
Pc c,
Pc c' =>
c =? c'
|
PX P i n Q,
PX P' i' n' Q' =>
match Pos.compare i i',
Pos.compare n n' with
|
Eq,
Eq =>
if Peq P P' then Peq Q Q' else false
|
_,
_ =>
false
end
|
_,
_ =>
false
end.
Instance equalityb_pol :
Equalityb Pol :=
{
equalityb x y :=
Peq x y}.
Definition mkPX P i n Q :=
match P with
|
Pc c =>
if c =? 0
then Q else PX P i n Q
|
PX P' i' n' Q' =>
match Pos.compare i i' with
|
Eq =>
if Q' =? P0 then PX P' i (
n + n')
Q else PX P i n Q
|
_ =>
PX P i n Q
end
end.
Definition mkXi i n :=
PX P1 i n P0.
Definition mkX i :=
mkXi i 1.
Opposite of addition
Addition et subtraction
Multiplication
Evaluation of a polynomial towards R
Proofs
Ltac destr_pos_sub H :=
match goal with |-
context [
Z.pos_sub ?
x ?
y] =>
assert (
H :=
Z.pos_sub_discr x y);
destruct (
Z.pos_sub x y)
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 mkPX_ok :
forall l P i n Q,
(mkPX P i n Q)@l == P@l * (pow_pos (
nth 0
i l)
n) + Q@l.
Ltac Esimpl :=
repeat (
progress (
match goal with
| |-
context [?
P@?
l] =>
match P with
|
P0 =>
rewrite (
Pphi0 l)
|
P1 =>
rewrite (
Pphi1 l)
| (
mkPX ?
P ?
i ?
n ?
Q) =>
rewrite (
mkPX_ok l P i n Q)
end
| |-
context [
[?
c]] =>
match c with
| 0 =>
rewrite ring_morphism0
| 1 =>
rewrite ring_morphism1
| ?
x + ?
y =>
rewrite ring_morphism_add
| ?
x * ?
y =>
rewrite ring_morphism_mul
| ?
x - ?
y =>
rewrite ring_morphism_sub
|
- ?
x =>
rewrite ring_morphism_opp
end
end));
simpl;
rsimpl.
Lemma PaddCl_ok :
forall c P l,
(PaddCl c P)@l == [c] + P@l .
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 [
(PaddCl ?
c ?
P)@?
l] =>
rewrite (
PaddCl_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 PaddXPX:
forall P i n Q,
PaddX Padd P i n Q =
match Q with
|
Pc c =>
mkPX P i n Q
|
PX P' i' n' Q' =>
match Pos.compare i i' with
|
Gt =>
mkPX P i n Q
|
Lt =>
mkPX P' i' n' (
PaddX Padd P i n Q')
|
Eq =>
match Z.pos_sub n n' with
|
Zpos k =>
mkPX (
PaddX Padd P i k P')
i' n' Q'
|
Z0 =>
mkPX (
Padd P P')
i n Q'
|
Zneg k =>
mkPX (
Padd P (
mkPX P' i k P0))
i n Q'
end
end
end.
Lemma PaddX_ok2 :
forall P2,
(forall P l,
(P2 ++ P) @ l == P2 @ l + P @ l)
/\
(forall P k n l,
(PaddX Padd P2 k n P) @ l ==
P2 @ l * pow_pos (
nth 0
k l)
n + P @ l).
Lemma Padd_ok :
forall P Q l,
(P ++ Q) @ l == P @ l + Q @ l.
Lemma PaddX_ok :
forall P2 P k n l,
(PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (
nth 0
k l)
n + P @ l.
Lemma Psub_ok :
forall P' P l,
(P -- P')@l == P@l - 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.
Definition of polynomial expressions
Specification of the power function
evaluation of polynomial expressions towards R
Correctness proofs
Normalization and rewriting