Library MathComp.closed_field

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import bigop ssralg poly polydiv.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.
Local Open Scope ring_scope.

Import Pdiv.Ring.
Import PreClosedField.

Section ClosedFieldQE.

Variable F : Field.type.

Variable axiom : ClosedField.axiom F.

Notation fF := (formula F).
Notation qf f := (qf_form f && rformula f).

Definition polyF := seq (term F).

Fixpoint eval_poly (e : seq F) pf :=
  if pf is c::qf then (eval_poly e qf)*'X + (eval e c)%:P else 0.

Definition rpoly (p : polyF) := all (@rterm F) p.

Fixpoint sizeT (k : natfF) (p : polyF) :=
  if p is c::q then
    sizeT (fun n
      if n is m.+1 then k m.+2 else
        GRing.If (c == 0) (k 0%N) (k 1%N)) q
   else k O%N.

Lemma sizeTP (k : natformula F) (pf : polyF) (e : seq F) :
  qf_eval e (sizeT k pf) = qf_eval e (k (size (eval_poly e pf))).
Proof.
elim: pf e k; first by move⇒ *; rewrite size_poly0.
movec qf Pqf e k; rewrite Pqf.
rewrite size_MXaddC -(size_poly_eq0 (eval_poly _ _)).
by case: (size (eval_poly e qf))=> //=; case: eqP; rewrite // orbF.
Qed.

Lemma sizeT_qf (k : natformula F) (p : polyF) :
  ( n, qf (k n)) → rpoly pqf (sizeT k p).
Proof.
elim: p k ⇒ /= [|c q ihp] k kP rp; first exact: kP.
case/andP: rprc rq.
apply: ihp; rewrite ?rq //; case⇒ [|n]; last exact: kP.
have [/andP[qf0 rf0] /andP[qf1 rf1]] := (kP 0, kP 1)%N.
by rewrite If_form_qf ?If_form_rf //= andbT.
Qed.

Definition isnull (k : boolfF) (p : polyF) :=
  sizeT (fun nk (n == 0%N)) p.

Lemma isnullP (k : boolformula F) (p : polyF) (e : seq F) :
  qf_eval e (isnull k p) = qf_eval e (k (eval_poly e p == 0)).
Proof. by rewrite sizeTP size_poly_eq0. Qed.

Lemma isnull_qf (k : boolformula F) (p : polyF) :
  ( b, qf (k b)) → rpoly pqf (isnull k p).
Proof. by move⇒ *; apply: sizeT_qf. Qed.

Definition lt_sizeT (k : boolfF) (p q : polyF) : fF :=
  sizeT (fun nsizeT (fun mk (n<m)) q) p.

Definition lift (p : {poly F}) := let: q := p in map Const q.

Lemma eval_lift (e : seq F) (p : {poly F}) : eval_poly e (lift p) = p.
Proof.
elim/poly_ind: p ⇒ [|p c]; first by rewrite /lift polyseq0.
rewrite -cons_poly_def /lift polyseq_cons /nilp.
case pn0: (_ == _) ⇒ /=; last by move->; rewrite -cons_poly_def.
move_; rewrite polyseqC.
case c0: (_==_)=> /=.
  move: pn0; rewrite (eqP c0) size_poly_eq0; move/eqP→.
  by apply:val_inj⇒ /=; rewrite polyseq_cons // polyseq0.
by rewrite mul0r add0r; apply:val_inj⇒ /=; rewrite polyseq_cons // /nilp pn0.
Qed.

Fixpoint lead_coefT (k : term FfF) p :=
  if p is c::q then
    lead_coefT (fun lGRing.If (l == 0) (k c) (k l)) q
  else k (Const 0).

Lemma lead_coefTP (k : term Fformula F) :
 ( x e, qf_eval e (k x) = qf_eval e (k (Const (eval e x)))) →
   (p : polyF) (e : seq F),
  qf_eval e (lead_coefT k p) = qf_eval e (k (Const (lead_coef (eval_poly e p)))).
