Library Coq.setoid_ring.Field_theory
Require Ring.
Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List.
Require Import ZArith_base.
Section MakeFieldPol.
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 / y" := (
rdiv x y).
Notation "- x" := (
ropp x).
Notation "/ x" := (
rinv x).
Notation "x == y" := (
req x y) (
at level 70,
no associativity).
Variable Rsth :
Setoid_Theory R 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 :=
AFth.(
AF_AR).
Let rI_neq_rO :=
AFth.(
AF_1_neq_0).
Let rdiv_def :=
AFth.(
AFdiv_def).
Let rinv_l :=
AFth.(
AFinv_l).
Variable C:
Type.
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.
Lemma ceqb_rect :
forall c1 c2 (
A:
Type) (
x y:
A) (
P:
A->
Type),
(
phi c1 == phi c2 ->
P x) ->
P y ->
P (
if ceqb c1 c2 then x else y).
Notation "x +! y" := (
cadd x y) (
at level 50).
Notation "x *! y " := (
cmul x y) (
at level 40).
Notation "x -! y " := (
csub x y) (
at level 50).
Notation "-! x" := (
copp x) (
at level 35).
Notation " x ?=! y" := (
ceqb x y) (
at level 70,
no associativity).
Notation "[ x ]" := (
phi x) (
at level 0).
Add Setoid R req Rsth as R_set1.
Add Morphism radd :
radd_ext.
Add Morphism rmul :
rmul_ext.
Add Morphism ropp :
ropp_ext.
Add Morphism rsub :
rsub_ext.
Add Morphism rinv :
rinv_ext.
Let eq_trans :=
Setoid.Seq_trans _ _ Rsth.
Let eq_sym :=
Setoid.Seq_sym _ _ Rsth.
Let eq_refl :=
Setoid.Seq_refl _ _ Rsth.
Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(
morph1) .
Hint Resolve (
Rmul_ext Reqe) (
Rmul_ext Reqe) (
Radd_ext Reqe)
(
ARsub_ext Rsth Reqe ARth) (
Ropp_ext Reqe)
SRinv_ext.
Hint Resolve (
ARadd_0_l ARth) (
ARadd_comm ARth) (
ARadd_assoc ARth)
(
ARmul_1_l ARth) (
ARmul_0_l ARth)
(
ARmul_comm ARth) (
ARmul_assoc ARth) (
ARdistr_l ARth)
(
ARopp_mul_l ARth) (
ARopp_add ARth)
(
ARsub_def ARth) .
Variable Cpow :
Set.
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.
Notation NPEeval := (
PEeval rO radd rmul rsub ropp phi Cp_phi rpow).
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 :
forall r, 0
- r == - r.
Lemma rsub_0_r :
forall r,
r - 0
== r.
Theorem rdiv_simpl:
forall p q,
~ q == 0 ->
q * (p / q) == p.
Hint Resolve rdiv_simpl .
Theorem SRdiv_ext:
forall p1 p2,
p1 == p2 ->
forall q1 q2,
q1 == q2 ->
p1 / q1 == p2 / q2.
Hint Resolve SRdiv_ext .
Add Morphism rdiv :
rdiv_ext.
Lemma rmul_reg_l :
forall p q1 q2,
~ p == 0 ->
p * q1 == p * q2 ->
q1 == q2.
Theorem field_is_integral_domain :
forall r1 r2,
~ r1 == 0 ->
~ r2 == 0 ->
~ r1 * r2 == 0.
Theorem ropp_neq_0 :
forall r,
~ -(1)
== 0 ->
~ r == 0 ->
~ -r == 0.
Theorem rdiv_r_r :
forall r,
~ r == 0 ->
r / r == 1.
Theorem rdiv1:
forall r,
r == r / 1.
Theorem rdiv2:
forall r1 r2 r3 r4,
~ r2 == 0 ->
~ r4 == 0 ->
r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4).
Theorem rdiv2b:
forall r1 r2 r3 r4 r5,
~ (r2*r5) == 0 ->
~ (r4*r5) == 0 ->
r1 / (r2*r5) + r3 / (r4*r5) == (r1 * r4 + r3 * r2) / (r2 * (r4 * r5)).
Theorem rdiv5:
forall r1 r2,
- (r1 / r2) == - r1 / r2.
Hint Resolve rdiv5 .
Theorem rdiv3:
forall r1 r2 r3 r4,
~ r2 == 0 ->
~ r4 == 0 ->
r1 / r2 - r3 / r4 == (r1 * r4 - r3 * r2) / (r2 * r4).
Theorem rdiv3b:
forall r1 r2 r3 r4 r5,
~ (r2 * r5) == 0 ->
~ (r4 * r5) == 0 ->
r1 / (r2*r5) - r3 / (r4*r5) == (r1 * r4 - r3 * r2) / (r2 * (r4 * r5)).
Theorem rdiv6:
forall r1 r2,
~ r1 == 0 ->
~ r2 == 0 ->
/ (r1 / r2) == r2 / r1.
Hint Resolve rdiv6 .
Theorem rdiv4:
forall r1 r2 r3 r4,
~ r2 == 0 ->
~ r4 == 0 ->
(r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4).
Theorem rdiv4b:
forall r1 r2 r3 r4 r5 r6,
~ r2 * r5 == 0 ->
~ r4 * r6 == 0 ->
((r1 * r6) / (r2 * r5)) * ((r3 * r5) / (r4 * r6)) == (r1 * r3) / (r2 * r4).
Theorem rdiv7:
forall r1 r2 r3 r4,
~ r2 == 0 ->
~ r3 == 0 ->
~ r4 == 0 ->
(r1 / r2) / (r3 / r4) == (r1 * r4) / (r2 * r3).
Theorem rdiv7b:
forall r1 r2 r3 r4 r5 r6,
~ r2 * r6 == 0 ->
~ r3 * r5 == 0 ->
~ r4 * r6 == 0 ->
((r1 * r5) / (r2 * r6)) / ((r3 * r5) / (r4 * r6)) == (r1 * r4) / (r2 * r3).
Theorem rdiv8:
forall r1 r2,
~ r2 == 0 ->
r1 == 0 ->
r1 / r2 == 0.
Theorem cross_product_eq :
forall r1 r2 r3 r4,
~ r2 == 0 ->
~ r4 == 0 ->
r1 * r4 == r3 * r2 ->
r1 / r2 == r3 / r4.
Fixpoint positive_eq (
p1 p2 :
positive) {
struct p1} :
bool :=
match p1,
p2 with
xH,
xH =>
true
|
xO p3,
xO p4 =>
positive_eq p3 p4
|
xI p3,
xI p4 =>
positive_eq p3 p4
|
_,
_ =>
false
end.
Theorem positive_eq_correct:
forall p1 p2,
if positive_eq p1 p2 then p1 = p2 else p1 <> p2.
Definition N_eq n1 n2 :=
match n1,
n2 with
|
N0,
N0 =>
true
|
Npos p1,
Npos p2 =>
positive_eq p1 p2
|
_,
_ =>
false
end.
Lemma N_eq_correct :
forall n1 n2,
if N_eq n1 n2 then n1 = n2 else n1 <> n2.
Fixpoint PExpr_eq (
e1 e2 :
PExpr C) {
struct e1} :
bool :=
match e1,
e2 with
PEc c1,
PEc c2 =>
ceqb c1 c2
|
PEX p1,
PEX p2 =>
positive_eq p1 p2
|
PEadd e3 e5,
PEadd e4 e6 =>
if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
|
PEsub e3 e5,
PEsub e4 e6 =>
if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
|
PEmul e3 e5,
PEmul e4 e6 =>
if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false
|
PEopp e3,
PEopp e4 =>
PExpr_eq e3 e4
|
PEpow e3 n3,
PEpow e4 n4 =>
if N_eq n3 n4 then PExpr_eq e3 e4 else false
|
_,
_ =>
false
end.
Add Morphism (
pow_pos rmul)
with signature req ==> eq ==> req as pow_morph.
Qed.
Add Morphism (
pow_N rI rmul)
with signature req ==> eq ==> req as pow_N_morph.
Qed.
Theorem PExpr_eq_semi_correct:
forall l e1 e2,
PExpr_eq e1 e2 = true ->
NPEeval l e1 == NPEeval l e2.
Definition NPEadd e1 e2 :=
match e1,
e2 with
PEc c1,
PEc c2 =>
PEc (
cadd c1 c2)
|
PEc c,
_ =>
if ceqb c cO then e2 else PEadd e1 e2
|
_,
PEc c =>
if ceqb c cO then e1 else PEadd e1 e2
|
_,
_ =>
PEadd e1 e2
end.
Theorem NPEadd_correct:
forall l e1 e2,
NPEeval l (
NPEadd e1 e2)
== NPEeval l (
PEadd e1 e2).
Definition NPEpow x n :=
match n with
|
N0 =>
PEc cI
|
Npos p =>
if positive_eq p xH then x else
match x with
|
PEc c =>
if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (
pow_pos cmul c p)
|
_ =>
PEpow x n
end
end.
Theorem NPEpow_correct :
forall l e n,
NPEeval l (
NPEpow e n)
== NPEeval l (
PEpow e n).
Fixpoint NPEmul (
x y :
PExpr C) {
struct x} :
PExpr C :=
match x,
y with
PEc c1,
PEc c2 =>
PEc (
cmul c1 c2)
|
PEc c,
_ =>
if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y
|
_,
PEc c =>
if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y
|
PEpow e1 n1,
PEpow e2 n2 =>
if N_eq n1 n2 then NPEpow (
NPEmul e1 e2)
n1 else PEmul x y
|
_,
_ =>
PEmul x y
end.
Lemma pow_pos_mul :
forall x y p,
pow_pos rmul (
x * y)
p == pow_pos rmul x p * pow_pos rmul y p.
Theorem NPEmul_correct :
forall l e1 e2,
NPEeval l (
NPEmul e1 e2)
== NPEeval l (
PEmul e1 e2).
Definition NPEsub e1 e2 :=
match e1,
e2 with
PEc c1,
PEc c2 =>
PEc (
csub c1 c2)
|
PEc c,
_ =>
if ceqb c cO then PEopp e2 else PEsub e1 e2
|
_,
PEc c =>
if ceqb c cO then e1 else PEsub e1 e2
|
_,
_ =>
PEsub e1 e2
end.
Theorem NPEsub_correct:
forall l e1 e2,
NPEeval l (
NPEsub e1 e2)
== NPEeval l (
PEsub e1 e2).
Definition NPEopp e1 :=
match e1 with PEc c1 =>
PEc (
copp c1) |
_ =>
PEopp e1 end.
Theorem NPEopp_correct:
forall l e1,
NPEeval l (
NPEopp e1)
== NPEeval l (
PEopp e1).
Fixpoint PExpr_simp (
e :
PExpr C) :
PExpr C :=
match e with
PEadd e1 e2 =>
NPEadd (
PExpr_simp e1) (
PExpr_simp e2)
|
PEmul e1 e2 =>
NPEmul (
PExpr_simp e1) (
PExpr_simp e2)
|
PEsub e1 e2 =>
NPEsub (
PExpr_simp e1) (
PExpr_simp e2)
|
PEopp e1 =>
NPEopp (
PExpr_simp e1)
|
PEpow e1 n1 =>
NPEpow (
PExpr_simp e1)
n1
|
_ =>
e
end.
Theorem PExpr_simp_correct:
forall l e,
NPEeval l (
PExpr_simp e)
== NPEeval l e.
Inductive FExpr :
Type :=
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
|
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 (
NPEeval l e1)
rO
|
e1 :: l1 =>
~ req (
NPEeval l e1)
rO /\ PCond l l1
end.
Theorem PCond_cons_inv_l :
forall l a l1,
PCond l (
a::l1) ->
~ NPEeval l a == 0.
Theorem PCond_cons_inv_r :
forall l a l1,
PCond l (
a :: l1) ->
PCond l l1.
Theorem PCond_app_inv_l:
forall l l1 l2,
PCond l (
l1 ++ l2) ->
PCond l l1.
Theorem PCond_app_inv_r:
forall l l1 l2,
PCond l (
l1 ++ l2) ->
PCond l l2.
Definition absurd_PCond :=
cons (
PEc cO)
nil.
Lemma absurd_PCond_bottom :
forall l,
~ PCond l absurd_PCond.
Fixpoint isIn (
e1:
PExpr C) (
p1:
positive)
(
e2:
PExpr C) (
p2:
positive) {
struct e2}:
option (
N * PExpr C) :=
match e2 with
|
PEmul e3 e4 =>
match isIn e1 p1 e3 p2 with
|
Some (N0, e5) =>
Some (N0, NPEmul e5 (
NPEpow e4 (
Npos p2))
)
|
Some (Npos p, e5) =>
match isIn e1 p e4 p2 with
|
Some (n, e6) =>
Some (n, NPEmul e5 e6)
|
None =>
Some (Npos p, NPEmul e5 (
NPEpow e4 (
Npos p2))
)
end
|
None =>
match isIn e1 p1 e4 p2 with
|
Some (n, e5) =>
Some (n,NPEmul (
NPEpow e3 (
Npos p2))
e5)
|
None =>
None
end
end
|
PEpow e3 N0 =>
None
|
PEpow e3 (
Npos p3) =>
isIn e1 p1 e3 (
Pmult p3 p2)
|
_ =>
if PExpr_eq e1 e2 then
match Zminus (
Zpos p1) (
Zpos p2)
with
|
Zpos p =>
Some (Npos p, PEc cI)
|
Z0 =>
Some (N0, PEc cI)
|
Zneg p =>
Some (N0, NPEpow e2 (
Npos p)
)
end
else None
end.
Definition ZtoN z :=
match z with Zpos p =>
Npos p |
_ =>
N0 end.
Definition NtoZ n :=
match n with Npos p =>
Zpos p |
_ =>
Z0 end.
Notation pow_pos_plus := (
Ring_theory.pow_pos_Pplus _ Rsth Reqe.(
Rmul_ext)
ARth.(
ARmul_comm)
ARth.(
ARmul_assoc)).
Lemma isIn_correct_aux :
forall l e1 e2 p1 p2,
match
(
if PExpr_eq e1 e2 then
match Zminus (
Zpos p1) (
Zpos p2)
with
|
Zpos p =>
Some (Npos p, PEc cI)
|
Z0 =>
Some (N0, PEc cI)
|
Zneg p =>
Some (N0, NPEpow e2 (
Npos p)
)
end
else None)
with
|
Some(n, e3) =>
NPEeval l (
PEpow e2 (
Npos p2))
==
NPEeval l (
PEmul (
PEpow e1 (
ZtoN (
Zpos p1 - NtoZ n)))
e3)
/\
(
Zpos p1 > NtoZ n)%
Z
|
_ =>
True
end.
Lemma pow_pos_pow_pos :
forall x p1 p2,
pow_pos rmul (
pow_pos rmul x p1)
p2 == pow_pos rmul x (
p1*p2).
Theorem isIn_correct:
forall l e1 p1 e2 p2,
match isIn e1 p1 e2 p2 with
|
Some(n, e3) =>
NPEeval l (
PEpow e2 (
Npos p2))
==
NPEeval l (
PEmul (
PEpow e1 (
ZtoN (
Zpos p1 - NtoZ n)))
e3)
/\
(
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:
PExpr C) (
p:
positive) (
e2:
PExpr C) {
struct e1}:
rsplit :=
match e1 with
|
PEmul e3 e4 =>
let r1 :=
split_aux e3 p e2 in
let r2 :=
split_aux e4 p (
right r1)
in
mk_rsplit (
NPEmul (
left r1) (
left r2))
(
NPEmul (
common r1) (
common r2))
(
right r2)
|
PEpow e3 N0 =>
mk_rsplit (
PEc cI) (
PEc cI)
e2
|
PEpow e3 (
Npos p3) =>
split_aux e3 (
Pmult p3 p)
e2
|
_ =>
match isIn e1 p e2 xH with
|
Some (N0,e3) =>
mk_rsplit (
PEc cI) (
NPEpow e1 (
Npos p))
e3
|
Some (Npos q, e3) =>
mk_rsplit (
NPEpow e1 (
Npos q)) (
NPEpow e1 (
Npos (
p - q)))
e3
|
None =>
mk_rsplit (
NPEpow e1 (
Npos p)) (
PEc cI)
e2
end
end.
Lemma split_aux_correct_1 :
forall l e1 p e2,
let res :=
match isIn e1 p e2 xH with
|
Some (N0,e3) =>
mk_rsplit (
PEc cI) (
NPEpow e1 (
Npos p))
e3
|
Some (Npos q, e3) =>
mk_rsplit (
NPEpow e1 (
Npos q)) (
NPEpow e1 (
Npos (
p - q)))
e3
|
None =>
mk_rsplit (
NPEpow e1 (
Npos p)) (
PEc cI)
e2
end in
NPEeval l (
PEpow e1 (
Npos p))
== NPEeval l (
NPEmul (
left res) (
common res))
/\
NPEeval l e2 == NPEeval l (
NPEmul (
right res) (
common res)).
Opaque NPEpow NPEmul.
Theorem split_aux_correct:
forall l e1 p e2,
NPEeval l (
PEpow e1 (
Npos p))
==
NPEeval l (
NPEmul (
left (
split_aux e1 p e2)) (
common (
split_aux e1 p e2)))
/\
NPEeval l e2 == NPEeval l (
NPEmul (
right (
split_aux e1 p e2))
(
common (
split_aux e1 p e2))).
Definition split e1 e2 :=
split_aux e1 xH e2.
Theorem split_correct_l:
forall l e1 e2,
NPEeval l e1 == NPEeval l (
NPEmul (
left (
split e1 e2))
(
common (
split e1 e2))).
Theorem split_correct_r:
forall l e1 e2,
NPEeval l e2 == NPEeval l (
NPEmul (
right (
split e1 e2))
(
common (
split e1 e2))).
Fixpoint Fnorm (
e :
FExpr) :
linear :=
match e with
|
FEc c =>
mk_linear (
PEc c) (
PEc cI)
nil
|
FEX x =>
mk_linear (
PEX C x) (
PEc cI)
nil
|
FEadd e1 e2 =>
let x :=
Fnorm e1 in
let y :=
Fnorm e2 in
let s :=
split (
denum x) (
denum y)
in
mk_linear
(
NPEadd (
NPEmul (
num x) (
right s)) (
NPEmul (
num y) (
left s)))
(
NPEmul (
left s) (
NPEmul (
right s) (
common s)))
(
condition x ++ condition y)
|
FEsub e1 e2 =>
let x :=
Fnorm e1 in
let y :=
Fnorm e2 in
let s :=
split (
denum x) (
denum y)
in
mk_linear
(
NPEsub (
NPEmul (
num x) (
right s)) (
NPEmul (
num y) (
left s)))
(
NPEmul (
left s) (
NPEmul (
right s) (
common s)))
(
condition x ++ condition y)
|
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 (
NPEmul (
left s1) (
left s2))
(
NPEmul (
right s2) (
right s1))
(
condition x ++ condition y)
|
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 (
NPEmul (
left s1) (
right s2))
(
NPEmul (
left s2) (
right s1))
(
num y :: condition x ++ condition y)
|
FEpow e1 n =>
let x :=
Fnorm e1 in
mk_linear (
NPEpow (
num x)
n) (
NPEpow (
denum x)
n) (
condition x)
end.
Lemma pow_pos_not_0 :
forall x,
~x==0 ->
forall p,
~pow_pos rmul x p == 0.
Theorem Pcond_Fnorm:
forall l e,
PCond l (
condition (
Fnorm e)) ->
~ NPEeval l (
denum (
Fnorm e))
== 0.
Hint Resolve Pcond_Fnorm.
Theorem Fnorm_FEeval_PEeval:
forall l fe,
PCond l (
condition (
Fnorm fe)) ->
FEeval l fe == NPEeval l (
num (
Fnorm fe))
/ NPEeval l (
denum (
Fnorm fe)).
Theorem Fnorm_crossproduct:
forall l fe1 fe2,
let nfe1 :=
Fnorm fe1 in
let nfe2 :=
Fnorm fe2 in
NPEeval l (
PEmul (
num nfe1) (
denum nfe2))
==
NPEeval l (
PEmul (
num nfe2) (
denum nfe1)) ->
PCond l (
condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
Notation Ninterp_PElist := (
interp_PElist rO 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_correct:
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.
Definition display_linear l num den :=
NPphi_dev l num / NPphi_dev l den.
Definition display_pow_linear l num den :=
NPphi_pow l num / NPphi_pow l den.
Theorem Field_rw_correct :
forall 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 :
forall 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 :
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 ->
Peq ceqb (
Nnorm n lmp (
PEmul (
num nfe1) (
denum nfe2)))
(
Nnorm n lmp (
PEmul (
num nfe2) (
denum nfe1)))
= true ->
PCond l (
condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
Theorem Field_simplify_eq_old_correct :
forall l fe1 fe2 nfe1 nfe2,
Fnorm fe1 = nfe1 ->
Fnorm fe2 = nfe2 ->
NPphi_dev l (
Nnorm O nil (
PEmul (
num nfe1) (
denum nfe2)))
==
NPphi_dev l (
Nnorm O nil (
PEmul (
num nfe2) (
denum nfe1))) ->
PCond l (
condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
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 (
PEmul (
num nfe1) (
right den)))
==
NPphi_dev l (
Nnorm n lmp (
PEmul (
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 (
PEmul (
num nfe1) (
right den)))
==
NPphi_pow l (
Nnorm n lmp (
PEmul (
num nfe2) (
left den))) ->
PCond l (
condition nfe1 ++ condition nfe2) ->
FEeval l fe1 == FEeval l fe2.
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 (
PEmul (
num nfe1) (
right den))
= np1 ->
forall np2,
Nnorm n lmp (
PEmul (
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 (
PEmul (
num nfe1) (
right den))
= np1 ->
forall np2,
Nnorm n lmp (
PEmul (
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) ->
~ NPEeval l a == 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_correct :
forall l l1,
PCond l (
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) ->
~ NPEeval l a == 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) ->
~ NPEeval l a == 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) ->
~ NPEeval l a == 0
/\ PCond l l1.
Definition Pcond_simpl_gen :=
fcons_correct _ PFcons00_fcons_inv.
Hypothesis ceqb_complete :
forall c1 c2,
phi c1 == phi c2 ->
ceqb c1 c2 = true.
Lemma ceqb_rect_complete :
forall c1 c2 (
A:
Type) (
x y:
A) (
P:
A->
Type),
(
phi c1 == phi c2 ->
P x) ->
(
~ phi c1 == phi c2 ->
P y) ->
P (
if ceqb c1 c2 then x else y).
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 ceqb (
copp cI)
cO then absurd_PCond else Fcons1 e l
|
PEc c =>
if ceqb c cO then absurd_PCond else l
|
_ =>
Fcons0 e l
end.
Theorem PFcons1_fcons_inv:
forall l a l1,
PCond l (
Fcons1 a l1) ->
~ NPEeval l a == 0
/\ PCond l l1.
Definition Fcons2 e l :=
Fcons1 (
PExpr_simp e)
l.
Theorem PFcons2_fcons_inv:
forall l a l1,
PCond l (
Fcons2 a l1) ->
~ NPEeval l a == 0
/\ PCond l l1.
Definition Pcond_simpl_complete :=
fcons_correct _ 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.(
F_R))
f.(
F_1_neq_0)
f.(
Fdiv_def)
f.(
Finv_l).
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.(
SF_SR))
sf.(
SF_1_neq_0)
sf.(
SFdiv_def)
sf.(
SFinv_l).
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 Setoid R req Rsth as R_setoid3.
Variable Reqe :
ring_eq_ext radd rmul ropp req.
Add Morphism radd :
radd_ext3.
Add Morphism rmul :
rmul_ext3.
Add Morphism ropp :
ropp_ext3.
Section AlmostField.
Variable AFth :
almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Let ARth :=
AFth.(
AF_AR).
Let rI_neq_rO :=
AFth.(
AF_1_neq_0).
Let rdiv_def :=
AFth.(
AFdiv_def).
Let rinv_l :=
AFth.(
AFinv_l).
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 :
forall p x y,
gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y ->
x==y.
Lemma gen_phiPOS_inj :
forall x y,
gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y ->
x = y.
Lemma gen_phiN_inj :
forall x y,
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
x = y.
Lemma gen_phiN_complete :
forall x y,
gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
Neq_bool x y = true.
End AlmostField.
Section Field.
Variable Fth :
field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Let Rth :=
Fth.(
F_R).
Let rI_neq_rO :=
Fth.(
F_1_neq_0).
Let rdiv_def :=
Fth.(
Fdiv_def).
Let rinv_l :=
Fth.(
Finv_l).
Let AFth :=
F2AF Rsth Reqe Fth.
Let ARth :=
Rth_ARth Rsth Reqe Rth.
Lemma ring_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.
Let gen_phiPOS_inject :=
gen_phiPOS_inj AFth ring_S_inj gen_phiPOS_not_0.
Lemma gen_phiPOS_discr_sgn :
forall x y,
~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
Lemma gen_phiZ_inj :
forall x y,
gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
x = y.
Lemma gen_phiZ_complete :
forall 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.