(Joint Center)Library realalg

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigop ssralg ssrnum ssrint rat poly polydiv polyorder.
Require Import perm matrix mxpoly polyXY binomial generic_quotient.
Require Import cauchyreals separable zmodp bigenough.

Import GRing.Theory Num.Theory BigEnough.

Set Implicit Arguments.

Reserved Notation "{ 'realalg' T }" (at level 0, format "{ 'realalg' T }").
Reserved Notation "{ 'alg' T }" (at level 0, format "{ 'alg' T }").

Module RealAlg.

Local Open Scope ring_scope.
Local Notation eval := horner_eval.

Section RealAlg.

Variable F : archiFieldType.
Local Notation m0 := (fun _ ⇒ 0%N).

CoInductive algcreal := AlgCReal {
  creal_of_alg :> creal F;
  annul_creal : {poly F};
  _ : annul_creal \is monic;
  _ : (annul_creal.[creal_of_alg] == 0)%CR
}.

Lemma monic_annul_creal x : annul_creal x \is monic.
Hint Resolve monic_annul_creal.

Lemma annul_creal_eq0 x : (annul_creal x == 0) = false.

Lemma root_annul_creal x : ((annul_creal x).[x] == 0)%CR.
Hint Resolve root_annul_creal.

Definition cst_algcreal (x : F) :=
  AlgCReal (monicXsubC _) (@root_cst_creal _ x).

Local Notation zero_algcreal := (cst_algcreal 0).
Local Notation one_algcreal := (cst_algcreal 1).

Lemma size_annul_creal_gt1 (x : algcreal) :
  (1 < size (annul_creal x))%N.

Lemma is_root_annul_creal (x : algcreal) (y : creal F) :
  (x == y)%CR → ((annul_creal x).[y] == 0)%CR.

Definition AlgCRealOf (p : {poly F}) (x : creal F)
  (p_neq0 : p != 0) (px_eq0 : (p.[x] == 0)%CR) :=
  AlgCReal (monic_monic_from_neq0 p_neq0) (root_monic_from_neq0 px_eq0).

Lemma sub_annihilant_algcreal_neq0 (x y : algcreal) :
  sub_annihilant (annul_creal x) (annul_creal y) != 0.

Lemma root_sub_algcreal (x y : algcreal) :
  ((sub_annihilant (annul_creal x) (annul_creal y)).[x - y] == 0)%CR.

Definition sub_algcreal (x y : algcreal) : algcreal :=
  AlgCRealOf (sub_annihilant_algcreal_neq0 x y) (@root_sub_algcreal x y).

Lemma root_opp_algcreal (x : algcreal) :
  ((annul_creal (sub_algcreal (cst_algcreal 0) x)).[- x] == 0)%CR.

Definition opp_algcreal (x : algcreal) : algcreal :=
  AlgCReal (@monic_annul_creal _) (@root_opp_algcreal x).

Lemma root_add_algcreal (x y : algcreal) :
  ((annul_creal (sub_algcreal x (opp_algcreal y))).[x + y] == 0)%CR.

Definition add_algcreal (x y : algcreal) : algcreal :=
  AlgCReal (@monic_annul_creal _) (@root_add_algcreal x y).

Lemma div_annihilant_algcreal_neq0 (x y : algcreal) :
   (annul_creal y).[0] != 0 →
   div_annihilant (annul_creal x) (annul_creal y) != 0.

Hint Resolve eq_creal_refl.
Hint Resolve le_creal_refl.

Lemma simplify_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) :
  {y | ((annul_creal y).[0] != 0) & ((y != 0)%CR × (x == y)%CR)%type}.

Lemma algcreal_eq0_dec (x : algcreal) :
  {(x == 0)%CR} + {(x != 0)%CR}.

Lemma eq_algcreal_dec (x y : algcreal) : {(x == y)%CR} + {(x != y)%CR}.

Definition eq_algcreal : rel algcreal := eq_algcreal_dec.

Lemma eq_algcrealP (x y : algcreal) : reflect (x == y)%CR (eq_algcreal x y).
Implicit Arguments eq_algcrealP [x y].

Lemma neq_algcrealP (x y : algcreal) : reflect (x != y)%CR (~~ eq_algcreal x y).
Implicit Arguments neq_algcrealP [x y].

Fact eq_algcreal_is_equiv : equiv_class_of eq_algcreal.