Proof.
movePk p e; elim: p k Pk ⇒ /= [*|a p' Pp' k Pk]; first by rewrite lead_coef0.
rewrite Pp'; last by move⇒ *; rewrite //= -Pk.
rewrite GRing.eval_If /= lead_coef_eq0.
case p'0: (_ == _); first by rewrite (eqP p'0) mul0r add0r lead_coefC -Pk.
rewrite lead_coefDl ?lead_coefMX // polyseqC size_mul ?p'0 //; last first.
  by rewrite -size_poly_eq0 size_polyX.
rewrite size_polyX addnC /=; case: (_ == _)=> //=.
by rewrite ltnS lt0n size_poly_eq0 p'0.
Qed.

Lemma lead_coefT_qf (k : term Fformula F) (p : polyF) :
 ( c, rterm cqf (k c)) → rpoly pqf (lead_coefT k p).
Proof.
elim: p k ⇒ /= [|c q ihp] k kP rp; first exact: kP.
move: rp; case/andPrc rq; apply: ihp; rewrite ?rq // ⇒ l rl.
have [/andP[qfc rfc] /andP[qfl rfl]] := (kP c rc, kP l rl).
by rewrite If_form_qf ?If_form_rf //= andbT.
Qed.

Fixpoint amulXnT (a : term F) (n : nat) : polyF :=
  if n is n'.+1 then (Const 0) :: (amulXnT a n') else [::a].

Lemma eval_amulXnT (a : term F) (n : nat) (e : seq F) :
  eval_poly e (amulXnT a n) = (eval e a)%:P × 'X^n.
Proof.
elim: n⇒ [|n] /=; first by rewrite expr0 mulr1 mul0r add0r.
by move->; rewrite addr0 -mulrA -exprSr.
Qed.

Lemma ramulXnT: a n, rterm arpoly (amulXnT a n).
Proof. by movea n; elim: n a⇒ [a /= → //|n ihn a ra]; apply: ihn. Qed.

Fixpoint sumpT (p q : polyF) :=
  if p is a::p' then
    if q is b::q' then (Add a b)::(sumpT p' q')
      else p
    else q.

Lemma eval_sumpT (p q : polyF) (e : seq F) :
  eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).
Proof.
elim: p q ⇒ [|a p Hp] q /=; first by rewrite add0r.
case: q ⇒ [|b q] /=; first by rewrite addr0.
rewrite Hp mulrDl -!addrA; congr (_+_); rewrite polyC_add addrC -addrA.
by congr (_+_); rewrite addrC.
Qed.

Lemma rsumpT (p q : polyF) : rpoly prpoly qrpoly (sumpT p q).
Proof.
elim: p q⇒ [|a p ihp] q rp rq //; move: rp; case/andPra rp.
case: q rq ⇒ [|b q]; rewrite /= ?ra ?rp //=.
by case/andP⇒ → rq //=; apply: ihp.
Qed.

Fixpoint mulpT (p q : polyF) :=
  if p is a :: p' then sumpT (map (Mul a) q) (Const 0::(mulpT p' q)) else [::].

Lemma eval_mulpT (p q : polyF) (e : seq F) :
  eval_poly e (mulpT p q) = (eval_poly e p) × (eval_poly e q).
Proof.
elim: p q⇒ [|a p Hp] q /=; first by rewrite mul0r.
rewrite eval_sumpT /= Hp addr0 mulrDl addrC mulrAC; congr (_+_).
elim: q⇒ [|b q Hq] /=; first by rewrite mulr0.
by rewrite Hq polyC_mul mulrDr mulrA.
Qed.

Lemma rpoly_map_mul (t : term F) (p : polyF) (rt : rterm t) :
  rpoly (map (Mul t) p) = rpoly p.
Proof.
by rewrite /rpoly all_map /= (@eq_all _ _ (@rterm _)) // ⇒ x; rewrite /= rt.
Qed.

Lemma rmulpT (p q : polyF) : rpoly prpoly qrpoly (mulpT p q).
Proof.
elim: p q⇒ [|a p ihp] q rp rq //=; move: rp; case/andPra rp /=.
apply: rsumpT; last exact: ihp.
by rewrite rpoly_map_mul.
Qed.

