Library mathcomp.field.closed_field
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- 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.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.
- -
-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 ']' ']'").
- -
-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 e ⇒ y))
- (e ident, 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
- | [::], 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 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%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 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_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.
- -
-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]}}}.
- -
-Lemma countable_algebraic_closure (F : countFieldType) :
- {K : countClosedFieldType & {FtoK : {rmorphism F → K} | integralRange FtoK}}.
-
--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.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.
- -
-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 ']' ']'").
- -
-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 e ⇒ y))
- (e ident, 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
- | [::], 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 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%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 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_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.
- -
-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]}}}.
- -
-Lemma countable_algebraic_closure (F : countFieldType) :
- {K : countClosedFieldType & {FtoK : {rmorphism F → K} | integralRange FtoK}}.
-