From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.field.closed_field.html | 544 ++++++++++++++------------ 1 file changed, 292 insertions(+), 252 deletions(-) (limited to 'docs/htmldoc/mathcomp.field.closed_field.html') diff --git a/docs/htmldoc/mathcomp.field.closed_field.html b/docs/htmldoc/mathcomp.field.closed_field.html index 2ee6879..ca8c82a 100644 --- a/docs/htmldoc/mathcomp.field.closed_field.html +++ b/docs/htmldoc/mathcomp.field.closed_field.html @@ -21,29 +21,34 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

- 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 + 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
- This file constructs an instance of quantifier elimination mixin, + 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.
- This file hence deals with the transformation of formulae part, which we - address by implementing one CPS style formula transformer per effective - 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.
@@ -51,7 +56,7 @@ Set Implicit Arguments.

-Import GRing.
+Import GRing.Theory.
Local Open Scope ring_scope.

@@ -59,404 +64,439 @@ Import PreClosedField.

-Section ClosedFieldQE.
+Module ClosedFieldQE.
+Section ClosedFieldQE.

-Variable F : Field.type.
+Variables (F : fieldType) (F_closed : GRing.ClosedField.axiom F).

-Variable axiom : ClosedField.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.

-Notation fF := (formula F).
-Notation qf f := (qf_form f && rformula f).
+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.
+ +
+Definition bind T1 T2 (x : cps T1) (f : T1 → cps T2) : cps T2 :=
+  fun k ⇒ x (fun x ⇒ f x 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).
+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 ']' ']'").

-Definition polyF := seq (term F).
+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.
+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 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.
+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).

-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))).
+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 ident, at level 90, format "x ->_ e y").

-Lemma sizeT_qf (k : nat → formula F) (p : polyF) :
-  (∀ n, qf (k n)) → rpoly p → qf (sizeT k p).
+Definition qf_cps T D (x : cps T) :=
+  ∀ k, (∀ y, D y → qf (k y)) → qf (x k).

-Definition isnull (k : bool → fF) (p : polyF) :=
-  sizeT (fun n ⇒ k (n == 0%N)) p.
+Lemma qf_cps_ret T D (x : T) : D x → qf_cps D (ret x).
+ Hint Resolve qf_cps_ret : core.

-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 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 isnull_qf (k : bool → formula F) (p : polyF) :
-  (∀ b, qf (k b)) → rpoly p → qf (isnull k p).
+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).

-Definition lt_sizeT (k : bool → fF) (p q : polyF) : fF :=
-  sizeT (fun n ⇒ sizeT (fun m ⇒ k (n<m)) q) p.
+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}) := let: q := p in map Const q.
+Definition lift (p : {poly F}) := map GRing.Const p.

-Lemma eval_lift (e : seq F) (p : {poly F}) : eval_poly e (lift p) = p.
+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).
+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 : 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_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 (k : term F → formula F) (p : polyF) :
- (∀ c, rterm c → qf (k c)) → rpoly p → qf (lead_coefT k p).
+Lemma lead_coefT_qf (p : polyF) : rpoly p → qf_cps (@rterm _) (lead_coefT p).

-Fixpoint amulXnT (a : term F) (n : nat) : polyF :=
-  if n is n'.+1 then (Const 0) :: (amulXnT a n') else [::a].
+Fixpoint amulXnT (a : tF) (n : nat) : polyF :=
+  if n is n'.+1 then 0%T :: (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 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).
+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.
+Fixpoint sumpT (p q : polyF) :=
+  match p, q with a :: p, b :: q ⇒ (a + b)%T :: sumpT p q
+                | [::], q ⇒ q | p, [::] ⇒ p end.

-Lemma eval_sumpT (p q : polyF) (e : seq F) :
-  eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e 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).
+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 [::].
+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 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 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).
+Lemma rmulpT (p q : polyF) : rpoly p → rpoly q → rpoly (mulpT p q).

-Definition opppT := map (Mul (@Const F (-1))).
+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.
+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)).
+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.
+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_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).
+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_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 : 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).
+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) (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.
+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;
+  '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 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).
+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)).

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

-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.
+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_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.
+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.

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

-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 rgcdp_loopT_qf (n : nat) (p : polyF) (q : polyF) :
+  rpoly p → rpoly q → qf_cps rpoly (rgcdp_loopT n 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)))).
+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 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).
+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)))).

-Fixpoint rgcdpTs k (ps : seq polyF) : fF :=
-  if ps is p::pr then rgcdpTs (rgcdpT p k) pr else k [::Const 0].
+Lemma rgcdpT_qf (p : polyF) (q : polyF) :
+   rpoly p → rpoly q → qf_cps rpoly (rgcdpT p q).

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

-Definition rseq_poly ps := all rpoly ps.
+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 (k : polyF → formula F) (ps : seq polyF) :
-  (∀ r, rpoly r → qf (k r)) → rseq_poly ps → qf (rgcdpTs k ps).
+Lemma rgcdpTs_qf (ps : seq polyF) :
+   all rpoly ps → qf_cps rpoly (rgcdpTs 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.
+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 → 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_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 (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).
+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 k p := sizeT (rgdcop_recT q k p) p.
+Definition rgdcopT q p := 'let sp <- sizeT p; rgdcop_recT sp q 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 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) (k : polyF → formula F) (q : polyF) :
-  (∀ r, rpoly r → qf (k r)) → rpoly p → rpoly q → qf (rgdcopT p k 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) :=
-  (rgcdpTs (rgdcopT q (sizeT (fun n ⇒ Bool (n != 1%N)))) ps).
+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_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).
+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 : term F) :=
+Fixpoint abstrX (i : nat) (t : tF) :=
  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.
+    | '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 : 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 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 : term F) : rterm t → rpoly (abstrX i t).
+Lemma rabstrX (i : nat) (t : tF) : rterm t → rpoly (abstrX i t).

-Implicit Types tx ty : term F.
+Implicit Types tx ty : tF.

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

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

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

-Lemma eval_poly1 e : eval_poly e [::Const 1] = 1.
+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).
+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).
+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 (term F) × seq (term F)) :=
-  ex_elim_seq (map (abstrX x) pqs.1)
-  (abstrX x (\big[Mul/Const 1]_(q <- pqs.2) q)).
+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 (term F) × seq (term F)) :
-  dnf_rterm pqs → qf (ex_elim x pqs).
+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 →
-  (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_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 (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_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 holds_ex_elim: GRing.valid_QE_proj ex_elim.

-Lemma wf_ex_elim : GRing.wf_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.
+Definition Mixin := QEdecFieldMixin wf_ex_elim holds_ex_elim.
+ +
+End ClosedFieldQE.
+End ClosedFieldQE.
+Notation closed_field_QEMixin := ClosedFieldQE.Mixin.
+ +
+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]}}}.

-End ClosedFieldQE.
+Lemma countable_algebraic_closure (F : countFieldType) :
+  {K : countClosedFieldType & {FtoK : {rmorphism F → K} | integralRange FtoK}}.
-- cgit v1.2.3