diff options
| -rw-r--r-- | ChangeLog | 9 | ||||
| -rw-r--r-- | mathcomp/Make | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/Make | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/all_algebra.v | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/countalg.v (renamed from mathcomp/field/countalg.v) | 325 | ||||
| -rw-r--r-- | mathcomp/algebra/finalg.v | 59 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 32 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 11 | ||||
| -rw-r--r-- | mathcomp/field/Make | 1 | ||||
| -rw-r--r-- | mathcomp/field/algC.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 4 | ||||
| -rw-r--r-- | mathcomp/field/all_field.v | 1 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 839 |
16 files changed, 692 insertions, 625 deletions
@@ -3,6 +3,15 @@ * Added companion matrix of a polynomial `companionmx p` and the theorems: companionmxK, map_mx_companion and companion_map_poly + * Reshuffled theorems inside files and packages: + * countalg goes from the field to the algebra package + * finalg now gets inheritance from countalg + * closed_field now contains the construction of algebraic closure + for countable fields that used to be in countalg. + + * Rewritten proof of quantifier elimination for closed field in a + monadic style. + * Added allsigs, the dependent version of allpairs, with notation `[seq E | i <- s & j <- t]` diff --git a/mathcomp/Make b/mathcomp/Make index 865234c..df99405 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -1,5 +1,6 @@ algebra/all_algebra.v algebra/finalg.v +algebra/countalg.v algebra/fraction.v algebra/intdiv.v algebra/interval.v @@ -30,7 +31,6 @@ field/algebraics_fundamentals.v field/algnum.v field/all_field.v field/closed_field.v -field/countalg.v field/cyclotomic.v field/falgebra.v field/fieldext.v diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make index 7d12cb4..b3001f9 100644 --- a/mathcomp/algebra/Make +++ b/mathcomp/algebra/Make @@ -1,4 +1,5 @@ all_algebra.v +countalg.v finalg.v fraction.v intdiv.v diff --git a/mathcomp/algebra/all_algebra.v b/mathcomp/algebra/all_algebra.v index 8a31d60..a937b0c 100644 --- a/mathcomp/algebra/all_algebra.v +++ b/mathcomp/algebra/all_algebra.v @@ -1,6 +1,7 @@ Require Export ssralg. Require Export ssrnum. Require Export finalg. +Require Export countalg. Require Export poly. Require Export polydiv. Require Export polyXY. diff --git a/mathcomp/field/countalg.v b/mathcomp/algebra/countalg.v index a6d11b3..21000e4 100644 --- a/mathcomp/field/countalg.v +++ b/mathcomp/algebra/countalg.v @@ -4,11 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. From mathcomp -Require Import bigop ssralg finalg zmodp matrix mxalgebra. -From mathcomp -Require Import poly polydiv mxpoly generic_quotient ring_quotient closed_field. -From mathcomp -Require Import ssrint rat. +Require Import bigop ssralg generic_quotient ring_quotient. (*****************************************************************************) (* This file clones part of ssralg hierachy for countable types; it does not *) @@ -27,7 +23,7 @@ Require Import ssrint rat. (* zmodType and countType structures. *) (* ... etc *) (* This file provides constructions for both simple extension and algebraic *) -(* closure of countable fields. *) +(* closure of countable fields. *) (*****************************************************************************) Set Implicit Arguments. @@ -798,319 +794,4 @@ End CountRing. Import CountRing. Export Zmodule.Exports Ring.Exports ComRing.Exports UnitRing.Exports. Export ComUnitRing.Exports IntegralDomain.Exports. -Export Field.Exports DecidableField.Exports ClosedField.Exports. - -From mathcomp -Require Import poly polydiv generic_quotient ring_quotient. -From mathcomp -Require Import mxpoly polyXY. -Import GRing.Theory. -From mathcomp -Require Import closed_field. - -Canonical Zp_countZmodType m := [countZmodType of 'I_m.+1]. -Canonical Zp_countRingType m := [countRingType of 'I_m.+2]. -Canonical Zp_countComRingType m := [countComRingType of 'I_m.+2]. -Canonical Zp_countUnitRingType m := [countUnitRingType of 'I_m.+2]. -Canonical Zp_countComUnitRingType m := [countComUnitRingType of 'I_m.+2]. -Canonical Fp_countIdomainType p := [countIdomainType of 'F_p]. -Canonical Fp_countFieldType p := [countFieldType of 'F_p]. -Canonical Fp_countDecFieldType p := [countDecFieldType of 'F_p]. - -Canonical matrix_countZmodType (M : countZmodType) m n := - [countZmodType of 'M[M]_(m, n)]. -Canonical matrix_countRingType (R : countRingType) n := - [countRingType of 'M[R]_n.+1]. -Canonical matrix_countUnitRingType (R : countComUnitRingType) n := - [countUnitRingType of 'M[R]_n.+1]. - -Definition poly_countMixin (R : countRingType) := - [countMixin of polynomial R by <:]. -Canonical polynomial_countType R := CountType _ (poly_countMixin R). -Canonical poly_countType (R : countRingType) := [countType of {poly R}]. -Canonical polynomial_countZmodType (R : countRingType) := - [countZmodType of polynomial R]. -Canonical poly_countZmodType (R : countRingType) := [countZmodType of {poly R}]. -Canonical polynomial_countRingType (R : countRingType) := - [countRingType of polynomial R]. -Canonical poly_countRingType (R : countRingType) := [countRingType of {poly R}]. -Canonical polynomial_countComRingType (R : countComRingType) := - [countComRingType of polynomial R]. -Canonical poly_countComRingType (R : countComRingType) := - [countComRingType of {poly R}]. -Canonical polynomial_countUnitRingType (R : countIdomainType) := - [countUnitRingType of polynomial R]. -Canonical poly_countUnitRingType (R : countIdomainType) := - [countUnitRingType of {poly R}]. -Canonical polynomial_countComUnitRingType (R : countIdomainType) := - [countComUnitRingType of polynomial R]. -Canonical poly_countComUnitRingType (R : countIdomainType) := - [countComUnitRingType of {poly R}]. -Canonical polynomial_countIdomainType (R : countIdomainType) := - [countIdomainType of polynomial R]. -Canonical poly_countIdomainType (R : countIdomainType) := - [countIdomainType of {poly R}]. - -Canonical int_countZmodType := [countZmodType of int]. -Canonical int_countRingType := [countRingType of int]. -Canonical int_countComRingType := [countComRingType of int]. -Canonical int_countUnitRingType := [countUnitRingType of int]. -Canonical int_countComUnitRingType := [countComUnitRingType of int]. -Canonical int_countIdomainType := [countIdomainType of int]. - -Canonical rat_countZmodType := [countZmodType of rat]. -Canonical rat_countRingType := [countRingType of rat]. -Canonical rat_countComRingType := [countComRingType of rat]. -Canonical rat_countUnitRingType := [countUnitRingType of rat]. -Canonical rat_countComUnitRingType := [countComUnitRingType of rat]. -Canonical rat_countIdomainType := [countIdomainType of rat]. -Canonical rat_countFieldType := [countFieldType of rat]. - -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 - & forall u : E, exists q, u = (map_poly FtoE q).[w]}}}. -Proof. -pose fix d i := - if i is i1.+1 then - let d1 := oapp (gcdp (d i1)) 0 (unpickle i1) in - if size d1 > 1 then d1 else d i1 - else p. -move=> p_gt1; have sz_d i: size (d i) > 1 by elim: i => //= i IHi; case: ifP. -have dv_d i j: i <= j -> d j %| d i. - move/subnK <-; elim: {j}(j - i)%N => //= j IHj; case: ifP => //=. - case: (unpickle _) => /= [q _|]; last by rewrite size_poly0. - exact: dvdp_trans (dvdp_gcdl _ _) IHj. -pose I : pred {poly F} := [pred q | d (pickle q).+1 %| q]. -have I'co q i: q \notin I -> i > pickle q -> coprimep q (d i). - rewrite inE => I'q /dv_d/coprimep_dvdl-> //; apply: contraR I'q. - rewrite coprimep_sym /coprimep /= pickleK /= neq_ltn. - case: ifP => [_ _| ->]; first exact: dvdp_gcdr. - rewrite orbF ltnS leqn0 size_poly_eq0 gcdp_eq0 -size_poly_eq0. - by rewrite -leqn0 leqNgt ltnW //. -have memI q: reflect (exists i, d i %| q) (q \in I). - apply: (iffP idP) => [|[i dv_di_q]]; first by exists (pickle q).+1. - have [le_i_q | /I'co i_co_q] := leqP i (pickle q). - rewrite inE /= pickleK /=; case: ifP => _; first exact: dvdp_gcdr. - exact: dvdp_trans (dv_d _ _ le_i_q) dv_di_q. - apply: contraR i_co_q _. - by rewrite /coprimep (eqp_size (dvdp_gcd_idr dv_di_q)) neq_ltn sz_d orbT. -have I_ideal : idealr_closed I. - split=> [||a q1 q2 Iq1 Iq2]; first exact: dvdp0. - by apply/memI=> [[i /idPn[]]]; rewrite dvdp1 neq_ltn sz_d orbT. - apply/memI; exists (maxn (pickle q1).+1 (pickle q2).+1); apply: dvdp_add. - by apply: dvdp_mull; apply: dvdp_trans Iq1; apply/dv_d/leq_maxl. - by apply: dvdp_trans Iq2; apply/dv_d/leq_maxr. -pose Iaddkey := GRing.Pred.Add (DefaultPredKey I) I_ideal. -pose Iidkey := MkIdeal (GRing.Pred.Zmod Iaddkey I_ideal) I_ideal. -pose E := ComRingType _ (@Quotient.mulqC _ _ _ (KeyedPred Iidkey)). -pose PtoE : {rmorphism {poly F} -> E} := [rmorphism of \pi_E%qT : {poly F} -> E]. -have PtoEd i: PtoE (d i) = 0. - by apply/eqP; rewrite piE Quotient.equivE subr0; apply/memI; exists i. -pose Einv (z : E) (q := repr z) (dq := d (pickle q).+1) := - let q_unitP := Bezout_eq1_coprimepP q dq in - if q_unitP is ReflectT ex_uv then PtoE (sval (sig_eqW ex_uv)).1 else 0. -have Einv0: Einv 0 = 0. - rewrite /Einv; case: Bezout_eq1_coprimepP => // ex_uv. - case/negP: (oner_neq0 E); rewrite piE -[_ 1]/(PtoE 1); have [uv <-] := ex_uv. - by rewrite rmorphD !rmorphM PtoEd /= reprK !mulr0 addr0. -have EmulV: GRing.Field.axiom Einv. - rewrite /Einv=> z nz_z; case: Bezout_eq1_coprimepP => [ex_uv |]; last first. - move/Bezout_eq1_coprimepP; rewrite I'co //. - by rewrite piE -{1}[z]reprK -Quotient.idealrBE subr0 in nz_z. - apply/eqP; case: sig_eqW => {ex_uv} [uv uv1]; set i := _.+1 in uv1 *. - rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE. - by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull. -pose EringU := [comUnitRingType of UnitRingType _ (FieldUnitMixin EmulV Einv0)]. -have Eunitf := @FieldMixin _ _ EmulV Einv0. -pose Efield := FieldType (IdomainType EringU (FieldIdomainMixin Eunitf)) Eunitf. -pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)). -pose FtoE := [rmorphism of PtoE \o polyC]; pose w : E := PtoE 'X. -have defPtoE q: (map_poly FtoE q).[w] = PtoE q. - by rewrite map_poly_comp horner_map [_.['X]]comp_polyXr. -exists [countFieldType of Ecount], FtoE, w => [|u]. - by rewrite /root defPtoE (PtoEd 0%N). -by exists (repr u); rewrite defPtoE /= reprK. -Qed. - -Lemma countable_algebraic_closure (F : countFieldType) : - {K : countClosedFieldType & {FtoK : {rmorphism F -> K} | integralRange FtoK}}. -Proof. -pose minXp (R : ringType) (p : {poly R}) := if size p > 1 then p else 'X. -have minXp_gt1 R p: size (minXp R p) > 1. - by rewrite /minXp; case: ifP => // _; rewrite size_polyX. -have minXpE (R : ringType) (p : {poly R}) : size p > 1 -> minXp R p = p. - by rewrite /minXp => ->. -have ext1 p := countable_field_extension (minXp_gt1 _ p). -pose ext1fT E p := tag (ext1 E p). -pose ext1to E p : {rmorphism _ -> ext1fT E p} := tag (tagged (ext1 E p)). -pose ext1w E p : ext1fT E p := s2val (tagged (tagged (ext1 E p))). -have ext1root E p: root (map_poly (ext1to E p) (minXp E p)) (ext1w E p). - by rewrite /ext1w; case: (tagged (tagged (ext1 E p))). -have ext1gen E p u: {q | u = (map_poly (ext1to E p) q).[ext1w E p]}. - by apply: sig_eqW; rewrite /ext1w; case: (tagged (tagged (ext1 E p))) u. -pose pExtEnum (E : countFieldType) := nat -> {poly E}. -pose Ext := {E : countFieldType & pExtEnum E}; pose MkExt : Ext := Tagged _ _. -pose EtoInc (E : Ext) i := ext1to (tag E) (tagged E i). -pose incEp E i j := - let v := map_poly (EtoInc E i) (tagged E j) in - if decode j is [:: i1; k] then - if i1 == i then odflt v (unpickle k) else v - else v. -pose fix E_ i := if i is i1.+1 then MkExt _ (incEp (E_ i1) i1) else MkExt F \0. -pose E i := tag (E_ i); pose Krep := {i : nat & E i}. -pose fix toEadd i k : {rmorphism E i -> E (k + i)%N} := - if k is k1.+1 then [rmorphism of EtoInc _ (k1 + i)%N \o toEadd _ _] - else [rmorphism of idfun]. -pose toE i j (le_ij : i <= j) := - ecast j {rmorphism E i -> E j} (subnK le_ij) (toEadd i (j - i)%N). -have toEeq i le_ii: toE i i le_ii =1 id. - by rewrite /toE; move: (subnK _); rewrite subnn => ?; rewrite eq_axiomK. -have toEleS i j leij leiSj z: toE i j.+1 leiSj z = EtoInc _ _ (toE i j leij z). - rewrite /toE; move: (j - i)%N {leij leiSj}(subnK _) (subnK _) => k. - by case: j /; rewrite (addnK i k.+1) => eq_kk; rewrite [eq_kk]eq_axiomK. -have toEirr := congr1 ((toE _ _)^~ _) (bool_irrelevance _ _). -have toEtrans j i k leij lejk leik z: - toE i k leik z = toE j k lejk (toE i j leij z). -- elim: k leik lejk => [|k IHk] leiSk lejSk. - by case: j => // in leij lejSk *; rewrite toEeq. - have:= lejSk; rewrite {1}leq_eqVlt ltnS => /predU1P[Dk | lejk]. - by rewrite -Dk in leiSk lejSk *; rewrite toEeq. - by have leik := leq_trans leij lejk; rewrite !toEleS -IHk. -have [leMl leMr] := (leq_maxl, leq_maxr); pose le_max := (leq_max, leqnn, orbT). -pose pairK (x y : Krep) (m := maxn _ _) := - (toE _ m (leMl _ _) (tagged x), toE _ m (leMr _ _) (tagged y)). -pose eqKrep x y := prod_curry (@eq_op _) (pairK x y). -have eqKrefl : reflexive eqKrep by move=> z; apply/eqP; apply: toEirr. -have eqKsym : symmetric eqKrep. - move=> z1 z2; rewrite {1}/eqKrep /= eq_sym; move: (leMl _ _) (leMr _ _). - by rewrite maxnC => lez1m lez2m; congr (_ == _); apply: toEirr. -have eqKtrans : transitive eqKrep. - rewrite /eqKrep /= => z2 z1 z3 /eqP eq_z12 /eqP eq_z23. - rewrite -(inj_eq (fmorph_inj (toE _ _ (leMr (tag z2) _)))). - rewrite -!toEtrans ?le_max // maxnCA maxnA => lez3m lez1m. - rewrite {lez1m}(toEtrans (maxn (tag z1) (tag z2))) // {}eq_z12. - do [rewrite -toEtrans ?le_max // -maxnA => lez2m] in lez3m *. - by rewrite (toEtrans (maxn (tag z2) (tag z3))) // eq_z23 -toEtrans. -pose K := {eq_quot (EquivRel _ eqKrefl eqKsym eqKtrans)}%qT. -have cntK : Countable.mixin_of K := CanCountMixin (@reprK _ _). -pose EtoKrep i (x : E i) : K := \pi%qT (Tagged E x). -have [EtoK piEtoK]: {EtoK | forall i, EtoKrep i =1 EtoK i} by exists EtoKrep. -pose FtoK := EtoK 0%N; rewrite {}/EtoKrep in piEtoK. -have eqEtoK i j x y: - toE i _ (leMl i j) x = toE j _ (leMr i j) y -> EtoK i x = EtoK j y. -- by move/eqP=> eq_xy; rewrite -!piEtoK; apply/eqmodP. -have toEtoK j i leij x : EtoK j (toE i j leij x) = EtoK i x. - by apply: eqEtoK; rewrite -toEtrans. -have EtoK_0 i: EtoK i 0 = FtoK 0 by apply: eqEtoK; rewrite !rmorph0. -have EtoK_1 i: EtoK i 1 = FtoK 1 by apply: eqEtoK; rewrite !rmorph1. -have EtoKeq0 i x: (EtoK i x == FtoK 0) = (x == 0). - by rewrite /FtoK -!piEtoK eqmodE /= /eqKrep /= rmorph0 fmorph_eq0. -have toErepr m i leim x lerm: - toE _ m lerm (tagged (repr (EtoK i x))) = toE i m leim x. -- have: (Tagged E x == repr (EtoK i x) %[mod K])%qT by rewrite reprK piEtoK. - rewrite eqmodE /= /eqKrep; case: (repr _) => j y /= in lerm * => /eqP /=. - have leijm: maxn i j <= m by rewrite geq_max leim. - by move/(congr1 (toE _ _ leijm)); rewrite -!toEtrans. -pose Kadd (x y : K) := EtoK _ (prod_curry +%R (pairK (repr x) (repr y))). -pose Kopp (x : K) := EtoK _ (- tagged (repr x)). -pose Kmul (x y : K) := EtoK _ (prod_curry *%R (pairK (repr x) (repr y))). -pose Kinv (x : K) := EtoK _ (tagged (repr x))^-1. -have EtoK_D i: {morph EtoK i : x y / x + y >-> Kadd x y}. - move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphD. - by rewrite -!toEtrans ?le_max // => lexm leym; rewrite !toErepr. -have EtoK_N i: {morph EtoK i : x / - x >-> Kopp x}. - by move=> x; apply: eqEtoK; set j := tag _; rewrite !rmorphN toErepr. -have EtoK_M i: {morph EtoK i : x y / x * y >-> Kmul x y}. - move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphM. - by rewrite -!toEtrans ?le_max // => lexm leym; rewrite !toErepr. -have EtoK_V i: {morph EtoK i : x / x^-1 >-> Kinv x}. - by move=> x; apply: eqEtoK; set j := tag _; rewrite !fmorphV toErepr. -case: {toErepr}I in (Kadd) (Kopp) (Kmul) (Kinv) EtoK_D EtoK_N EtoK_M EtoK_V. -pose inEi i z := {x : E i | z = EtoK i x}; have KtoE z: {i : nat & inEi i z}. - by elim/quotW: z => [[i x] /=]; exists i, x; rewrite piEtoK. -have inEle i j z: i <= j -> inEi i z -> inEi j z. - by move=> leij [x ->]; exists (toE i j leij x); rewrite toEtoK. -have KtoE2 z1 z2: {i : nat & inEi i z1 & inEi i z2}. - have [[i1 Ez1] [i2 Ez2]] := (KtoE z1, KtoE z2). - by exists (maxn i1 i2); [apply: inEle Ez1 | apply: inEle Ez2]. -have KtoE3 z1 z2 z3: {i : nat & inEi i z1 & inEi i z2 * inEi i z3}%type. - have [[i1 Ez1] [i2 Ez2 Ez3]] := (KtoE z1, KtoE2 z2 z3). - by exists (maxn i1 i2); [apply: inEle Ez1 | split; apply: inEle (leMr _ _) _]. -have KaddC: commutative Kadd. - by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_D addrC. -have KaddA: associative Kadd. - move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. - by rewrite -!EtoK_D addrA. -have Kadd0: left_id (FtoK 0) Kadd. - by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_0 i) -EtoK_D add0r. -have KaddN: left_inverse (FtoK 0) Kopp Kadd. - by move=> u; have [i [x ->]] := KtoE u; rewrite -EtoK_N -EtoK_D addNr EtoK_0. -pose Kzmod := ZmodType K (ZmodMixin KaddA KaddC Kadd0 KaddN). -have KmulC: commutative Kmul. - by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_M mulrC. -have KmulA: @associative Kzmod Kmul. - move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. - by rewrite -!EtoK_M mulrA. -have Kmul1: left_id (FtoK 1) Kmul. - by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_1 i) -EtoK_M mul1r. -have KmulD: left_distributive Kmul Kadd. - move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. - by rewrite -!(EtoK_M, EtoK_D) mulrDl. -have Kone_nz: FtoK 1 != FtoK 0 by rewrite EtoKeq0 oner_neq0. -pose KringMixin := ComRingMixin KmulA KmulC Kmul1 KmulD Kone_nz. -pose Kring := ComRingType (RingType Kzmod KringMixin) KmulC. -have KmulV: @GRing.Field.axiom Kring Kinv. - move=> u; have [i [x ->]] := KtoE u; rewrite EtoKeq0 => nz_x. - by rewrite -EtoK_V -[_ * _]EtoK_M mulVf ?EtoK_1. -have Kinv0: Kinv (FtoK 0) = FtoK 0 by rewrite -EtoK_V invr0. -pose Kuring := [comUnitRingType of UnitRingType _ (FieldUnitMixin KmulV Kinv0)]. -pose KfieldMixin := @FieldMixin _ _ KmulV Kinv0. -pose Kidomain := IdomainType Kuring (FieldIdomainMixin KfieldMixin). -pose Kfield := FieldType Kidomain KfieldMixin. -have EtoKrmorphism i: rmorphism (EtoK i : E i -> Kfield). - by do 2?split=> [x y|]; rewrite ?EtoK_D ?EtoK_N ?EtoK_M ?EtoK_1. -pose EtoKM := RMorphism (EtoKrmorphism _); have EtoK_E: EtoK _ = EtoKM _ by []. -have toEtoKp := @eq_map_poly _ Kring _ _(toEtoK _ _ _). -have Kclosed: GRing.ClosedField.axiom Kfield. - move=> n pK n_gt0; pose m0 := \max_(i < n) tag (KtoE (pK i)); pose m := m0.+1. - have /fin_all_exists[pE DpE] (i : 'I_n): exists y, EtoK m y = pK i. - pose u := KtoE (pK i); have leum0: tag u <= m0 by rewrite (bigmax_sup i). - by have [y ->] := tagged u; exists (toE _ _ (leqW leum0) y); rewrite toEtoK. - pose p := 'X^n - rVpoly (\row_i pE i); pose j := code [:: m0; pickle p]. - pose pj := tagged (E_ j) j; pose w : E j.+1 := ext1w (E j) pj. - have lemj: m <= j by rewrite (allP (ltn_code _)) ?mem_head. - exists (EtoKM j.+1 w); apply/eqP; rewrite -subr_eq0; apply/eqP. - transitivity (EtoKM j.+1 (map_poly (toE m j.+1 (leqW lemj)) p).[w]). - rewrite -horner_map -map_poly_comp toEtoKp EtoK_E; move/EtoKM: w => w. - rewrite rmorphB [_ 'X^n]map_polyXn !hornerE hornerXn; congr (_ - _ : Kring). - rewrite (@horner_coef_wide _ n) ?size_map_poly ?size_poly //. - by apply: eq_bigr => i _; rewrite coef_map coef_rVpoly valK mxE /= DpE. - suffices Dpj: map_poly (toE m j lemj) p = pj. - apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj. - rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly. - by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly. - rewrite {w}/pj; elim: {-9}j lemj => // k IHk lemSk. - move: lemSk (lemSk); rewrite {1}leq_eqVlt ltnS => /predU1P[<- | lemk] lemSk. - rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)) map_poly_id //= /incEp. - by rewrite codeK eqxx pickleK. - rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK. - by rewrite -if_neg neq_ltn lemk. -suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. - pose Kdec := DecFieldType Kfield (closed_fields_QEMixin Kclosed). - pose KclosedField := ClosedFieldType Kdec Kclosed. - by exists [countClosedFieldType of CountType KclosedField cntK]. -exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z. -suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT). - by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p. -rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen. -move: (i - 0)%N (subnK _) => n; case: i /. -elim: n => [|n IHn] /= z; first exact: integral_id. -have{z} [q ->] := ext1gen _ _ z; set pn := tagged (E_ _) _. -apply: integral_horner. - by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph. -apply: integral_root (ext1root _ _) _. - by rewrite map_poly_eq0 -size_poly_gt0 ltnW. -by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph. -Qed. +Export Field.Exports DecidableField.Exports ClosedField.Exports.
\ No newline at end of file diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index 7a1cacf..939cd38 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. From mathcomp -Require Import ssralg finset fingroup morphism perm action. +Require Import ssralg finset fingroup morphism perm action countalg. (*****************************************************************************) (* This file clones the entire ssralg hierachy for finite types; this allows *) @@ -136,6 +136,7 @@ Notation "[ 'baseFinGroupType' 'of' R 'for' +%R ]" := Notation "[ 'finGroupType' 'of' R 'for' +%R ]" := (@FinGroup.clone R _ (finGroupType _) id _ id) (at level 0, format "[ 'finGroupType' 'of' R 'for' +%R ]") : form_scope. +Canonical countZmodType (T : type) := [countZmodType of T]. End Exports. End Zmodule. @@ -219,6 +220,8 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. End Exports. Section Unit. @@ -330,6 +333,9 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. End Exports. End ComRing. @@ -407,6 +413,9 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. End Exports. End UnitRing. @@ -590,6 +599,11 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. +Canonical countComUnitRingType (T : type) := [countComUnitRingType of T]. End Exports. End ComUnitRing. @@ -691,6 +705,12 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. +Canonical countComUnitRingType (T : type) := [countComUnitRingType of T]. +Canonical countIdomainType (T : type) := [countIdomainType of T]. End Exports. End IntegralDomain. @@ -800,6 +820,13 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. +Canonical countComUnitRingType (T : type) := [countComUnitRingType of T]. +Canonical countIdomainType (T : type) := [countIdomainType of T]. +Canonical countFieldType (T : type) := [countFieldType of T]. End Exports. End Field. @@ -871,6 +898,7 @@ Canonical finComUnitRingType. Canonical finIdomainType. Canonical baseFinGroupType. Canonical finGroupType. + End Exports. End DecField. @@ -940,6 +968,10 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : ringType) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +End counttype. End Exports. End Lmodule. @@ -1036,6 +1068,11 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : GRing.Ring.type) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +Canonical countRingType := [countRingType of T]. +End counttype. End Exports. End Lalgebra. @@ -1131,18 +1168,23 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : GRing.Ring.type) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +Canonical countRingType := [countRingType of T]. +End counttype. End Exports. End Algebra. Import Algebra.Exports. Module UnitAlgebra. - + Section ClassDef. Variable R : unitRingType. - -Record class_of M := + +Record class_of M := Class { base : GRing.UnitAlgebra.class_of R M; mixin : mixin_of M base }. Definition base2 M (c : class_of M) := Algebra.Class (mixin c). Definition base3 M (c : class_of M) := @UnitRing.Class _ (base c) (mixin c). @@ -1257,12 +1299,18 @@ Canonical ujoin_finLmodType. Canonical ujoin_finLalgType. Canonical ujoin_finAlgType. Notation finUnitAlgType R := (type (Phant R)). -Notation "[ 'finUnitAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T) +Notation "[ 'finUnitAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T) (at level 0, format "[ 'finUnitAlgType' R 'of' T ]") : form_scope. Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : GRing.UnitRing.type) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +Canonical countRingType := [countRingType of T]. +Canonical countUnitRingType := [countUnitRingType of T]. +End counttype. End Exports. End UnitAlgebra. @@ -1297,4 +1345,3 @@ Notation "{ 'unit' R }" := (unit_of (Phant R)) Prenex Implicits FinRing.uval. Notation "''U'" := (unit_action _) (at level 8) : action_scope. Notation "''U'" := (unit_groupAction _) (at level 8) : groupAction_scope. - diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index fca25a9..2a701a2 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -6,7 +6,7 @@ Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. From mathcomp Require Import finfun bigop prime binomial ssralg finset fingroup finalg. From mathcomp -Require Import perm zmodp. +Require Import perm zmodp countalg. (******************************************************************************) (* Basic concrete linear algebra : definition of type for matrices, and all *) @@ -2071,6 +2071,10 @@ Proof. by apply/matrixP=> k i; rewrite !mxE; apply: eq_bigr => j _; rewrite !mxE. Qed. +Canonical matrix_countZmodType (M : countZmodType) m n := + [countZmodType of 'M[M]_(m, n)]. +Canonical matrix_countRingType (R : countRingType) n := + [countRingType of 'M[R]_n.+1]. Canonical matrix_finLmodType (R : finRingType) m n := [finLmodType R of 'M[R]_(m, n)]. Canonical matrix_finRingType (R : finRingType) n' := @@ -2644,6 +2648,9 @@ End MatrixInv. Prenex Implicits unitmx invmx. +Canonical matrix_countUnitRingType (R : countComUnitRingType) n := + [countUnitRingType of 'M[R]_n.+1]. + (* Finite inversible matrices and the general linear group. *) Section FinUnitMatrix. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 0f97bb0..040b3a8 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. From mathcomp -Require Import bigop ssralg binomial tuple. +Require Import bigop ssralg countalg binomial tuple. (******************************************************************************) (* This file provides a library for univariate polynomials over ring *) @@ -152,6 +152,11 @@ Arguments coefp_head _ _ _%N _%R. Notation "{ 'poly' T }" := (poly_of (Phant T)). Notation coefp i := (coefp_head tt i). +Definition poly_countMixin (R : countRingType) := + [countMixin of polynomial R by <:]. +Canonical polynomial_countType R := CountType _ (poly_countMixin R). +Canonical poly_countType (R : countRingType) := [countType of {poly R}]. + Section PolynomialTheory. Variable R : ringType. @@ -1690,6 +1695,13 @@ Arguments rootPt [R p x]. Arguments unity_rootP [R n z]. Arguments polyOverP {R S0 addS kS p}. +Canonical polynomial_countZmodType (R : countRingType) := + [countZmodType of polynomial R]. +Canonical poly_countZmodType (R : countRingType) := [countZmodType of {poly R}]. +Canonical polynomial_countRingType (R : countRingType) := + [countRingType of polynomial R]. +Canonical poly_countRingType (R : countRingType) := [countRingType of {poly R}]. + (* Container morphism. *) Section MapPoly. @@ -2116,6 +2128,11 @@ Definition derivCE := (derivE, deriv_exp). End PolynomialComRing. +Canonical polynomial_countComRingType (R : countComRingType) := + [countComRingType of polynomial R]. +Canonical poly_countComRingType (R : countComRingType) := + [countComRingType of {poly R}]. + Section PolynomialIdomain. (* Integral domain structure on poly *) @@ -2353,6 +2370,19 @@ Proof. by move=> ??; apply: contraTeq => ?; rewrite leqNgt max_poly_roots. Qed. End PolynomialIdomain. +Canonical polynomial_countUnitRingType (R : countIdomainType) := + [countUnitRingType of polynomial R]. +Canonical poly_countUnitRingType (R : countIdomainType) := + [countUnitRingType of {poly R}]. +Canonical polynomial_countComUnitRingType (R : countIdomainType) := + [countComUnitRingType of polynomial R]. +Canonical poly_countComUnitRingType (R : countIdomainType) := + [countComUnitRingType of {poly R}]. +Canonical polynomial_countIdomainType (R : countIdomainType) := + [countIdomainType of polynomial R]. +Canonical poly_countIdomainType (R : countIdomainType) := + [countIdomainType of {poly R}]. + Section MapFieldPoly. Variables (F : fieldType) (R : ringType) (f : {rmorphism F -> R}). diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index b56bc2a..6015f33 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. From mathcomp -Require Import bigop ssralg div ssrnum ssrint. +Require Import bigop ssralg countalg div ssrnum ssrint. (******************************************************************************) (* This file defines a datatype for rational numbers and equips it with a *) @@ -350,6 +350,14 @@ Canonical rat_iDomain := Eval hnf in IdomainType rat (FieldIdomainMixin rat_field_axiom). Canonical rat_fieldType := FieldType rat rat_field_axiom. +Canonical rat_countZmodType := [countZmodType of rat]. +Canonical rat_countRingType := [countRingType of rat]. +Canonical rat_countComRingType := [countComRingType of rat]. +Canonical rat_countUnitRingType := [countUnitRingType of rat]. +Canonical rat_countComUnitRingType := [countComUnitRingType of rat]. +Canonical rat_countIdomainType := [countIdomainType of rat]. +Canonical rat_countFieldType := [countFieldType of rat]. + Lemma numq_eq0 x : (numq x == 0) = (x == 0). Proof. rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {x} x k0]. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index f12784b..d0214dd 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat choice seq. From mathcomp -Require Import fintype finfun bigop ssralg ssrnum poly. +Require Import fintype finfun bigop ssralg countalg ssrnum poly. Import GRing.Theory Num.Theory. (******************************************************************************) @@ -359,6 +359,13 @@ Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int]. Canonical int_iDomain := Eval hnf in IdomainType int intUnitRing.idomain_axiomz. +Canonical int_countZmodType := [countZmodType of int]. +Canonical int_countRingType := [countRingType of int]. +Canonical int_countComRingType := [countComRingType of int]. +Canonical int_countUnitRingType := [countUnitRingType of int]. +Canonical int_countComUnitRingType := [countComUnitRingType of int]. +Canonical int_countIdomainType := [countIdomainType of int]. + Definition absz m := match m with Posz p => p | Negz n => n.+1 end. Notation "m - n" := (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index f9bdaaa..ba6c1b3 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq div. From mathcomp -Require Import fintype bigop finset prime fingroup ssralg finalg. +Require Import fintype bigop finset prime fingroup ssralg finalg countalg. (******************************************************************************) (* Definition of the additive group and ring Zp, represented as 'I_p *) @@ -364,3 +364,12 @@ Canonical Fp_decFieldType := Eval hnf in [decFieldType of 'F_p for Fp_finFieldType]. End PrimeField. + +Canonical Zp_countZmodType m := [countZmodType of 'I_m.+1]. +Canonical Zp_countRingType m := [countRingType of 'I_m.+2]. +Canonical Zp_countComRingType m := [countComRingType of 'I_m.+2]. +Canonical Zp_countUnitRingType m := [countUnitRingType of 'I_m.+2]. +Canonical Zp_countComUnitRingType m := [countComUnitRingType of 'I_m.+2]. +Canonical Fp_countIdomainType p := [countIdomainType of 'F_p]. +Canonical Fp_countFieldType p := [countFieldType of 'F_p]. +Canonical Fp_countDecFieldType p := [countDecFieldType of 'F_p]. diff --git a/mathcomp/field/Make b/mathcomp/field/Make index 00aa7a5..b7c3f13 100644 --- a/mathcomp/field/Make +++ b/mathcomp/field/Make @@ -3,7 +3,6 @@ algC.v algebraics_fundamentals.v algnum.v closed_field.v -countalg.v cyclotomic.v falgebra.v fieldext.v diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index f7cb614..aef136a 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -6,7 +6,7 @@ Require Import ssrbool ssrfun ssrnat eqtype seq choice div fintype. From mathcomp Require Import path bigop finset prime ssralg poly polydiv mxpoly. From mathcomp -Require Import generic_quotient countalg ssrnum ssrint rat intdiv. +Require Import generic_quotient countalg closed_field ssrnum ssrint rat intdiv. From mathcomp Require Import algebraics_fundamentals. @@ -400,7 +400,7 @@ rewrite horner_poly rmorph_sum; apply: eq_bigr => k _. by rewrite rmorphM rmorphX /= LtoC_K. Qed. -Definition decFieldMixin := closed_field.closed_fields_QEMixin closedFieldAxiom. +Definition decFieldMixin := closed_field_QEMixin closedFieldAxiom. Canonical decFieldType := DecFieldType type decFieldMixin. Canonical closedFieldType := ClosedFieldType type closedFieldAxiom. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 3696316..8a65f2b 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -6,7 +6,7 @@ Require Import ssrbool ssrfun ssrnat eqtype seq choice div fintype. From mathcomp Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly. From mathcomp -Require Import countalg ssrnum ssrint rat intdiv. +Require Import countalg closed_field ssrnum ssrint rat intdiv. From mathcomp Require Import fingroup finalg zmodp cyclic pgroup sylow. From mathcomp @@ -27,7 +27,7 @@ Require Import vector falgebra fieldext separable galois. (* algebraics as a subfield. To avoid some duplication a few basic properties *) (* of the algebraics, such as the existence of minimal polynomials, that are *) (* required by the proof of the Theorem, are also proved here. *) -(* The main theorem of countalg.v supplies us directly with an algebraic *) +(* The main theorem of closed_field supplies us directly with an algebraic *) (* closure of the rationals (as the rationals are a countable field), so all *) (* we really need to construct is a conjugation automorphism that exchanges *) (* the two roots (i and -i) of X^2 + 1, and fixes a (real) subfield of *) diff --git a/mathcomp/field/all_field.v b/mathcomp/field/all_field.v index a57ac19..2641bbe 100644 --- a/mathcomp/field/all_field.v +++ b/mathcomp/field/all_field.v @@ -2,7 +2,6 @@ Require Export algC. Require Export algebraics_fundamentals. Require Export algnum. Require Export closed_field. -Require Export countalg. Require Export cyclotomic. Require Export falgebra. Require Export fieldext. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 5c57df8..1ae025b 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -2,94 +2,143 @@ (* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq. +Require Import ssrfun ssrbool eqtype choice ssrnat seq fintype generic_quotient. From mathcomp -Require Import bigop ssralg poly polydiv. +Require Import bigop ssralg poly polydiv matrix mxpoly countalg ring_quotient. (******************************************************************************) -(* 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. *) (******************************************************************************) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GRing. +Import GRing.Theory. Local Open Scope ring_scope. Import Pdiv.Ring. Import PreClosedField. +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). +Proof. by split=> /andP[]. Qed. -Definition polyF := seq (term F). +Notation cps T := ((T -> fF) -> fF). +Definition ret T1 : T1 -> cps T1 := fun x k => k x. +Arguments ret T1 x k /. -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 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. -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). + +Definition qf_red_cps T (x : cps T) (y : _ -> T) := + forall 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) := + forall k, (forall y, D y -> qf (k y)) -> qf (x k). -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 qf_cps_ret T D (x : T) : D x -> qf_cps D (ret x). +Proof. move=> ??; exact. Qed. +Hint Resolve qf_cps_ret. + +Lemma qf_cps_bind T1 D1 T2 D2 (x : cps T1) (f : T1 -> cps T2) : + qf_cps D1 x -> (forall x, D1 x -> qf_cps D2 (f x)) -> qf_cps D2 (bind x f). +Proof. by move=> xP fP k kP /=; apply: xP => y ?; apply: fP. Qed. + +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). Proof. -elim: pf e k; first by move=> *; rewrite size_poly0. -move=> c qf Pqf e k; rewrite Pqf. -rewrite size_MXaddC -(size_poly_eq0 (eval_poly _ _)). +move=> qfc Dt De k kP /=; have [qft qfe] := (kP _ Dt, kP _ De). +by do !rewrite qf_simpl //. +Qed. + +Lemma sizeTP (pf : polyF) : sizeT pf ->_e size (eval_poly e pf). +Proof. +elim: pf=> [|c qf qfP /=]; first by rewrite /= size_poly0. +move=> e k; rewrite size_MXaddC qfP -(size_poly_eq0 (eval_poly _ _)). by case: (size (eval_poly e qf))=> //=; case: eqP; rewrite // orbF. Qed. -Lemma sizeT_qf (k : nat -> formula F) (p : polyF) : - (forall n, qf (k n)) -> rpoly p -> qf (sizeT k p). +Lemma sizeT_qf (p : polyF) : rpoly p -> qf_cps xpredT (sizeT p). Proof. -elim: p k => /= [|c q ihp] k kP rp; first exact: kP. -case/andP: rp=> rc rq. -apply: ihp; rewrite ?rq //; case=> [|n]; last exact: kP. -have [/andP[qf0 rf0] /andP[qf1 rf1]] := (kP 0, kP 1)%N. -by rewrite If_form_qf ?If_form_rf //= andbT. +elim: p => /= [_|c p ihp /andP[rc rq]]; first exact: qf_cps_ret. +apply: qf_cps_bind; first exact: ihp. +move=> [|n] //= _; last exact: qf_cps_ret. +by apply: qf_cps_if; rewrite //= rc. Qed. -Definition isnull (k : bool -> fF) (p : polyF) := - sizeT (fun n => k (n == 0%N)) p. +Definition isnull (p : polyF) : cps bool := + 'let n <- sizeT p; ret (n == 0%N). -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)). -Proof. by rewrite sizeTP size_poly_eq0. Qed. +Lemma isnullP (p : polyF) : isnull p ->_e (eval_poly e p == 0). +Proof. by move=> e k; rewrite sizeTP size_poly_eq0. Qed. -Lemma isnull_qf (k : bool -> formula F) (p : polyF) : - (forall b, qf (k b)) -> rpoly p -> qf (isnull k p). -Proof. by move=> *; apply: sizeT_qf. Qed. +Lemma isnull_qf (p : polyF) : rpoly p -> qf_cps xpredT (isnull p). +Proof. +move=> rp; apply: qf_cps_bind; first exact: sizeT_qf. +by move=> ? _; apply: qf_cps_ret. +Qed. -Definition lt_sizeT (k : bool -> fF) (p q : polyF) : fF := - sizeT (fun n => sizeT (fun m => k (n<m)) q) 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. Proof. @@ -103,39 +152,38 @@ case c0: (_==_)=> /=. by rewrite mul0r add0r; apply: val_inj=> /=; rewrite polyseq_cons // /nilp pn0. Qed. -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) : - (forall x e, qf_eval e (k x) = qf_eval e (k (Const (eval e x)))) -> +Lemma lead_coefTP (k : tF -> fF) : + (forall x e, qf_eval e (k x) = qf_eval e (k (eval e x)%:T%T)) -> forall (p : polyF) (e : seq F), - qf_eval e (lead_coefT k p) = qf_eval e (k (Const (lead_coef (eval_poly e p)))). + qf_eval e (lead_coefT p k) = qf_eval e (k (lead_coef (eval_poly e p))%:T%T). Proof. -move=> Pk p e; elim: p k Pk => /= [*|a p' Pp' k Pk]; first by rewrite lead_coef0. -rewrite Pp'; last by move=> *; rewrite //= -Pk. +move=> kP p e; elim: p => [|a p IHp]/= in k kP e *. + by rewrite lead_coef0 kP. +rewrite IHp; last by move=> *; rewrite //= -kP. rewrite GRing.eval_If /= lead_coef_eq0. -case p'0: (_ == _); first by rewrite (eqP p'0) mul0r add0r lead_coefC -Pk. +case p'0: (_ == _); first by rewrite (eqP p'0) mul0r add0r lead_coefC -kP. rewrite lead_coefDl ?lead_coefMX // polyseqC size_mul ?p'0 //; last first. by rewrite -size_poly_eq0 size_polyX. rewrite size_polyX addnC /=; case: (_ == _)=> //=. by rewrite ltnS lt0n size_poly_eq0 p'0. Qed. -Lemma lead_coefT_qf (k : term F -> formula F) (p : polyF) : - (forall 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). Proof. -elim: p k => /= [|c q ihp] k kP rp; first exact: kP. -move: rp; case/andP=> rc rq; apply: ihp; rewrite ?rq // => l rl. -have [/andP[qfc rfc] /andP[qfl rfl]] := (kP c rc, kP l rl). -by rewrite If_form_qf ?If_form_rf //= andbT. +elim: p => [_|c q ihp //= /andP[rc rq]]; first by apply: qf_cps_ret. +apply: qf_cps_bind => [|y ty]; first exact: ihp. +by apply: qf_cps_if; rewrite //= ty. Qed. -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) : +Lemma eval_amulXnT (a : tF) (n : nat) (e : seq F) : eval_poly e (amulXnT a n) = (eval e a)%:P * 'X^n. Proof. elim: n=> [|n] /=; first by rewrite expr0 mulr1 mul0r add0r. @@ -146,10 +194,8 @@ Lemma ramulXnT: forall a n, rterm a -> rpoly (amulXnT a n). Proof. by move=> a n; elim: n a=> [a /= -> //|n ihn a ra]; apply: ihn. Qed. 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. + 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). @@ -168,7 +214,8 @@ by case/andP=> -> rq //=; apply: ihp. Qed. Fixpoint mulpT (p q : polyF) := - if p is a :: p' then sumpT (map (Mul a) q) (Const 0::(mulpT p' q)) else [::]. + 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). @@ -179,8 +226,8 @@ elim: q=> [|b q Hq] /=; first by rewrite mulr0. by rewrite Hq polyC_mul mulrDr mulrA. Qed. -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. Proof. by rewrite /rpoly all_map /= (@eq_all _ _ (@rterm _)) // => x; rewrite /= rt. Qed. @@ -192,15 +239,15 @@ apply: rsumpT; last exact: ihp. by rewrite rpoly_map_mul. Qed. -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. Proof. by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyC_opp mul1r. Qed. -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. @@ -210,21 +257,19 @@ rewrite mulrnDl mulr_natl polyC_muln; congr (_ + _). by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC. Qed. -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} := +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 @@ -232,13 +277,13 @@ Fixpoint redivp_rec_loop (q : {poly F}) sq cq 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) : - (forall c qq r e, qf_eval e (k (c,qq,r)) +Lemma redivp_rec_loopTP (k : nat * polyF * polyF -> fF) : + (forall 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)))) - -> forall q sq cq c qq r n e + -> forall 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 (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)). Proof. move=> Pk q sq cq c qq r n e /=. @@ -259,221 +304,192 @@ rewrite Pk ?(eval_lift,eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT). by rewrite mul_polyC ?(mul0r,add0r). Qed. -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) : - (forall r, [&& rpoly r.1.2 & rpoly r.2] -> qf (k r)) -> +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 (redivp_rec_loopT q sq cq k c qq r n). -Proof. -elim: n q sq cq k c qq r => [|n ihn] q sq cq k c qq r kP rq rcq rqq rr. - apply: sizeT_qf=> // n; case: (_ < _); first by apply: kP; rewrite // rqq rr. - apply: lead_coefT_qf=> // l rl; apply: kP. - by rewrite /= ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq. -apply: sizeT_qf=> // m; case: (_ < _); first by apply: kP => //=; rewrite rqq rr. -apply: lead_coefT_qf=> // l rl; apply: ihn; rewrite //= ?rcq //. - by rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq. -by rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq. -Qed. - -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. + qf_cps (fun x => [&& rpoly x.1.2 & rpoly x.2]) + (redivp_rec_loopT q sq cq c qq r n). +Proof. +do ![move=>x/(pair x){x}] => rw; elim: n => [|n IHn]//= in q sq cq c qq r rw *; +apply: qf_cps_bind; do ?[by apply: sizeT_qf; rewrite !rw] => sr _; +case: ifPn => // _; do ?[by apply: qf_cps_ret; rewrite //= ?rw]; +apply: qf_cps_bind; do ?[by apply: lead_coefT_qf; rewrite !rw] => lr /= rlr; +[apply: qf_cps_ret|apply: IHn]; +by do !rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul,rlr,rw) //=. +Qed. + +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. Proof. by elim: n c qq r => [| n Pn] c qq r //=; rewrite Pn. Qed. -Lemma redivpTP (k : nat * polyF * polyF -> formula F) : - (forall c qq r e, - qf_eval e (k (c,qq,r)) = +Lemma redivpTP (k : nat * polyF * polyF -> fF) : + (forall 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)))) -> forall 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)). + qf_eval e (redivpT p q k) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)). Proof. -move=> Pk p q e /=; rewrite isnullP unlock. -case q0 : (_ == _); first by rewrite Pk /= mul0r add0r polyC0. +move=> Pk p q e /=; rewrite isnullP unlock /=. +case q0 : (eval_poly e q == 0) => /=; first by rewrite Pk /= mul0r add0r polyC0. rewrite !sizeTP lead_coefTP /=; last by move=> *; rewrite !redivp_rec_loopTP. rewrite redivp_rec_loopTP /=; last by move=> *; rewrite Pk. by rewrite mul0r add0r polyC0 redivp_rec_loopP. Qed. -Lemma redivpT_qf (p : polyF) (k : nat * polyF * polyF -> formula F) (q : polyF) : - (forall r, [&& rpoly r.1.2 & rpoly r.2] -> qf (k r)) -> - rpoly p -> rpoly q -> qf (redivpT p 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). Proof. -move=> kP rp rq; rewrite /redivpT; apply: isnull_qf=> // [[]]; first exact: kP. -apply: sizeT_qf => // sq; apply: sizeT_qf=> // sp. -by apply: lead_coefT_qf=> // lq rlq; apply: redivp_rec_loopT_qf. +move=> rp rq; apply: qf_cps_bind => [|[] _]; first exact: isnull_qf. + by apply: qf_cps_ret. +apply: qf_cps_bind => [|sp _]; first exact: sizeT_qf. +apply: qf_cps_bind => [|sq _]; first exact: sizeT_qf. +apply: qf_cps_bind => [|lq rlq]; first exact: lead_coefT_qf. +by apply: redivp_rec_loopT_qf => //=. Qed. -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. +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} := - 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) : + 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) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> - forall n p q e, - qf_eval e (rgcdp_loopT p k n q) = + forall 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)))). Proof. -move=> Pk n p q e. -elim: n p q e => /= [| m Pm] p q e. - rewrite redivpTP; last by move=> *; rewrite !isnullP eval_lift. - rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk. - by rewrite redivpTP; last by move=> *; rewrite Pk. -rewrite redivpTP; last by move=> *; rewrite !isnullP eval_lift. -rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk. -by rewrite redivpTP => *; rewrite ?Pm !eval_lift. -Qed. - -Lemma rgcdp_loopT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) (n : nat) : - (forall r, rpoly r -> qf (k r)) -> - rpoly p -> rpoly q -> qf (rgcdp_loopT p k n q). -elim: n p k q => [|n ihn] p k q kP rp rq. - apply: redivpT_qf=> // r; case/andP=> _ rr. - apply: isnull_qf=> // [[]]; first exact: kP. - by apply: redivpT_qf=> // r'; case/andP=> _ rr'; apply: kP. -apply: redivpT_qf=> // r; case/andP=> _ rr. -apply: isnull_qf=> // [[]]; first exact: kP. -by apply: redivpT_qf=> // r'; case/andP=> _ rr'; apply: ihn. -Qed. - -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) : +move=> Pk n p q e; elim: n => /= [| m IHm] in p q e *; +rewrite redivpTP /==> *; rewrite ?isnullP ?eval_lift -/(rmodp _ _); +by case: (_ == _); do ?by rewrite -?Pk ?IHm ?eval_lift. +Qed. + +Lemma rgcdp_loopT_qf (n : nat) (p : polyF) (q : polyF) : + rpoly p -> rpoly q -> qf_cps rpoly (rgcdp_loopT n p q). +Proof. +elim: n => [|n IHn] in p q * => rp rq /=; +(apply: qf_cps_bind=> [|rr rrr]; [ + apply: qf_cps_bind => [|[[a u] v]]; do ?exact: redivpT_qf; + by move=> /andP[/= ??]; apply: (@qf_cps_ret _ rpoly)| +apply: qf_cps_bind => [|[] _]; +by [apply: isnull_qf|apply: qf_cps_ret|apply: IHn]]). +Qed. + +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) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> - forall p q e, qf_eval e (rgcdpT p k q) = + forall p q e, qf_eval e (rgcdpT p q k) = qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))). Proof. -move=> Pk p q e; rewrite /rgcdpT !sizeTP; case lqp: (_ < _). - rewrite isnullP; case q0: (_ == _); first by rewrite Pk (eqP q0) rgcdp0. - rewrite sizeTP rgcdp_loopP => [|e' p']; last by rewrite Pk. - by rewrite /rgcdp lqp q0. -rewrite isnullP; case p0: (_ == _); first by rewrite Pk (eqP p0) rgcd0p. -rewrite sizeTP rgcdp_loopP => [|e' p']; last by rewrite Pk. -by rewrite /rgcdp lqp p0. +move=> Pk p q e; rewrite /rgcdpT /rgcdp !sizeTP /=. +case: (_ < _); rewrite !isnullP /=; case: (_ == _); rewrite -?Pk ?sizeTP; +by rewrite ?rgcdp_loopP. Qed. -Lemma rgcdpT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) : - (forall r, rpoly r -> qf (k r)) -> rpoly p -> rpoly q -> qf (rgcdpT p k q). +Lemma rgcdpT_qf (p : polyF) (q : polyF) : + rpoly p -> rpoly q -> qf_cps rpoly (rgcdpT p q). Proof. -move=> kP rp rq; apply: sizeT_qf=> // n; apply: sizeT_qf=> // m. -by case: (_ < _); - apply: isnull_qf=> //; case; do ?apply: kP=> //; - apply: sizeT_qf=> // n'; apply: rgcdp_loopT_qf. +move=> rp rq k kP; rewrite /rgcdpT /=; do ![rewrite sizeT_qf => // ? _]. +case: (_ < _); rewrite ?isnull_qf // => -[]; rewrite ?kP // => _; +by rewrite sizeT_qf => // ? _; rewrite rgcdp_loopT_qf. Qed. -Fixpoint rgcdpTs k (ps : seq polyF) : fF := - if ps is p::pr then rgcdpTs (rgcdpT p k) pr else k [::Const 0]. +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 -> formula F) : +Lemma rgcdpTsP (k : polyF -> fF) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> - forall ps e, - qf_eval e (rgcdpTs k ps) = + forall ps e, + qf_eval e (rgcdpTs ps k) = qf_eval e (k (lift (\big[@rgcdp _/0%:P]_(i <- ps)(eval_poly e i)))). Proof. -move=> Pk ps e. -elim: ps k Pk; first by move=> p Pk; rewrite /= big_nil Pk /= mul0r add0r. -move=> p ps Pps /= k Pk /=; rewrite big_cons Pps => [|p' e']. - by rewrite rgcdpTP // eval_lift. -by rewrite !rgcdpTP // Pk !eval_lift . +move=> Pk ps e; elim: ps k Pk => [|p ps Pps] /= k Pk. + by rewrite /= big_nil Pk /= mul0r add0r. +by rewrite big_cons Pps => *; rewrite !rgcdpTP // !eval_lift -?Pk. Qed. -Definition rseq_poly ps := all rpoly ps. - -Lemma rgcdpTs_qf (k : polyF -> formula F) (ps : seq polyF) : - (forall 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). Proof. -elim: ps k=> [|c p ihp] k kP rps=> /=; first exact: kP. -by move: rps; case/andP=> rc rp; apply: ihp=> // r rr; apply: rgcdpT_qf. +elim: ps => [_|c p ihp /andP[rc rp]] //=; first exact: qf_cps_ret. +by apply: qf_cps_bind => [|r rr]; [apply: ihp|apply: rgcdpT_qf]. Qed. -Fixpoint rgdcop_recT (q : polyF) k (p : polyF) n := +Fixpoint rgdcop_recT n (q : polyF) (p : polyF) := 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. + '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) : +Lemma rgdcop_recTP (k : polyF -> fF) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) - -> forall p q n e, qf_eval e (rgdcop_recT p k q n) + -> forall 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))). Proof. -move=> Pk p q n e. -elim: n k Pk p q e => [|n Pn] k Pk p q e /=. +move=> Pk p q n e; elim: n => [|n Pn] /= in k Pk p q e *. rewrite isnullP /=. by case: (_ == _); rewrite Pk /= mul0r add0r ?(polyC0, polyC1). -rewrite rgcdpTP ?sizeTP ?eval_lift //. - rewrite /rcoprimep; case se : (_==_); rewrite Pk //. - do ?[rewrite (rgcdpTP,Pn,eval_lift,redivpTP) | move=> * //=]. -by do ?[rewrite (sizeTP,eval_lift) | move=> * //=]. +rewrite /rcoprimep rgcdpTP ?sizeTP ?eval_lift => * /=. + case: (_ == _); + by do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *]. +do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *]. +case: (_ == _); +by do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *]. Qed. -Lemma rgdcop_recT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) (n : nat) : - (forall 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). Proof. -elim: n p k q => [|n ihn] p k q kP rp rq /=. -apply: isnull_qf=> //; first by case; rewrite kP. -apply: rgcdpT_qf=> // g rg; apply: sizeT_qf=> // n'. -case: (_ == _); first exact: kP. -apply: rgcdpT_qf=> // g' rg'; apply: redivpT_qf=> // r; case/andP=> rr _. -exact: ihn. +elim: n => [|n ihn] in p q * => k kP rp rq /=. + by rewrite isnull_qf => //*; rewrite rq. +rewrite rgcdpT_qf=> //*; rewrite sizeT_qf=> //*. +case: (_ == _); rewrite ?kP ?rq //= redivpT_qf=> //= ? /andP[??]. +by rewrite ihn. Qed. -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) : +Lemma rgdcopTP (k : polyF -> fF) : (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) -> - forall p q e, qf_eval e (rgdcopT p k q) = + forall p q e, qf_eval e (rgdcopT p q k) = qf_eval e (k (lift (rgdcop (eval_poly e p) (eval_poly e q)))). Proof. by move=> *; rewrite sizeTP rgdcop_recTP 1?Pk. Qed. -Lemma rgdcopT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) : - (forall 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). Proof. -by move=> kP rp rq; apply: sizeT_qf => // n; apply: rgdcop_recT_qf. +by move=> rp rq k kP; rewrite sizeT_qf => //*; rewrite rgdcop_recT_qf. Qed. - -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 @@ -483,25 +499,24 @@ by do ![rewrite (rgcdpTsP,rgdcopTP,sizeTP,eval_lift) //= | move=> * //=]. Qed. Lemma ex_elim_seq_qf (ps : seq polyF) (q : polyF) : - rseq_poly ps -> rpoly q -> qf (ex_elim_seq ps q). + all rpoly ps -> rpoly q -> qf (ex_elim_seq ps q). Proof. move=> rps rq; apply: rgcdpTs_qf=> // g rg; apply: rgdcopT_qf=> // d rd. exact : sizeT_qf. Qed. -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] + | '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. + end%T. -Lemma abstrXP (i : nat) (t : term F) (e : seq F) (x : F) : +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. Proof. elim: t => [n | r | n | t tP s sP | t tP | t tP n | t tP s sP | t tP | t tP n] h. @@ -519,7 +534,7 @@ elim: t => [n | r | n | t tP s sP | t tP | t tP n | t tP s sP | t tP | t tP n] h by rewrite /= eval_mulpT exprSr hornerM ihn // mulrC tP. Qed. -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). Proof. elim: t; do ?[ by move=> * //=; do ?case: (_ == _)]. - move=> t irt s irs /=; case/andP=> rt rs. @@ -532,36 +547,36 @@ elim: t; do ?[ by move=> * //=; do ?case: (_ == _)]. exact: rmulpT. Qed. -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}. -Proof. done. Qed. +Lemma abstrX_mulM (i : nat) : {morph abstrX i : x y / x * y >-> mulpT x y}%T. +Proof. by []. Qed. -Lemma abstrX1 (i : nat) : abstrX i (Const 1) = [::Const 1]. +Lemma abstrX1 (i : nat) : abstrX i 1%T = [::1%T]. Proof. done. Qed. -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}. Proof. by move=> x y; rewrite eval_mulpT. Qed. -Lemma eval_poly1 e : eval_poly e [::Const 1] = 1. +Lemma eval_poly1 e : eval_poly e [::1%T] = 1. Proof. by rewrite /= mul0r add0r. Qed. 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). Proof. by elim: ts => //= t ts iht; case/andP=> rt rts; rewrite rabstrX // iht. Qed. -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). +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). case: pqs => ps qs; case/andP=> /= rps rqs. apply: ex_elim_seq_qf; first exact: rseq_poly_map. apply: rabstrX=> /=. @@ -570,7 +585,8 @@ by case/andP=> rt rts; rewrite big_cons /= rt /= iht. Qed. Lemma holds_conj : forall e i x ps, all (@rterm _) ps -> - (holds (set_nth 0 e i x) (foldr (fun t : term F => And (t == 0)) True 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)). Proof. move=> e i x; elim=> [|p ps ihps] //=. @@ -579,9 +595,10 @@ constructor; first by case=> -> hps; rewrite eqxx /=; apply/ihps. by case/andP; move/eqP=> -> psr; split=> //; apply/ihps. Qed. -Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq (term F)) : +Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq tF) : all (@rterm _) ps -> - (holds (set_nth 0 e i x) (foldr (fun t : term F => And (t != 0)) True 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)). Proof. elim: ps => [|p ps ihps] //=. @@ -611,12 +628,12 @@ case g0: (\big[(@rgcdp F)/0%:P]_(j <- map (eval_poly e \o abstrX i) ps) j == 0). case=> _; move/holds_conjn=> hc; move/hc:rqs. by rewrite -root_bigmul //= (eqP m0) root0. constructor; move/negP:m0; move/negP=>m0. - case: (closed_nonrootP axiom _ m0) => x {m0}. + case: (closed_nonrootP F_closed _ m0) => x {m0}. rewrite abstrX_bigmul eval_bigmul -bigmap_id root_bigmul=> m0. exists x; do 2?constructor=> //; last by apply/holds_conjn. apply/holds_conj; rewrite //= -root_biggcd. by rewrite (eqp_root (aux _ _ _ )) (eqP g0) root0. -apply: (iffP (closed_rootP axiom _)); case=> x Px; exists x; move: Px => //=. +apply: (iffP (closed_rootP F_closed _)) => -[x Px]; exists x; move: Px => //=. rewrite (eqp_root (eqp_rgdco_gdco _ _)) root_gdco ?g0 //. rewrite -(eqp_root (aux _ _ _ )) root_biggcd abstrX_bigmul eval_bigmul. rewrite -bigmap_id root_bigmul; case/andP=> psr qsr. @@ -632,7 +649,259 @@ Qed. Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim. Proof. by move=> i bc /= rbc; apply: ex_elim_qf. Qed. -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 + & forall u : E, exists q, u = (map_poly FtoE q).[w]}}}. +Proof. +pose fix d i := + if i is i1.+1 then + let d1 := oapp (gcdp (d i1)) 0 (unpickle i1) in + if size d1 > 1 then d1 else d i1 + else p. +move=> p_gt1; have sz_d i: size (d i) > 1 by elim: i => //= i IHi; case: ifP. +have dv_d i j: i <= j -> d j %| d i. + move/subnK <-; elim: {j}(j - i)%N => //= j IHj; case: ifP => //=. + case: (unpickle _) => /= [q _|]; last by rewrite size_poly0. + exact: dvdp_trans (dvdp_gcdl _ _) IHj. +pose I : pred {poly F} := [pred q | d (pickle q).+1 %| q]. +have I'co q i: q \notin I -> i > pickle q -> coprimep q (d i). + rewrite inE => I'q /dv_d/coprimep_dvdl-> //; apply: contraR I'q. + rewrite coprimep_sym /coprimep /= pickleK /= neq_ltn. + case: ifP => [_ _| ->]; first exact: dvdp_gcdr. + rewrite orbF ltnS leqn0 size_poly_eq0 gcdp_eq0 -size_poly_eq0. + by rewrite -leqn0 leqNgt ltnW //. +have memI q: reflect (exists i, d i %| q) (q \in I). + apply: (iffP idP) => [|[i dv_di_q]]; first by exists (pickle q).+1. + have [le_i_q | /I'co i_co_q] := leqP i (pickle q). + rewrite inE /= pickleK /=; case: ifP => _; first exact: dvdp_gcdr. + exact: dvdp_trans (dv_d _ _ le_i_q) dv_di_q. + apply: contraR i_co_q _. + by rewrite /coprimep (eqp_size (dvdp_gcd_idr dv_di_q)) neq_ltn sz_d orbT. +have I_ideal : idealr_closed I. + split=> [||a q1 q2 Iq1 Iq2]; first exact: dvdp0. + by apply/memI=> [[i /idPn[]]]; rewrite dvdp1 neq_ltn sz_d orbT. + apply/memI; exists (maxn (pickle q1).+1 (pickle q2).+1); apply: dvdp_add. + by apply: dvdp_mull; apply: dvdp_trans Iq1; apply/dv_d/leq_maxl. + by apply: dvdp_trans Iq2; apply/dv_d/leq_maxr. +pose Iaddkey := GRing.Pred.Add (DefaultPredKey I) I_ideal. +pose Iidkey := MkIdeal (GRing.Pred.Zmod Iaddkey I_ideal) I_ideal. +pose E := ComRingType _ (@Quotient.mulqC _ _ _ (KeyedPred Iidkey)). +pose PtoE : {rmorphism {poly F} -> E} := [rmorphism of \pi_E%qT : {poly F} -> E]. +have PtoEd i: PtoE (d i) = 0. + by apply/eqP; rewrite piE Quotient.equivE subr0; apply/memI; exists i. +pose Einv (z : E) (q := repr z) (dq := d (pickle q).+1) := + let q_unitP := Bezout_eq1_coprimepP q dq in + if q_unitP is ReflectT ex_uv then PtoE (sval (sig_eqW ex_uv)).1 else 0. +have Einv0: Einv 0 = 0. + rewrite /Einv; case: Bezout_eq1_coprimepP => // ex_uv. + case/negP: (oner_neq0 E); rewrite piE -[_ 1]/(PtoE 1); have [uv <-] := ex_uv. + by rewrite rmorphD !rmorphM PtoEd /= reprK !mulr0 addr0. +have EmulV: GRing.Field.axiom Einv. + rewrite /Einv=> z nz_z; case: Bezout_eq1_coprimepP => [ex_uv |]; last first. + move/Bezout_eq1_coprimepP; rewrite I'co //. + by rewrite piE -{1}[z]reprK -Quotient.idealrBE subr0 in nz_z. + apply/eqP; case: sig_eqW => {ex_uv} [uv uv1]; set i := _.+1 in uv1 *. + rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE. + by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull. +pose EringU := [comUnitRingType of UnitRingType _ (FieldUnitMixin EmulV Einv0)]. +have Eunitf := @FieldMixin _ _ EmulV Einv0. +pose Efield := FieldType (IdomainType EringU (FieldIdomainMixin Eunitf)) Eunitf. +pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)). +pose FtoE := [rmorphism of PtoE \o polyC]; pose w : E := PtoE 'X. +have defPtoE q: (map_poly FtoE q).[w] = PtoE q. + by rewrite map_poly_comp horner_map [_.['X]]comp_polyXr. +exists [countFieldType of Ecount], FtoE, w => [|u]. + by rewrite /root defPtoE (PtoEd 0%N). +by exists (repr u); rewrite defPtoE /= reprK. +Qed. + +Lemma countable_algebraic_closure (F : countFieldType) : + {K : countClosedFieldType & {FtoK : {rmorphism F -> K} | integralRange FtoK}}. +Proof. +pose minXp (R : ringType) (p : {poly R}) := if size p > 1 then p else 'X. +have minXp_gt1 R p: size (minXp R p) > 1. + by rewrite /minXp; case: ifP => // _; rewrite size_polyX. +have minXpE (R : ringType) (p : {poly R}) : size p > 1 -> minXp R p = p. + by rewrite /minXp => ->. +have ext1 p := countable_field_extension (minXp_gt1 _ p). +pose ext1fT E p := tag (ext1 E p). +pose ext1to E p : {rmorphism _ -> ext1fT E p} := tag (tagged (ext1 E p)). +pose ext1w E p : ext1fT E p := s2val (tagged (tagged (ext1 E p))). +have ext1root E p: root (map_poly (ext1to E p) (minXp E p)) (ext1w E p). + by rewrite /ext1w; case: (tagged (tagged (ext1 E p))). +have ext1gen E p u: {q | u = (map_poly (ext1to E p) q).[ext1w E p]}. + by apply: sig_eqW; rewrite /ext1w; case: (tagged (tagged (ext1 E p))) u. +pose pExtEnum (E : countFieldType) := nat -> {poly E}. +pose Ext := {E : countFieldType & pExtEnum E}; pose MkExt : Ext := Tagged _ _. +pose EtoInc (E : Ext) i := ext1to (tag E) (tagged E i). +pose incEp E i j := + let v := map_poly (EtoInc E i) (tagged E j) in + if decode j is [:: i1; k] then + if i1 == i then odflt v (unpickle k) else v + else v. +pose fix E_ i := if i is i1.+1 then MkExt _ (incEp (E_ i1) i1) else MkExt F \0. +pose E i := tag (E_ i); pose Krep := {i : nat & E i}. +pose fix toEadd i k : {rmorphism E i -> E (k + i)%N} := + if k is k1.+1 then [rmorphism of EtoInc _ (k1 + i)%N \o toEadd _ _] + else [rmorphism of idfun]. +pose toE i j (le_ij : i <= j) := + ecast j {rmorphism E i -> E j} (subnK le_ij) (toEadd i (j - i)%N). +have toEeq i le_ii: toE i i le_ii =1 id. + by rewrite /toE; move: (subnK _); rewrite subnn => ?; rewrite eq_axiomK. +have toEleS i j leij leiSj z: toE i j.+1 leiSj z = EtoInc _ _ (toE i j leij z). + rewrite /toE; move: (j - i)%N {leij leiSj}(subnK _) (subnK _) => k. + by case: j /; rewrite (addnK i k.+1) => eq_kk; rewrite [eq_kk]eq_axiomK. +have toEirr := congr1 ((toE _ _)^~ _) (bool_irrelevance _ _). +have toEtrans j i k leij lejk leik z: + toE i k leik z = toE j k lejk (toE i j leij z). +- elim: k leik lejk => [|k IHk] leiSk lejSk. + by case: j => // in leij lejSk *; rewrite toEeq. + have:= lejSk; rewrite {1}leq_eqVlt ltnS => /predU1P[Dk | lejk]. + by rewrite -Dk in leiSk lejSk *; rewrite toEeq. + by have leik := leq_trans leij lejk; rewrite !toEleS -IHk. +have [leMl leMr] := (leq_maxl, leq_maxr); pose le_max := (leq_max, leqnn, orbT). +pose pairK (x y : Krep) (m := maxn _ _) := + (toE _ m (leMl _ _) (tagged x), toE _ m (leMr _ _) (tagged y)). +pose eqKrep x y := prod_curry (@eq_op _) (pairK x y). +have eqKrefl : reflexive eqKrep by move=> z; apply/eqP; apply: toEirr. +have eqKsym : symmetric eqKrep. + move=> z1 z2; rewrite {1}/eqKrep /= eq_sym; move: (leMl _ _) (leMr _ _). + by rewrite maxnC => lez1m lez2m; congr (_ == _); apply: toEirr. +have eqKtrans : transitive eqKrep. + rewrite /eqKrep /= => z2 z1 z3 /eqP eq_z12 /eqP eq_z23. + rewrite -(inj_eq (fmorph_inj (toE _ _ (leMr (tag z2) _)))). + rewrite -!toEtrans ?le_max // maxnCA maxnA => lez3m lez1m. + rewrite {lez1m}(toEtrans (maxn (tag z1) (tag z2))) // {}eq_z12. + do [rewrite -toEtrans ?le_max // -maxnA => lez2m] in lez3m *. + by rewrite (toEtrans (maxn (tag z2) (tag z3))) // eq_z23 -toEtrans. +pose K := {eq_quot (EquivRel _ eqKrefl eqKsym eqKtrans)}%qT. +have cntK : Countable.mixin_of K := CanCountMixin (@reprK _ _). +pose EtoKrep i (x : E i) : K := \pi%qT (Tagged E x). +have [EtoK piEtoK]: {EtoK | forall i, EtoKrep i =1 EtoK i} by exists EtoKrep. +pose FtoK := EtoK 0%N; rewrite {}/EtoKrep in piEtoK. +have eqEtoK i j x y: + toE i _ (leMl i j) x = toE j _ (leMr i j) y -> EtoK i x = EtoK j y. +- by move/eqP=> eq_xy; rewrite -!piEtoK; apply/eqmodP. +have toEtoK j i leij x : EtoK j (toE i j leij x) = EtoK i x. + by apply: eqEtoK; rewrite -toEtrans. +have EtoK_0 i: EtoK i 0 = FtoK 0 by apply: eqEtoK; rewrite !rmorph0. +have EtoK_1 i: EtoK i 1 = FtoK 1 by apply: eqEtoK; rewrite !rmorph1. +have EtoKeq0 i x: (EtoK i x == FtoK 0) = (x == 0). + by rewrite /FtoK -!piEtoK eqmodE /= /eqKrep /= rmorph0 fmorph_eq0. +have toErepr m i leim x lerm: + toE _ m lerm (tagged (repr (EtoK i x))) = toE i m leim x. +- have: (Tagged E x == repr (EtoK i x) %[mod K])%qT by rewrite reprK piEtoK. + rewrite eqmodE /= /eqKrep; case: (repr _) => j y /= in lerm * => /eqP /=. + have leijm: maxn i j <= m by rewrite geq_max leim. + by move/(congr1 (toE _ _ leijm)); rewrite -!toEtrans. +pose Kadd (x y : K) := EtoK _ (prod_curry +%R (pairK (repr x) (repr y))). +pose Kopp (x : K) := EtoK _ (- tagged (repr x)). +pose Kmul (x y : K) := EtoK _ (prod_curry *%R (pairK (repr x) (repr y))). +pose Kinv (x : K) := EtoK _ (tagged (repr x))^-1. +have EtoK_D i: {morph EtoK i : x y / x + y >-> Kadd x y}. + move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphD. + by rewrite -!toEtrans ?le_max // => lexm leym; rewrite !toErepr. +have EtoK_N i: {morph EtoK i : x / - x >-> Kopp x}. + by move=> x; apply: eqEtoK; set j := tag _; rewrite !rmorphN toErepr. +have EtoK_M i: {morph EtoK i : x y / x * y >-> Kmul x y}. + move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphM. + by rewrite -!toEtrans ?le_max // => lexm leym; rewrite !toErepr. +have EtoK_V i: {morph EtoK i : x / x^-1 >-> Kinv x}. + by move=> x; apply: eqEtoK; set j := tag _; rewrite !fmorphV toErepr. +case: {toErepr}I in (Kadd) (Kopp) (Kmul) (Kinv) EtoK_D EtoK_N EtoK_M EtoK_V. +pose inEi i z := {x : E i | z = EtoK i x}; have KtoE z: {i : nat & inEi i z}. + by elim/quotW: z => [[i x] /=]; exists i, x; rewrite piEtoK. +have inEle i j z: i <= j -> inEi i z -> inEi j z. + by move=> leij [x ->]; exists (toE i j leij x); rewrite toEtoK. +have KtoE2 z1 z2: {i : nat & inEi i z1 & inEi i z2}. + have [[i1 Ez1] [i2 Ez2]] := (KtoE z1, KtoE z2). + by exists (maxn i1 i2); [apply: inEle Ez1 | apply: inEle Ez2]. +have KtoE3 z1 z2 z3: {i : nat & inEi i z1 & inEi i z2 * inEi i z3}%type. + have [[i1 Ez1] [i2 Ez2 Ez3]] := (KtoE z1, KtoE2 z2 z3). + by exists (maxn i1 i2); [apply: inEle Ez1 | split; apply: inEle (leMr _ _) _]. +have KaddC: commutative Kadd. + by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_D addrC. +have KaddA: associative Kadd. + move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. + by rewrite -!EtoK_D addrA. +have Kadd0: left_id (FtoK 0) Kadd. + by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_0 i) -EtoK_D add0r. +have KaddN: left_inverse (FtoK 0) Kopp Kadd. + by move=> u; have [i [x ->]] := KtoE u; rewrite -EtoK_N -EtoK_D addNr EtoK_0. +pose Kzmod := ZmodType K (ZmodMixin KaddA KaddC Kadd0 KaddN). +have KmulC: commutative Kmul. + by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_M mulrC. +have KmulA: @associative Kzmod Kmul. + move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. + by rewrite -!EtoK_M mulrA. +have Kmul1: left_id (FtoK 1) Kmul. + by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_1 i) -EtoK_M mul1r. +have KmulD: left_distributive Kmul Kadd. + move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w. + by rewrite -!(EtoK_M, EtoK_D) mulrDl. +have Kone_nz: FtoK 1 != FtoK 0 by rewrite EtoKeq0 oner_neq0. +pose KringMixin := ComRingMixin KmulA KmulC Kmul1 KmulD Kone_nz. +pose Kring := ComRingType (RingType Kzmod KringMixin) KmulC. +have KmulV: @GRing.Field.axiom Kring Kinv. + move=> u; have [i [x ->]] := KtoE u; rewrite EtoKeq0 => nz_x. + by rewrite -EtoK_V -[_ * _]EtoK_M mulVf ?EtoK_1. +have Kinv0: Kinv (FtoK 0) = FtoK 0 by rewrite -EtoK_V invr0. +pose Kuring := [comUnitRingType of UnitRingType _ (FieldUnitMixin KmulV Kinv0)]. +pose KfieldMixin := @FieldMixin _ _ KmulV Kinv0. +pose Kidomain := IdomainType Kuring (FieldIdomainMixin KfieldMixin). +pose Kfield := FieldType Kidomain KfieldMixin. +have EtoKrmorphism i: rmorphism (EtoK i : E i -> Kfield). + by do 2?split=> [x y|]; rewrite ?EtoK_D ?EtoK_N ?EtoK_M ?EtoK_1. +pose EtoKM := RMorphism (EtoKrmorphism _); have EtoK_E: EtoK _ = EtoKM _ by []. +have toEtoKp := @eq_map_poly _ Kring _ _(toEtoK _ _ _). +have Kclosed: GRing.ClosedField.axiom Kfield. + move=> n pK n_gt0; pose m0 := \max_(i < n) tag (KtoE (pK i)); pose m := m0.+1. + have /fin_all_exists[pE DpE] (i : 'I_n): exists y, EtoK m y = pK i. + pose u := KtoE (pK i); have leum0: tag u <= m0 by rewrite (bigmax_sup i). + by have [y ->] := tagged u; exists (toE _ _ (leqW leum0) y); rewrite toEtoK. + pose p := 'X^n - rVpoly (\row_i pE i); pose j := code [:: m0; pickle p]. + pose pj := tagged (E_ j) j; pose w : E j.+1 := ext1w (E j) pj. + have lemj: m <= j by rewrite (allP (ltn_code _)) ?mem_head. + exists (EtoKM j.+1 w); apply/eqP; rewrite -subr_eq0; apply/eqP. + transitivity (EtoKM j.+1 (map_poly (toE m j.+1 (leqW lemj)) p).[w]). + rewrite -horner_map -map_poly_comp toEtoKp EtoK_E; move/EtoKM: w => w. + rewrite rmorphB [_ 'X^n]map_polyXn !hornerE hornerXn; congr (_ - _ : Kring). + rewrite (@horner_coef_wide _ n) ?size_map_poly ?size_poly //. + by apply: eq_bigr => i _; rewrite coef_map coef_rVpoly valK mxE /= DpE. + suffices Dpj: map_poly (toE m j lemj) p = pj. + apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj. + rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly. + by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly. + rewrite {w}/pj; elim: {-9}j lemj => // k IHk lemSk. + move: lemSk (lemSk); rewrite {1}leq_eqVlt ltnS => /predU1P[<- | lemk] lemSk. + rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)) map_poly_id //= /incEp. + by rewrite codeK eqxx pickleK. + rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK. + by rewrite -if_neg neq_ltn lemk. +suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. + pose Kdec := DecFieldType Kfield (closed_field_QEMixin Kclosed). + pose KclosedField := ClosedFieldType Kdec Kclosed. + by exists [countClosedFieldType of CountType KclosedField cntK]. +exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z. +suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT). + by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p. +rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen. +move: (i - 0)%N (subnK _) => n; case: i /. +elim: n => [|n IHn] /= z; first exact: integral_id. +have{z} [q ->] := ext1gen _ _ z; set pn := tagged (E_ _) _. +apply: integral_horner. + by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph. +apply: integral_root (ext1root _ _) _. + by rewrite map_poly_eq0 -size_poly_gt0 ltnW. +by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph. +Qed. |