Library Coq.setoid_ring.Field_theory
Require Ring.
Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms.
Require Import ZArith_base.
Set Implicit Arguments.
Section MakeFieldPol.
Variable R:
Type.
Delimit Scope R_scope with ring.
Local Open Scope R_scope.
Variable (
rO rI :
R) (
radd rmul rsub:
R->R->R) (
ropp :
R->R).
Variable (
rdiv :
R->R->R) (
rinv :
R->R).
Variable req :
R -> R -> Prop.
Notation "0" :=
rO :
R_scope.
Notation "1" :=
rI :
R_scope.
Infix "+" :=
radd :
R_scope.
Infix "-" :=
rsub :
R_scope.
Infix "*" :=
rmul :
R_scope.
Infix "/" :=
rdiv :
R_scope.
Notation "- x" := (
ropp x) :
R_scope.
Notation "/ x" := (
rinv x) :
R_scope.
Infix "==" :=
req (
at level 70,
no associativity) :
R_scope.
Variable Rsth :
Equivalence req.
Variable Reqe :
ring_eq_ext radd rmul ropp req.
Variable SRinv_ext :
forall p q,
p == q -> / p == / q.
Record almost_field_theory :
Prop :=
mk_afield {
AF_AR :
almost_ring_theory rO rI radd rmul rsub ropp req;
AF_1_neq_0 :
~ 1
== 0;
AFdiv_def :
forall p q,
p / q == p * / q;
AFinv_l :
forall p,
~ p == 0
-> / p * p == 1
}.
Section AlmostField.
Variable AFth :
almost_field_theory.
Let ARth := (
AF_AR AFth).
Let rI_neq_rO := (
AF_1_neq_0 AFth).
Let rdiv_def := (
AFdiv_def AFth).
Let rinv_l := (
AFinv_l AFth).
Add Morphism radd with signature (
req ==> req ==> req)
as radd_ext.
Add Morphism rmul with signature (
req ==> req ==> req)
as rmul_ext.
Add Morphism ropp with signature (
req ==> req)
as ropp_ext.
Add Morphism rsub with signature (
req ==> req ==> req)
as rsub_ext.
Add Morphism rinv with signature (
req ==> req)
as rinv_ext.
Let eq_trans :=
Setoid.Seq_trans _ _ Rsth.
Let eq_sym :=
Setoid.Seq_sym _ _ Rsth.
Let eq_refl :=
Setoid.Seq_refl _ _ Rsth.
Let radd_0_l :=
ARadd_0_l ARth.
Let radd_comm :=
ARadd_comm ARth.
Let radd_assoc :=
ARadd_assoc ARth.
Let rmul_1_l :=
ARmul_1_l ARth.
Let rmul_0_l :=
ARmul_0_l ARth.
Let rmul_comm :=
ARmul_comm ARth.
Let rmul_assoc :=
ARmul_assoc ARth.
Let rdistr_l :=
ARdistr_l ARth.
Let ropp_mul_l :=
ARopp_mul_l ARth.
Let ropp_add :=
ARopp_add ARth.
Let rsub_def :=
ARsub_def ARth.
Let radd_0_r :=
ARadd_0_r Rsth ARth.
Let rmul_0_r :=
ARmul_0_r Rsth ARth.
Let rmul_1_r :=
ARmul_1_r Rsth ARth.
Let ropp_0 :=
ARopp_zero Rsth Reqe ARth.
Let rdistr_r :=
ARdistr_r Rsth Reqe ARth.
Variable C:
Type.
Delimit Scope C_scope with coef.
Variable (
cO cI:
C) (
cadd cmul csub :
C->C->C) (
copp :
C->C).
Variable ceqb :
C->C->bool.
Variable phi :
C -> R.
Variable CRmorph :
ring_morph rO rI radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
Notation "0" :=
cO :
C_scope.
Notation "1" :=
cI :
C_scope.
Infix "+" :=
cadd :
C_scope.
Infix "-" :=
csub :
C_scope.
Infix "*" :=
cmul :
C_scope.
Notation "- x" := (
copp x) :
C_scope.
Infix "=?" :=
ceqb :
C_scope.
Notation "[ x ]" := (
phi x) (
at level 0).
Let phi_0 := (
morph0 CRmorph).
Let phi_1 := (
morph1 CRmorph).
Lemma ceqb_spec c c' :
BoolSpec (
[c] == [c'])
True (
c =? c')%
coef.
Variable Cpow :
Type.
Variable Cp_phi :
N -> Cpow.
Variable rpow :
R -> Cpow -> R.
Variable pow_th :
power_theory rI rmul req Cp_phi rpow.
Variable get_sign :
C -> option C.
Variable get_sign_spec :
sign_theory copp ceqb get_sign.
Variable cdiv:
C -> C -> C*C.
Variable cdiv_th :
div_theory req cadd cmul phi cdiv.
Let rpow_pow := (
rpow_pow_N pow_th).
Delimit Scope PE_scope with poly.
Notation NPEeval := (
PEeval rO rI radd rmul rsub ropp phi Cp_phi rpow).
Notation "P @ l" := (
NPEeval l P) (
at level 10,
no associativity).
Notation "0" := (
PEc 0) :
PE_scope.
Notation "1" := (
PEc 1) :
PE_scope.
Infix "+" :=
PEadd :
PE_scope.
Infix "-" :=
PEsub :
PE_scope.
Infix "*" :=
PEmul :
PE_scope.
Notation "- e" := (
PEopp e) :
PE_scope.
Infix "^" :=
PEpow :
PE_scope.
Definition NPEequiv e e' :=
forall l,
e@l == e'@l.
Infix "===" :=
NPEequiv (
at level 70,
no associativity) :
PE_scope.
Instance NPEequiv_eq :
Equivalence NPEequiv.
Instance NPEeval_ext :
Proper (
eq ==> NPEequiv ==> req)
NPEeval.
Notation Nnorm :=
(
norm_subst cO cI cadd cmul csub copp ceqb cdiv).
Notation NPphi_dev :=
(
Pphi_dev rO rI radd rmul rsub ropp cO cI ceqb phi get_sign).
Notation NPphi_pow :=
(
Pphi_pow rO rI radd rmul rsub ropp cO cI ceqb phi Cp_phi rpow get_sign).
Add Ring Rring : (
ARth_SRth ARth).
Lemma rsub_0_l r : 0
- r == - r.
Lemma rsub_0_r r :
r - 0
== r.
Theorem rdiv_simpl p q :
~ q == 0
-> q * (p / q) == p.
Instance rdiv_ext:
Proper (
req ==> req ==> req)
rdiv.
Lemma rmul_reg_l p q1 q2 :
~ p == 0
-> p * q1 == p * q2 -> q1 == q2.
Theorem field_is_integral_domain r1 r2 :
~ r1 == 0
-> ~ r2 == 0
-> ~ r1 * r2 == 0.
Theorem ropp_neq_0 r :
~ -(1)
== 0
-> ~ r == 0
-> ~ -r == 0.
Theorem rdiv_r_r r :
~ r == 0
-> r / r == 1.
Theorem rdiv1 r :
r == r / 1.
Theorem rdiv2 a b c d :
~ b == 0
->
~ d == 0
->
a / b + c / d == (a * d + c * b) / (b * d).
Theorem rdiv2b a b c d e :
~ (b*e) == 0
->
~ (d*e) == 0
->
a / (b*e) + c / (d*e) == (a * d + c * b) / (b * (d * e)).
Theorem rdiv5 a b :
- (a / b) == - a / b.
Theorem rdiv3b a b c d e :
~ (b * e) == 0
->
~ (d * e) == 0
->
a / (b*e) - c / (d*e) == (a * d - c * b) / (b * (d * e)).
Theorem rdiv6 a b :
~ a == 0
-> ~ b == 0
-> / (a / b) == b / a.
Theorem rdiv4 a b c d :
~ b == 0
->
~ d == 0
->
(a / b) * (c / d) == (a * c) / (b * d).
Theorem rdiv4b a b c d e f :
~ b * e == 0
->
~ d * f == 0
->
((a * f) / (b * e)) * ((c * e) / (d * f)) == (a * c) / (b * d).
Theorem rdiv7 a b c d :
~ b == 0
->
~ c == 0
->
~ d == 0
->
(a / b) / (c / d) == (a * d) / (b * c).
Theorem rdiv7b a b c d e f :
~ b * f == 0
->
~ c * e == 0
->
~ d * f == 0
->
((a * e) / (b * f)) / ((c * e) / (d * f)) == (a * d) / (b * c).
Theorem rinv_nz a :
~ a == 0
-> ~ /a == 0.
Theorem rdiv8 a b :
~ b == 0
-> a == 0
-> a / b == 0.
Theorem cross_product_eq a b c d :
~ b == 0
-> ~ d == 0
-> a * d == c * b -> a / b == c / d.
Instance pow_ext :
Proper (
req ==> eq ==> req) (
pow_pos rmul).
Instance pow_N_ext :
Proper (
req ==> eq ==> req) (
pow_N rI rmul).
Lemma pow_pos_0 p :
pow_pos rmul 0
p == 0.
Lemma pow_pos_1 p :
pow_pos rmul 1
p == 1.
Lemma pow_pos_cst c p :
pow_pos rmul [c] p == [pow_pos cmul c p].
Lemma pow_pos_mul_l x y p :
pow_pos rmul (
x * y)
p == pow_pos rmul x p * pow_pos rmul y p.
Lemma pow_pos_add_r x p1 p2 :
pow_pos rmul x (
p1+p2)
== pow_pos rmul x p1 * pow_pos rmul x p2.
Lemma pow_pos_mul_r x p1 p2 :
pow_pos rmul x (
p1*p2)
== pow_pos rmul (
pow_pos rmul x p1)
p2.
Lemma pow_pos_nz x p :
~x==0
-> ~pow_pos rmul x p == 0.
Lemma pow_pos_div a b p :
~ b == 0
->
pow_pos rmul (
a / b)
p == pow_pos rmul a p / pow_pos rmul b p.
Instance PEadd_ext :
Proper (
NPEequiv ==> NPEequiv ==> NPEequiv) (@
PEadd C).
Instance PEsub_ext :
Proper (
NPEequiv ==> NPEequiv ==> NPEequiv) (@
PEsub C).
Instance PEmul_ext :
Proper (
NPEequiv ==> NPEequiv ==> NPEequiv) (@
PEmul C).
Instance PEopp_ext :
Proper (
NPEequiv ==> NPEequiv) (@
PEopp C).
Instance PEpow_ext :
Proper (
NPEequiv ==> eq ==> NPEequiv) (@
PEpow C).
Lemma PE_1_l (
e :
PExpr C) : (1
* e === e)%
poly.
Lemma PE_1_r (
e :
PExpr C) : (
e * 1
=== e)%
poly.
Lemma PEpow_0_r (
e :
PExpr C) : (
e ^ 0
=== 1)%
poly.
Lemma PEpow_1_r (
e :
PExpr C) : (
e ^ 1
=== e)%
poly.
Lemma PEpow_1_l n : (1
^ n === 1)%
poly.
Lemma PEpow_add_r (
e :
PExpr C)
n n' :
(
e ^ (n+n') === e ^ n * e ^ n')%
poly.
Lemma PEpow_mul_l (
e e' :
PExpr C)
n :
(
(e * e') ^ n === e ^ n * e' ^ n)%
poly.
Lemma PEpow_mul_r (
e :
PExpr C)
n n' :
(
e ^ (n * n') === (e ^ n) ^ n')%
poly.
Lemma PEpow_nz l e n :
~ e @ l == 0
-> ~ (e^n) @ l == 0.
Fixpoint PExpr_eq (
e e' :
PExpr C) {
struct e} :
bool :=
match e,
e' with
|
PEc c,
PEc c' =>
ceqb c c'
|
PEX _ p,
PEX _ p' =>
Pos.eqb p p'
|
e1 + e2,
e1' + e2' =>
PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
|
e1 - e2,
e1' - e2' =>
PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
|
e1 * e2,
e1' * e2' =>
PExpr_eq e1 e1' &&& PExpr_eq e2 e2'
|
- e,
- e' =>
PExpr_eq e e'
|
e ^ n,
e' ^ n' =>
N.eqb n n' &&& PExpr_eq e e'
|
_,
_ =>
false
end%
poly.
Lemma if_true (
a b :
bool) :
a &&& b = true -> a = true /\ b = true.
Theorem PExpr_eq_semi_ok e e' :
PExpr_eq e e' = true -> (
e === e')%
poly.
Lemma PExpr_eq_spec e e' :
BoolSpec (
e === e')%
poly True (
PExpr_eq e e').
Smart constructors for polynomial expression,
with reduction of constants
Definition NPEadd e1 e2 :=
match e1,
e2 with
|
PEc c1,
PEc c2 =>
PEc (
c1 + c2)
|
PEc c,
_ =>
if (
c =? 0)%
coef then e2 else e1 + e2
|
_,
PEc c =>
if (
c =? 0)%
coef then e1 else e1 + e2
|
_,
_ => (
e1 + e2)
end%
poly.
Infix "++" :=
NPEadd (
at level 60,
right associativity).
Theorem NPEadd_ok e1 e2 : (
e1 ++ e2 === e1 + e2)%
poly.
Definition NPEsub e1 e2 :=
match e1,
e2 with
|
PEc c1,
PEc c2 =>
PEc (
c1 - c2)
|
PEc c,
_ =>
if (
c =? 0)%
coef then - e2 else e1 - e2
|
_,
PEc c =>
if (
c =? 0)%
coef then e1 else e1 - e2
|
_,
_ =>
e1 - e2
end%
poly.
Infix "--" :=
NPEsub (
at level 50,
left associativity).
Theorem NPEsub_ok e1 e2: (
e1 -- e2 === e1 - e2)%
poly.
Definition NPEopp e1 :=
match e1 with PEc c1 =>
PEc (
- c1) |
_ =>
- e1 end%
poly.
Theorem NPEopp_ok e : (
NPEopp e === -e)%
poly.
Definition NPEpow x n :=
match n with
|
N0 => 1
|
Npos p =>
if (
p =? 1)%
positive then x else
match x with
|
PEc c =>
if (
c =? 1)%
coef then 1
else if (
c =? 0)%
coef then 0
else PEc (
pow_pos cmul c p)
|
_ =>
x ^ n
end
end%
poly.
Infix "^^" :=
NPEpow (
at level 35,
right associativity).
Theorem NPEpow_ok e n : (
e ^^ n === e ^ n)%
poly.
Fixpoint NPEmul (
x y :
PExpr C) {
struct x} :
PExpr C :=
match x,
y with
|
PEc c1,
PEc c2 =>
PEc (
c1 * c2)
|
PEc c,
_ =>
if (
c =? 1)%
coef then y else if (
c =? 0)%
coef then 0
else x * y
|
_,
PEc c =>
if (
c =? 1)%
coef then x else if (
c =? 0)%
coef then 0
else x * y
|
e1 ^ n1,
e2 ^ n2 =>
if (
n1 =? n2)%
N then (NPEmul e1 e2)^^n1 else x * y
|
_,
_ =>
x * y
end%
poly.
Infix "**" :=
NPEmul (
at level 40,
left associativity).
Theorem NPEmul_ok e1 e2 : (
e1 ** e2 === e1 * e2)%
poly.
Fixpoint PEsimp (
e :
PExpr C) :
PExpr C :=
match e with
|
e1 + e2 =>
(PEsimp e1) ++ (PEsimp e2)
|
e1 * e2 =>
(PEsimp e1) ** (PEsimp e2)
|
e1 - e2 =>
(PEsimp e1) -- (PEsimp e2)
|
- e1 =>
NPEopp (
PEsimp e1)
|
e1 ^ n1 =>
(PEsimp e1) ^^ n1
|
_ =>
e
end%
poly.
Theorem PEsimp_ok e : (
PEsimp e === e)%
poly.
Inductive FExpr :
Type :=
|
FEO :
FExpr
|
FEI :
FExpr
|
FEc:
C -> FExpr
|
FEX:
positive -> FExpr
|
FEadd:
FExpr -> FExpr -> FExpr
|
FEsub:
FExpr -> FExpr -> FExpr
|
FEmul:
FExpr -> FExpr -> FExpr
|
FEopp:
FExpr -> FExpr
|
FEinv:
FExpr -> FExpr
|
FEdiv:
FExpr -> FExpr -> FExpr
|
FEpow:
FExpr -> N -> FExpr .
Fixpoint FEeval (
l :
list R) (
pe :
FExpr) {
struct pe} :
R :=
match pe with
|
FEO =>
rO
|
FEI =>
rI
|
FEc c =>
phi c
|
FEX x =>
BinList.nth 0
x l
|
FEadd x y =>
FEeval l x + FEeval l y
|
FEsub x y =>
FEeval l x - FEeval l y
|
FEmul x y =>
FEeval l x * FEeval l y
|
FEopp x =>
- FEeval l x
|
FEinv x =>
/ FEeval l x
|
FEdiv x y =>
FEeval l x / FEeval l y
|
FEpow x n =>
rpow (
FEeval l x) (
Cp_phi n)
end.
Record linear :
Type :=
mk_linear {
num :
PExpr C;
denum :
PExpr C;
condition :
list (
PExpr C) }.
Fixpoint PCond (
l :
list R) (
le :
list (
PExpr C)) {
struct le} :
Prop :=
match le with
|
nil =>
True
|
e1 :: nil =>
~ req (
e1 @ l)
rO
|
e1 :: l1 =>
~ req (
e1 @ l)
rO /\ PCond l l1
end.
Theorem PCond_cons l a l1 :
PCond l (
a :: l1)
<-> ~ a @ l == 0
/\ PCond l l1.
Theorem PCond_cons_inv_l l a l1 :
PCond l (
a::l1)
-> ~ a @ l == 0.
Theorem PCond_cons_inv_r l a l1 :
PCond l (
a :: l1)
-> PCond l l1.
Theorem PCond_app l l1 l2 :
PCond l (
l1 ++ l2)
<-> PCond l l1 /\ PCond l l2.
Definition absurd_PCond :=
cons 0%
poly nil.
Lemma absurd_PCond_bottom :
forall l,
~ PCond l absurd_PCond.
Definition default_isIn e1 p1 e2 p2 :=
if PExpr_eq e1 e2 then
match Z.pos_sub p1 p2 with
|
Zpos p =>
Some (Npos p, 1%
poly)
|
Z0 =>
Some (N0, 1%
poly)
|
Zneg p =>
Some (N0, e2 ^^ Npos p)
end
else None.
Fixpoint isIn e1 p1 e2 p2 {
struct e2}:
option (
N * PExpr C) :=
match e2 with
|
e3 * e4 =>
match isIn e1 p1 e3 p2 with
|
Some (N0, e5) =>
Some (N0, e5 ** (e4 ^^ Npos p2))
|
Some (Npos p, e5) =>
match isIn e1 p e4 p2 with
|
Some (n, e6) =>
Some (n, e5 ** e6)
|
None =>
Some (Npos p, e5 ** (e4 ^^ Npos p2))
end
|
None =>
match isIn e1 p1 e4 p2 with
|
Some (n, e5) =>
Some (n, (e3 ^^ Npos p2) ** e5)
|
None =>
None
end
end
|
e3 ^ N0 =>
None
|
e3 ^ Npos p3 =>
isIn e1 p1 e3 (
Pos.mul p3 p2)
|
_ =>
default_isIn e1 p1 e2 p2
end%
poly.
Definition ZtoN z :=
match z with Zpos p =>
Npos p |
_ =>
N0 end.
Definition NtoZ n :=
match n with Npos p =>
Zpos p |
_ =>
Z0 end.
Lemma Z_pos_sub_gt p q : (
p > q)%
positive ->
Z.pos_sub p q = Zpos (
p - q).
Ltac simpl_pos_sub :=
rewrite ?
Z_pos_sub_gt in *
by assumption.
Lemma default_isIn_ok e1 e2 p1 p2 :
match default_isIn e1 p1 e2 p2 with
|
Some(n, e3) =>
let n' :=
ZtoN (
Zpos p1 - NtoZ n)
in
(
e2 ^ N.pos p2 === e1 ^ n' * e3)%
poly
/\ (
Zpos p1 > NtoZ n)%
Z
|
_ =>
True
end.
Ltac npe_simpl :=
rewrite ?
NPEmul_ok, ?
NPEpow_ok, ?
PEpow_mul_l.
Ltac npe_ring :=
intro l;
simpl;
ring.
Theorem isIn_ok e1 p1 e2 p2 :
match isIn e1 p1 e2 p2 with
|
Some(n, e3) =>
let n' :=
ZtoN (
Zpos p1 - NtoZ n)
in
(
e2 ^ N.pos p2 === e1 ^ n' * e3)%
poly
/\ (
Zpos p1 > NtoZ n)%
Z
|
_ =>
True
end.
Opaque NPEpow.
Record rsplit :
Type :=
mk_rsplit {
rsplit_left :
PExpr C;
rsplit_common :
PExpr C;
rsplit_right :
PExpr C}.
Notation left :=
rsplit_left.
Notation right :=
rsplit_right.
Notation common :=
rsplit_common.
Fixpoint split_aux e1 p e2 {
struct e1}:
rsplit :=
match e1 with
|
e3 * e4 =>
let r1 :=
split_aux e3 p e2 in
let r2 :=
split_aux e4 p (
right r1)
in
mk_rsplit (
left r1 ** left r2)
(
common r1 ** common r2)
(
right r2)
|
e3 ^ N0 =>
mk_rsplit 1 1
e2
|
e3 ^ Npos p3 =>
split_aux e3 (
Pos.mul p3 p)
e2
|
_ =>
match isIn e1 p e2 1
with
|
Some (N0,e3) =>
mk_rsplit 1 (
e1 ^^ Npos p)
e3
|
Some (Npos q, e3) =>
mk_rsplit (
e1 ^^ Npos q) (
e1 ^^ Npos (
p - q))
e3
|
None =>
mk_rsplit (
e1 ^^ Npos p) 1
e2
end
end%
poly.
Lemma split_aux_ok1 e1 p e2 :
(
let res :=
match isIn e1 p e2 1
with
|
Some (N0,e3) =>
mk_rsplit 1 (
e1 ^^ Npos p)
e3
|
Some (Npos q, e3) =>
mk_rsplit (
e1 ^^ Npos q) (
e1 ^^ Npos (
p - q))
e3
|
None =>
mk_rsplit (
e1 ^^ Npos p) 1
e2
end
in
e1 ^ Npos p === left res * common res
/\ e2 === right res * common res)%
poly.
Opaque NPEpow NPEmul.
Theorem split_aux_ok:
forall e1 p e2,
(
e1 ^ Npos p === left (
split_aux e1 p e2)
* common (
split_aux e1 p e2)
/\ e2 === right (
split_aux e1 p e2)
* common (
split_aux e1 p e2))%
poly.
Definition split e1 e2 :=
split_aux e1 xH e2.
Theorem split_ok_l e1 e2 :
(
e1 === left (
split e1 e2)
* common (
split e1 e2))%
poly.
Theorem split_ok_r e1 e2 :
(
e2 === right (
split e1 e2)
* common (
split e1 e2))%
poly.
Lemma split_nz_l l e1 e2 :
~ e1 @ l == 0
-> ~ left (
split e1 e2)
@ l == 0.
Lemma split_nz_r l e1 e2 :
~ e2 @ l == 0
-> ~ right (
split e1 e2)
@ l == 0.
Fixpoint Fnorm (
e :
FExpr) :
linear :=
match e with
|
FEO =>
mk_linear 0 1
nil
|
FEI =>
mk_linear 1 1
nil
|
FEc c =>
mk_linear (
PEc c) 1
nil
|
FEX x =>
mk_linear (
PEX C x) 1
nil
|
FEadd e1 e2 =>
let x :=
Fnorm e1 in
let y :=
Fnorm e2 in
let s :=
split (
denum x) (
denum y)
in
mk_linear
(
(num x ** right s) ++ (num y ** left s))
(
left s ** (right s ** common s))
(
condition x ++ condition y)%
list
|
FEsub e1 e2 =>
let x :=
Fnorm e1 in
let y :=
Fnorm e2 in
let s :=
split (
denum x) (
denum y)
in
mk_linear
(
(num x ** right s) -- (num y ** left s))
(
left s ** (right s ** common s))
(
condition x ++ condition y)%
list
|
FEmul e1 e2 =>
let x :=
Fnorm e1 in
let y :=
Fnorm e2 in
let s1 :=
split (
num x) (
denum y)
in
let s2 :=
split (
num y) (
denum x)
in
mk_linear (
left s1 ** left s2)
(
right s2 ** right s1)
(
condition x ++ condition y)%
list
|
FEopp e1 =>
let x :=
Fnorm e1 in
mk_linear (
NPEopp (
num x)) (
denum x) (
condition x)
|
FEinv e1 =>
let x :=
Fnorm e1 in
mk_linear (
denum x) (
num x) (
num x :: condition x)
|
FEdiv e1 e2 =>
let x :=
Fnorm e1 in
let y :=
Fnorm e2 in
let s1 :=
split (
num x) (
num y)
in
let s2 :=
split (
denum x) (
denum y)
in
mk_linear (
left s1 ** right s2)
(
left s2 ** right s1)
(
num y :: condition x ++ condition y)%
list
|
FEpow e1 n =>
let x :=
Fnorm e1 in
mk_linear (
(num x)^^n) (
(denum x)^^n) (
condition x)
end.
Theorem Pcond_Fnorm l e :
PCond l (
condition (
Fnorm e))
-> ~ (denum (
Fnorm e)
)@l == 0.
Ltac uneval :=
repeat match goal with
| |-
context [ ?
x @ ?
l * ?
y @ ?
l ] =>
change (
x@l * y@l)
with (
(x*y)@l)
| |-
context [ ?
x @ ?
l + ?
y @ ?
l ] =>
change (
x@l + y@l)
with (
(x+y)@l)
end.
Theorem Fnorm_FEeval_PEeval l fe:
PCond l (
condition (
Fnorm fe))
->
FEeval l fe == (num (
Fnorm fe)
) @ l / (denum (
Fnorm fe)
) @ l.
Theorem Fnorm_crossproduct l fe1 fe2 :
let nfe1 :=
Fnorm fe1 in
let nfe2 :=
Fnorm fe2 in
(num nfe1 * denum nfe2) @ l == (num nfe2 * denum nfe1) @ l ->
PCond l (
condition nfe1 ++ condition nfe2)
->
FEeval l fe1 == FEeval l fe2.
Notation Ninterp_PElist :=
(
interp_PElist rO rI radd rmul rsub ropp req phi Cp_phi rpow).
Notation Nmk_monpol_list :=
(
mk_monpol_list cO cI cadd cmul csub copp ceqb cdiv).
Theorem Fnorm_ok:
forall n l lpe fe,
Ninterp_PElist l lpe ->
Peq ceqb (
Nnorm n (
Nmk_monpol_list lpe) (
num (
Fnorm fe))) (
Pc cO)
= true ->
PCond l (
condition (
Fnorm fe))
-> FEeval l fe == 0.
Notation ring_rw_correct :=
(
ring_rw_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
Notation ring_rw_pow_correct :=
(
ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th cdiv_th get_sign_spec).
Notation ring_correct :=
(
ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th).
Definition display_linear l num den :=
let lnum :=
NPphi_dev l num in
match den with
|
Pc c =>
if ceqb c cI then lnum else lnum / NPphi_dev l den
|
_ =>
lnum / NPphi_dev l den
end.
Definition display_pow_linear l num den :=
let lnum :=
NPphi_pow l num in
match den with
|
Pc c =>
if ceqb c cI then lnum else lnum / NPphi_pow l den
|
_ =>
lnum / NPphi_pow l den
end.
Theorem Field_rw_correct n lpe l :
Ninterp_PElist l lpe ->
forall lmp,
Nmk_monpol_list lpe = lmp ->
forall fe nfe,
Fnorm fe = nfe ->
PCond l (
condition nfe)
->
FEeval l fe ==
display_linear l (
Nnorm n lmp (
num nfe)) (
Nnorm n lmp (
denum nfe)).
Theorem Field_rw_pow_correct n lpe l :
Ninterp_PElist l lpe ->
forall lmp,
Nmk_monpol_list lpe = lmp ->
forall fe nfe,
Fnorm fe = nfe ->
PCond l (
condition nfe)
->
FEeval l fe ==
display_pow_linear l (
Nnorm n lmp (
num nfe)) (
Nnorm n lmp (
denum nfe)).
Theorem Field_correct n l lpe fe1 fe2 :
Ninterp_PElist l lpe ->
forall lmp,
Nmk_monpol_list lpe = lmp ->
forall nfe1,
Fnorm fe1 = nfe1 ->
forall nfe2,
Fnorm fe2 = nfe2 ->
Peq ceqb (
Nnorm n lmp (
num nfe1 * denum nfe2))
(
Nnorm n lmp (
num nfe2 * denum nfe1))
= true ->
PCond l (
condition nfe1 ++ condition nfe2)
->
FEeval l fe1 == FEeval l fe2.
This allows rewriting modulo the simplification of PEeval on PMul
Theorem Field_simplify_eq_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp,
Nmk_monpol_list lpe = lmp ->
forall nfe1,
Fnorm fe1 = nfe1 ->
forall nfe2,
Fnorm fe2 = nfe2 ->
forall den,
split (
denum nfe1) (
denum nfe2)
= den ->
NPphi_dev l (
Nnorm n lmp (
num nfe1 * right den))
==
NPphi_dev l (
Nnorm n lmp (
num nfe2 * left den))
->
PCond l (
condition nfe1 ++ condition nfe2)
->
FEeval l fe1 == FEeval l fe2.
Theorem Field_simplify_eq_pow_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp,
Nmk_monpol_list lpe = lmp ->
forall nfe1,
Fnorm fe1 = nfe1 ->
forall nfe2,
Fnorm fe2 = nfe2 ->
forall den,
split (
denum nfe1) (
denum nfe2)
= den ->
NPphi_pow l (
Nnorm n lmp (
num nfe1 * right den))
==
NPphi_pow l (
Nnorm n lmp (
num nfe2 * left den))
->
PCond l (
condition nfe1 ++ condition nfe2)
->
FEeval l fe1 == FEeval l fe2.
Theorem Field_simplify_aux_ok l fe1 fe2 den :
FEeval l fe1 == FEeval l fe2 ->
split (
denum (
Fnorm fe1)) (
denum (
Fnorm fe2))
= den ->
PCond l (
condition (
Fnorm fe1)
++ condition (
Fnorm fe2))
->
(num (
Fnorm fe1)
* right den) @ l == (num (
Fnorm fe2)
* left den) @ l.
Theorem Field_simplify_eq_pow_in_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp,
Nmk_monpol_list lpe = lmp ->
forall nfe1,
Fnorm fe1 = nfe1 ->
forall nfe2,
Fnorm fe2 = nfe2 ->
forall den,
split (
denum nfe1) (
denum nfe2)
= den ->
forall np1,
Nnorm n lmp (
num nfe1 * right den)
= np1 ->
forall np2,
Nnorm n lmp (
num nfe2 * left den)
= np2 ->
FEeval l fe1 == FEeval l fe2 ->
PCond l (
condition nfe1 ++ condition nfe2)
->
NPphi_pow l np1 ==
NPphi_pow l np2.
Theorem Field_simplify_eq_in_correct :
forall n l lpe fe1 fe2,
Ninterp_PElist l lpe ->
forall lmp,
Nmk_monpol_list lpe = lmp ->
forall nfe1,
Fnorm fe1 = nfe1 ->
forall nfe2,
Fnorm fe2 = nfe2 ->
forall den,
split (
denum nfe1) (
denum nfe2)
= den ->
forall np1,
Nnorm n lmp (
num nfe1 * right den)
= np1 ->
forall np2,
Nnorm n lmp (
num nfe2 * left den)
= np2 ->
FEeval l fe1 == FEeval l fe2 ->
PCond l (
condition nfe1 ++ condition nfe2)
->
NPphi_dev l np1 == NPphi_dev l np2.
Section Fcons_impl.
Variable Fcons :
PExpr C -> list (
PExpr C)
-> list (
PExpr C).
Hypothesis PCond_fcons_inv :
forall l a l1,
PCond l (
Fcons a l1)
-> ~ a @ l == 0
/\ PCond l l1.
Fixpoint Fapp (
l m:
list (
PExpr C)) {
struct l} :
list (
PExpr C) :=
match l with
|
nil =>
m
|
cons a l1 =>
Fcons a (
Fapp l1 m)
end.
Lemma fcons_ok :
forall l l1,
(forall lock,
lock = PCond l -> lock (
Fapp l1 nil)
) -> PCond l l1.
End Fcons_impl.
Section Fcons_simpl.
Fixpoint Fcons (
e:
PExpr C) (
l:
list (
PExpr C)) {
struct l} :
list (
PExpr C) :=
match l with
nil =>
cons e nil
|
cons a l1 =>
if PExpr_eq e a then l else cons a (
Fcons e l1)
end.
Theorem PFcons_fcons_inv:
forall l a l1,
PCond l (
Fcons a l1)
-> ~ a @ l == 0
/\ PCond l l1.
Fixpoint Fcons0 (
e:
PExpr C) (
l:
list (
PExpr C)) {
struct l} :
list (
PExpr C) :=
match l with
nil =>
cons e nil
|
cons a l1 =>
if Peq ceqb (
Nnorm O nil e) (
Nnorm O nil a)
then l
else cons a (
Fcons0 e l1)
end.
Theorem PFcons0_fcons_inv:
forall l a l1,
PCond l (
Fcons0 a l1)
-> ~ a @ l == 0
/\ PCond l l1.
Fixpoint Fcons00 (
e:
PExpr C) (
l:
list (
PExpr C)) {
struct e} :
list (
PExpr C) :=
match e with
PEmul e1 e2 =>
Fcons00 e1 (
Fcons00 e2 l)
|
PEpow e1 _ =>
Fcons00 e1 l
|
_ =>
Fcons0 e l
end.
Theorem PFcons00_fcons_inv:
forall l a l1,
PCond l (
Fcons00 a l1)
-> ~ a @ l == 0
/\ PCond l l1.
Definition Pcond_simpl_gen :=
fcons_ok _ PFcons00_fcons_inv.
Hypothesis ceqb_complete :
forall c1 c2,
[c1] == [c2] -> ceqb c1 c2 = true.
Lemma ceqb_spec' c1 c2 :
Bool.reflect (
[c1] == [c2]) (
ceqb c1 c2).
Fixpoint Fcons1 (
e:
PExpr C) (
l:
list (
PExpr C)) {
struct e} :
list (
PExpr C) :=
match e with
|
PEmul e1 e2 =>
Fcons1 e1 (
Fcons1 e2 l)
|
PEpow e _ =>
Fcons1 e l
|
PEopp e =>
if (
-(1)
=? 0)%
coef then absurd_PCond else Fcons1 e l
|
PEc c =>
if (
c =? 0)%
coef then absurd_PCond else l
|
_ =>
Fcons0 e l
end.
Theorem PFcons1_fcons_inv:
forall l a l1,
PCond l (
Fcons1 a l1)
-> ~ a @ l == 0
/\ PCond l l1.
Definition Fcons2 e l :=
Fcons1 (
PEsimp e)
l.
Theorem PFcons2_fcons_inv:
forall l a l1,
PCond l (
Fcons2 a l1)
-> ~ a @ l == 0
/\ PCond l l1.
Definition Pcond_simpl_complete :=
fcons_ok _ PFcons2_fcons_inv.
End Fcons_simpl.
End AlmostField.
Section FieldAndSemiField.
Record field_theory :
Prop :=
mk_field {
F_R :
ring_theory rO rI radd rmul rsub ropp req;
F_1_neq_0 :
~ 1
== 0;
Fdiv_def :
forall p q,
p / q == p * / q;
Finv_l :
forall p,
~ p == 0
-> / p * p == 1
}.
Definition F2AF f :=
mk_afield
(
Rth_ARth Rsth Reqe (
F_R f)) (
F_1_neq_0 f) (
Fdiv_def f) (
Finv_l f).
Record semi_field_theory :
Prop :=
mk_sfield {
SF_SR :
semi_ring_theory rO rI radd rmul req;
SF_1_neq_0 :
~ 1
== 0;
SFdiv_def :
forall p q,
p / q == p * / q;
SFinv_l :
forall p,
~ p == 0
-> / p * p == 1
}.
End FieldAndSemiField.
End MakeFieldPol.
Definition SF2AF R (
rO rI:
R)
radd rmul rdiv rinv req Rsth
(
sf:
semi_field_theory rO rI radd rmul rdiv rinv req) :=
mk_afield _ _
(
SRth_ARth Rsth (
SF_SR sf))
(
SF_1_neq_0 sf)
(
SFdiv_def sf)
(
SFinv_l sf).
Section Complete.
Variable R :
Type.
Variable (
rO rI :
R) (
radd rmul rsub:
R->R->R) (
ropp :
R -> R).
Variable (
rdiv :
R -> R -> R) (
rinv :
R -> R).
Variable req :
R -> R -> Prop.
Notation "0" :=
rO.
Notation "1" :=
rI.
Notation "x + y" := (
radd x y).
Notation "x * y " := (
rmul x y).
Notation "x - y " := (
rsub x y).
Notation "- x" := (
ropp x).
Notation "x / y " := (
rdiv x y).
Notation "/ x" := (
rinv x).
Notation "x == y" := (
req x y) (
at level 70,
no associativity).
Variable Rsth :
Setoid_Theory R req.
Add Parametric Relation :
R req
reflexivity proved by (@
Equivalence_Reflexive _ _ Rsth)
symmetry proved by (@
Equivalence_Symmetric _ _ Rsth)
transitivity proved by (@
Equivalence_Transitive _ _ Rsth)
as R_setoid3.
Variable Reqe :
ring_eq_ext radd rmul ropp req.
Add Morphism radd with signature (
req ==> req ==> req)
as radd_ext3.
Add Morphism rmul with signature (
req ==> req ==> req)
as rmul_ext3.
Add Morphism ropp with signature (
req ==> req)
as ropp_ext3.
Section AlmostField.
Variable AFth :
almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Let ARth := (
AF_AR AFth).
Let rI_neq_rO := (
AF_1_neq_0 AFth).
Let rdiv_def := (
AFdiv_def AFth).
Let rinv_l := (
AFinv_l AFth).
Hypothesis S_inj :
forall x y, 1
+x==1
+y -> x==y.
Hypothesis gen_phiPOS_not_0 :
forall p,
~ gen_phiPOS1 rI radd rmul p == 0.
Lemma add_inj_r p x y :
gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
Lemma gen_phiPOS_inj x y :
gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
x = y.
Lemma gen_phiN_inj x y :
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
x = y.
Lemma gen_phiN_complete x y :
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
N.eqb x y = true.
End AlmostField.
Section Field.
Variable Fth :
field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Let Rth := (
F_R Fth).
Let rI_neq_rO := (
F_1_neq_0 Fth).
Let rdiv_def := (
Fdiv_def Fth).
Let rinv_l := (
Finv_l Fth).
Let AFth :=
F2AF Rsth Reqe Fth.
Let ARth :=
Rth_ARth Rsth Reqe Rth.
Lemma ring_S_inj x y : 1
+x==1
+y -> x==y.
Hypothesis gen_phiPOS_not_0 :
forall p,
~ gen_phiPOS1 rI radd rmul p == 0.
Let gen_phiPOS_inject :=
gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
Lemma gen_phiPOS_discr_sgn x y :
~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
Lemma gen_phiZ_inj x y :
gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
x = y.
Lemma gen_phiZ_complete x y :
gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
Zeq_bool x y = true.
End Field.
End Complete.