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.