Library mathcomp.field.closed_field

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
From mathcomp Require Import fintype generic_quotient bigop ssralg poly.
From mathcomp Require Import polydiv matrix mxpoly countalg ring_quotient.

Set Implicit Arguments.

Import GRing.Theory.
Local Open Scope ring_scope.

Import Pdiv.Ring.
Import PreClosedField.

Module ClosedFieldQE.
Section ClosedFieldQE.

Variables (F : fieldType) (F_closed : GRing.closed_field_axiom F).

Notation fF := (@GRing.formula F).
Notation tF := (@GRing.term F).
Notation qf f := (GRing.qf_form f && GRing.rformula f).
Definition polyF := seq tF.

Lemma qf_simpl (f : fF) :
  (qf f → GRing.qf_form f) × (qf f → GRing.rformula f).

Notation cps T := ((T → fF) → fF).
Definition ret T1 : T1 → cps T1 := fun x k ⇒ k x.
Arguments ret {T1} x k /.

Definition bind T1 T2 (x : cps T1) (f : T1 → cps T2) : cps T2 :=
  fun k ⇒ x (fun x ⇒ f x k).
Arguments bind {T1 T2} x f k /.
Notation "''let' x <- y ; z" :=
  (bind y (fun x ⇒ z)) (at level 99, x at level 0, y at level 0,
    format "'[hv' ''let' x <- y ; '/' z ']'").

Definition cpsif T (c : fF) (t : T) (e : T) : cps T :=
  fun k ⇒ GRing.If c (k t) (k e).
Arguments cpsif {T} c t e k /.
Notation "''if' c1 'then' c2 'else' c3" := (cpsif c1%T c2%T c3%T)
  (at level 200, right associativity, format
"'[hv ' ''if' c1 '/' '[' 'then' c2 ']' '/' '[' 'else' c3 ']' ']'").

Notation eval := GRing.eval.
Notation rterm := GRing.rterm.
Notation qf_eval := GRing.qf_eval.

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

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

Definition sizeT : polyF → cps nat := (fix loop p :=
  if p isn't c :: q then ret 0
  else 'let n <- loop q;
       if n is m.+1 then ret m.+2 else
       'if (c == 0) then 0%N else 1%N).

Definition qf_red_cps T (x : cps T) (y : _ → T) :=
   ∀ e k, qf_eval e (x k) = qf_eval e (k (y e)).
Notation "x ->_ e y" := (qf_red_cps x (fun e ⇒ y))
  (e name, at level 90, format "x ->_ e y").

Definition qf_cps T D (x : cps T) :=
  ∀ k, (∀ y, D y → qf (k y)) → qf (x k).

Lemma qf_cps_ret T D (x : T) : D x → qf_cps D (ret x).
Hint Resolve qf_cps_ret : core.

Lemma qf_cps_bind T1 D1 T2 D2 (x : cps T1) (f : T1 → cps T2) :
  qf_cps D1 x → (∀ x, D1 x → qf_cps D2 (f x)) → qf_cps D2 (bind x f).

Lemma qf_cps_if T D (c : fF) (t : T) (e : T) : qf c → D t → D e →
  qf_cps D ('if c then t else e).

Lemma sizeTP (pf : polyF) : sizeT pf →_e size (eval_poly e pf).

Lemma sizeT_qf (p : polyF) : rpoly p → qf_cps xpredT (sizeT p).

Definition isnull (p : polyF) : cps bool :=
  'let n <- sizeT p; ret (n == 0).

Lemma isnullP (p : polyF) : isnull p →_e (eval_poly e p == 0).

Lemma isnull_qf (p : polyF) : rpoly p → qf_cps xpredT (isnull p).

Definition lt_sizeT (p q : polyF) : cps bool :=
  'let n <- sizeT p; 'let m <- sizeT q; ret (n < m).

Definition lift (p : {poly F}) := map GRing.Const p.

Lemma eval_lift (e : seq F) (p : {poly F}) : eval_poly e (lift p) = p.

Fixpoint lead_coefT p : cps tF :=
  if p is c :: q then
    'let l <- lead_coefT q; 'if (l == 0) then c else l
  else ret 0%T.

Lemma lead_coefTP (k : tF → fF) :
 (∀ x e, qf_eval e (k x) = qf_eval e (k (eval e x)%:T%T)) →
  ∀ (p : polyF) (e : seq F),
  qf_eval e (lead_coefT p k) = qf_eval e (k (lead_coef (eval_poly e p))%:T%T).

Lemma lead_coefT_qf (p : polyF) : rpoly p → qf_cps (@rterm _) (lead_coefT p).

Fixpoint amulXnT (a : tF) (n : nat) : polyF :=
  if n is n'.+1 then 0%T :: (amulXnT a n') else [:: a].

Lemma eval_amulXnT (a : tF) (n : nat) (e : seq F) :
  eval_poly e (amulXnT a n) = (eval e a)%:P × 'X^n.

Lemma ramulXnT: ∀ a n, rterm a → rpoly (amulXnT a n).

Fixpoint sumpT (p q : polyF) :=
  match p, q with a :: p, b :: q ⇒ (a + b)%T :: sumpT p q
                | [::], q ⇒ q | p, [::] ⇒ p end.
Arguments sumpT : simpl nomatch.

Lemma eval_sumpT (p q : polyF) (e : seq F) :
  eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).