Definition opppT := map (Mul (@Const F (-1))).

Lemma eval_opppT (p : polyF) (e : seq F) :
 eval_poly e (opppT p) = - eval_poly e p.
Proof.
by elim: p; rewrite /= ?oppr0 // ⇒ ? ? ->; rewrite !mulNr opprD polyC_opp mul1r.
Qed.

Definition natmulpT n := map (Mul (@NatConst F n)).

Lemma eval_natmulpT (p : polyF) (n : nat) (e : seq F) :
  eval_poly e (natmulpT n p) = (eval_poly e p) *+ n.
Proof.
elim: p; rewrite //= ?mul0rn // ⇒ c p →.
rewrite mulrnDl mulr_natl polyC_muln; congr (_+_).
by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC.
Qed.

Fixpoint redivp_rec_loopT (q : polyF) sq cq (k : nat × polyF × polyFfF)
  (c : nat) (qq r : polyF) (n : nat) {struct n}:=
  sizeT (fun sr
    if sr < sq then k (c, qq, r) else
      lead_coefT (fun lr
        let m := amulXnT lr (sr - sq) in
        let qq1 := sumpT (mulpT qq [::cq]) m in
        let r1 := sumpT (mulpT r ([::cq])) (opppT (mulpT m q)) in
        if n is n1.+1 then redivp_rec_loopT q sq cq k c.+1 qq1 r1 n1
        else k (c.+1, qq1, r1)
      ) r
  ) r.

Fixpoint redivp_rec_loop (q : {poly F}) sq cq
   (k : nat) (qq r : {poly F})(n : nat) {struct n} :=
    if size r < sq then (k, qq, r) else
      let m := (lead_coef r) *: 'X^(size r - sq) in
      let qq1 := qq × cq%:P + m in
      let r1 := r × cq%:P - m × q in
      if n is n1.+1 then redivp_rec_loop q sq cq k.+1 qq1 r1 n1 else
        (k.+1, qq1, r1).

Lemma redivp_rec_loopTP (k : nat × polyF × polyFformula F) :
  ( c qq r e, qf_eval e (k (c,qq,r))
    = qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r))))
  → q sq cq c qq r n e
    (d := redivp_rec_loop (eval_poly e q) sq (eval e cq)
      c (eval_poly e qq) (eval_poly e r) n),
    qf_eval e (redivp_rec_loopT q sq cq k c qq r n)
    = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
Proof.
movePk q sq cq c qq r n e /=.
elim: n c qq r k Pk e ⇒ [|n Pn] c qq r k Pk e; rewrite sizeTP.
  case ltrq : (_ < _); first by rewrite /= ltrq /= -Pk.
  rewrite lead_coefTP ⇒ [|a p]; rewrite Pk.
    rewrite ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=.
    by rewrite ltrq //= mul_polyC ?(mul0r,add0r).
  by symmetry; rewrite Pk ?(eval_mulpT,eval_amulXnT,eval_sumpT, eval_opppT).
case ltrq : (_<_); first by rewrite /= ltrq Pk.
rewrite lead_coefTP.
  rewrite Pn ?(eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT) //=.
  by rewrite ltrq //= mul_polyC ?(mul0r,add0r).
rewrite -/redivp_rec_loopTx e'.
rewrite Pn; last by move=>*; rewrite Pk.
symmetry; rewrite Pn; last by move=>*; rewrite Pk.
rewrite Pk ?(eval_lift,eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT).
by rewrite mul_polyC ?(mul0r,add0r).
Qed.

Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : term F)
 (k : nat × polyF × polyFformula F) (c : nat) (qq r : polyF) (n : nat) :
  ( r, [&& rpoly r.1.2 & rpoly r.2]qf (k r)) →
  rpoly qrterm cqrpoly qqrpoly r
    qf (redivp_rec_loopT q sq cq k c qq r n).
Proof.
elim: n q sq cq k c qq r ⇒ [|n ihn] q sq cq k c qq r kP rq rcq rqq rr.
  apply: sizeT_qf⇒ // n; case: (_ < _); first by apply: kP; rewrite // rqq rr.
  apply: lead_coefT_qf⇒ // l rl; apply: kP.
  by rewrite /= ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq.
