Library mathcomp.field.closed_field

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.

Set Implicit Arguments.

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::q then (eval_poly e q)*'X + (eval e c)%:P else 0.

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

Fixpoint sizeT (k : nat → fF) (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 : nat → formula F) (pf : polyF) (e : seq F) :
  qf_eval e (sizeT k pf) = qf_eval e (k (size (eval_poly e pf))).

Lemma sizeT_qf (k : nat → formula F) (p : polyF) :
  (∀ n, qf (k n)) → rpoly p → qf (sizeT k p).

Definition isnull (k : bool → fF) (p : polyF) :=
  sizeT (fun n ⇒ k (n == 0%N)) p.

Lemma isnullP (k : bool → formula F) (p : polyF) (e : seq F) :
  qf_eval e (isnull k p) = qf_eval e (k (eval_poly e p == 0)).

Lemma isnull_qf (k : bool → formula F) (p : polyF) :
  (∀ b, qf (k b)) → rpoly p → qf (isnull k p).

Definition lt_sizeT (k : bool → fF) (p q : polyF) : fF :=
  sizeT (fun n ⇒ sizeT (fun m ⇒ k (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.

Fixpoint lead_coefT (k : term F → fF) p :=
  if p is c::q then
    lead_coefT (fun l ⇒ GRing.If (l == 0) (k c) (k l)) q
  else k (Const 0).

Lemma lead_coefTP (k : term F → formula 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)))).

Lemma lead_coefT_qf (k : term F → formula F) (p : polyF) :
 (∀ c, rterm c → qf (k c)) → rpoly p → qf (lead_coefT k p).

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.

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

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

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

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

Lemma rpoly_map_mul (t : term F) (p : polyF) (rt : rterm t) :
  rpoly (map (Mul t) p) = rpoly p.

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

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

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

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.

Fixpoint redivp_rec_loopT (q : polyF) sq cq (k : nat × polyF × polyF → fF)
  (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 × polyF → formula 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)).

Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : term F)
 (k : nat × polyF × polyF → formula F) (c : nat) (qq r : polyF) (n : nat) :
  (∀ r, [&& rpoly r.1.2 & rpoly r.2] → qf (k r)) →
  rpoly q → rterm cq → rpoly qq → rpoly r →
    qf (redivp_rec_loopT q sq cq k c qq r n).

Definition redivpT (p : polyF) (k : nat × polyF × polyF → fF)
                   (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.

Lemma redivpTP (k : nat × polyF × polyF → formula 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)).

Lemma redivpT_qf (p : polyF) (k : nat × polyF × polyF → formula F) (q : polyF) :
  (∀ r, [&& rpoly r.1.2 & rpoly r.2] → qf (k r)) →
   rpoly p → rpoly q → qf (redivpT p k q).

Definition rmodpT (p : polyF) (k : polyF → fF) (q : polyF) : fF :=
  redivpT p (fun d ⇒ k d.2) q.
Definition rdivpT (p : polyF) (k:polyF → fF) (q : polyF) : fF :=
  redivpT p (fun d ⇒ k d.1.2) q.
Definition rscalpT (p : polyF) (k: nat → fF) (q : polyF) : fF :=
  redivpT p (fun d ⇒ k d.1.1) q.
Definition rdvdpT (p : polyF) (k:bool → fF) (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 : polyF → formula F) n (qq : polyF) :=
  rmodpT pp (isnull
    (fun b ⇒ if 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 : polyF → formula 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)))).

Lemma rgcdp_loopT_qf (p : polyF) (k : polyF → formula F) (q : polyF) (n : nat) :
  (∀ r, rpoly r → qf (k r)) →
  rpoly p → rpoly q → qf (rgcdp_loopT p k n q).

Definition rgcdpT (p : polyF) k (q : polyF) : fF :=
  let aux p1 k q1 := isnull
    (fun b ⇒ if b
      then (k q1)
      else (sizeT (fun n ⇒ (rgcdp_loopT p1 k n q1)) p1)) p1
    in (lt_sizeT (fun b ⇒ if 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)))).

Lemma rgcdpT_qf (p : polyF) (k : polyF → formula F) (q : polyF) :
  (∀ r, rpoly r → qf (k r)) → rpoly p → rpoly q → qf (rgcdpT p k q).

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 : polyF → formula 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)))).

Definition rseq_poly ps := all rpoly ps.

Lemma rgcdpTs_qf (k : polyF → formula F) (ps : seq polyF) :
  (∀ r, rpoly r → qf (k r)) → rseq_poly ps → qf (rgcdpTs k ps).

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 r ⇒ rgdcop_recT q k r m)) q
    )) q
  else isnull (fun b ⇒ k [::Const b%:R]) q.

Lemma rgdcop_recTP (k : polyF → formula 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))).

Lemma rgdcop_recT_qf (p : polyF) (k : polyF → formula F) (q : polyF) (n : nat) :
 (∀ r, rpoly r → qf (k r)) →
 rpoly p → rpoly q → qf (rgdcop_recT p k q n).

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

Lemma rgdcopTP (k : polyF → formula 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)))).

Lemma rgdcopT_qf (p : polyF) (k : polyF → formula F) (q : polyF) :
  (∀ r, rpoly r → qf (k r)) → rpoly p → rpoly q → qf (rgdcopT p k q).

Definition ex_elim_seq (ps : seq polyF) (q : polyF) :=
  (rgcdpTs (rgdcopT q (sizeT (fun n ⇒ Bool (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).

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

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.

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

Implicit Types tx ty : term F.

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

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

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

Lemma eval_poly1 e : eval_poly e [::Const 1] = 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 (term F)) :
  all (@rterm _) ts → rseq_poly (map (abstrX x) ts).

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 pqs → qf (ex_elim x pqs).

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

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 F ⇒ And (t != 0)) 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.

Definition closed_fields_QEMixin :=
  QEdecFieldMixin wf_ex_elim holds_ex_elim.

End ClosedFieldQE.