Canonical eq_algcreal_rel := EquivRelPack eq_algcreal_is_equiv.

Lemma root_div_algcreal (x y : algcreal) (y_neq0 : (y != 0)%CR) :
  (annul_creal y).[0] != 0 →
  ((div_annihilant (annul_creal x) (annul_creal y)).[x / y_neq0] == 0)%CR.

Definition div_algcreal (x y : algcreal) :=
  match eq_algcreal_dec y (cst_algcreal 0) with
    | left y_eq0cst_algcreal 0
    | right y_neq0
      let: exist2 y' py'0_neq0 (y'_neq0, _) := simplify_algcreal y_neq0 in
      AlgCRealOf (div_annihilant_algcreal_neq0 x py'0_neq0)
                 (@root_div_algcreal x y' y'_neq0 py'0_neq0)
  end.

Lemma root_inv_algcreal (x : algcreal) (x_neq0 : (x != 0)%CR) :
  ((annul_creal (div_algcreal (cst_algcreal 1) x)).[x_neq0^-1] == 0)%CR.

Definition inv_algcreal (x : algcreal) :=
  match eq_algcreal_dec x (cst_algcreal 0) with
    | left x_eq0cst_algcreal 0
    | right x_neq0
      AlgCReal (@monic_annul_creal _) (@root_inv_algcreal _ x_neq0)
  end.

Lemma div_creal_creal (y : creal F) (y_neq0 : (y != 0)%CR) :
  (y / y_neq0 == 1%:CR)%CR.

Lemma root_mul_algcreal (x y : algcreal) :
  ((annul_creal (div_algcreal x (inv_algcreal y))).[x × y] == 0)%CR.

Definition mul_algcreal (x y : algcreal) :=
  AlgCReal (@monic_annul_creal _) (@root_mul_algcreal x y).

Lemma le_creal_neqVlt (x y : algcreal) : (x y)%CR{(x == y)%CR} + {(x < y)%CR}.

Lemma ltVge_algcreal_dec (x y : algcreal) : {(x < y)%CR} + {(y x)%CR}.

Definition lt_algcreal : rel algcreal := ltVge_algcreal_dec.
Definition le_algcreal : rel algcreal := fun x y~~ ltVge_algcreal_dec y x.

Lemma lt_algcrealP (x y : algcreal) : reflect (x < y)%CR (lt_algcreal x y).
Implicit Arguments lt_algcrealP [x y].

Lemma le_algcrealP (x y : algcreal) : reflect (x y)%CR (le_algcreal x y).
Implicit Arguments le_algcrealP [x y].

Definition exp_algcreal x n := iterop n mul_algcreal x one_algcreal.

Lemma exp_algcrealE x n : (exp_algcreal x n == x ^+ n)%CR.

Definition horner_algcreal (p : {poly F}) x : algcreal :=
  \big[add_algcreal/zero_algcreal]_(i < size p)
   mul_algcreal (cst_algcreal p`_i) (exp_algcreal x i).

Lemma horner_algcrealE p x : (horner_algcreal p x == p.[x])%CR.

Definition norm_algcreal (x : algcreal) :=
  if le_algcreal zero_algcreal x then x else opp_algcreal x.

Lemma norm_algcrealE (x : algcreal) : (norm_algcreal x == `| x |)%CR.

Theory of algdom

CoInductive algdom := AlgDom {
  annul_algdom : {poly F};
  center_alg : F;
  radius_alg : F;
  _ : annul_algdom \is monic;
  _ : radius_alg 0;
  _ : annul_algdom.[center_alg - radius_alg]
      × annul_algdom.[center_alg + radius_alg] 0
}.

Lemma radius_alg_ge0 x : 0 radius_alg x.

Lemma monic_annul_algdom x : annul_algdom x \is monic.
Hint Resolve monic_annul_algdom.

Lemma annul_algdom_eq0 x : (annul_algdom x == 0) = false.

Lemma algdomP x : (annul_algdom x).[center_alg x - radius_alg x]
  × (annul_algdom x).[center_alg x + radius_alg x] 0.

Definition algdom' := seq F.

Definition encode_algdom (x : algdom) : algdom' :=
  [:: center_alg x, radius_alg x & (annul_algdom x)].

Definition decode_algdom (x : algdom') : option algdom :=
  if x is [::c, r & p']
  then let p := Poly p' in
    if ((p \is monic) =P true, (r 0) =P true,
       (p.[c - r] × p.[c + r] 0) =P true)
    is (ReflectT monic_p, ReflectT r_gt0, ReflectT hp)
      then Some (AlgDom monic_p r_gt0 hp)
      else None
  else None.

Lemma encode_algdomK : pcancel encode_algdom decode_algdom.

Definition algdom_EqMixin := PcanEqMixin encode_algdomK.
Canonical algdom_eqType := EqType algdom algdom_EqMixin.

Definition algdom_ChoiceMixin := PcanChoiceMixin encode_algdomK.
Canonical algdom_choiceType := ChoiceType algdom algdom_ChoiceMixin.

Fixpoint to_algcreal_of (p : {poly F}) (c r : F) (i : nat) : F :=
  match i with
    | 0 ⇒ c
    | i.+1
      let c' := to_algcreal_of p c r i in
        if p.[c' - r / 2%:R ^+ i] × p.[c'] 0
          then c' - r / 2%:R ^+ i.+1
          else c' + r / 2%:R ^+ i.+1
  end.

Lemma to_algcreal_of_recP p c r i : 0 r
  `|to_algcreal_of p c r i.+1 - to_algcreal_of p c r i| r × 2%:R ^- i.+1.

Lemma to_algcreal_ofP p c r i j : 0 r → (i j)%N
  `|to_algcreal_of p c r j - to_algcreal_of p c r i| r × 2%:R ^- i.

Lemma alg_to_crealP (x : algdom) :
  creal_axiom (to_algcreal_of (annul_algdom x) (center_alg x) (radius_alg x)).

Definition alg_to_creal x := CReal (alg_to_crealP x).

Lemma exp2k_crealP : @creal_axiom F (fun i ⇒ 2%:R ^- i).
Definition exp2k_creal := CReal exp2k_crealP.

Lemma exp2k_creal_eq0 : (exp2k_creal == 0)%CR.

Notation lbound0_of p := (@lbound0P _ _ p _ _ _).

Lemma to_algcrealP (x : algdom) : ((annul_algdom x).[alg_to_creal x] == 0)%CR.

Definition to_algcreal_rec (x : algdom) :=
  AlgCReal (monic_annul_algdom x) (@to_algcrealP x).
Definition to_algcreal := locked to_algcreal_rec.

Lemma to_algdom_exists (x : algcreal) :
  { y : algdom | (to_algcreal y == x)%CR }.

Definition to_algdom x := projT1 (to_algdom_exists x).

Lemma to_algdomK x : (to_algcreal (to_algdom x) == x)%CR.

Lemma eq_algcreal_to_algdom x : eq_algcreal (to_algcreal (to_algdom x)) x.

Canonical eq_algcreal_encModRel := EncModRel eq_algcreal eq_algcreal_to_algdom.

Local Open Scope quotient_scope.

Definition alg := {eq_quot eq_algcreal}.

Definition alg_of of (phant F) := alg.
Identity Coercion type_alg_of : alg_of >-> alg.

Notation "{ 'alg' F }" := (alg_of (Phant F)).

Canonical alg_eqType := [eqType of alg].
Canonical alg_choiceType := [choiceType of alg].
Canonical alg_quotType := [quotType of alg].
Canonical alg_eqQuotType := [eqQuotType eq_algcreal of alg].
Canonical alg_of_eqType := [eqType of {alg F}].
Canonical alg_of_choiceType := [choiceType of {alg F}].
Canonical alg_of_quotType := [quotType of {alg F}].
Canonical alg_of_eqQuotType := [eqQuotType eq_algcreal of {alg F}].

Definition to_alg_def (phF : phant F) : F{alg F} :=
  lift_embed {alg F} cst_algcreal.
Notation to_alg := (@to_alg_def (Phant F)).
Notation "x %:RA" := (to_alg x)
  (at level 2, left associativity, format "x %:RA").

Canonical to_alg_pi_morph := PiEmbed to_alg.

Local Notation zero_alg := 0%:RA.
Local Notation one_alg := 1%:RA.

Lemma equiv_alg (x y : algcreal) : (x == y)%CR (x = y %[mod {alg F}]).

Lemma nequiv_alg (x y : algcreal) : reflect (x != y)%CR (x != y %[mod {alg F}]).
Implicit Arguments nequiv_alg [x y].

Lemma pi_algK (x : algcreal) : (repr (\pi_{alg F} x) == x)%CR.

Definition add_alg := lift_op2 {alg F} add_algcreal.

Lemma pi_add : {morph \pi_{alg F} : x y / add_algcreal x y >-> add_alg x y}.

Canonical add_pi_morph := PiMorph2 pi_add.

Definition opp_alg := lift_op1 {alg F} opp_algcreal.

Lemma pi_opp : {morph \pi_{alg F} : x / opp_algcreal x >-> opp_alg x}.

Canonical opp_pi_morph := PiMorph1 pi_opp.

Definition mul_alg := lift_op2 {alg F} mul_algcreal.

Lemma pi_mul : {morph \pi_{alg F} : x y / mul_algcreal x y >-> mul_alg x y}.

Canonical mul_pi_morph := PiMorph2 pi_mul.

Definition inv_alg := lift_op1 {alg F} inv_algcreal.

Lemma pi_inv : {morph \pi_{alg F} : x / inv_algcreal x >-> inv_alg x}.

Canonical inv_pi_morph := PiMorph1 pi_inv.

Lemma add_algA : associative add_alg.

Lemma add_algC : commutative add_alg.

Lemma add_0alg : left_id zero_alg add_alg.

Lemma add_Nalg : left_inverse zero_alg opp_alg add_alg.

Definition alg_zmodMixin := ZmodMixin add_algA add_algC add_0alg add_Nalg.
Canonical alg_zmodType := Eval hnf in ZmodType alg alg_zmodMixin.
Canonical alg_of_zmodType := Eval hnf in ZmodType {alg F} alg_zmodMixin.

Lemma add_pi x y : \pi_{alg F} x + \pi_{alg F} y
  = \pi_{alg F} (add_algcreal x y).

Lemma opp_pi x : - \pi_{alg F} x = \pi_{alg F} (opp_algcreal x).

Lemma zeroE : 0 = \pi_{alg F} zero_algcreal.

Lemma sub_pi x y : \pi_{alg F} x - \pi_{alg F} y
  = \pi_{alg F} (add_algcreal x (opp_algcreal y)).

Lemma mul_algC : commutative mul_alg.

Lemma mul_algA : associative mul_alg.

Lemma mul_1alg : left_id one_alg mul_alg.

Lemma mul_alg_addl : left_distributive mul_alg add_alg.

Implicit Arguments neq_creal_cst [F x y].

Lemma nonzero1_alg : one_alg != zero_alg.

Definition alg_comRingMixin :=
  ComRingMixin mul_algA mul_algC mul_1alg mul_alg_addl nonzero1_alg.
Canonical alg_Ring := Eval hnf in RingType alg alg_comRingMixin.
Canonical alg_comRing := Eval hnf in ComRingType alg mul_algC.
Canonical alg_of_Ring := Eval hnf in RingType {alg F} alg_comRingMixin.
Canonical alg_of_comRing := Eval hnf in ComRingType {alg F} mul_algC.

Lemma mul_pi x y : \pi_{alg F} x × \pi_{alg F} y
  = \pi_{alg F} (mul_algcreal x y).

Lemma oneE : 1 = \pi_{alg F} one_algcreal.

Lemma mul_Valg (x : alg) : x != zero_algmul_alg (inv_alg x) x = one_alg.

Lemma inv_alg0 : inv_alg zero_alg = zero_alg.

Definition AlgFieldUnitMixin := FieldUnitMixin mul_Valg inv_alg0.
Canonical alg_unitRing :=
  Eval hnf in UnitRingType alg AlgFieldUnitMixin.
Canonical alg_comUnitRing := Eval hnf in [comUnitRingType of alg].
Canonical alg_of_unitRing :=
  Eval hnf in UnitRingType {alg F} AlgFieldUnitMixin.
Canonical alg_of_comUnitRing := Eval hnf in [comUnitRingType of {alg F}].

Lemma field_axiom : GRing.Field.mixin_of alg_unitRing.

Definition AlgFieldIdomainMixin := (FieldIdomainMixin field_axiom).
Canonical alg_iDomain :=
  Eval hnf in IdomainType alg (FieldIdomainMixin field_axiom).
Canonical alg_fieldType := FieldType alg field_axiom.
Canonical alg_of_iDomain :=
  Eval hnf in IdomainType {alg F} (FieldIdomainMixin field_axiom).
Canonical alg_of_fieldType := FieldType {alg F} field_axiom.

Lemma inv_pi x : (\pi_{alg F} x)^-1 = \pi_{alg F} (inv_algcreal x).

Lemma div_pi x y : \pi_{alg F} x / \pi_{alg F} y
  = \pi_{alg F} (mul_algcreal x (inv_algcreal y)).

Definition lt_alg := lift_fun2 {alg F} lt_algcreal.
Definition le_alg := lift_fun2 {alg F} le_algcreal.

Lemma lt_alg_pi : {mono \pi_{alg F} : x y / lt_algcreal x y >-> lt_alg x y}.

Canonical lt_alg_pi_mono := PiMono2 lt_alg_pi.

Lemma le_alg_pi : {mono \pi_{alg F} : x y / le_algcreal x y >-> le_alg x y}.

Canonical le_alg_pi_mono := PiMono2 le_alg_pi.

Definition norm_alg := lift_op1 {alg F} norm_algcreal.

Lemma norm_alg_pi : {morph \pi_{alg F} : x / norm_algcreal x >-> norm_alg x}.

Canonical norm_alg_pi_morph := PiMorph1 norm_alg_pi.

Lemma norm_pi (x : algcreal) : `|\pi_{alg F} x| = \pi (norm_algcreal x). Proof. by rewrite /norm_algcreal -lt_pi -zeroE -lerNgt fun_if -opp_pi. Qed.

Lemma add_alg_gt0 x y : lt_alg zero_alg xlt_alg zero_alg y
  lt_alg zero_alg (x + y).

Lemma mul_alg_gt0 x y : lt_alg zero_alg xlt_alg zero_alg y
  lt_alg zero_alg (x × y).

Lemma gt0_alg_nlt0 x : lt_alg zero_alg x~~ lt_alg x zero_alg.

Lemma sub_alg_gt0 x y : lt_alg zero_alg (y - x) = lt_alg x y.

Lemma lt0_alg_total (x : alg) : x != zero_alg
  lt_alg zero_alg x || lt_alg x zero_alg.

Lemma norm_algN x : norm_alg (- x) = norm_alg x.

Lemma ge0_norm_alg x : le_alg 0 xnorm_alg x = x.

Lemma lt_alg0N (x : alg) : lt_alg 0 (- x) = lt_alg x 0.

Lemma lt_alg00 : lt_alg zero_alg zero_alg = false.

Lemma le_alg_def x y : le_alg x y = (y == x) || lt_alg x y.

Definition AlgNumFieldMixin := RealLtMixin add_alg_gt0 mul_alg_gt0
  gt0_alg_nlt0 sub_alg_gt0 lt0_alg_total norm_algN ge0_norm_alg le_alg_def.
Canonical alg_numDomainType := NumDomainType alg AlgNumFieldMixin.
Canonical alg_numFieldType := [numFieldType of alg].
Canonical alg_of_numDomainType := [numDomainType of {alg F}].
Canonical alg_of_numFieldType := [numFieldType of {alg F}].

Definition AlgRealFieldMixin := RealLeAxiom alg.
Canonical alg_realDomainType := RealDomainType alg AlgRealFieldMixin.
Canonical alg_realFieldType := [realFieldType of alg].
Canonical alg_of_realDomainType := [realDomainType of {alg F}].
Canonical alg_of_realFieldType := [realFieldType of {alg F}].

Lemma lt_pi x y : \pi_{alg F} x < \pi y = lt_algcreal x y.

Lemma le_pi x y : \pi_{alg F} x \pi y = le_algcreal x y.

Lemma norm_pi (x : algcreal) : `|\pi_{alg F} x| = \pi (norm_algcreal x).

Lemma lt_algP (x y : algcreal) : reflect (x < y)%CR (\pi_{alg F} x < \pi y).
Implicit Arguments lt_algP [x y].

Lemma le_algP (x y : algcreal) : reflect (x y)%CR (\pi_{alg F} x \pi y).
Implicit Arguments le_algP [x y].

Lemma to_alg_additive : additive to_alg.

Canonical to_alg_is_additive := Additive to_alg_additive.

Lemma to_alg_multiplicative : multiplicative to_alg.

Canonical to_alg_is_rmorphism := AddRMorphism to_alg_multiplicative.

Definition annul_alg : {alg F}{poly F} := locked (annul_creal \o repr).

Local Notation "p ^ f" := (map_poly f p) : ring_scope.
Notation "'Y" := 'X%:P.

Lemma expn_pi (x : algcreal) (n : nat) :
  (\pi_{alg F} x) ^+ n = \pi (exp_algcreal x n).

Lemma horner_pi (p : {poly F}) (x : algcreal) :
  (p ^ to_alg).[\pi_alg x] = \pi (horner_algcreal p x).

Lemma root_annul_algcreal (x : algcreal) : ((annul_alg (\pi x)).[x] == 0)%CR.

Lemma root_annul_alg (x : {alg F}) : root ((annul_alg x) ^ to_alg) x.

Lemma monic_annul_alg (x : {alg F}) : annul_alg x \is monic.

Lemma annul_alg_neq0 (x : {alg F}) : annul_alg x != 0.

Lemma map_comp_poly (aR : fieldType) (rR : idomainType) (f : {rmorphism aRrR})
   (p q : {poly aR}) : (p \Po q) ^ f = (p ^ f) \Po (q ^ f).

Lemma ler_to_alg : {mono to_alg : x y / x y}.

Lemma ltr_to_alg : {mono to_alg : x y / x < y}.

Lemma inf_alg_proof x : {d | 0 < d & 0 < x → (d%:RA < x)}.

Definition inf_alg (x : {alg F}) : F :=
  let: exist2 d _ _ := inf_alg_proof x in d.

Lemma inf_alg_gt0 x : 0 < inf_alg x.

Lemma inf_lt_alg x : 0 < x(inf_alg x)%:RA < x.

Lemma approx_proof x e : {y | 0 < e`|x - y%:RA| < e}.

Definition approx := locked
  (fun (x : alg) (e : alg) ⇒ projT1 (approx_proof x e) : F).

Lemma approxP (x e e': alg) : 0 < ee e'`|x - (approx x e)%:RA| < e'.

Lemma pet_alg_proof (s : seq alg) :
  { ap : {alg F} × seq {poly F} |
    [ i : 'I_(size s), (ap.2`_i ^ to_alg).[ap.1] == s`_i]
    & size ap.2 = size s }.

Lemma weak_ivt (p : {poly F}) (a b : F) : a bp.[a] 0 p.[b]
  { x : alg | a%:RA x b%:RA & root (p ^ to_alg) x }.

Lemma alg_archi : Num.archimedean_axiom alg_of_numDomainType.

Canonical alg_archiFieldType := ArchiFieldType alg alg_archi.
Canonical alg_of_archiFieldType := [archiFieldType of {alg F}].

Lemma normr_to_alg : { morph to_alg : x / `|x| }.

Definition pet_alg s : {alg F} :=
  let: exist2 (a, _) _ _ := pet_alg_proof s in a.
Definition pet_alg_poly s : seq {poly F}:=
  let: exist2 (_, sp) _ _ := pet_alg_proof s in sp.

Lemma size_pet_alg_poly s : size (pet_alg_poly s) = size s.

Lemma pet_algK s i :
   ((pet_alg_poly s)`_i ^ to_alg).[pet_alg s] = s`_i.

Definition poly_ground := locked (fun (p : {poly {alg F}}) ⇒
  swapXY (Poly (pet_alg_poly p)) : {poly {poly F}}).

Lemma sizeY_poly_ground p : sizeY (poly_ground p) = size p.

Lemma poly_ground_eq0 p : (poly_ground p == 0) = (p == 0).

Lemma poly_ground0 : poly_ground 0 = 0.

Lemma poly_groundK p :
  ((poly_ground p) ^ (map_poly to_alg)).[(pet_alg p)%:P] = p.

Lemma annul_from_alg_proof (p : {poly alg}) (q : {poly F}) :
  p != 0 → q != 0 → root (q ^ to_alg) (pet_alg p)
  → {r | resultant (poly_ground p) (r ^ polyC) != 0
        & (r != 0) && (root (r ^ to_alg) (pet_alg p))}.

Definition annul_pet_alg (p : {poly {alg F}}) : {poly F} :=
    if (p != 0) =P true is ReflectT p_neq0 then
      let: exist2 r _ _ :=
        annul_from_alg_proof p_neq0 (annul_alg_neq0 _) (root_annul_alg _) in r
      else 0.

Lemma root_annul_pet_alg p : root (annul_pet_alg p ^ to_alg) (pet_alg p).

Definition annul_from_alg p :=
  if (size (poly_ground p) == 1)%N then lead_coef (poly_ground p)
    else resultant (poly_ground p) (annul_pet_alg p ^ polyC).

Lemma annul_from_alg_neq0 p : p != 0 → annul_from_alg p != 0.

Lemma annul_pet_alg_neq0 p : p != 0 → annul_pet_alg p != 0.

End RealAlg.

Notation to_alg F := (@to_alg_def _ (Phant F)).
Notation "x %:RA" := (to_alg _ x)
  (at level 2, left associativity, format "x %:RA").

Lemma upper_nthrootVP (F : archiFieldType) (x : F) (i : nat) :
   0 < x → (Num.bound (x ^-1) i)%N → 2%:R ^- i < x.

Notation "{ 'alg' F }" := (alg_of (Phant F)).

Section AlgAlg.

Variable F : archiFieldType.

Local Open Scope ring_scope.

Local Notation "p ^ f" := (map_poly f p) : ring_scope.
Local Notation "'Y" := 'X%:P.
Local Notation m0 := (fun _ ⇒ 0%N).

Definition approx2 (x : {alg {alg F}}) i :=
  approx (approx x (2%:R ^- i)) (2%:R ^- i).

Lemma asympt_approx2 x : { asympt e : i / `|(approx2 x i)%:RA%:RA - x| < e }.

Lemma from_alg_crealP (x : {alg {alg F}}) : creal_axiom (approx2 x).

Definition from_alg_creal := locked (fun xCReal (from_alg_crealP x)).

Lemma to_alg_crealP (x : creal F) : creal_axiom (fun ito_alg F (x i)).
Definition to_alg_creal x := CReal (to_alg_crealP x).

Lemma horner_to_alg_creal p x :
  ((p ^ to_alg F).[to_alg_creal x] == to_alg_creal p.[x])%CR.

Lemma neq_to_alg_creal x y :
  (to_alg_creal x != to_alg_creal y)%CR (x != y)%CR.

Lemma eq_to_alg_creal x y :
  (to_alg_creal x == to_alg_creal y)%CR → (x == y)%CR.

Lemma to_alg_creal0 : (to_alg_creal 0 == 0)%CR.

Import Setoid.

Add Morphism to_alg_creal
 with signature (@eq_creal _) ==> (@eq_creal _) as to_alg_creal_morph.
Global
Lemma to_alg_creal_repr (x : {alg F}) : (to_alg_creal (repr x) == x%:CR)%CR.

Local Open Scope quotient_scope.

Lemma cst_pi (x : algcreal F) : ((\pi_{alg F} x)%:CR == to_alg_creal x)%CR.

End AlgAlg.

Section AlgAlgAlg.

Variable F : archiFieldType.

Local Open Scope ring_scope.

Local Notation "p ^ f" := (map_poly f p) : ring_scope.
Local Notation "'Y" := 'X%:P.

Lemma from_alg_crealK (x : {alg {alg F}}) :
  (to_alg_creal (to_alg_creal (from_alg_creal x)) == x%:CR)%CR.

Lemma root_annul_from_alg_creal (x : {alg {alg F}}) :
  ((annul_from_alg (annul_alg x)).[from_alg_creal x] == 0)%CR.

Lemma annul_alg_from_alg_creal_neq0 (x : {alg {alg F}}) :
  annul_from_alg (annul_alg x) != 0.

Definition from_alg_algcreal x :=
  AlgCRealOf (@annul_alg_from_alg_creal_neq0 x) (@root_annul_from_alg_creal x).

Definition from_alg : {alg {alg F}}{alg F} :=
  locked (\pi%qT \o from_alg_algcreal).

Lemma from_algK : cancel from_alg (to_alg _).

Lemma ivt (p : {poly (alg F)}) (a b : alg F) : a b
  p.[a] 0 p.[b]exists2 x : alg F, a x b & root p x.

Canonical alg_rcfType := RcfType (alg F) ivt.
Canonical alg_of_rcfType := [rcfType of {alg F}].

End AlgAlgAlg.
End RealAlg.

Notation "{ 'realclosure' F }" := (RealAlg.alg_of (Phant F)).

Notation annul_realalg := RealAlg.annul_alg.
Notation realalg_of F := (@RealAlg.to_alg_def _ (Phant F)).
Notation "x %:RA" := (realalg_of x)
  (at level 2, left associativity, format "x %:RA").

Canonical RealAlg.alg_eqType.
Canonical RealAlg.alg_choiceType.
Canonical RealAlg.alg_zmodType.
Canonical RealAlg.alg_Ring.
Canonical RealAlg.alg_comRing.
Canonical RealAlg.alg_unitRing.
Canonical RealAlg.alg_comUnitRing.
Canonical RealAlg.alg_iDomain.
Canonical RealAlg.alg_fieldType.
Canonical RealAlg.alg_numDomainType.
Canonical RealAlg.alg_numFieldType.
Canonical RealAlg.alg_realDomainType.
Canonical RealAlg.alg_realFieldType.
Canonical RealAlg.alg_archiFieldType.
Canonical RealAlg.alg_rcfType.

Canonical RealAlg.alg_of_eqType.
Canonical RealAlg.alg_of_choiceType.
Canonical RealAlg.alg_of_zmodType.
Canonical RealAlg.alg_of_Ring.
Canonical RealAlg.alg_of_comRing.
Canonical RealAlg.alg_of_unitRing.
Canonical RealAlg.alg_of_comUnitRing.
Canonical RealAlg.alg_of_iDomain.
Canonical RealAlg.alg_of_fieldType.
Canonical RealAlg.alg_of_numDomainType.
Canonical RealAlg.alg_of_numFieldType.
Canonical RealAlg.alg_of_realDomainType.
Canonical RealAlg.alg_of_realFieldType.
Canonical RealAlg.alg_of_archiFieldType.
Canonical RealAlg.alg_of_rcfType.

Canonical RealAlg.to_alg_is_rmorphism.
Canonical RealAlg.to_alg_is_additive.

Section RealClosureTheory.

Variable F : archiFieldType.
Notation R := {realclosure F}.

Local Notation "p ^ f" := (map_poly f p) : ring_scope.

Lemma root_annul_realalg (x : R) : root ((annul_realalg x) ^ realalg_of _) x.
Hint Resolve root_annul_realalg.

Lemma monic_annul_realalg (x : R) : annul_realalg x \is monic.
Hint Resolve monic_annul_realalg.

Lemma annul_realalg_neq0 (x : R) : annul_realalg x != 0%R.
Hint Resolve annul_realalg_neq0.

Lemma realalg_algebraic : integralRange (realalg_of F).

End RealClosureTheory.

Definition realalg := {realclosure rat}.
Canonical realalg_eqType := [eqType of realalg].
Canonical realalg_choiceType := [choiceType of realalg].
Canonical realalg_zmodType := [zmodType of realalg].
Canonical realalg_ringType := [ringType of realalg].
Canonical realalg_comRingType := [comRingType of realalg].
Canonical realalg_unitRingType := [unitRingType of realalg].
Canonical realalg_comUnitRingType := [comUnitRingType of realalg].
Canonical realalg_idomainType := [idomainType of realalg].
Canonical realalg_fieldTypeType := [fieldType of realalg].
Canonical realalg_numDomainType := [numDomainType of realalg].
Canonical realalg_numFieldType := [numFieldType of realalg].
Canonical realalg_realDomainType := [realDomainType of realalg].
Canonical realalg_realFieldType := [realFieldType of realalg].
Canonical realalg_archiFieldType := [archiFieldType of realalg].
Canonical realalg_rcfType := [rcfType of realalg].

Module RatRealAlg.
Canonical RealAlg.algdom_choiceType.
Definition realalgdom_CountMixin :=
   PcanCountMixin (@RealAlg.encode_algdomK [archiFieldType of rat]).
Canonical realalgdom_countType :=
   CountType (RealAlg.algdom [archiFieldType of rat]) realalgdom_CountMixin.
Definition realalg_countType := [countType of realalg].
End RatRealAlg.

Canonical RatRealAlg.realalg_countType.

Require Import countalg. Canonical realalg_countZmodType := [countZmodType of realalg]. Canonical realalg_countRingType := [countRingType of realalg]. Canonical realalg_countComRingType := [countComRingType of realalg]. Canonical realalg_countUnitRingType := [countUnitRingType of realalg]. Canonical realalg_countComUnitRingType := [countComUnitRingType of realalg]. Canonical realalg_countIdomainType := [countIdomainType of realalg]. Canonical realalg_countFieldTypeType := [countFieldType of realalg].