apply: sizeT_qf⇒ // m; case: (_ < _); first by apply: kP ⇒ //=; rewrite rqq rr.
apply: lead_coefT_qf⇒ // l rl; apply: ihn; rewrite //= ?rcq //.
  by rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq.
by rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq.
Qed.

Definition redivpT (p : polyF) (k : nat × polyF × polyFfF)
                   (q : polyF) : fF :=
  isnull (fun b
    if b then k (0%N, [::Const 0], p) else
      sizeT (fun sq
        sizeT (fun sp
          lead_coefT (fun lq
            redivp_rec_loopT q sq lq k 0 [::Const 0] p sp
          ) q
        ) p
      ) q
  ) q.

Lemma redivp_rec_loopP (q : {poly F}) (c : nat) (qq r : {poly F}) (n : nat) :
  redivp_rec q c qq r n = redivp_rec_loop q (size q) (lead_coef q) c qq r n.
Proof. by elim: n c qq r ⇒ [| n Pn] c qq r //=; rewrite Pn. Qed.

Lemma redivpTP (k : nat × polyF × polyFformula F) :
  ( c qq r e,
     qf_eval e (k (c,qq,r)) =
     qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r)))) →
   p q e (d := redivp (eval_poly e p) (eval_poly e q)),
    qf_eval e (redivpT p k q) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
Proof.
movePk p q e /=; rewrite isnullP unlock.
case q0 : (_ == _); first by rewrite Pk /= mul0r add0r polyC0.
rewrite !sizeTP lead_coefTP /=; last by move⇒ *; rewrite !redivp_rec_loopTP.
rewrite redivp_rec_loopTP /=; last by move⇒ *; rewrite Pk.
by rewrite mul0r add0r polyC0 redivp_rec_loopP.
Qed.

Lemma redivpT_qf (p : polyF) (k : nat × polyF × polyFformula F) (q : polyF) :
  ( r, [&& rpoly r.1.2 & rpoly r.2]qf (k r)) →
   rpoly prpoly qqf (redivpT p k q).
Proof.
movekP rp rq; rewrite /redivpT; apply: isnull_qf⇒ // [[]]; first exact: kP.
apply: sizeT_qf ⇒ // sq; apply: sizeT_qf⇒ // sp.
apply: lead_coefT_qf⇒ // lq rlq; exact: redivp_rec_loopT_qf.
Qed.

Definition rmodpT (p : polyF) (k : polyFfF) (q : polyF) : fF :=
  redivpT p (fun dk d.2) q.
Definition rdivpT (p : polyF) (k:polyFfF) (q : polyF) : fF :=
  redivpT p (fun dk d.1.2) q.
Definition rscalpT (p : polyF) (k: natfF) (q : polyF) : fF :=
  redivpT p (fun dk d.1.1) q.
Definition rdvdpT (p : polyF) (k:boolfF) (q : polyF) : fF :=
  rmodpT p (isnull k) q.

Fixpoint rgcdp_loop n (pp qq : {poly F}) {struct n} :=
  if rmodp pp qq == 0 then qq
    else if n is n1.+1 then rgcdp_loop n1 qq (rmodp pp qq)
         else rmodp pp qq.

Fixpoint rgcdp_loopT (pp : polyF) (k : polyFformula F) n (qq : polyF) :=
  rmodpT pp (isnull
    (fun bif b then (k qq)
              else (if n is n1.+1
                    then rmodpT pp (rgcdp_loopT qq k n1) qq
                    else rmodpT pp k qq)
    )
            ) qq.

