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.