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

This files contains two main contributions: 1. Theorem "closed_field_QEMixin" A proof that algebraically closed field enjoy quantifier elimination, as described in ``A formal quantifier elimination for algebraically closed fields'', proceedings of Calculemus 2010, by Cyril Cohen and Assia Mahboubi
We constructs an instance of quantifier elimination mixin, (see the ssralg library) from the theory of polynomials with coefficients is an algebraically closed field (see the polydiv library). The algebraic operations operating on fomulae are implemented in CPS style We provide one CPS counterpart for each operation involved in the proof of quantifier elimination. See the paper for more details.
2. Theorems "countable_field_extension" and "countable_algebraic_closure" constructions for both simple extension and algebraic closure of countable fields, by Georges Gonthier. Note that the construction of the algebraic closure relies on the above mentionned quantifier elimination.

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 kk x.
Arguments ret {T1} x k /.

Definition bind T1 T2 (x : cps T1) (f : T1 cps T2) : cps T2 :=
fun kx (fun xf x k).
Arguments bind {T1 T2} x f k /.
Notation "''let' x <- y ; z" :=
(bind y (fun xz)) (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 kGRing.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%N
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 ey))
(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%N).

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
| [::], qq | 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 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%N, [::0%T], p) else
'let sq <- sizeT q; 'let sp <- sizeT p;
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%N 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%N)) 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%N).

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_nif n == i then [::0; 1] else [::t]
| - xopppT (abstrX i x)
| x + ysumpT (abstrX i x) (abstrX i y)
| x × ymulpT (abstrX i x) (abstrX i y)
| x *+ nnatmulpT n (abstrX i x)
| x ^+ nlet 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 : tFGRing.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 : tFGRing.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}}.