Lemma rgcdp_loopP (k : polyFformula F) :
  ( p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
   n p q e,
    qf_eval e (rgcdp_loopT p k n q) =
    qf_eval e (k (lift (rgcdp_loop n (eval_poly e p) (eval_poly e q)))).
Proof.
movePk n p q e.
elim: n p q e ⇒ /= [| m Pm] p q e.
  rewrite redivpTP; last by move=>*; rewrite !isnullP eval_lift.
  rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk.
  by rewrite redivpTP; last by move=>*; rewrite Pk.
rewrite redivpTP; last by move=>*; rewrite !isnullP eval_lift.
rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk.
by rewrite redivpTP; move=>*; rewrite ?Pm !eval_lift.
Qed.

Lemma rgcdp_loopT_qf (p : polyF) (k : polyFformula F) (q : polyF) (n : nat) :
  ( r, rpoly rqf (k r)) →
  rpoly prpoly qqf (rgcdp_loopT p k n q).
elim: n p k q ⇒ [|n ihn] p k q kP rp rq.
  apply: redivpT_qf⇒ // r; case/andP_ rr.
  apply: isnull_qf⇒ // [[]]; first exact: kP.
  by apply: redivpT_qf⇒ // r'; case/andP_ rr'; apply: kP.
apply: redivpT_qf⇒ // r; case/andP_ rr.
apply: isnull_qf⇒ // [[]]; first exact: kP.
by apply: redivpT_qf⇒ // r'; case/andP_ rr'; apply: ihn.
Qed.

Definition rgcdpT (p : polyF) k (q : polyF) : fF :=
  let aux p1 k q1 := isnull
    (fun bif b
      then (k q1)
      else (sizeT (fun n ⇒ (rgcdp_loopT p1 k n q1)) p1)) p1
    in (lt_sizeT (fun bif b then (aux q k p) else (aux p k q)) p q).

Lemma rgcdpTP (k : seq (term F) → formula F) :
  ( p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
    p q e, qf_eval e (rgcdpT p k q) =
                 qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))).
Proof.
movePk p q e; rewrite /rgcdpT !sizeTP; case lqp: (_ < _).
  rewrite isnullP; case q0: (_ == _); first by rewrite Pk (eqP q0) rgcdp0.
  rewrite sizeTP rgcdp_loopP ⇒ [|e' p']; last by rewrite Pk.
  by rewrite /rgcdp lqp q0.
rewrite isnullP; case p0: (_ == _); first by rewrite Pk (eqP p0) rgcd0p.
rewrite sizeTP rgcdp_loopP ⇒ [|e' p']; last by rewrite Pk.
by rewrite /rgcdp lqp p0.
Qed.

Lemma rgcdpT_qf (p : polyF) (k : polyFformula F) (q : polyF) :
  ( r, rpoly rqf (k r)) → rpoly prpoly qqf (rgcdpT p k q).
Proof.
movekP rp rq; apply: sizeT_qf⇒ // n; apply: sizeT_qf⇒ // m.
by case:(_ < _);
   apply: isnull_qf⇒ //; case; do ?apply: kP⇒ //;
   apply: sizeT_qf⇒ // n'; apply: rgcdp_loopT_qf.
Qed.

Fixpoint rgcdpTs k (ps : seq polyF) : fF :=
  if ps is p::pr then rgcdpTs (rgcdpT p k) pr else k [::Const 0].

Lemma rgcdpTsP (k : polyFformula F) :
  ( p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
   ps e,
    qf_eval e (rgcdpTs k ps) =
    qf_eval e (k (lift (\big[@rgcdp _/0%:P]_(i <- ps)(eval_poly e i)))).
Proof.
movePk ps e.
elim: ps k Pk; first by movep Pk; rewrite /= big_nil Pk /= mul0r add0r.
movep ps Pps /= k Pk /=; rewrite big_cons Pps ⇒ [|p' e'].
  by rewrite rgcdpTP // eval_lift.
by rewrite !rgcdpTP // Pk !eval_lift .
Qed.

Definition rseq_poly ps := all rpoly ps.

Lemma rgcdpTs_qf (k : polyFformula F) (ps : seq polyF) :
  ( r, rpoly rqf (k r)) → rseq_poly psqf (rgcdpTs k ps).
Proof.
elim: ps k⇒ [|c p ihp] k kP rps⇒ /=; first exact: kP.
by move: rps; case/andPrc rp; apply: ihp⇒ // r rr; apply: rgcdpT_qf.
Qed.

Fixpoint rgdcop_recT (q : polyF) k (p : polyF) n :=
  if n is m.+1 then
    rgcdpT p (sizeT (fun sd
      if sd == 1%N then k p
      else rgcdpT p (rdivpT p (fun rrgdcop_recT q k r m)) q
    )) q
  else isnull (fun bk [::Const b%:R]) q.

Lemma rgdcop_recTP (k : polyFformula F) :
  ( p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p))))
  → p q n e, qf_eval e (rgdcop_recT p k q n)
    = qf_eval e (k (lift (rgdcop_rec (eval_poly e p) (eval_poly e q) n))).
