Correct and improve implicits and documentation of MatrixGenField

Refactored and completed implicit and scope signatures of constants of
MatrixGenField, the module that contains the construction of an
extension field for an irreducible representation, and for decidability
definitions.
  Completed and corrected some errors in the corresponding header
documentation.

1 files changed, 103 insertions, 71 deletions

diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 0968347..532b382 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -113,7 +113,7 @@ Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly.
 (*                 classically; the socleType structure encapsulates this     *)
 (*                 use of classical logic.                                    *)
 (* DecSocleType rG == a socleType rG structure, for a representation over a   *)
-(*                 decidable field type.                                      *)
+(*                 decidable field type. DecSocleType rG is opaque.           *)
 (*    socle_base W == for W : (sG : socleType), a simple module whose         *)
 (*                 component is W; socle_simple W and socle_module W are      *)
 (*                 proofs that socle_base W is a simple module.               *)
@@ -219,48 +219,66 @@ Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly.
 (*                 H, with nsGH : H <| G, given by Clifford's theorem. More   *)
 (*                 precisely this is a total action of G on socle_sort sH,    *)
 (*                 where sH : socleType (subg_repr rG (normal_sub sGH)).      *)
+(* We build on the MatrixFormula toolkit to define decision procedures for    *)
+(* the reducibility property:                                                 *)
+(*  mxmodule_form rG U == a formula asserting that the interpretation of U is *)
+(*                 a module of the representation rG.                         *)
+(*  mxnonsimple_form rG U == a formula asserting that the interpretation of U *)
+(*                 contains a proper nontrivial rG-module.                    *)
+(*  mxnonsimple_sat rG U <=> mxnonsimple_form rG U is satisfied.              *)
 (* More involved constructions are encapsulated in two Coq submodules:        *)
 (* MatrixGenField == a module that encapsulates the lengthy details of the    *)
 (*                 construction of appropriate extension fields. We assume we *)
-(*                 have an irreducible representation r of a group G, and a   *)
-(*                 non-scalar matrix A that centralises an r(G), as this data *)
+(*                 have an irreducible representation rG of a group G, and a  *)
+(*                 non-scalar matrix A that centralises rG(G), as this data   *)
 (*                 is readily extracted from the Jacobson density theorem. It *)
 (*                 then follows from Schur's lemma that the ring generated by *)
 (*                 A is a field on which the extension of the representation  *)
-(*                 r of G is reducible. Note that this is equivalent to the   *)
+(*                 rG of G is reducible. Note that this is equivalent to the  *)
 (*                 more traditional quotient of the polynomial ring by an     *)
 (*                 irreducible polynomial (the minimal polynomial of A), but  *)
 (*                 much better suited to our needs.                           *)
 (*   Here are the main definitions of MatrixGenField; they all have three     *)
-(* proofs as arguments: rG : mx_repr r G, irrG : mx_irreducible rG, and       *)
-(* cGA : centgmx rG A, which ensure the validity of the construction and      *)
-(* allow us to define Canonical instances (the ~~ is_scalar_mx A assumption   *)
-(* is only needed to prove reducibility).                                     *)
+(* proofs as arguments: (implicit) rG : mx_repr n G, irrG : mx_irreducible rG *)
+(* and cGA : centgmx rG A. These ensure the validity of the construction and  *)
+(* allow us to define Canonical instances; we assume degree_mxminpoly A > 1   *)
+(* (which is equivalent to ~~ is_scalar_mx A) only to prove reducibility.     *)
 (*  + gen_of irrG cGA == the carrier type of the field generated by A. It is  *)
 (*                 at least equipped with a fieldType structure; we also      *)
 (*                 propagate any decFieldType/finFieldType structures on the  *)
 (*                 original field.                                            *)
-(*  + gen irrG cGA == the morphism injecting into gen_of rG irrG cGA.         *)
-(*  + groot irrG cGA == the root of mxminpoly A in the gen_of field.          *)
+(*  + gen irrG cGA == the morphism injecting into gen_of irrG cGA.            *)
+(*  + groot irrG cGA == the root of mxminpoly A in the gen_of irrG cGA field. *)
+(*  + pval x, rVval x, mxval x == the interpretation of x : gen_of irrG cGA   *)
+(*                 as a polynomial, a row vector, and a matrix, respectively. *)
+(*                 Both irrG and cGA are implicit arguments here.             *)
 (*  + gen_repr irrG cGA == an alternative to the field extension              *)
 (*                 representation, which consists in reconsidering the        *)
 (*                 original module as a module over the new gen_of field,     *)
 (*                 thereby DIVIDING the original dimension n by the degree of *)
 (*                 the minimal polynomial of A. This can be simpler than the  *)
-(*                 extension method, and is actually required by the proof    *)
-(*                 that odd groups are p-stable (B & G 6.1-2, and Appendix A) *)
-(*                 but is only applicable if G is the LARGEST group           *)
-(*                 represented by rG (e.g., NOT for B & G 2.6).               *)
-(*  + val_gen/in_gen rG irrG cGA : the bijections from/to the module          *)
-(*                 corresponding to gen_repr.                                 *)
-(*  + rowval_gen rG irrG cGA : the projection of row spaces in the module     *)
-(*                 corresponding to gen_repr to row spaces in 'rV_n.          *)
-(* We build on the MatrixFormula toolkit to define decision procedures for    *)
-(* the reducibility property:                                                 *)
-(*  + mxmodule_form rG U == a formula asserting that the interpretation of U  *)
-(*                 is a module of the representation rG of G via r.           *)
-(*  + mxnonsimple_form rG U == a formula asserting that the interpretation    *)
-(*                 of U contains a proper nontrivial rG-module.               *)
+(*                 extension method, is actually required by the proof that   *)
+(*                 odd groups are p-stable (B & G 6.1-2, and Appendix A), but *)
+(*                 is only applicable if G is the LARGEST group represented   *)
+(*                 by rG (e.g., NOT for B & G 2.6).                           *)
+(*  + gen_dim A == the dimension of gen_repr irrG cGA (only depends on A).    *)
+(*  + in_gen irrG cGA W == the ROWWISE image of a matrix W : 'M[F]_(m, n),    *)
+(*                 i.e., interpreting W as a sequence of m tow vectors,       *)
+(*                 under the bijection from rG to gen_repr irrG cGA.          *)
+(*                 The sequence length m is a maximal implicit argument       *)
+(*                 passed between the explicit argument cGA and W.            *)
+(*  + val_gen W == the ROWWISE image of an 'M[gen_of irrG cGA]_(m, gen_dim A) *)
+(*                 matrix W under the bijection from gen_repr irrG cGA to rG. *)
+(*  + rowval_gen W == the ROWSPACE image of W under the bijection from        *)
+(*                 gen_repr irrG cGA to rG, i.e., a 'M[F]_n matrix whose row  *)
+(*                 space is the image of the row space of W.                  *)
+(*                 This is the A-ideal generated by val_gen W.                *)
+(*  + gen_sat e f <=> f : GRing.formula (gen_of irrG cGA) is satisfied in     *)
+(*                 environment e : seq (gen_of irrG cGA), provided F has a    *)
+(*                 decFieldType structure.                                    *)
+(*  + gen_env e, gen_term t, gen_form f == interpretations of environments,   *)
+(*                 terms, and RING formulas over gen_of irrG cGA as row       *)
+(*                 vector formulae, used to construct gen_sat.                *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -4873,6 +4891,8 @@ Qed.
 
 End DecideRed.
 
+Prenex Implicits mxmodule_form mxnonsimple_form mxnonsimple_sat.
+
 (* Change of representation field (by tensoring) *)
 Section ChangeOfField.
   
@@ -5029,7 +5049,18 @@ End ChangeOfField.
 (* minimal polynomial pA of A (of degree d).                                  *)
 (* The details of the construction of FA are encapsulated in a submodule.     *)
 Module Import MatrixGenField.
-  
+
+(* The type definition must come before the main section so that the Bind     *)
+(* Scope directive applies to all lemmas and definition discharged at the     *)
+(* of the section.                                                            *)
+Record gen_of {F : fieldType} {gT : finGroupType} {G : {group gT}} {n' : nat}
+              {rG : mx_representation F G n'.+1} {A : 'M[F]_n'.+1}
+              (irrG : mx_irreducible rG) (cGA : centgmx rG A) :=
+   Gen {rVval : 'rV[F]_(degree_mxminpoly A)}.
+
+Local Arguments rVval {F gT G%G n'%N rG A%R irrG cGA} x%R : rename.
+Bind Scope ring_scope with gen_of.
+ 
 Section GenField.
 
 Variables (F : fieldType) (gT : finGroupType) (G : {group gT}) (n' : nat).
@@ -5042,15 +5073,12 @@ Local Notation pA := (mxminpoly A).
 Let d_gt0 := mxminpoly_nonconstant A.
 Local Notation irr := mx_irreducible.
 
-Record gen_of (irrG : irr rG) (cGA : centgmx rG A) := Gen {rVval : 'rV[F]_d}.
-Prenex Implicits rVval.
-
 Hypotheses (irrG : irr rG) (cGA : centgmx rG A).
 
 Notation FA := (gen_of irrG cGA).
 Let inFA := Gen irrG cGA.
 
-Canonical gen_subType := Eval hnf in [newType for @rVval irrG cGA].
+Canonical gen_subType := Eval hnf in [newType for rVval : FA -> 'rV_d].
 Definition gen_eqMixin := Eval hnf in [eqMixin of FA by <:].
 Canonical gen_eqType := Eval hnf in EqType FA gen_eqMixin.
 Definition gen_choiceMixin := [choiceMixin of FA by <:].
@@ -5181,7 +5209,8 @@ Lemma gen_invr0 : genV 0 = 0.
 Proof. by apply: mxval_inj; rewrite mxval_genV !mxval0 -{2}invr0. Qed.
 
 Definition gen_unitRingMixin := FieldUnitMixin gen_mulVr gen_invr0.
-Canonical gen_unitRingType := Eval hnf in UnitRingType FA gen_unitRingMixin.
+Canonical gen_unitRingType :=
+  Eval hnf in UnitRingType FA gen_unitRingMixin.
 Canonical gen_comUnitRingType := Eval hnf in [comUnitRingType of FA].
 Definition gen_fieldMixin :=
   @FieldMixin _ _ _ _ : GRing.Field.mixin_of gen_unitRingType.
@@ -5261,37 +5290,37 @@ Qed.
 (* remain unchanged -- because we're restricting ourselves to row matrices;   *)
 (* we have to use explicit bijections to convert between the two views.       *)
 
-Definition subbase m (B : 'rV_m) : 'M_(m * d, n) :=
+Definition subbase nA (B : 'rV_nA) : 'M_(nA * d, n) :=
   \matrix_ik mxvec (\matrix_(i, k) (row (B 0 i) (A ^+ k))) 0 ik.
 
-Lemma gen_dim_ex_proof : exists m, [exists B : 'rV_m, row_free (subbase B)].
+Lemma gen_dim_ex_proof : exists nA, [exists B : 'rV_nA, row_free (subbase B)].
 Proof. by exists 0%N; apply/existsP; exists 0. Qed.
 
-Lemma gen_dim_ub_proof m :
-  [exists B : 'rV_m, row_free (subbase B)] -> (m <= n)%N.
+Lemma gen_dim_ub_proof nA :
+  [exists B : 'rV_nA, row_free (subbase B)] -> (nA <= n)%N.
 Proof.
-case/existsP=> B /eqnP def_md.
-by rewrite (leq_trans _ (rank_leq_col (subbase B))) // def_md leq_pmulr.
+case/existsP=> B /eqnP def_nAd.
+by rewrite (leq_trans _ (rank_leq_col (subbase B))) // def_nAd leq_pmulr.
 Qed.
 
 Definition gen_dim := ex_maxn gen_dim_ex_proof gen_dim_ub_proof.
-Notation m := gen_dim.
+Notation nA := gen_dim.
 
-Definition gen_base : 'rV_m := odflt 0 [pick B | row_free (subbase B)].
+Definition gen_base : 'rV_nA := odflt 0 [pick B | row_free (subbase B)].
 Definition base := subbase gen_base.
 
 Lemma base_free : row_free base.
 Proof.
-rewrite /base /gen_base /m; case: pickP => //; case: ex_maxnP => m_max.
+rewrite /base /gen_base /nA; case: pickP => //; case: ex_maxnP => nA_max.
 by case/existsP=> B Bfree _ no_free; rewrite no_free in Bfree.
 Qed.
 
 Lemma base_full : row_full base.
 Proof.
-rewrite /row_full (eqnP base_free) /m; case: ex_maxnP => m.
-case/existsP=> /= B /eqnP Bfree m_max; rewrite -Bfree eqn_leq rank_leq_col.
+rewrite /row_full (eqnP base_free) /nA; case: ex_maxnP => nA.
+case/existsP=> /= B /eqnP Bfree nA_max; rewrite -Bfree eqn_leq rank_leq_col.
 rewrite -{1}(mxrank1 F n) mxrankS //; apply/row_subP=> j; set u := row _ _.
-move/implyP: {m_max}(m_max m.+1); rewrite ltnn implybF.
+move/implyP: {nA_max}(nA_max nA.+1); rewrite ltnn implybF.
 apply: contraR => nBj; apply/existsP.
 exists (row_mx (const_mx j : 'M_1) B); rewrite -row_leq_rank.
 pose Bj := Ad *m lin1_mx (mulmx u \o vec_mx).
@@ -5303,7 +5332,7 @@ have rBj: \rank Bj = d.
   rewrite mul0mx /= -mulmxA -mxvalM divff // mxval1 mulmx1.
   by move/rowP/(_ j)/eqP; rewrite !mxE !eqxx oner_eq0.
 rewrite {1}mulSn -Bfree -{1}rBj {rBj} -mxrank_disjoint_sum.
-  rewrite mxrankS // addsmx_sub -[m.+1]/(1 + m)%N; apply/andP; split.
+  rewrite mxrankS // addsmx_sub -[nA.+1]/(1 + nA)%N; apply/andP; split.
     apply/row_subP=> k; rewrite row_mul mul_rV_lin1 /=.
     apply: eq_row_sub (mxvec_index (lshift _ 0) k)  _.
     by rewrite !rowK mxvecK mxvecE mxE row_mxEl mxE -row_mul mul1mx.
@@ -5325,20 +5354,20 @@ rewrite !linearZ scalemx_sub //= rowK mxvecK -rowE.
 by apply: eq_row_sub (mxvec_index i k) _; rewrite rowK mxvecE mxE.
 Qed.
 
-Lemma gen_dim_factor : (m * d)%N = n.
+Lemma gen_dim_factor : (nA * d)%N = n.
 Proof. by rewrite -(eqnP base_free) (eqnP base_full). Qed.
 
-Lemma gen_dim_gt0 : m > 0.
+Lemma gen_dim_gt0 : nA > 0.
 Proof. by case: posnP gen_dim_factor => // ->. Qed.
 
 Section Bijection.
 
-Variable m1 : nat.
+Variable m : nat.
 
-Definition in_gen (W : 'M[F]_(m1, n)) : 'M[FA]_(m1, m) :=
+Definition in_gen (W : 'M[F]_(m, n)) : 'M[FA]_(m, nA) :=
   \matrix_(i, j) inFA (row j (vec_mx (row i W *m pinvmx base))).
 
-Definition val_gen (W : 'M[FA]_(m1, m)) : 'M[F]_(m1, n) :=
+Definition val_gen (W : 'M[FA]_(m, nA)) : 'M[F]_(m, n) :=
   \matrix_i (mxvec (\matrix_j val (W i j)) *m base).
 
 Lemma in_genK : cancel in_gen val_gen.
@@ -5394,24 +5423,24 @@ End Bijection.
 
 Prenex Implicits val_genK in_genK.
 
-Lemma val_gen_rV (w : 'rV_m) :
+Lemma val_gen_rV (w : 'rV_nA) :
   val_gen w = mxvec (\matrix_j val (w 0 j)) *m base.
 Proof. by apply/rowP=> j; rewrite mxE. Qed.
 
 Section Bijection2.
 
-Variable m1 : nat.
+Variable m : nat.
 
-Lemma val_gen_row W (i : 'I_m1) : val_gen (row i W) = row i (val_gen W).
+Lemma val_gen_row W (i : 'I_m) : val_gen (row i W) = row i (val_gen W).
 Proof.
 rewrite val_gen_rV rowK; congr (mxvec _ *m _).
 by apply/matrixP=> j k; rewrite !mxE.
 Qed.
 
-Lemma in_gen_row W (i : 'I_m1) : in_gen (row i W) = row i (in_gen W).
+Lemma in_gen_row W (i : 'I_m) : in_gen (row i W) = row i (in_gen W).
 Proof. by apply: (canLR val_genK); rewrite val_gen_row in_genK. Qed.
 
-Lemma row_gen_sum_mxval W (i : 'I_m1) :
+Lemma row_gen_sum_mxval W (i : 'I_m) :
   row i (val_gen W) = \sum_j row (gen_base 0 j) (mxval (W i j)).
 Proof.
 rewrite -val_gen_row [row i W]row_sum_delta val_gen_sum.
@@ -5431,7 +5460,7 @@ apply/row_matrixP=> j'; rewrite rowK !mxE mulr_natr rowE mul_delta_mx_cond.
 by rewrite !mulrb (fun_if rVval).
 Qed.
 
-Lemma val_genZ x : {morph @val_gen m1 : W / x *: W >-> W *m mxval x}.
+Lemma val_genZ x : {morph @val_gen m : W / x *: W >-> W *m mxval x}.
 Proof.
 move=> W; apply/row_matrixP=> i; rewrite row_mul !row_gen_sum_mxval.
 by rewrite mulmx_suml; apply: eq_bigr => j _; rewrite mxE mulrC mxvalM row_mul.
@@ -5502,11 +5531,11 @@ rewrite -[rfix_mx rGA H]val_genK; apply: submx_in_gen.
 by apply/rfix_mxP=> g Hg; rewrite -val_genJ ?rfix_mx_id ?sHG.
 Qed.
 
-Definition rowval_gen m1 U :=
+Definition rowval_gen m U :=
   <<\matrix_ik
-      mxvec (\matrix_(i < m1, k < d) (row i (val_gen U) *m A ^+ k)) 0 ik>>%MS.
+      mxvec (\matrix_(i < m, k < d) (row i (val_gen U) *m A ^+ k)) 0 ik>>%MS.
 
-Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, m)) :
+Lemma submx_rowval_gen m1 m2 (U : 'M_(m1, n)) (V : 'M_(m2, nA)) :
   (U <= rowval_gen V)%MS = (in_gen U <= V)%MS.
 Proof.
 rewrite genmxE; apply/idP/idP=> sUV.
@@ -5523,40 +5552,40 @@ rewrite !linearZ scalemx_sub {u}//= rowK mxvecK val_gen_row.
 by apply: (eq_row_sub (mxvec_index i k)); rewrite rowK mxvecE mxE.
 Qed.
 
-Lemma rowval_genK m1 (U : 'M_(m1,  m)) : (in_gen (rowval_gen U) :=: U)%MS.
+Lemma rowval_genK m (U : 'M_(m,  nA)) : (in_gen (rowval_gen U) :=: U)%MS.
 Proof.
 apply/eqmxP; rewrite -submx_rowval_gen submx_refl /=.
 by rewrite -{1}[U]val_genK submx_in_gen // submx_rowval_gen val_genK.
 Qed.
 
-Lemma rowval_gen_stable m1 (U : 'M_(m1, m)) :
+Lemma rowval_gen_stable m (U : 'M_(m, nA)) :
   (rowval_gen U *m A <= rowval_gen U)%MS.
 Proof.
 rewrite -[A]mxval_groot -{1}[_ U]in_genK -val_genZ.
 by rewrite submx_rowval_gen val_genK scalemx_sub // rowval_genK.
 Qed.
 
-Lemma rstab_in_gen m1 (U : 'M_(m1, n)) : rstab rGA (in_gen U) = rstab rG U.
+Lemma rstab_in_gen m (U : 'M_(m, n)) : rstab rGA (in_gen U) = rstab rG U.
 Proof.
 apply/setP=> x; rewrite !inE; case Gx: (x \in G) => //=.
 by rewrite -in_genJ // (inj_eq (can_inj in_genK)).
 Qed.
 
-Lemma rstabs_in_gen m1 (U : 'M_(m1, n)) :
+Lemma rstabs_in_gen m (U : 'M_(m, n)) :
   rstabs rG U \subset rstabs rGA (in_gen U).
 Proof.
 apply/subsetP=> x; rewrite !inE => /andP[Gx nUx].
 by rewrite -in_genJ Gx // submx_in_gen.
 Qed.
 
-Lemma rstabs_rowval_gen m1 (U : 'M_(m1, m)) :
+Lemma rstabs_rowval_gen m (U : 'M_(m, nA)) :
   rstabs rG (rowval_gen U) = rstabs rGA U.
 Proof.
 apply/setP=> x; rewrite !inE; case Gx: (x \in G) => //=.
 by rewrite submx_rowval_gen in_genJ // (eqmxMr _ (rowval_genK U)).
 Qed.
 
-Lemma mxmodule_rowval_gen m1 (U : 'M_(m1, m)) :
+Lemma mxmodule_rowval_gen m (U : 'M_(m, nA)) :
   mxmodule rG (rowval_gen U) = mxmodule rGA U.
 Proof. by rewrite /mxmodule rstabs_rowval_gen. Qed.
 
@@ -5582,11 +5611,6 @@ Proof. by rewrite /mx_faithful rker_gen. Qed.
 
 End GenField.
 
-Arguments in_gen {F gT G n' rG A} irrG cGA {m1} W.
-Arguments val_gen {F gT G n' rG A} irrG cGA {m1} W.
-Arguments in_genK {F gT G n' rG A} irrG cGA {m1} W : rename.
-Arguments val_genK {F gT G n' rG A} irrG cGA {m1} W : rename.
-
 Section DecideGenField.
 
 Import MatrixFormula.
@@ -5674,10 +5698,8 @@ elim: n1 => [|n1 IHn1] /=; first by rewrite eval_mx_term.
 by rewrite eval_mulT exprS IH1 IHn1.
 Qed.
 
-(* WARNING: Coq will core dump if the Notation Bool is used in the match *)
-(* pattern here.                                                         *)
 Fixpoint gen_form f := match f with
-| GRing.Bool b => Bool b
+| Bool b => Bool b
 | t1 == t2 => mxrank_form 0 (gen_term (t1 - t2))
 | GRing.Unit t1 => mxrank_form 1 (gen_term t1)
 | f1 /\ f2 => gen_form f1 /\ gen_form f2
@@ -5764,6 +5786,16 @@ End FiniteGenField.
 
 End MatrixGenField.
 
+Bind Scope ring_scope with gen_of.
+Arguments rVval {F gT G%G n'%N rG A%R irrG cGA} x%R : rename.
+Prenex Implicits gen_of Gen rVval pval mxval gen groot.
+Arguments subbase {F n'} A {nA}.
+Prenex Implicits gen_dim gen_base base val_gen gen_mx rowval_gen.
+Arguments in_gen {F gT G n' rG A} irrG cGA {m} W.
+Arguments in_genK {F gT G n' rG A} irrG cGA {m} W : rename.
+Arguments val_genK {F gT G n' rG A irrG cGA m} W : rename.
+Prenex Implicits gen_env gen_term gen_form gen_sat.
+
 Canonical gen_subType.
 Canonical gen_eqType.
 Canonical gen_choiceType.