Lemma rsumpT (p q : polyF) : rpoly p → rpoly q → rpoly (sumpT p q).

Fixpoint mulpT (p q : polyF) :=
  if p isn't a :: p then [::]
  else sumpT [seq (a × x)%T | x <- q] (0%T :: mulpT p q).

Lemma eval_mulpT (p q : polyF) (e : seq F) :
  eval_poly e (mulpT p q) = (eval_poly e p) × (eval_poly e q).

Lemma rpoly_map_mul (t : tF) (p : polyF) (rt : rterm t) :
  rpoly [seq (t × x)%T | x <- p] = rpoly p.

Lemma rmulpT (p q : polyF) : rpoly p → rpoly q → rpoly (mulpT p q).

Definition opppT : polyF → polyF := map (GRing.Mul (- 1%T)%T).

Lemma eval_opppT (p : polyF) (e : seq F) :
  eval_poly e (opppT p) = - eval_poly e p.

Definition natmulpT n : polyF → polyF := map (GRing.Mul n%:R%T).

Lemma eval_natmulpT (p : polyF) (n : nat) (e : seq F) :
  eval_poly e (natmulpT n p) = (eval_poly e p) *+ n.

Fixpoint redivp_rec_loopT (q : polyF) sq cq (c : nat) (qq r : polyF)
  (n : nat) {struct n} : cps (nat × polyF × polyF) :=
  'let sr <- sizeT r;
  if sr < sq then ret (c, qq, r) else
  'let lr <- lead_coefT r;
  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 c.+1 qq1 r1 n1
  else ret (c.+1, qq1, r1).

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 × polyF → fF) :
  (∀ 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 c qq r n k)
    = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).

Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : tF)
  (c : nat) (qq r : polyF) (n : nat) :
  rpoly q → rterm cq → rpoly qq → rpoly r →
  qf_cps (fun x ⇒ [&& rpoly x.1.2 & rpoly x.2])
         (redivp_rec_loopT q sq cq c qq r n).

Definition redivpT (p : polyF) (q : polyF) : cps (nat × polyF × polyF) :=
  'let b <- isnull q;
  if b then ret (0, [::0%T], p) else
  'let sq <- sizeT q; 'let sp <- sizeT p;
  'let lq <- lead_coefT q;
  redivp_rec_loopT q sq lq 0 [::0%T] p sp.

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.

Lemma redivpTP (k : nat × polyF × polyF → fF) :
  (∀ 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 q k) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).

Lemma redivpT_qf (p : polyF) (q : polyF) : rpoly p → rpoly q →
  qf_cps (fun x ⇒ [&& rpoly x.1.2 & rpoly x.2]) (redivpT p q).

Definition rmodpT (p : polyF) (q : polyF) : cps polyF :=
  'let d <- redivpT p q; ret d.2.
Definition rdivpT (p : polyF) (q : polyF) : cps polyF :=
  'let d <- redivpT p q; ret d.1.2.
Definition rscalpT (p : polyF) (q : polyF) : cps nat :=
  'let d <- redivpT p q; ret d.1.1.
Definition rdvdpT (p : polyF) (q : polyF) : cps bool :=
  'let d <- rmodpT p q; isnull d.

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

Fixpoint rgcdp_loopT n (pp : polyF) (qq : polyF) : cps polyF :=
  'let rr <- rmodpT pp qq; 'let nrr <- isnull rr; if nrr then ret qq
    else if n is n1.+1 then rgcdp_loopT n1 qq rr else ret rr.

Lemma rgcdp_loopP (k : polyF → fF) :
  (∀ 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 n p q k) =
    qf_eval e (k (lift (rgcdp_loop n (eval_poly e p) (eval_poly e q)))).

Lemma rgcdp_loopT_qf (n : nat) (p : polyF) (q : polyF) :
  rpoly p → rpoly q → qf_cps rpoly (rgcdp_loopT n p q).

Definition rgcdpT (p : polyF) (q : polyF) : cps polyF :=
  let aux p1 q1 : cps polyF :=
    'let b <- isnull p1; if b then ret q1
    else 'let n <- sizeT p1; rgcdp_loopT n p1 q1 in
  'let b <- lt_sizeT p q; if b then aux q p else aux p q.

Lemma rgcdpTP (k : polyF → fF) :
  (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
   ∀ p q e, qf_eval e (rgcdpT p q k) =
                 qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))).

Lemma rgcdpT_qf (p : polyF) (q : polyF) :
   rpoly p → rpoly q → qf_cps rpoly (rgcdpT p q).

Fixpoint rgcdpTs (ps : seq polyF) : cps polyF :=
  if ps is p :: pr then 'let pr <- rgcdpTs pr; rgcdpT p pr else ret [::0%T].