Proof.
movePk p q n e.
elim: n k Pk p q e ⇒ [|n Pn] k Pk p q e /=.
  rewrite isnullP /=.
  by case: (_ == _); rewrite Pk /= mul0r add0r ?(polyC0, polyC1).
rewrite rgcdpTP ?sizeTP ?eval_lift //.
  rewrite /rcoprimep; case se : (_==_); rewrite Pk //.
  do ?[rewrite (rgcdpTP,Pn,eval_lift,redivpTP) | move⇒ × //=].
by do ?[rewrite (sizeTP,eval_lift) | move⇒ × //=].
Qed.

Lemma rgdcop_recT_qf (p : polyF) (k : polyFformula F) (q : polyF) (n : nat) :
 ( r, rpoly rqf (k r)) →
 rpoly prpoly qqf (rgdcop_recT p k q n).
Proof.
elim: n p k q ⇒ [|n ihn] p k q kP rp rq /=.
apply: isnull_qf⇒ //; first by case; rewrite kP.
apply: rgcdpT_qf⇒ // g rg; apply: sizeT_qf⇒ // n'.
case: (_ == _); first exact: kP.
apply: rgcdpT_qf⇒ // g' rg'; apply: redivpT_qf⇒ // r; case/andPrr _.
exact: ihn.
Qed.

Definition rgdcopT q k p := sizeT (rgdcop_recT q k p) p.

Lemma rgdcopTP (k : polyFformula F) :
  ( p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
   p q e, qf_eval e (rgdcopT p k q) =
                qf_eval e (k (lift (rgdcop (eval_poly e p) (eval_poly e q)))).
Proof. by move⇒ *; rewrite sizeTP rgdcop_recTP 1?Pk. Qed.

Lemma rgdcopT_qf (p : polyF) (k : polyFformula F) (q : polyF) :
  ( r, rpoly rqf (k r)) → rpoly prpoly qqf (rgdcopT p k q).
Proof.
by movekP rp rq; apply: sizeT_qf ⇒ // n; apply: rgdcop_recT_qf.
Qed.

Definition ex_elim_seq (ps : seq polyF) (q : polyF) :=
  (rgcdpTs (rgdcopT q (sizeT (fun nBool (n != 1%N)))) ps).

Lemma ex_elim_seqP (ps : seq polyF) (q : polyF) (e : seq F) :
  let gp := (\big[@rgcdp _/0%:P]_(p <- ps)(eval_poly e p)) in
  qf_eval e (ex_elim_seq ps q) = (size (rgdcop (eval_poly e q) gp) != 1%N).
Proof.
by do ![rewrite (rgcdpTsP,rgdcopTP,sizeTP,eval_lift) //= | move⇒ × //=].
Qed.

Lemma ex_elim_seq_qf (ps : seq polyF) (q : polyF) :
  rseq_poly psrpoly qqf (ex_elim_seq ps q).
Proof.
moverps rq; apply: rgcdpTs_qf⇒ // g rg; apply: rgdcopT_qf⇒ // d rd.
exact : sizeT_qf.
Qed.

Fixpoint abstrX (i : nat) (t : term F) :=
  match t with
    | (Var n) ⇒ if n == i then [::Const 0; Const 1] else [::t]
    | (Opp x) ⇒ opppT (abstrX i x)
    | (Add x y) ⇒ sumpT (abstrX i x) (abstrX i y)
    | (Mul x y) ⇒ mulpT (abstrX i x) (abstrX i y)
    | (NatMul x n) ⇒ natmulpT n (abstrX i x)
    | (Exp x n) ⇒ let ax := (abstrX i x) in
      iter n (mulpT ax) [::Const 1]
    | _[::t]
  end.

Lemma abstrXP (i : nat) (t : term F) (e : seq F) (x : F) :
  rterm t(eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.
Proof.
elim: t ⇒ [n | r | n | t tP s sP | t tP | t tP n | t tP s sP | t tP | t tP n] h.
- move⇒ /=; case ni: (_ == _);
    rewrite //= ?(mul0r,add0r,addr0,polyC1,mul1r,hornerX,hornerC);
    by rewrite // nth_set_nth /= ni.
- by rewrite /= mul0r add0r hornerC.
- by rewrite /= mul0r add0r hornerC.
- by case/andP: h ⇒ *; rewrite /= eval_sumpT hornerD tP ?sP.
- by rewrite /= eval_opppT hornerN tP.
- by rewrite /= eval_natmulpT hornerMn tP.
- by case/andP: h ⇒ *; rewrite /= eval_mulpT hornerM tP ?sP.
- by [].
- elim: n h ⇒ [|n ihn] rt; first by rewrite /= expr0 mul0r add0r hornerC.
  by rewrite /= eval_mulpT exprSr hornerM ihn // mulrC tP.
Qed.

Lemma rabstrX (i : nat) (t : term F) : rterm trpoly (abstrX i t).
Proof.
elim: t; do ?[ by move⇒ × //=; do ?case: (_ == _)].
- movet irt s irs /=; case/andPrt rs.
  by apply: rsumpT; rewrite ?irt ?irs //.
- by movet irt /= rt; rewrite rpoly_map_mul ?irt //.
- by movet irt /= n rt; rewrite rpoly_map_mul ?irt //.
- movet irt s irs /=; case/andPrt rs.
  by apply: rmulpT; rewrite ?irt ?irs //.
- movet irt /= n rt; move: (irt rt)=> {rt} rt; elim: n ⇒ [|n ihn] //=.
  exact: rmulpT.
Qed.

Implicit Types tx ty : term F.

Lemma abstrX_mulM (i : nat) : {morph abstrX i : x y / Mul x y >-> mulpT x y}.
Proof. done. Qed.

Lemma abstrX1 (i : nat) : abstrX i (Const 1) = [::Const 1].
Proof. done. Qed.

Lemma eval_poly_mulM e : {morph eval_poly e : x y / mulpT x y >-> mul x y}.
Proof. by movex y; rewrite eval_mulpT. Qed.

Lemma eval_poly1 e : eval_poly e [::Const 1] = 1.
Proof. by rewrite /= mul0r add0r. Qed.

Notation abstrX_bigmul := (big_morph _ (abstrX_mulM _) (abstrX1 _)).
Notation eval_bigmul := (big_morph _ (eval_poly_mulM _) (eval_poly1 _)).
Notation bigmap_id := (big_map _ (fun _true) id).

Lemma rseq_poly_map (x : nat) (ts : seq (term F)) :
  all (@rterm _) tsrseq_poly (map (abstrX x) ts).
Proof.
by elim: ts ⇒ //= t ts iht; case/andPrt rts; rewrite rabstrX // iht.
Qed.

Definition ex_elim (x : nat) (pqs : seq (term F) × seq (term F)) :=
  ex_elim_seq (map (abstrX x) pqs.1)
  (abstrX x (\big[Mul/Const 1]_(q <- pqs.2) q)).

Lemma ex_elim_qf (x : nat) (pqs : seq (term F) × seq (term F)) :
  dnf_rterm pqsqf (ex_elim x pqs).
case: pqsps qs; case/andP⇒ /= rps rqs.
apply: ex_elim_seq_qf; first exact: rseq_poly_map.
apply: rabstrX⇒ /=.
elim: qs rqs⇒ [|t ts iht] //=; first by rewrite big_nil.
by case/andPrt rts; rewrite big_cons /= rt /= iht.
Qed.

Lemma holds_conj : e i x ps, all (@rterm _) ps
  (holds (set_nth 0 e i x) (foldr (fun t : term FAnd (t == 0)) True ps)
   all ((@root _)^~ x) (map (eval_poly e \o abstrX i) ps)).
Proof.
movee i x; elim⇒ [|p ps ihps] //=.
case/andPrp rps; rewrite rootE abstrXP //.
constructor; first by case⇒ → hps; rewrite eqxx /=; apply/ihps.
by case/andP; move/eqP⇒ → psr; split⇒ //; apply/ihps.
Qed.

Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq (term F)) :
  all (@rterm _) ps
  (holds (set_nth 0 e i x) (foldr (fun t : term FAnd (t != 0)) True ps)
  all (fun p~~root p x) (map (eval_poly e \o abstrX i) ps)).
Proof.
elim: ps ⇒ [|p ps ihps] //=.
case/andPrp rps; rewrite rootE abstrXP //.
constructor; first by case⇒ /eqPhps /=; apply/ihps.
by case/andPpr psr; split; first apply/eqP⇒ //; apply/ihps.
Qed.

Lemma holds_ex_elim : GRing.valid_QE_proj ex_elim.
Proof.
movei [ps qs] /= e; case/andP⇒ /= rps rqs.
rewrite ex_elim_seqP big_map.
have → : \big[@rgcdp _/0%:P]_(j <- ps) eval_poly e (abstrX i j) =
          \big[@rgcdp _/0%:P]_(j <- (map (eval_poly e) (map (abstrX i) (ps)))) j.
  by rewrite !big_map.
rewrite -!map_comp.
  have aux I (l : seq I) (P : I{poly F}) :
    \big[(@gcdp F)/0]_(j <- l) P j %= \big[(@rgcdp F)/0]_(j <- l) P j.
    elim: l ⇒ [| u l ihl] /=; first by rewrite !big_nil eqpxx.
    rewrite !big_cons; move: ihl; move/(eqp_gcdr (P u)) ⇒ h.
    apply: eqp_trans h _; rewrite eqp_sym; exact: eqp_rgcd_gcd.
case g0: (\big[(@rgcdp F)/0%:P]_(j <- map (eval_poly e \o abstrX i) ps) j == 0).
  rewrite (eqP g0) rgdcop0.
  case m0 : (_ == 0)=> //=; rewrite ?(size_poly1,size_poly0) //=.
    rewrite abstrX_bigmul eval_bigmul -bigmap_id in m0.
    constructor⇒ [[x] // []] //.
    case_; move/holds_conjnhc; move/hc:rqs.
    by rewrite -root_bigmul //= (eqP m0) root0.
  constructor; move/negP:m0; move/negPm0.
  case: (closed_nonrootP axiom _ m0) ⇒ x {m0}.
  rewrite abstrX_bigmul eval_bigmul -bigmap_id root_bigmulm0.
   x; do 2?constructor⇒ //; last by apply/holds_conjn.
  apply/holds_conj; rewrite //= -root_biggcd.
  by rewrite (eqp_root (aux _ _ _ )) (eqP g0) root0.
apply:(iffP (closed_rootP axiom _)); casex Px; x; move:Px ⇒ //=.
  rewrite (eqp_root (eqp_rgdco_gdco _ _)) root_gdco ?g0 //.
  rewrite -(eqp_root (aux _ _ _ )) root_biggcd abstrX_bigmul eval_bigmul.
  rewrite -bigmap_id root_bigmul; case/andPpsr qsr.
  do 2?constructor; first by apply/holds_conj.
  by apply/holds_conjn.
rewrite (eqp_root (eqp_rgdco_gdco _ _)) root_gdco ?g0 // -(eqp_root (aux _ _ _)).
rewrite root_biggcd abstrX_bigmul eval_bigmul -bigmap_id.
rewrite root_bigmul⇒ [[] // [hps hqs]]; apply/andP.
constructor; first by apply/holds_conj.
by apply/holds_conjn.
Qed.

Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim.
Proof. by movei bc /= rbc; apply: ex_elim_qf. Qed.

Definition closed_fields_QEMixin :=
  QEdecFieldMixin wf_ex_elim holds_ex_elim.

End ClosedFieldQE.