From 6832d38a63ca703d95fbb4f582da400b4d9a3d99 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 May 2022 15:12:37 +0200 Subject: [PATCH] Port to hierarchy builder --- theories/abel.v | 74 +++++++++++++++----------------- theories/xmathcomp/algR.v | 63 +++++++++------------------ theories/xmathcomp/classic_ext.v | 9 +++- theories/xmathcomp/map_gal.v | 14 +++--- theories/xmathcomp/various.v | 35 ++++++++------- 5 files changed, 91 insertions(+), 104 deletions(-) diff --git a/theories/abel.v b/theories/abel.v index 17e5f2d..e64fd85 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra. From mathcomp Require Import all_solvable all_field polyrcf. From Abel Require Import various classic_ext map_gal algR. @@ -657,7 +658,8 @@ apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0). exists rs => //; suff <- : limg iota = 1%VS by []. apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v. by move=> /memv_imgP[u _ ->]; rewrite iotaF/= rpredZ// rpred1. - pose S := SplittingFieldType F L splitL. + pose sM := FieldExt_IsSplittingField.Build F L splitL. + pose S : splittingFieldType F := HB.pack L sM. exists S, rs; split => //=; first by rewrite -(eq_map_poly iotaF). by apply: (sol_p S rs); rewrite -(eq_map_poly iotaF). move=> L rs prs; apply: sol_p => -[M [rs' [prs']]]. @@ -682,7 +684,8 @@ have splitK : splittingFieldFor 1 (p ^^ in_alg K) fullv. by rewrite lfunE subvsP. have sfK : SplittingField.axiom K. by exists (p ^^ in_alg K) => //; apply/polyOver1P; exists p. -pose S := SplittingFieldType F K sfK. +pose sM := FieldExt_IsSplittingField.Build F K sfK. +pose S : splittingFieldType F := HB.pack K sM. have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by []. have splitM : splittingFieldFor 1 (p ^^ in_alg M) <<1 & rs'>> by exists rs'. have splitL : splittingFieldFor 1 (p ^^ in_alg L) <<1 & rs>> by exists rs. @@ -719,7 +722,8 @@ have splitL : SplittingField.axiom L. exists rs => //; suff <- : limg f = 1%VS by []. apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v. by move=> /memv_imgP[u _ ->]; rewrite fF/= rpredZ// rpred1. -pose S := SplittingFieldType F L splitL. +pose sM := FieldExt_IsSplittingField.Build F L splitL. +pose S : splittingFieldType F := HB.pack L sM. pose d := \dim <<1 & (rs : seq S)>>. have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F. by have /charf0P-> := charF0; rewrite -lt0n adim_gt0. @@ -750,7 +754,9 @@ have prs : p ^^ in_alg L %= \prod_(z <- rs) ('X - z%:P). by rewrite (eq_map_poly (fmorph_eq_rat _)). have splitL : SplittingField.axiom L. by exists (p ^^ in_alg L); [by apply/polyOver1P; exists p | exists rs]. -pose S := SplittingFieldType rat L splitL. +pose Frat := [the fieldType of rat : Type]. +pose sM := FieldExt_IsSplittingField.Build Frat L splitL. +pose S : splittingFieldType Frat := HB.pack L sM. pose d := \dim <<1 & (rs : seq S)>>. have d_gt0 : (d > 0)%N by rewrite adim_gt0. have [ralg ralg_prim] := C_prim_root_exists d_gt0. @@ -767,7 +773,8 @@ have splitL' : SplittingField.axiom L'. have [us cycloE usw] := splitting_Fadjoin_cyclotomic 1%AS w_prim. exists (us ++ rs'); last by rewrite adjoin_cat usw -adjoin_cons. by rewrite big_cat/= (eqp_trans (eqp_mulr _ cycloE))// eqp_mull//. -pose S' := SplittingFieldType rat L' splitL'. +pose sM' := FieldExt_IsSplittingField.Build Frat L' splitL'. +pose S' : splittingFieldType Frat := HB.pack L' sM'. have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by exists rs. have splitS' : splittingFieldFor 1 (p ^^ in_alg S') <<1 & rs'>> by exists rs'. have [f /= imgf] := splitting_ahom splitS splitS'. @@ -778,10 +785,10 @@ Qed. Lemma splitting_num_field (p : {poly rat}) : {L : splittingFieldType rat & { LtoC : {rmorphism L -> algC} | (p != 0 -> splittingFieldFor 1 (p ^^ in_alg L) {:L}) - /\ (p = 0 -> L = [splittingFieldType rat of rat^o]) }}. + /\ (p = 0 -> L = [the splittingFieldType rat of rat^o]) }}. Proof. have [->|p_neq0] := eqVneq p 0. - by exists [splittingFieldType rat of rat^o], [rmorphism of ratr]; split. + by exists [the splittingFieldType rat of rat^o], [rmorphism of ratr]; split. have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)). have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P). by rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx// lead_coef_eq0 map_poly_eq0. @@ -791,7 +798,10 @@ have splitL' : splittingFieldFor 1 (p ^^ in_alg L') {: L'}%AS. by rewrite -map_poly_comp map_prod_XsubC rs'E (eq_map_poly (fmorph_eq_rat _)). have splitaxL' : SplittingField.axiom L'. by exists (p ^^ in_alg L'); first by apply/polyOver1P; exists p. -exists (SplittingFieldType rat L' splitaxL'), L'toC; split => //. +pose Frat := [the fieldType of rat : Type]. +pose sM' := FieldExt_IsSplittingField.Build Frat L' splitaxL'. +pose S' : splittingFieldType Frat := HB.pack L' sM'. +exists S', L'toC; split => //. by move=> p_eq0; rewrite p_eq0 eqxx in p_neq0. Qed. @@ -811,7 +821,7 @@ Qed. Definition numfield (p : {poly rat}) : splittingFieldType rat := projT1 (splitting_num_field p). -Lemma numfield0 : numfield 0 = [splittingFieldType rat of rat^o]. +Lemma numfield0 : numfield 0 = [the splittingFieldType rat of rat^o]. Proof. by rewrite /numfield; case: splitting_num_field => //= ? [? [_ ->]]. Qed. Definition numfield_inC (p : {poly rat}) : @@ -901,7 +911,7 @@ Qed. Let rp'_uniq : uniq rp'. Proof. rewrite -separable_prod_XsubC -(eqp_separable ratr_p'). -rewrite -char0_ratrE separable_map. +rewrite -char0_ratrE separable_map separable_poly.unlock. apply/coprimepP => d; have [sp_gt1 eqp] := p_irr => /eqp. rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1). move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv. @@ -1073,7 +1083,7 @@ Lemma gal_perm_cycle_order : #[(gal_perm gal_cycle)]%g = d. Proof. by rewrite order_injm ?gal_cycle_order ?injm_gal_perm ?gal1. Qed. Definition conjL : {lrmorphism L -> L} := - projT1 (restrict_aut_to_normal_num_field iota conjC). + projT1 (restrict_aut_to_normal_num_field iota Num.conj_op). Definition iotaJ : {morph iota : x / conjL x >-> x^*} := projT2 (restrict_aut_to_normal_num_field _ _). @@ -1209,6 +1219,7 @@ Hint Resolve irreducible_example : core. Lemma separable_example : separable_poly poly_example. Proof. +rewrite separable_poly.unlock. apply/coprimepP => q /(irredp_XsubCP irreducible_example) [//| eqq]. have size_deriv_example : size poly_example^`() = 5%N. rewrite !derivCE addr0 alg_polyC -scaler_nat addr0. @@ -1354,12 +1365,7 @@ Definition decode_const (n : nat) : const := match n with 0 => Zero | 1 => One | n.+2 => URoot n end. Lemma code_constK : cancel encode_const decode_const. Proof. by case. Qed. -Definition const_eqMixin := CanEqMixin code_constK. -Canonical const_eqType := EqType const const_eqMixin. -Definition const_choiceMixin := CanChoiceMixin code_constK. -Canonical const_choiceType := ChoiceType const const_choiceMixin. -Definition const_countMixin := CanCountMixin code_constK. -Canonical const_countType := CountType const const_countMixin. +HB.instance Definition _ := Countable.copy const (can_type code_constK). Definition encode_binOp (c : binOp) : bool := match c with Add => false | Mul => true end. @@ -1367,12 +1373,7 @@ Definition decode_binOp (b : bool) : binOp := match b with false => Add | _ => Mul end. Lemma code_binOpK : cancel encode_binOp decode_binOp. Proof. by case. Qed. -Definition binOp_eqMixin := CanEqMixin code_binOpK. -Canonical binOp_eqType := EqType binOp binOp_eqMixin. -Definition binOp_choiceMixin := CanChoiceMixin code_binOpK. -Canonical binOp_choiceType := ChoiceType binOp binOp_choiceMixin. -Definition binOp_countMixin := CanCountMixin code_binOpK. -Canonical binOp_countType := CountType binOp binOp_countMixin. +HB.instance Definition _ := Countable.copy binOp (can_type code_binOpK). Definition encode_unOp (c : unOp) : nat + nat := match c with Opp => inl _ 0%N | Inv => inl _ 1%N @@ -1382,12 +1383,7 @@ Definition decode_unOp (n : nat + nat) : unOp := | inl n.+2 => Exp n | inr n => Root n end. Lemma code_unOpK : cancel encode_unOp decode_unOp. Proof. by case. Qed. -Definition unOp_eqMixin := CanEqMixin code_unOpK. -Canonical unOp_eqType := EqType unOp unOp_eqMixin. -Definition unOp_choiceMixin := CanChoiceMixin code_unOpK. -Canonical unOp_choiceType := ChoiceType unOp unOp_choiceMixin. -Definition unOp_countMixin := CanCountMixin code_unOpK. -Canonical unOp_countType := CountType unOp unOp_countMixin. +HB.instance Definition _ := Countable.copy unOp (can_type code_unOpK). Fixpoint encode_algT F (f : algterm F) : GenTree.tree (F + const) := let T_ isbin := if isbin then binOp else unOp in @@ -1414,14 +1410,12 @@ Lemma code_algTK F : cancel (@encode_algT F) (@decode_algT F). Proof. by elim => // [u f IHf|b f IHf f' IHf']/=; rewrite pickleK -lock ?IHf ?IHf'. Qed. -Definition algT_eqMixin (F : eqType) := CanEqMixin (@code_algTK F). -Canonical algT_eqType (F : eqType) := EqType (algterm F) (@algT_eqMixin F). -Definition algT_choiceMixin (F : choiceType) := CanChoiceMixin (@code_algTK F). -Canonical algT_choiceType (F : choiceType) := - ChoiceType (algterm F) (@algT_choiceMixin F). -Definition algT_countMixin (F : countType) := CanCountMixin (@code_algTK F). -Canonical algT_countType (F : countType) := - CountType (algterm F) (@algT_countMixin F). +HB.instance Definition _ (F : eqType) := Equality.copy (algterm F) + (can_type (@code_algTK F)). +HB.instance Definition _ (F : choiceType) := Choice.copy (algterm F) + (can_type (@code_algTK F)). +HB.instance Definition _ (F : countType) := Countable.copy (algterm F) + (can_type (@code_algTK F)). Declare Scope algT_scope. Delimit Scope algT_scope with algT. @@ -1551,7 +1545,9 @@ have mprs : mp ^^ in_alg L %= \prod_(z <- rsmp) ('X - z%:P). by rewrite -char0_ratrE// (eq_map_poly (fmorph_eq_rat _)) eqpxx. have splitL : SplittingField.axiom L. by exists (mp ^^ in_alg L); [apply/polyOver1P; exists mp | exists rsmp]. -pose S := SplittingFieldType rat L splitL. +pose Frat := [the fieldType of rat : Type]. +pose sM := FieldExt_IsSplittingField.Build Frat L splitL. +pose S : splittingFieldType Frat := HB.pack L sM. have algsW: {subset rsalg <= algs}. move=> x; rewrite -fsE => /mapP[{x}f ffs ->]. apply/flattenP; exists (subeval ratr f); rewrite ?map_f//. @@ -1573,7 +1569,7 @@ rewrite {p p_neq0 mkalg pE prs rsmp iota_rs mprs rsf rs rsE mp suff: forall (L : splittingFieldType rat) (iota : {rmorphism L -> algC}) als, map iota als = algs -> radical.-ext 1%VS <<1 & als>>%VS. by move=> /(_ S iota als alsE). -move=> {}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE. +move=> {sM}L {}iota {splitL S} {}als {}alsE; rewrite {}/algs in alsE. elim: fs => [|f fs IHfs]//= in rsalg fsE als alsE *. case: als => []// in alsE *. by rewrite Fadjoin_nil; apply: rext_refl. diff --git a/theories/xmathcomp/algR.v b/theories/xmathcomp/algR.v index d16fcc2..ec39c95 100644 --- a/theories/xmathcomp/algR.v +++ b/theories/xmathcomp/algR.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra. From mathcomp Require Import all_solvable all_field. From Abel Require Import various. @@ -15,33 +16,18 @@ Local Notation "p ^^ f" := (map_poly f p) Record algR := in_algR {algRval : algC; algRvalP : algRval \is Num.real}. -Canonical algR_subType := [subType for algRval]. -Definition algR_eqMixin := [eqMixin of algR by <:]. -Canonical algR_eqType := EqType algR algR_eqMixin. -Definition algR_choiceMixin := [choiceMixin of algR by <:]. -Canonical algR_choiceType := ChoiceType algR algR_choiceMixin. -Definition algR_countMixin := [countMixin of algR by <:]. -Canonical algR_countType := CountType algR algR_countMixin. -Definition algR_zmodMixin := [zmodMixin of algR by <:]. -Canonical algR_zmodType := ZmodType algR algR_zmodMixin. -Definition algR_ringMixin := [ringMixin of algR by <:]. -Canonical algR_ringType := RingType algR algR_ringMixin. -Definition algR_comRingMixin := [comRingMixin of algR by <:]. -Canonical algR_comRingType := ComRingType algR algR_comRingMixin. -Definition algR_unitRingMixin := [unitRingMixin of algR by <:]. -Canonical algR_unitRingType := UnitRingType algR algR_unitRingMixin. -Canonical algR_comUnitRingType := [comUnitRingType of algR]. -Definition algR_idomainMixin := [idomainMixin of algR by <:]. -Canonical algR_idomainType := IdomainType algR algR_idomainMixin. -Definition algR_fieldMixin := [fieldMixin of algR by <:]. -Canonical algR_fieldType := FieldType algR algR_fieldMixin. -Definition algR_porderMixin := [porderMixin of algR by <:]. -Canonical algR_porderType := POrderType ring_display algR algR_porderMixin. -Lemma total_algR : totalPOrderMixin [porderType of algR]. +HB.instance Definition _ := [IsSUB for algRval]. +HB.instance Definition _ := [Countable of algR by <:]. +HB.instance Definition _ := [zmodMixin of algR by <:]. +HB.instance Definition _ := [ringMixin of algR by <:]. +HB.instance Definition _ := [comRingMixin of algR by <:]. +HB.instance Definition _ := [unitRingMixin of algR by <:]. +HB.instance Definition _ := [idomainMixin of algR by <:]. +HB.instance Definition _ := [fieldMixin of algR by <:]. +HB.instance Definition _ := [POrder of algR by <:]. +Lemma total_algR : total (<=%O : rel [porderType of algR]). Proof. by move=> x y; apply/real_leVge/valP/valP. Qed. -Canonical algR_latticeType := LatticeType algR total_algR. -Canonical algR_distrLatticeType := DistrLatticeType algR total_algR. -Canonical algR_orderType := OrderType algR total_algR. +HB.instance Definition _ := Order.POrder_IsTotal.Build _ algR total_algR. Lemma algRval_is_rmorphism : rmorphism algRval. Proof. by []. Qed. Canonical algRval_additive := Additive algRval_is_rmorphism. @@ -58,8 +44,6 @@ Lemma algR_normrN x : algR_norm (- x) = algR_norm x. Proof. by apply/val_inj; apply: normrN. Qed. Section Num. -Definition algR_normedMixin := - Num.NormedMixin algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN. Section withz. Let z : algR := 0. @@ -73,18 +57,10 @@ Lemma algR_ler_def (x y : algR) : (x <= y) = (algR_norm (y - x) == y - x). Proof. by apply: ler_def. Qed. End withz. -Let algR_ring := (GRing.Ring.Pack (GRing.ComRing.base - (GRing.ComUnitRing.base (GRing.IntegralDomain.base - (GRing.IntegralDomain.class [idomainType of algR]))))). -Definition algR_numMixin : @Num.mixin_of algR_ring _ _ := - @Num.Mixin _ _ algR_normedMixin - algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def. - -Canonical algR_numDomainType := NumDomainType algR algR_numMixin. -Canonical algR_normedZmodType := NormedZmodType algR algR algR_normedMixin. -Canonical algR_numFieldType := [numFieldType of algR]. -Canonical algR_realDomainType := [realDomainType of algR]. -Canonical algR_realFieldType := [realFieldType of algR]. +HB.instance Definition _ := Num.Zmodule_IsNormed.Build _ algR + algR_ler_norm_add algR_normr0_eq0 algR_normrMn algR_normrN. +HB.instance Definition _ := Num.IsNumDomain.Build _ algR + algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def. End Num. Definition algR_archiFieldMixin : Num.archimedean_axiom [numDomainType of algR]. @@ -96,7 +72,8 @@ set n := floorC _; have [n_lt0|n_ge0] := ltP n 0. move=> x_lt; exists (`|(n + 1)%R|%N); apply: lt_le_trans x_lt _. by rewrite /= rmorphMn/= pmulrn gez0_abs// addr_ge0. Qed. -Canonical algR_archiFieldType := ArchiFieldType algR algR_archiFieldMixin. +HB.instance Definition _ := Num.RealField_IsArchimedean.Build algR + algR_archiFieldMixin. Definition algRpfactor (x : algC) : {poly algR} := if x \is Num.real =P true is ReflectT xR then 'X - (in_algR xR)%:P else @@ -205,7 +182,7 @@ elim: n r => // n IHn [|x r]/= in p pr *. rewrite ltnS => r_lt. have xJxr : x^* \in x :: r. rewrite -root_prod_XsubC -pr. - have /eq_map_poly-> : algRval =1 conjC \o algRval. + have /eq_map_poly-> : algRval =1 Num.conj_op \o algRval. by move=> a /=; rewrite (CrealP (algRvalP _)). by rewrite map_poly_comp mapf_root pr root_prod_XsubC mem_head. have xJr : (x \isn't Num.real) ==> (x^* \in r) by rewrite implyNb CrealE. @@ -270,4 +247,4 @@ move=> /andP[xR rsabR] /andP[axb arsb] prsab. exists (in_algR xR) => //=. by rewrite -(mapf_root [rmorphism of algRval])//= prsab rootM root_XsubC eqxx. Qed. -Canonical algR_rcfType := RcfType algR algR_rcfMixin. +HB.instance Definition _ := Num.RealField_IsClosed.Build algR algR_rcfMixin. diff --git a/theories/xmathcomp/classic_ext.v b/theories/xmathcomp/classic_ext.v index 21eb643..4b01994 100644 --- a/theories/xmathcomp/classic_ext.v +++ b/theories/xmathcomp/classic_ext.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra. From mathcomp Require Import all_solvable all_field. From Abel Require Import various cyclotomic_ext. @@ -164,7 +165,9 @@ Proof. move=> /(@classic_cycloExt _ L). apply/classic_bind => -[M [w [iota wfull wprim]]]; apply/classicW. suff splitM : SplittingField.axiom M. - by exists (SplittingFieldType F0 M splitM), w, iota. + pose mM := FieldExt_IsSplittingField.Build F0 M splitM. + pose mT : splittingFieldType F0 := HB.pack M mM. + by exists mT, w, iota. apply: (@SplittingFieldExt _ L ('Phi_n ^^ intr) _ iota). rewrite -map_poly_comp (eq_map_poly (rmorph_int _)) -wfull. by rewrite (Phi_cyclotomic wprim); apply: splitting_Fadjoin_cyclotomic. @@ -181,7 +184,9 @@ move=> nN0; suff: classically { L' : fieldExtType F & { w : L' & have splitL : SplittingField.axiom L. exists (cyclotomic w n); rewrite ?cyclotomic_over// -wfull. exact: splitting_Fadjoin_cyclotomic. - by exists (SplittingFieldType F L splitL), w. + pose lM := FieldExt_IsSplittingField.Build F L splitL. + pose lT : splittingFieldType F := HB.pack L lM. + by exists lT, w. pose Fo := [splittingFieldType F of F^o]. apply: classic_bind (@classic_cycloExt _ Fo n nN0). case=> [L [w [iota wfull wprim]]]; apply/classicW. diff --git a/theories/xmathcomp/map_gal.v b/theories/xmathcomp/map_gal.v index 0c70e6a..99365b6 100644 --- a/theories/xmathcomp/map_gal.v +++ b/theories/xmathcomp/map_gal.v @@ -672,7 +672,7 @@ Implicit Types (K E F : {subfield L}). Lemma separable_aimgr E F s : s \in kAEndf E -> separable E (s @: F) = separable E F. Proof. -rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -(separable_aimg _ _ s). +rewrite inE => /kHom_kAut_sub/kAHomP s_id; rewrite -[RHS](separable_aimg _ _ s). suff /eq_in_limg->: {in E, s =1 \1%VF} by rewrite lim1g. by move=> x xE; rewrite lfunE/= s_id. Qed. @@ -773,7 +773,8 @@ Lemma solvable_ext_refl E : solvable_ext E E. Proof. by apply/solvable_extP; exists E; rewrite subvv galois_refl/= galvv solvable1. Qed. -Hint Resolve solvable_ext_refl : core. +Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) => + (apply: solvable_ext_refl) : core. Lemma sub_solvable_ext F K E : (E <= F)%VS -> solvable_ext K F -> solvable_ext K E. @@ -837,10 +838,13 @@ Qed. End normalClosure. -Hint Resolve normalClosureSl : core. -Hint Resolve normalClosureSr : core. +Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) => + (apply: normalClosureSl) : core. +Hint Extern 0 (is_true (subsetv (asval _) (normalClosure _ _))) => + (apply: normalClosureSr) : core. Hint Resolve normalClosure_normal : core. -Hint Resolve solvable_ext_refl : core. +Hint Extern 0 (is_true (solvable_ext (asval _) (asval _))) => + (apply: solvable_ext_refl) : core. Lemma aimg_normalClosure (F0 : fieldType) (L L' : splittingFieldType F0) (iota : 'AHom(L, L')) (K E : {subfield L}) : diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index 3138b31..99cdaa0 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -1,3 +1,4 @@ +From HB Require Import structures. From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable. From mathcomp Require Import all_field. @@ -160,11 +161,8 @@ Proof. by move=> x; apply/ffunP => i; rewrite !ffunE mulVg. Qed. Lemma extnprod_mulgA : associative extnprod_mulg. Proof. by move=> x y z; apply/ffunP => i; rewrite !ffunE mulgA. Qed. -Definition extnprod_groupMixin := - Eval hnf in FinGroup.Mixin extnprod_mulgA extnprod_mul1g extnprod_mulVg. -Canonical extnprod_baseFinGroupType := - Eval hnf in BaseFinGroupType gTn extnprod_groupMixin. -Canonical prod_group := FinGroupType extnprod_mulVg. +HB.instance Definition _ := IsMulGroup.Build gTn + extnprod_mulgA extnprod_mul1g extnprod_mulVg. End ExternalNDirProd. @@ -288,9 +286,9 @@ Section ssrnum. Import Num.Theory. Lemma CrealJ (C : numClosedFieldType) : - {mono (@conjC C) : x / x \is Num.real}. + {mono (@Num.conj_op C) : x / x \is Num.real}. Proof. -suff realK : {homo (@conjC C) : x / x \is Num.real}. +suff realK : {homo (@Num.conj_op C) : x / x \is Num.real}. by move=> x; apply/idP/idP => /realK//; rewrite conjCK. by move=> x xreal; rewrite conj_Creal. Qed. @@ -779,12 +777,13 @@ do [suff init (p : {poly L}) (k : {subfield L}) - case: sig_eqW => x; case: sig_eqW => /= v->; case: sig_eqW => /= w->. by rewrite -!in_algE -rmorphM => /fmorph_inj<-//; rewrite rmorphM. - case: sig_eqW => /= one /esym/eqP; rewrite algid1. - by rewrite -in_algE fmorph_eq1 => /eqP->; rewrite scale1r. + by rewrite -[X in X == _]in_algE fmorph_eq1 => /eqP->; rewrite scale1r. - case: sig_eqW => x; case: sig_eqW => /= v->. - rewrite -mulr_algl -in_algE -rmorphM => /fmorph_inj<-. + rewrite -[_ *: _]mulr_algl -in_algE -rmorphM => /fmorph_inj<-. by rewrite -in_algE rmorphM mulr_algl. exists (linfun_ahom (LRMorphism flr)) => v; rewrite lfunE/=. - by case: sig_eqW => /= x; rewrite algid1 -in_algE => /fmorph_inj->. + case: sig_eqW => /= x. + by rewrite algid1 -[in X in X -> _]in_algE => /fmorph_inj->. apply: (init (p ^^ in_alg L) 1%AS idF0) => //. by apply/polyOver1P; exists p. suff -> : limg idF0 = 1%VS. @@ -1107,7 +1106,9 @@ Lemma sol_setXn n (gT : 'I_n -> finGroupType) (G : forall i, {group gT i}) : Proof. elim: n => [|n IHn] in gT G * => solG; first by rewrite setX0 solvable1. pose gT' (i : 'I_n) := gT (lift ord0 i). -pose f (x : prod_group gT) : prod_group gT' := [ffun i => x (lift ord0 i)]. +pose prod_group_gT := [the finGroupType of {dffun forall i, gT i}]. +pose prod_group_gT' := [the finGroupType of {dffun forall i, gT' i}]. +pose f (x : prod_group_gT) : prod_group_gT' := [ffun i => x (lift ord0 i)]. have fm : morphic (setXn G) f. apply/'forall_implyP => -[a b]; rewrite !inE/=. by move=> /andP[/forallP aG /forallP bG]; apply/eqP/ffunP => i; rewrite !ffunE. @@ -1118,8 +1119,8 @@ have -> : (morphm fm @* setXn G)%g = setXn (fun i => G (lift ord0 i)). move=> /imsetP[/=x]; rewrite inE => /forallP/= xG ->. by move=> i; rewrite morphmE ffunE xG. move=> vG; apply/imsetP. - pose w : prod_group gT := [ffun i : 'I_n.+1 => - match unliftP ord0 i with + pose w := [ffun i : 'I_n.+1 => + match unliftP ord0 i return (gT i) : Type with | UnliftSome j i_eq => ecast i (gT i) (esym i_eq) (v j) | UnliftNone i0 => 1%g end]. @@ -1132,8 +1133,12 @@ have -> : (morphm fm @* setXn G)%g = setXn (fun i => G (lift ord0 i)). rewrite inE; apply/forallP => i. by case: (unliftP ord0 i) => [j|]->; rewrite ?wl ?w0 ?vG. rewrite IHn ?andbT//; last by move=> i; apply: solG. -pose k (x : gT ord0) : prod_group gT := - [ffun i : 'I_n.+1 => if (ord0 =P i) is ReflectT P then ecast i (gT i) P x else 1%g]. +pose k (x : gT ord0) : prod_group_gT := + [ffun i : 'I_n.+1 => + match (ord0 =P i) return (gT i) : Type with + | ReflectT P => ecast i (gT i) P x + | _ => 1%g + end]. have km : morphic (G ord0) k. apply/'forall_implyP => -[a b]; rewrite !inE/= => /andP[aG bG]. apply/eqP/ffunP => i; rewrite !ffunE; case: eqP => //; rewrite ?mulg1//.