Lemma rgcdpTsP (k : polyF → fF) :
  (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
  ∀ ps e,
    qf_eval e (rgcdpTs ps k) =
    qf_eval e (k (lift (\big[@rgcdp _/0%:P]_(i <- ps)(eval_poly e i)))).

Lemma rgcdpTs_qf (ps : seq polyF) :
   all rpoly ps → qf_cps rpoly (rgcdpTs ps).

Fixpoint rgdcop_recT n (q : polyF) (p : polyF) :=
  if n is m.+1 then
    'let g <- rgcdpT p q; 'let sg <- sizeT g;
    if sg == 1 then ret p
    else 'let r <- rdivpT p g;
          rgdcop_recT m q r
  else 'let b <- isnull q; ret [::b%:R%T].

Lemma rgdcop_recTP (k : polyF → fF) :
  (∀ 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 n p q k)
    = qf_eval e (k (lift (rgdcop_rec (eval_poly e p) (eval_poly e q) n))).

Lemma rgdcop_recT_qf (n : nat) (p : polyF) (q : polyF) :
  rpoly p → rpoly q → qf_cps rpoly (rgdcop_recT n p q).

Definition rgdcopT q p := 'let sp <- sizeT p; rgdcop_recT sp q p.

Lemma rgdcopTP (k : polyF → fF) :
  (∀ p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) →
  ∀ p q e, qf_eval e (rgdcopT p q k) =
                qf_eval e (k (lift (rgdcop (eval_poly e p) (eval_poly e q)))).

Lemma rgdcopT_qf (p : polyF) (q : polyF) :
  rpoly p → rpoly q → qf_cps rpoly (rgdcopT p q).

Definition ex_elim_seq (ps : seq polyF) (q : polyF) : fF :=
  ('let g <- rgcdpTs ps; 'let d <- rgdcopT q g;
  'let n <- sizeT d; ret (n != 1)) GRing.Bool.

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).

Lemma ex_elim_seq_qf (ps : seq polyF) (q : polyF) :
  all rpoly ps → rpoly q → qf (ex_elim_seq ps q).

Fixpoint abstrX (i : nat) (t : tF) :=
  match t with
    | 'X_n ⇒ if n == i then [::0; 1] else [::t]
    | - x ⇒ opppT (abstrX i x)
    | x + y ⇒ sumpT (abstrX i x) (abstrX i y)
    | x × y ⇒ mulpT (abstrX i x) (abstrX i y)
    | x *+ n ⇒ natmulpT n (abstrX i x)
    | x ^+ n ⇒ let ax := (abstrX i x) in iter n (mulpT ax) [::1]
    | _ ⇒ [::t]
  end%T.

Lemma abstrXP (i : nat) (t : tF) (e : seq F) (x : F) :
  rterm t → (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.

Lemma rabstrX (i : nat) (t : tF) : rterm t → rpoly (abstrX i t).

Implicit Types tx ty : tF.

Lemma abstrX_mulM (i : nat) : {morph abstrX i : x y / x × y >-> mulpT x y}%T.

Lemma abstrX1 (i : nat) : abstrX i 1%T = [::1%T].

Lemma eval_poly_mulM e : {morph eval_poly e : x y / mulpT x y >-> x × y}.

Lemma eval_poly1 e : eval_poly e [::1%T] = 1.

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 tF) :
  all (@rterm _) ts → all rpoly (map (abstrX x) ts).

Definition ex_elim (x : nat) (pqs : seq tF × seq tF) :=
  ex_elim_seq (map (abstrX x) pqs.1)
  (abstrX x (\big[GRing.Mul/1%T]_(q <- pqs.2) q)).

Lemma ex_elim_qf (x : nat) (pqs : seq tF × seq tF) :
  GRing.dnf_rterm pqs → qf (ex_elim x pqs).

Lemma holds_conj : ∀ e i x ps, all (@rterm _) ps →
  (GRing.holds (set_nth 0 e i x)
               (foldr (fun t : tF ⇒ GRing.And (t == 0)) GRing.True%T ps)
  ↔ all ((@root _)^~ x) (map (eval_poly e \o abstrX i) ps)).

Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq tF) :
  all (@rterm _) ps →
  (GRing.holds (set_nth 0 e i x)
               (foldr (fun t : tF ⇒ GRing.And (t != 0)) GRing.True ps) ↔
  all (fun p ⇒ ~~root p x) (map (eval_poly e \o abstrX i) ps)).

Lemma holds_ex_elim: GRing.valid_QE_proj ex_elim.

Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim.

End ClosedFieldQE.
End ClosedFieldQE.



Import CodeSeq.

Lemma countable_field_extension (F : countFieldType) (p : {poly F}) :
    size p > 1 →
  {E : countFieldType & {FtoE : {rmorphism F → E} &
  {w : E | root (map_poly FtoE p) w
         & ∀ u : E, ∃ q, u = (map_poly FtoE q).[w]}}}.

Lemma countable_algebraic_closure (F : countFieldType) :
  {K : countClosedFieldType & {FtoK : {rmorphism F → K} | integralRange FtoK}}.