diff options
34 files changed, 296 insertions, 178 deletions
@@ -24,7 +24,20 @@ from eqtype.v. They were already in ssrfun.v. * Specialized `bool_irrelevance` so that the statement reflects - the name + the name. + + * Changed the shape of the type of FieldMixin to allow one-line + in-proof definition of bespoke fieldType structure. + + * Refactored and extended Arguments directives to provide more + comprehensive signature information. + + * Added maximal implicits to reflection, injectivity and cancellation + lemmas so that they are easier to pass to combinator lemmas such as + sameP, inj_eq or canLR. + + * Added reindex_inj s shorthand for reindexing a bigop with a + permutation s. * Added lemma `eqmxMunitP`: two matrices with the same shape represent the same subspace iff they differ only by a change of diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 2f5e844..1da8313 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -714,7 +714,7 @@ rewrite mul1n; apply/dvdn_biggcdP/(all_nthP 0)=> a_dv_p i ltip /=. exact: a_dv_p. Qed. -Lemma map_poly_divzK a p : +Lemma map_poly_divzK {a} p : p \is a polyOver (dvdz a) -> a *: map_poly (divz^~ a) p = p. Proof. move/polyOverP=> a_dv_p; apply/polyP=> i. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 3fe8d01..3b12802 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -916,9 +916,10 @@ Arguments row_mxA {R m n1 n2 n3 A1 A2 A3}. Arguments col_mxA {R m1 m2 m3 n A1 A2 A3}. Arguments block_mxA {R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33}. -Prenex Implicits castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx. +Prenex Implicits castmx trmx trmxK lsubmx rsubmx usubmx dsubmx row_mx col_mx. Prenex Implicits block_mx ulsubmx ursubmx dlsubmx drsubmx. Prenex Implicits mxvec vec_mx mxvec_indexP mxvecK vec_mxK. +Arguments trmx_inj {R m n} [A1 A2] eqA12t : rename. Notation "A ^T" := (trmx A) : ring_scope. @@ -1031,6 +1032,8 @@ End Block. End MapMatrix. +Arguments map_mx {aT rT} f {m n} A. + (*****************************************************************************) (********************* Matrix Zmodule (additive) structure *******************) (*****************************************************************************) @@ -1180,9 +1183,7 @@ Qed. Lemma col_mx_eq0 (m1 m2 n : nat) (A1 : 'M_(m1, n)) (A2 : 'M_(m2, n)): (col_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0). -Proof. -by rewrite -) !trmx0 tr_col_mx row_mx_eq0. -Qed. +Proof. by rewrite - !trmx0 tr_col_mx row_mx_eq0. Qed. Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) : (block_mx Aul Aur Adl Adr == 0) = @@ -1332,29 +1333,29 @@ Proof. by rewrite {1}[u]matrix_sum_delta big_ord1. Qed. Lemma delta_mx_lshift m n1 n2 i j : delta_mx i (lshift n2 j) = row_mx (delta_mx i j) 0 :> 'M_(m, n1 + n2). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inl _ _)); case: split => ?; rewrite mxE ?andbF. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inl _ _)). +by case: split => ?; rewrite mxE ?andbF. Qed. Lemma delta_mx_rshift m n1 n2 i j : delta_mx i (rshift n1 j) = row_mx 0 (delta_mx i j) :> 'M_(m, n1 + n2). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inr _ _)); case: split => ?; rewrite mxE ?andbF. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inr _ _)). +by case: split => ?; rewrite mxE ?andbF. Qed. Lemma delta_mx_ushift m1 m2 n i j : delta_mx (lshift m2 i) j = col_mx (delta_mx i j) 0 :> 'M_(m1 + m2, n). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inl _ _)); case: split => ?; rewrite mxE. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inl _ _)). +by case: split => ?; rewrite mxE. Qed. Lemma delta_mx_dshift m1 m2 n i j : delta_mx (rshift m1 i) j = col_mx 0 (delta_mx i j) :> 'M_(m1 + m2, n). Proof. -apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)). -by rewrite (unsplitK (inr _ _)); case: split => ?; rewrite mxE. +apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inr _ _)). +by case: split => ?; rewrite mxE. Qed. Lemma vec_mx_delta m n i j : @@ -1628,7 +1629,7 @@ Qed. Lemma mul_col_perm m n p s (A : 'M_(m, n)) (B : 'M_(n, p)) : col_perm s A *m B = A *m row_perm s^-1 B. Proof. -apply/matrixP=> i k; rewrite !mxE (reindex_inj (@perm_inj _ s^-1)). +apply/matrixP=> i k; rewrite !mxE (reindex_perm s^-1). by apply: eq_bigr => j _ /=; rewrite !mxE permKV. Qed. @@ -2013,7 +2014,7 @@ Lemma lift0_mx_perm s : lift0_mx (perm_mx s) = perm_mx (lift0_perm s). Proof. apply/matrixP=> /= i j; rewrite !mxE split1 /=; case: unliftP => [i'|] -> /=. rewrite lift0_perm_lift !mxE split1 /=. - by case: unliftP => [j'|] ->; rewrite ?(inj_eq (@lift_inj _ _)) /= !mxE. + by case: unliftP => [j'|] ->; rewrite ?(inj_eq (lift_inj _)) /= !mxE. rewrite lift0_perm0 !mxE split1 /=. by case: unliftP => [j'|] ->; rewrite /= mxE. Qed. @@ -2142,7 +2143,7 @@ Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n. Proof. by rewrite map_mx_sub map_mx1 map_pid_mx. Qed. Lemma map_mx_is_multiplicative n' (n := n'.+1) : - multiplicative ((map_mx f) n n). + multiplicative (map_mx f : 'M_n -> 'M_n). Proof. by split; [apply: map_mxM | apply: map_mx1]. Qed. Canonical map_mx_rmorphism n' := AddRMorphism (map_mx_is_multiplicative n'). @@ -2291,14 +2292,14 @@ rewrite [\det A](bigID (@odd_perm _)) /=. apply: canLR (subrK _) _; rewrite add0r -sumrN. rewrite (reindex_inj (mulgI t)); apply: eq_big => //= s. rewrite oddMt => /negPf->; rewrite mulN1r mul1r; congr (- _). -rewrite (reindex_inj (@perm_inj _ t)); apply: eq_bigr => /= i _. +rewrite (reindex_perm t); apply: eq_bigr => /= i _. by rewrite permM tpermK /t; case: tpermP => // ->; rewrite eqA12. Qed. Lemma det_tr n (A : 'M[R]_n) : \det A^T = \det A. Proof. -rewrite [\det A^T](reindex_inj (@invg_inj _)) /=. -apply: eq_bigr => s _ /=; rewrite !odd_permV (reindex_inj (@perm_inj _ s)) /=. +rewrite [\det A^T](reindex_inj invg_inj) /=. +apply: eq_bigr => s _ /=; rewrite !odd_permV (reindex_perm s) /=. by congr (_ * _); apply: eq_bigr => i _; rewrite mxE permK. Qed. @@ -2349,7 +2350,7 @@ rewrite (bigID (fun f : F => injectiveb f)) /= addrC big1 ?add0r => [|f Uf]. rewrite (reindex_inj (mulgI s)); apply: eq_bigr => t _ /=. rewrite big_split /= mulrA mulrCA mulrA mulrCA mulrA. rewrite -signr_addb odd_permM !pvalE; congr (_ * _); symmetry. - by rewrite (reindex_inj (@perm_inj _ s)); apply: eq_bigr => i; rewrite permM. + by rewrite (reindex_perm s); apply: eq_bigr => i; rewrite permM. transitivity (\det (\matrix_(i, j) B (f i) j) * \prod_i A i (f i)). rewrite mulrC big_distrr /=; apply: eq_bigr => s _. rewrite mulrCA big_split //=; congr (_ * (_ * _)). @@ -2382,7 +2383,7 @@ rewrite (reindex (lift_perm i0 j0)); last first. pose ulsf i (s : 'S_n.+1) k := odflt k (unlift (s i) (s (lift i k))). have ulsfK i (s : 'S_n.+1) k: lift (s i) (ulsf i s k) = s (lift i k). rewrite /ulsf; have:= neq_lift i k. - by rewrite -(inj_eq (@perm_inj _ s)) => /unlift_some[] ? ? ->. + by rewrite -(can_eq (permK s)) => /unlift_some[] ? ? ->. have inj_ulsf: injective (ulsf i0 _). move=> s; apply: can_inj (ulsf (s i0) s^-1%g) _ => k'. by rewrite {1}/ulsf ulsfK !permK liftK. @@ -2497,8 +2498,8 @@ Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed. End ComMatrix. -Arguments lin_mul_row {R m n}. -Arguments lin_mulmx {R m n p}. +Arguments lin_mul_row {R m n} u. +Arguments lin_mulmx {R m n p} A. Canonical matrix_finAlgType (R : finComRingType) n' := [finAlgType R of 'M[R]_n'.+1]. @@ -2642,7 +2643,7 @@ Qed. End MatrixInv. -Prenex Implicits unitmx invmx. +Prenex Implicits unitmx invmx invmxK. Canonical matrix_countUnitRingType (R : countComUnitRingType) n := [countUnitRingType of 'M[R]_n.+1]. @@ -2790,7 +2791,7 @@ Section MapFieldMatrix. Variables (aF : fieldType) (rF : comUnitRingType) (f : {rmorphism aF -> rF}). Local Notation "A ^f" := (map_mx f A) : ring_scope. -Lemma map_mx_inj m n : injective ((map_mx f) m n). +Lemma map_mx_inj {m n} : injective (map_mx f : 'M_(m, n) -> 'M_(m, n)). Proof. move=> A B eq_AB; apply/matrixP=> i j. by move/matrixP/(_ i j): eq_AB; rewrite !mxE; apply: fmorph_inj. @@ -2811,7 +2812,7 @@ Proof. exact: map_unitmx. Qed. Lemma map_invmx n (A : 'M_n) : (invmx A)^f = invmx A^f. Proof. -rewrite /invmx map_unitmx (fun_if ((map_mx f) n n)). +rewrite /invmx map_unitmx (fun_if (map_mx f)). by rewrite map_mxZ map_mx_adj det_map_mx fmorphV. Qed. @@ -2819,10 +2820,12 @@ Lemma map_mx_inv n' (A : 'M_n'.+1) : A^-1^f = A^f^-1. Proof. exact: map_invmx. Qed. Lemma map_mx_eq0 m n (A : 'M_(m, n)) : (A^f == 0) = (A == 0). -Proof. by rewrite -(inj_eq (@map_mx_inj m n)) raddf0. Qed. +Proof. by rewrite -(inj_eq map_mx_inj) raddf0. Qed. End MapFieldMatrix. +Arguments map_mx_inj {aF rF f m n} [A1 A2] eqA12f : rename. + (*****************************************************************************) (****************************** LUP decomposion ******************************) (*****************************************************************************) diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index f679828..710adc6 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -29,7 +29,7 @@ Require Import poly polydiv. (* char_poly A == the characteristic polynomial of A. *) (* char_poly_mx A == a matrix whose determinant is char_poly A. *) (* companionmx p == a matrix whose char_poly is p *) -(* mxminpoly A == the minimal polynomial of A, i.e., the smallest monic *) +(* mxminpoly A == the minimal polynomial of A, i.e., the smallest monic *) (* polynomial that annihilates A (A must be nontrivial). *) (* degree_mxminpoly A == the (positive) degree of mxminpoly A. *) (* mx_inv_horner A == the inverse of horner_mx A for polynomials of degree *) @@ -116,8 +116,9 @@ Canonical rVpoly_linear := Linear rVpoly_is_linear. End RowPoly. +Prenex Implicits rVpoly rVpolyK. Arguments poly_rV {R d}. -Prenex Implicits rVpoly. +Arguments poly_rV_K {R d} [p] le_p_d. Section Resultant. @@ -140,6 +141,8 @@ Definition resultant := \det Sylvester_mx. End Resultant. +Prenex Implicits Sylvester_mx resultant. + Lemma resultant_in_ideal (R : comRingType) (p q : {poly R}) : size p > 1 -> size q > 1 -> {uv : {poly R} * {poly R} | size uv.1 < size q /\ size uv.2 < size p @@ -224,7 +227,7 @@ apply/det0P/idP=> [[uv nz_uv] | r_nonC]. rewrite addrC addr_eq0 => /eqP vq_up. have nz_v: v != 0. apply: contraNneq nz_uv => v0; apply/eqP. - congr row_mx; apply: (can_inj (@rVpolyK _ _)); rewrite linear0 // -/u. + congr row_mx; apply: (can_inj rVpolyK); rewrite linear0 // -/u. by apply: contra_eq vq_up; rewrite v0 mul0r -addr_eq0 add0r => /mulf_neq0->. have r_nz: r != 0 := dvdpN0 r_p p_nz. have /dvdpP [[c w] /= nz_c wv]: v %| m by rewrite dvdp_gcd !dvdp_mulr. @@ -298,6 +301,8 @@ Qed. End HornerMx. +Prenex Implicits horner_mx powers_mx. + Section CharPoly. Variables (R : ringType) (n : nat) (A : 'M[R]_n). @@ -330,7 +335,7 @@ apply: leq_trans (_ : #|[pred j | s j == j]|.+1 <= n.-1). by rewrite sub0r size_opp size_polyC leq_b1. rewrite -{8}[n]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS. apply: subset_leq_card; apply/subsetP=> j; move/(_ =P j)=> fix_j. -rewrite !inE -{1}fix_j (inj_eq (@perm_inj _ s)) orbb. +rewrite !inE -{1}fix_j (inj_eq perm_inj) orbb. by apply: contraNneq nfix_i => <-; rewrite fix_j. Qed. @@ -373,6 +378,8 @@ Qed. End CharPoly. +Prenex Implicits char_poly_mx char_poly. + Lemma mx_poly_ring_isom (R : ringType) n' (n := n'.+1) : exists phi : {rmorphism 'M[{poly R}]_n -> {poly 'M[R]_n}}, [/\ bijective phi, @@ -431,13 +438,11 @@ rewrite (big_morph _ (fun p q => hornerM p q a) (hornerC 1 a)). by apply: eq_bigr => i _; rewrite !mxE !(hornerE, hornerMn). Qed. -Section Companion. - -Definition companionmx (R : ringType) (p : seq R) (d := (size p).-1) := +Definition companionmx {R : ringType} (p : seq R) (d := (size p).-1) := \matrix_(i < d, j < d) if (i == d.-1 :> nat) then - p`_j else (i.+1 == j :> nat)%:R. -Lemma companionmxK (R : comRingType) (p : {poly R}) : +Lemma companionmxK {R : comRingType} (p : {poly R}) : p \is monic -> char_poly (companionmx p) = p. Proof. pose D n : 'M[{poly R}]_n := \matrix_(i, j) @@ -487,8 +492,6 @@ rewrite ltn_eqF ?big1 ?addr0 1?eq_sym //; last first. by move=> k /negPf ki_eqF; rewrite !mxE eqxx ki_eqF mul0r. Qed. -End Companion. - Section MinPoly. Variables (F : fieldType) (n' : nat). @@ -601,10 +604,10 @@ Qed. Lemma mxminpoly_min p : horner_mx A p = 0 -> p_A %| p. Proof. by move=> pA0; rewrite /dvdp -horner_mxK pA0 mx_inv_horner0. Qed. -Lemma horner_rVpoly_inj : @injective 'M_n 'rV_d (horner_mx A \o rVpoly). +Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d -> 'M_n). Proof. -apply: can_inj (poly_rV \o mx_inv_horner) _ => u. -by rewrite /= horner_rVpolyK rVpolyK. +apply: can_inj (poly_rV \o mx_inv_horner) _ => u /=. +by rewrite horner_rVpolyK rVpolyK. Qed. Lemma mxminpoly_linear_is_scalar : (d <= 1) = is_scalar_mx A. @@ -639,6 +642,11 @@ Qed. End MinPoly. +Prenex Implicits degree_mxminpoly mxminpoly mx_inv_horner. + +Arguments mx_inv_hornerK {F n' A} [B] AnB. +Arguments horner_rVpoly_inj {F n' A} [u1 u2] eq_u12A : rename. + (* Parametricity. *) Section MapRingMatrix. @@ -1044,9 +1052,9 @@ Local Notation holds := GRing.holds. Local Notation qf_form := GRing.qf_form. Local Notation qf_eval := GRing.qf_eval. -Definition eval_mx (e : seq F) := map_mx (eval e). +Definition eval_mx (e : seq F) := @map_mx term F (eval e). -Definition mx_term := map_mx (@GRing.Const F). +Definition mx_term := @map_mx F term GRing.Const. Lemma eval_mx_term e m n (A : 'M_(m, n)) : eval_mx e (mx_term A) = A. Proof. by apply/matrixP=> i j; rewrite !mxE. Qed. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 929c313..702dfc4 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -142,8 +142,8 @@ Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p`_i. End Polynomial. -(* We need to break off the section here to let the argument scope *) -(* directives take effect. *) +(* We need to break off the section here to let the Bind Scope directives *) +(* take effect. *) Bind Scope ring_scope with poly_of. Bind Scope ring_scope with polynomial. Arguments polyseq {R} p%R. @@ -1675,7 +1675,7 @@ Qed. End PolynomialTheory. -Prenex Implicits polyC Poly lead_coef root horner polyOver. +Prenex Implicits polyC polyCK Poly polyseqK lead_coef root horner polyOver. Arguments monic {R}. Notation "\poly_ ( i < n ) E" := (poly n (fun i => E)) : ring_scope. Notation "c %:P" := (polyC c) : ring_scope. @@ -1694,6 +1694,7 @@ Arguments rootPf {R p x}. Arguments rootPt {R p x}. Arguments unity_rootP {R n z}. Arguments polyOverP {R S0 addS kS p}. +Arguments polyC_inj {R} [x1 x2] eq_x12P. Canonical polynomial_countZmodType (R : countRingType) := [countZmodType of polynomial R]. @@ -1947,7 +1948,7 @@ Definition comp_poly q p := p^:P.[q]. Local Notation "p \Po q" := (comp_poly q p) : ring_scope. Lemma size_map_polyC p : size p^:P = size p. -Proof. exact: size_map_inj_poly (@polyC_inj R) _ _. Qed. +Proof. exact/(size_map_inj_poly polyC_inj). Qed. Lemma map_polyC_eq0 p : (p^:P == 0) = (p == 0). Proof. by rewrite -!size_poly_eq0 size_map_polyC. Qed. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 40a1f83..47cee1f 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -875,6 +875,7 @@ End ZmoduleTheory. Arguments addrI {V} y [x1 x2]. Arguments addIr {V} x [x1 x2]. +Arguments opprK {V}. Arguments oppr_inj {V} [x1 x2]. Module Ring. @@ -3031,6 +3032,7 @@ End ClosedPredicates. End UnitRingTheory. +Arguments invrK {R}. Arguments invr_inj {R} [x1 x2]. Section UnitRingMorphism. @@ -5370,7 +5372,8 @@ Arguments addrI {V} y [x1 x2]. Arguments addIr {V} x [x1 x2]. Arguments subrI {V} y [x1 x2]. Arguments subIr {V} x [x1 x2]. -Definition opprK := opprK. +Definition opprK := @opprK. +Arguments opprK {V}. Definition oppr_inj := @oppr_inj. Arguments oppr_inj {V} [x1 x2]. Definition oppr0 := oppr0. @@ -5554,7 +5557,8 @@ Definition divIr := divIr. Definition telescope_prodr := telescope_prodr. Definition commrV := commrV. Definition unitrE := unitrE. -Definition invrK := invrK. +Definition invrK := @invrK. +Arguments invrK {R}. Definition invr_inj := @invr_inj. Arguments invr_inj {R} [x1 x2]. Definition unitrV := unitrV. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index b734ad7..e6b0264 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -290,7 +290,7 @@ Lemma mulz_addl : left_distributive mulz (+%R). Proof. move=> x y z; elim: z=> [|n|n]; first by rewrite !(mul0z,mulzC). by rewrite !mulzS=> ->; rewrite !addrA [X in X + _]addrAC. -rewrite !mulzN !mulzS -!opprD=> /(inv_inj (@opprK _))->. +rewrite !mulzN !mulzS -!opprD=> /oppr_inj->. by rewrite !addrA [X in X + _]addrAC. Qed. @@ -330,22 +330,21 @@ Lemma mulVz : {in unitz, left_inverse 1%R invz *%R}. Proof. by move=> n /pred2P[] ->. Qed. Lemma mulzn_eq1 m (n : nat) : (m * n == 1) = (m == 1) && (n == 1%N). -Proof. by case: m=> m /=; [rewrite -PoszM [_==_]muln_eq1 | case: n]. Qed. +Proof. by case: m => m /=; [rewrite -PoszM [_==_]muln_eq1 | case: n]. Qed. Lemma unitzPl m n : n * m = 1 -> m \is a unitz. Proof. -case: m => m; move/eqP; rewrite qualifE. -* by rewrite mulzn_eq1; case/andP=> _; move/eqP->. -* by rewrite NegzE intS mulrN -mulNr mulzn_eq1; case/andP=> _. +rewrite qualifE => /eqP. +by case: m => m; rewrite ?NegzE ?mulrN -?mulNr mulzn_eq1 => /andP[_ /eqP->]. Qed. -Lemma invz_out : {in [predC unitz], invz =1 id}. +Lemma invz_out : {in [predC unitz], invz =1 id}. Proof. exact. Qed. Lemma idomain_axiomz m n : m * n = 0 -> (m == 0) || (n == 0). Proof. -by case: m n => m [] n //=; move/eqP; rewrite ?(NegzE,mulrN,mulNr); - rewrite ?(inv_eq (@opprK _)) -PoszM [_==_]muln_eq0. +by case: m n => m [] n //= /eqP; + rewrite ?(NegzE, mulrN, mulNr) ?oppr_eq0 -PoszM [_ == _]muln_eq0. Qed. Definition comMixin := ComUnitRingMixin mulVz unitzPl invz_out. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 2414e13..ec932a1 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1457,18 +1457,18 @@ Hint Resolve ltr_opp2 : core. Definition lter_opp2 := (ler_opp2, ltr_opp2). Lemma ler_oppr x y : (x <= - y) = (y <= - x). -Proof. by rewrite (monoRL (@opprK _) ler_opp2). Qed. +Proof. by rewrite (monoRL opprK ler_opp2). Qed. Lemma ltr_oppr x y : (x < - y) = (y < - x). -Proof. by rewrite (monoRL (@opprK _) (lerW_nmono _)). Qed. +Proof. by rewrite (monoRL opprK (lerW_nmono _)). Qed. Definition lter_oppr := (ler_oppr, ltr_oppr). Lemma ler_oppl x y : (- x <= y) = (- y <= x). -Proof. by rewrite (monoLR (@opprK _) ler_opp2). Qed. +Proof. by rewrite (monoLR opprK ler_opp2). Qed. Lemma ltr_oppl x y : (- x < y) = (- y < x). -Proof. by rewrite (monoLR (@opprK _) (lerW_nmono _)). Qed. +Proof. by rewrite (monoLR opprK (lerW_nmono _)). Qed. Definition lter_oppl := (ler_oppl, ltr_oppl). @@ -4797,12 +4797,17 @@ Qed. End ClosedFieldTheory. -Notation "n .-root" := (@nthroot _ n) (at level 2, format "n .-root") : ring_scope. +Notation "n .-root" := (@nthroot _ n) + (at level 2, format "n .-root") : ring_scope. Notation sqrtC := 2.-root. Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope. Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope. Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope. +Arguments conjCK {C} x. +Arguments sqrCK {C} [x] le0x. +Arguments sqrCK_P {C x}. + End Theory. Module RealMixin. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index c4c62c3..4766c74 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1355,6 +1355,8 @@ Proof. by elim/big_rec2: _ => [|i _ f _ <-]; rewrite lfunE. Qed. End LfunZmodType. +Arguments fun_of_lfunK {R aT rT}. + Section LfunVectType. Variables (R : comRingType) (aT rT : vectType R). @@ -1603,6 +1605,7 @@ Arguments lfunPn {K aT rT f g}. Arguments lker0P {K aT rT f}. Arguments eqlfunP {K aT rT f g v}. Arguments eqlfun_inP {K aT rT V f g}. +Arguments limg_lfunVK {K aT rT f} [x] f_x. Section FixedSpace. @@ -1718,6 +1721,8 @@ Qed. End LinearPreimage. +Arguments lpreimK {K aT rT f} [W] fW. + Section LfunAlgebra. (* This section is a bit of a place holder: the instances we build here can't *) (* be canonical because we are missing an interface for proper vectTypes, *) @@ -1944,7 +1949,7 @@ Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin. End SubVector. Prenex Implicits vsval vsproj vsvalK. Arguments subvs_inj {K vT U} [x1 x2]. -Arguments vsprojK {K vT U} [x]. +Arguments vsprojK {K vT U} [x] Ux. Section MatrixVectType. diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index ba6c1b3..5e931ef 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -180,7 +180,8 @@ End ZpDef. Arguments Zp0 {p'}. Arguments Zp1 {p'}. -Arguments inZp {p'}. +Arguments inZp {p'} i. +Arguments valZpK {p'} x. Lemma ord1 : all_equal_to (0 : 'I_1). Proof. by case=> [[] // ?]; apply: val_inj. Qed. @@ -259,6 +260,8 @@ Notation "''Z_' p" := 'I_(Zp_trunc p).+2 Notation "''F_' p" := 'Z_(pdiv p) (at level 8, p at level 2, format "''F_' p") : type_scope. +Arguments natr_Zp {p'} x. + Section Groups. Variable p : nat. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 9a61ebe..783c46f 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -817,7 +817,9 @@ Qed. End IrrClass. Arguments cfReg {gT} B%g. -Prenex Implicits cfIirr. +Prenex Implicits cfIirr irrK. +Arguments irrP {gT G xi}. +Arguments irr_reprP {gT G xi}. Arguments irr_inj {gT G} [x1 x2]. Section IsChar. @@ -1334,6 +1336,8 @@ Qed. End OrthogonalityRelations. +Prenex Implicits irr_class class_Iirr irr_classK. +Arguments class_IirrK {gT G%G} [xG%g] GxG : rename. Arguments character_table {gT} G%g. Section InnerProduct. @@ -1353,7 +1357,7 @@ Lemma irr_orthonormal : orthonormal (irr G). Proof. apply/orthonormalP; split; first exact: free_uniq (irr_free G). move=> _ _ /irrP[i ->] /irrP[j ->]. -by rewrite cfdot_irr (inj_eq (@irr_inj _ G)). +by rewrite cfdot_irr (inj_eq irr_inj). Qed. Lemma coord_cfdot phi i : coord (irr G) i phi = '[phi, 'chi_i]. @@ -1436,7 +1440,7 @@ Qed. Lemma eq_signed_irr (s t : bool) i j : ((-1) ^+ s *: 'chi[G]_i == (-1) ^+ t *: 'chi_j) = (s == t) && (i == j). -Proof. by rewrite eq_scaled_irr signr_eq0 (inj_eq (@signr_inj _)). Qed. +Proof. by rewrite eq_scaled_irr signr_eq0 (inj_eq signr_inj). Qed. Lemma eq_scale_irr a (i j : Iirr G) : (a *: 'chi_i == a *: 'chi_j) = (a == 0) || (i == j). @@ -2258,6 +2262,7 @@ Qed. End Aut. Arguments aut_Iirr_inj {gT G} u [i1 i2] : rename. +Arguments conjC_IirrK {gT G} i : rename. Section Coset. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index a4ecd2c..2048868 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -759,6 +759,7 @@ Arguments classfun_on {gT} B%g A%g. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. Arguments cfun_onP {gT G A phi}. +Arguments cfConjCK {gT G} phi : rename. Hint Resolve cfun_onT : core. Section DotProduct. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 22ab389..1d8f785 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -755,6 +755,8 @@ End SubGroup. End AbelemRepr. +Arguments rVabelem_inj {p%N gT E%G} abelE ntE [v1%R v2%R] : rename. + Section ModularRepresentation. Variables (F : fieldType) (p : nat) (gT : finGroupType). diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 560b61d..0968347 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -300,13 +300,13 @@ Lemma repr_mxM : {in G &, {morph rG : x y / (x * y)%g >-> x *m y}}. Proof. by case: rG => r []. Qed. Lemma repr_mxK m x : - x \in G -> cancel ((@mulmx _ m n n)^~ (rG x)) (mulmx^~ (rG x^-1)). + x \in G -> cancel ((@mulmx R m n n)^~ (rG x)) (mulmx^~ (rG x^-1)). Proof. by move=> Gx U; rewrite -mulmxA -repr_mxM ?groupV // mulgV repr_mx1 mulmx1. Qed. Lemma repr_mxKV m x : - x \in G -> cancel ((@mulmx _ m n n)^~ (rG x^-1)) (mulmx^~ (rG x)). + x \in G -> cancel ((@mulmx R m n n)^~ (rG x^-1)) (mulmx^~ (rG x)). Proof. by rewrite -groupV -{3}[x]invgK; apply: repr_mxK. Qed. Lemma repr_mx_unit x : x \in G -> rG x \in unitmx. @@ -821,7 +821,11 @@ Arguments regular_repr R {gT} G%g. Arguments centgmxP {R gT G n rG f}. Arguments rkerP {R gT G n rG x}. -Prenex Implicits gring_mxK. +Arguments repr_mxK {R gT G%G n%N} rG {m%N} [x%g] Gx. +Arguments repr_mxKV {R gT G%G n%N} rG {m%N} [x%g] Gx. +Arguments gring_valK {gT G%G} i%R : rename. +Arguments gring_indexK {gT G%G} x%g. +Arguments gring_mxK {R gT G%G} v%R : rename. Section ChangeOfRing. @@ -2377,7 +2381,16 @@ Arguments mxsimple_isoP {gT G n rG U V}. Arguments socleP {gT G n rG sG0 W W'}. Arguments mx_abs_irrP {gT G n rG}. +Arguments val_submod {n U m} W. +Arguments in_submod {n} U {m} W. +Arguments val_submodK {n U m} W : rename. +Arguments in_submodK {n U m} [W] sWU. Arguments val_submod_inj {n U m} [W1 W2] : rename. + +Arguments val_factmod {n U m} W. +Arguments in_factmod {n} U {m} W. +Arguments val_factmodK {n U m} W : rename. +Arguments in_factmodK {n} U {m} [W] sWU. Arguments val_factmod_inj {n U m} [W1 W2] : rename. Section Proper. @@ -3797,7 +3810,7 @@ rewrite !permM; case: (unliftP i_m i) => [j {simWUm}|] ->{i}; last first. apply: rsimT (rsimC _) {pUW}(rsimT (pUW j) _). by rewrite lift_max; apply: rsim_rcons. rewrite lift_perm_lift; case: (unliftP j_m (pU j)) => [k|] ->{j pU}. - rewrite tpermD ?(inj_eq (@lift_inj _ _)) ?neq_lift //. + rewrite tpermD ?(inj_eq lift_inj) ?neq_lift //. rewrite lift_perm_lift !lift_max; set j := lift j_m k. have ltjW: j < size W by have:= ltn_ord k; rewrite -(lift_max k) /= {1 3}szW. apply: rsimT (rsimT (pWV j) _); last by apply: rsim_rcons; rewrite -szV. @@ -4671,16 +4684,28 @@ Arguments socleP {F gT G n rG sG0 W W'}. Arguments mx_abs_irrP {F gT G n rG}. Arguments socle_rsimP {F gT G n rG sG W1 W2}. +Arguments val_submod {F n U m} W. +Arguments in_submod {F n} U {m} W. +Arguments val_submodK {F n U m} W : rename. +Arguments in_submodK {F n U m} [W] sWU. Arguments val_submod_inj {F n U m} [W1 W2] : rename. + +Arguments val_factmod {F n U m} W. +Arguments in_factmod {F n} U {m} W. +Arguments val_factmodK {F n U m} W : rename. +Arguments in_factmodK {F n} U {m} [W] sWU. Arguments val_factmod_inj {F n U m} [W1 W2] : rename. Notation "'Cl" := (Clifford_action _) : action_scope. +Arguments gring_row {R gT G} A. +Arguments gring_rowK {F gT G} [A] RG_A. + Bind Scope irrType_scope with socle_sort. Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope. Arguments irr_degree {F gT G%G sG} i%irr. -Arguments irr_repr [F gT G%G sG] i%irr _%g : extra scopes. -Arguments irr_mode [F gT G%G sG] i%irr z%g : rename. +Arguments irr_repr {F gT G%G sG} i%irr _%g : extra scopes. +Arguments irr_mode {F gT G%G sG} i%irr z%g : rename. Notation "''n_' i" := (irr_degree i) : group_ring_scope. Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope. Notation "''e_' i" := (Wedderburn_id i) : group_ring_scope. @@ -4973,7 +4998,7 @@ Proof. move=> splitG n rG irrG. have modU0: all ((mxmodule (regular_repr aF G)) #|G|) [::] by []. apply: (mx_Schreier modU0 _) => // [[U [compU lastU _]]]; have [modU _]:= compU. -pose Uf := map ((map_mx f) _ _) U. +pose Uf := map (map_mx f) U. have{lastU} lastUf: (last 0 Uf :=: 1%:M)%MS. by rewrite -(map_mx0 f) -(map_mx1 f) last_map; apply/map_eqmx. have modUf: mx_subseries (regular_repr rF G) Uf. @@ -5062,7 +5087,7 @@ by rewrite /mxval [pval _]poly_rV_K ?horner_mx_C // size_polyC; case: (x != 0). Qed. Lemma mxval_inj : injective mxval. -Proof. exact: inj_comp (@horner_rVpoly_inj _ _ A) val_inj. Qed. +Proof. exact: inj_comp horner_rVpoly_inj val_inj. Qed. Lemma mxval0 : mxval 0 = 0. Proof. by rewrite /mxval [pval _]raddf0 rmorph0. Qed. @@ -5557,6 +5582,11 @@ 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. @@ -5596,7 +5626,7 @@ Lemma eval_mulT e u v : eval_mx e (mulT u v) = val (inFA (eval_mx e u) * inFA (eval_mx e v)). Proof. rewrite !(eval_mulmx, eval_mxvec) !eval_mxT eval_mx_term. -by apply: (can_inj (@rVpolyK _ _)); rewrite -mxvalM [rVpoly _]horner_rVpolyK. +by apply: (can_inj rVpolyK); rewrite -mxvalM [rVpoly _]horner_rVpolyK. Qed. Fixpoint gen_term t := match t with diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index 5c9ca9b..246e955 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -749,7 +749,7 @@ Lemma cfdot_dirr f g : f \in dirr G -> g \in dirr G -> Proof. case/dirrP=> [b1 [i1 ->]] /dirrP[b2 [i2 ->]]. rewrite cfdotZl cfdotZr rmorph_sign mulrA -signr_addb cfdot_irr. -rewrite -scaleNr -signrN !eq_scaled_irr signr_eq0 !(inj_eq (@signr_inj _)) /=. +rewrite -scaleNr -signrN !eq_scaled_irr signr_eq0 !(inj_eq signr_inj) /=. by rewrite -!negb_add addbN mulr_sign -mulNrn mulrb; case: ifP. Qed. @@ -799,7 +799,7 @@ Lemma cfdot_dchi (i j : dIirr G) : '[dchi i, dchi j] = (i == j)%:R - (i == ndirr j)%:R. Proof. case: i => bi i; case: j => bj j; rewrite cfdot_dirr ?dirr_dchi // !xpair_eqE. -rewrite -dchi_ndirrE !eq_scaled_irr signr_eq0 !(inj_eq (@signr_inj _)) /=. +rewrite -dchi_ndirrE !eq_scaled_irr signr_eq0 !(inj_eq signr_inj) /=. by rewrite -!negb_add addbN negbK; case: andP => [[->]|]; rewrite ?subr0 ?add0r. Qed. @@ -811,7 +811,7 @@ Proof. by case: i => b i; rewrite cfnorm_sign cfnorm_irr. Qed. Lemma dirr_inj : injective (@dchi G). Proof. -case=> b1 i1 [b2 i2] /eqP; rewrite eq_scaled_irr (inj_eq (@signr_inj _)) /=. +case=> b1 i1 [b2 i2] /eqP; rewrite eq_scaled_irr (inj_eq signr_inj) /=. by rewrite signr_eq0 -xpair_eqE => /eqP. Qed. @@ -890,15 +890,13 @@ Lemma cfdot_todirrE (phi: 'CF(G)) i (phi_i := dchi (to_dirr phi i)) : Proof. by rewrite cfdotZr rmorph_sign mulrC -scalerA signrZK. Qed. Lemma cfun_sum_dconstt (phi : 'CF(G)) : - phi \in 'Z[irr G] -> + phi \in 'Z[irr G] -> phi = \sum_(i in dirr_constt phi) '[phi, dchi i] *: dchi i. Proof. -(* GG -- rewrite pattern fails in trunk - move=> PiZ; rewrite [X in X = _]cfun_sum_constt. *) -move=> PiZ; rewrite {1}[phi]cfun_sum_constt. +move=> PiZ; rewrite [LHS]cfun_sum_constt. rewrite (reindex (to_dirr phi))=> [/= |]; last first. by exists (@of_irr _)=> //; apply: of_irrK . -by apply: eq_big=> i; rewrite ?irr_constt_to_dirr // cfdot_todirrE. +by apply: eq_big => i; rewrite ?irr_constt_to_dirr // cfdot_todirrE. Qed. Lemma cnorm_dconstt (phi : 'CF(G)) : @@ -981,3 +979,6 @@ by case: (i1 == j) eq_phi_psi; case: (i2 == j); do 2!case: (_ (+) c). Qed. End Norm1vchar. + +Prenex Implicits ndirr ndirrK to_dirr to_dirrK of_irr. +Arguments of_irrK {gT G phi} [i] phi_i : rename. diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index fc01763..ae60027 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -279,7 +279,7 @@ Canonical eqType := EqType type eqMixin. Definition choiceMixin : Choice.mixin_of type := EquivQuot.choiceMixin _. Canonical choiceType := ChoiceType type choiceMixin. -Definition countMixin : Countable.mixin_of type := CanCountMixin (@reprK _ _). +Definition countMixin : Countable.mixin_of type := CanCountMixin reprK. Canonical countType := CountType type countMixin. Definition CtoL (u : type) := rootQtoL (repr u). @@ -607,7 +607,8 @@ Local Notation intrp := (map_poly intr). Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. + +Local Hint Resolve (intr_inj : injective ZtoC) : core. (* Specialization of a few basic ssrnum order lemmas. *) @@ -882,7 +883,7 @@ Lemma CintE x : (x \in Cint) = (x \in Cnat) || (- x \in Cnat). Proof. apply/idP/idP=> [/CintP[[n | n] ->] | ]; first by rewrite Cnat_nat. by rewrite NegzE opprK Cnat_nat orbT. -by case/pred2P=> [<- | /(canLR (@opprK _)) <-]; rewrite ?rpredN rpred_nat. +by case/pred2P=> [<- | /(canLR opprK) <-]; rewrite ?rpredN rpred_nat. Qed. Lemma Cnat_norm_Cint x : x \in Cint -> `|x| \in Cnat. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 1db4aa4..3053eb9 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -56,7 +56,7 @@ Local Notation pZtoQ := (map_poly ZtoQ). Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). -Local Hint Resolve (@intr_inj _ : injective ZtoC) : core. +Local Hint Resolve (intr_inj : injective ZtoC) : core. Local Notation QtoCm := [rmorphism of QtoC]. (* Number fields and rational spans. *) @@ -417,7 +417,7 @@ have ext1 mu0 x: {mu1 | exists y, x = Sinj mu1 y by apply/polyOverP=> i; rewrite coef_map memvZ ?memv_line. have splitQr: splittingFieldFor K pr fullv. apply: splittingFieldForS (sub1v (Sub K algK)) (subvf _) _; exists rr => //. - congr (_ %= _): (eqpxx pr); apply: (@map_poly_inj _ _ QrC). + congr (_ %= _): (eqpxx pr); apply/(map_poly_inj QrC). rewrite Sinj_poly Dr -Drr big_map rmorph_prod; apply: eq_bigr => zz _. by rewrite rmorphB /= map_polyX map_polyC. have [f1 aut_f1 Df1]:= kHom_extends (sub1v (ASpace algK)) hom_f Qpr splitQr. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 76039d1..c338002 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -714,7 +714,7 @@ have EmulV: GRing.Field.axiom Einv. rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE. by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull. pose Efield := FieldType _ (FieldMixin EmulV Einv0). -pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)). +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. @@ -783,7 +783,7 @@ have eqKtrans : transitive eqKrep. 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 _ _). +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. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 99db561..7c89607 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -1468,7 +1468,7 @@ Proof. move/subfx_irreducibleP: irr_p => /=/(_ nz_p) min_p; set d := (size p).-1. have Dd: d.+1 = size p by rewrite polySpred. pose Fz2v x : 'rV_d := poly_rV (sval (sig_eqW (subfxE x)) %% p). -pose vFz : 'rV_d -> subFExtend := subfx_eval \o @rVpoly F d. +pose vFz : 'rV_d -> subFExtend := subfx_eval \o rVpoly. have FLinj: injective subfx_inj by apply: fmorph_inj. have Fz2vK: cancel Fz2v vFz. move=> x; rewrite /vFz /Fz2v; case: (sig_eqW _) => /= q ->. @@ -1479,7 +1479,7 @@ suffices vFzK: cancel vFz Fz2v. apply: inj_can_sym Fz2vK _ => v1 v2 /(congr1 subfx_inj)/eqP. rewrite -subr_eq0 -!raddfB /= subfx_inj_eval // => /min_p/implyP. rewrite leqNgt implybNN -Dd ltnS size_poly linearB subr_eq0 /=. -by move/eqP/(can_inj (@rVpolyK _ _)). +by move/eqP/(can_inj rVpolyK). Qed. Definition SubfxVectMixin := VectMixin min_subfx_vectAxiom. @@ -1559,7 +1559,7 @@ pose ucrL := [comUnitRingType of ComRingType urL mulC]. have mul0 := GRing.Field.IdomainMixin unitE. pose fL := FieldType (IdomainType ucrL mul0) unitE. exists [fieldExtType F of faL for fL]; first by rewrite dimvf; apply: mul1n. -exists [linear of toPF as @rVpoly _ _]. +exists [linear of toPF as rVpoly]. suffices toLM: lrmorphism (toL : {poly F} -> aL) by exists (LRMorphism toLM). have toLlin: linear toL. by move=> a q1 q2; rewrite -linearP -modp_scalel -modp_add. @@ -1592,13 +1592,13 @@ have mul1: left_id L1 mul. move=> x; rewrite /mul L1K mul1r /toL modp_small ?rVpolyK // -Dn ltnS. by rewrite size_poly. have mulD: left_distributive mul +%R. - move=> x y z; apply: canLR (@rVpolyK _ _) _. + move=> x y z; apply: canLR rVpolyK _. by rewrite !raddfD mulrDl /= !toL_K /toL modp_add. -have nzL1: L1 != 0 by rewrite -(can_eq (@rVpolyK _ _)) L1K raddf0 oner_eq0. +have nzL1: L1 != 0 by rewrite -(can_eq rVpolyK) L1K raddf0 oner_eq0. pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. - move=> a x y; apply: canRL (@rVpolyK _ _) _; rewrite !linearZ /= toL_K. + move=> a x y; apply: canRL rVpolyK _; rewrite !linearZ /= toL_K. by rewrite -scalerAl modp_scalel. have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. @@ -1607,7 +1607,7 @@ pose uaL := [unitAlgType F of AlgType F urL mulZr]. pose faL := [FalgType F of uaL]. have unitE: GRing.Field.mixin_of urL. move=> x nz_x; apply/unitrP; set q := rVpoly x. - have nz_q: q != 0 by rewrite -(can_eq (@rVpolyK _ _)) raddf0 in nz_x. + have nz_q: q != 0 by rewrite -(can_eq rVpolyK) raddf0 in nz_x. have /Bezout_eq1_coprimepP[u upq1]: coprimep p q. have /contraR := irr_p _ _ (dvdp_gcdl p q); apply. have: size (gcdp p q) <= size q by apply: leq_gcdpr. @@ -1627,11 +1627,10 @@ have q_z q: rVpoly (map_poly iota q).[z] = q %% p. rewrite linearZ /= L1K alg_polyC modp_add; congr (_ + _); last first. by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW. by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul. -exists z; first by rewrite /root -(can_eq (@rVpolyK _ _)) q_z modpp linear0. +exists z; first by rewrite /root -(can_eq rVpolyK) q_z modpp linear0. apply/vspaceP=> x; rewrite memvf; apply/Fadjoin_polyP. exists (map_poly iota (rVpoly x)). by apply/polyOverP=> i; rewrite coef_map memvZ ?mem1v. -apply: (can_inj (@rVpolyK _ _)). -by rewrite q_z modp_small // -Dn ltnS size_poly. +by apply/(can_inj rVpolyK); rewrite q_z modp_small // -Dn ltnS size_poly. Qed. *) diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 252868d..fb96ffe 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1634,6 +1634,9 @@ End FundamentalTheoremOfGaloisTheory. End GaloisTheory. +Prenex Implicits gal_repr gal gal_reprK. +Arguments gal_repr_inj {F L V} [x1 x2]. + Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope. Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope. diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 9a8032d..e1f64c8 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -2703,6 +2703,7 @@ Canonical aut_groupAction := GroupAction autact_is_groupAction. End AutAct. +Arguments autact {gT} G%g. Arguments aut_action {gT} G%g. Arguments aut_groupAction {gT} G%g. Notation "[ 'Aut' G ]" := (aut_action G) : action_scope. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index f436102..4bb638c 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -577,7 +577,7 @@ Lemma conjg_inj : @left_injective T T T conjg. Proof. by move=> y; apply: can_inj (conjgK y). Qed. Lemma conjg_eq1 x y : (x ^ y == 1) = (x == 1). -Proof. by rewrite -(inj_eq (@conjg_inj y) x) conj1g. Qed. +Proof. by rewrite (canF_eq (conjgK _)) conj1g. Qed. Lemma conjg_prod I r (P : pred I) F z : (\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z). @@ -1854,6 +1854,9 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope. Prenex Implicits subg sgval subg_of. Bind Scope group_scope with subg_of. +Arguments subgK {gT G}. +Arguments sgvalK {gT G}. +Arguments subg_inj {gT G} [u1 u2] eq_u12 : rename. Arguments trivgP {gT G}. Arguments trivGP {gT G}. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index cb02991..aa2a809 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -873,6 +873,7 @@ Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope. Notation "f @: D" := (morph_dom_group f D) : Group_scope. Arguments injmP {aT rT D f}. +Arguments morphpreK {aT rT D f} [R] sRf. Section IdentityMorphism. @@ -1491,10 +1492,10 @@ Canonical sgval_morphism := Morphism (@sgvalM _ G). Canonical subg_morphism := Morphism (@subgM _ G). Lemma injm_sgval : 'injm sgval. -Proof. by apply/injmP; apply: in2W; apply: subg_inj. Qed. +Proof. exact/injmP/(in2W subg_inj). Qed. Lemma injm_subg : 'injm (subg G). -Proof. by apply/injmP; apply: can_in_inj (@subgK _ _). Qed. +Proof. exact/injmP/(can_in_inj subgK). Qed. Hint Resolve injm_sgval injm_subg : core. Lemma ker_sgval : 'ker sgval = 1. Proof. exact/trivgP. Qed. @@ -1537,3 +1538,6 @@ Proof. exact: isom_isog isom_subg. Qed. End SubMorphism. +Arguments sgvalmK {gT G} A. +Arguments subgmK {gT G} [A] sAG. + diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index b1a7dd7..8c97ab1 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -125,10 +125,8 @@ Proof. by rewrite [@fun_of_perm]unlock. Qed. Lemma permE f f_inj : @perm T f f_inj =1 f. Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed. -Lemma perm_inj s : injective s. +Lemma perm_inj {s} : injective s. Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed. - -Arguments perm_inj : clear implicits. Hint Resolve perm_inj : core. Lemma perm_onto s : codom s =i predT. @@ -141,7 +139,7 @@ Proof. by move=> x /=; rewrite f_iinv. Qed. Definition perm_inv s := perm (can_inj (perm_invK s)). -Definition perm_mul s t := perm (inj_comp (perm_inj t) (perm_inj s)). +Definition perm_mul s t := perm (inj_comp (@perm_inj t) (@perm_inj s)). Lemma perm_oneP : left_id perm_one perm_mul. Proof. by move=> s; apply/permP => x; rewrite permE /= permE. Qed. @@ -191,7 +189,7 @@ Definition perm_on S : pred {perm T} := fun s => [pred x | s x != x] \subset S. Lemma perm_closed S s x : perm_on S s -> (s x \in S) = (x \in S). Proof. move/subsetP=> s_on_S; have [-> // | nfix_s_x] := eqVneq (s x) x. -by rewrite !s_on_S // inE /= ?(inj_eq (perm_inj s)). +by rewrite !s_on_S // inE /= ?(inj_eq perm_inj). Qed. Lemma perm_on1 H : perm_on H 1. @@ -282,7 +280,11 @@ Qed. End Theory. -Prenex Implicits tperm. +Prenex Implicits tperm permK permKV tpermK. +Arguments perm_inj {T s} [x1 x2] eq_sx12. + +(* Shorthand for using a permutation to reindex a bigop. *) +Notation reindex_perm s := (reindex_inj (@perm_inj _ s)). Lemma inj_tperm (T T' : finType) (f : T -> T') x y z : injective f -> f (tperm x y z) = tperm (f x) (f y) (f z). @@ -291,8 +293,7 @@ Proof. by move=> injf; rewrite !permE /= !(inj_eq injf) !(fun_if f). Qed. Lemma tpermJ (T : finType) x y (s : {perm T}) : (tperm x y) ^ s = tperm (s x) (s y). Proof. -apply/permP => z; rewrite -(permKV s z) permJ; apply: inj_tperm. -exact: perm_inj. +by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj. Qed. Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} : @@ -554,7 +555,7 @@ congr (_ (+) _); last first. elim: ts => [|t ts IHts] /=; first by rewrite big_nil lift_perm1 !odd_perm1. rewrite big_cons odd_mul_tperm -(lift_permM _ j) odd_permM {}IHts //. congr (_ (+) _); transitivity (tperm (lift j t.1) (lift j t.2)); last first. - by rewrite odd_tperm (inj_eq (@lift_inj _ _)). + by rewrite odd_tperm (inj_eq (pcan_inj (liftK j))). congr odd_perm; apply/permP=> k; case: (unliftP j k) => [k'|] ->. by rewrite lift_perm_lift inj_tperm //; apply: lift_inj. by rewrite lift_perm_id tpermD // eq_sym neq_lift. @@ -576,5 +577,7 @@ Qed. End LiftPerm. +Prenex Implicits lift_perm lift_permK. + diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 97b2eba..61b0cd9 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -198,13 +198,14 @@ Lemma quotientE : quotient = coset @* Q. Proof. by []. Qed. End Cosets. -Arguments coset_of {_} _%g. -Arguments coset {_} _%g _%g. -Arguments quotient _ _%g _%g. +Arguments coset_of {gT} H%g : rename. +Arguments coset {gT} H%g x%g : rename. +Arguments quotient {gT} A%g H%g : rename. +Arguments coset_reprK {gT H%g} xbar%g : rename. Bind Scope group_scope with coset_of. -Notation "A / B" := (quotient A B) : group_scope. +Notation "A / H" := (quotient A H) : group_scope. Section CosetOfGroupTheory. @@ -454,7 +455,7 @@ Proof. by rewrite /normal -{1}ker_coset; apply: morphim_injG. Qed. Lemma quotient_inj G1 G2 : H <| G1 -> H <| G2 -> G1 / H = G2 / H -> G1 :=: G2. -Proof. by rewrite /normal -{1 3}ker_coset; apply: morphim_inj. Qed. +Proof. by rewrite /normal -[in mem H]ker_coset; apply: morphim_inj. Qed. Lemma quotient_neq1 A : H <| A -> (A / H != 1) = (H \proper A). Proof. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index 73a3b1b..b0e4c22 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -235,12 +235,12 @@ have FF (H : {group {perm T}}): H <| 'Alt_T -> H :<>: 1 -> 20 %| #|H|. have DnS1: S1 \in 3.-dtuple(setT). rewrite inE memtE subset_all /= !inE /= !negb_or -!andbA /= andbT. rewrite -{1}[h]expg1 !diff_hnx_x // expgSr permM. - by rewrite (inj_eq (@perm_inj _ _)) diff_hnx_x. + by rewrite (inj_eq perm_inj) diff_hnx_x. pose S2 := [tuple x; h x; (h ^+ 2) x]. have DnS2: S2 \in 3.-dtuple(setT). rewrite inE memtE subset_all /= !inE /= !negb_or -!andbA /= andbT. rewrite -{1}[h]expg1 !diff_hnx_x // expgSr permM. - by rewrite (inj_eq (@perm_inj _ _)) diff_hnx_x. + by rewrite (inj_eq perm_inj) diff_hnx_x. case: (atransP2 F2 DnS1 DnS2) => g Hg [/=]. rewrite /aperm => Hgx Hghx Hgh3x. have h_g_com: h * g = g * h. @@ -290,8 +290,8 @@ Notation T' := {y | y != x}. Lemma rfd_funP (p : {perm T}) (u : T') : let p1 := if p x == x then p else 1 in p1 (val u) != x. Proof. -case: (p x =P x) => /= [pxx|_]; last by rewrite perm1 (valP u). -by rewrite -{2}pxx (inj_eq (@perm_inj _ p)); apply: (valP u). +case: (p x =P x) => /= [pxx | _]; last by rewrite perm1 (valP u). +by rewrite -[x in _ != x]pxx (inj_eq perm_inj); apply: (valP u). Qed. Definition rfd_fun p := [fun u => Sub ((_ : {perm T}) _) (rfd_funP p u) : T']. @@ -299,7 +299,7 @@ Definition rfd_fun p := [fun u => Sub ((_ : {perm T}) _) (rfd_funP p u) : T']. Lemma rfdP p : injective (rfd_fun p). Proof. apply: can_inj (rfd_fun p^-1) _ => u; apply: val_inj => /=. -rewrite -(inj_eq (@perm_inj _ p)) permKV eq_sym. +rewrite -(can_eq (permK p)) permKV eq_sym. by case: eqP => _; rewrite !(perm1, permK). Qed. @@ -350,8 +350,7 @@ have Hp1: p1 x = x. have Hcp1: #|[set x | p1 x != x]| <= n. have F1 y: p y = y -> p1 y = y. move=> Hy; rewrite /p1 permM Hy. - case tpermP => //; first by move=> <-. - by move=> Hpx1; apply: (@perm_inj _ p); rewrite -Hpx1. + by case: tpermP => [<-|/(canLR (permK p))<-|] //; apply/(canLR (permK p)). have F2: p1 x1 = x1 by rewrite /p1 permM tpermR. have F3: [set x | p1 x != x] \subset [predD1 [set x | p x != x] & x1]. apply/subsetP => z; rewrite !inE permM. @@ -494,8 +493,7 @@ case diff_hgx_hx: ((h * g) x == h x). case/negP: diff_1_g; apply/eqP. by apply: (Hreg _ (h x)) => //; apply/eqP; rewrite -permM. case diff_hgx_gx: ((h * g) x == g x). - case/eqP: diff_hx_x; apply: (@perm_inj _ g) => //. - by apply/eqP; rewrite -permM. + by case/idP: diff_hx_x; rewrite -(can_eq (permK g)) -permM. case Ez: (pred0b (predD1 (predD1 (predD1 (predD1 T x) (h x)) (g x)) ((h * g) x))). - move: oT; rewrite /pred0b in Ez. diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v index 5a2b35b..9afe26a 100644 --- a/mathcomp/solvable/finmodule.v +++ b/mathcomp/solvable/finmodule.v @@ -243,6 +243,11 @@ Canonical FiniteModule.fmod_finZmodType. Canonical FiniteModule.fmod_baseFinGroupType. Canonical FiniteModule.fmod_finGroupType. +Arguments FiniteModule.fmodK {gT A} abelA [x] Ax. +Arguments FiniteModule.fmvalK {gT A abelA} x. +Arguments FiniteModule.actrK {gT A abelA} x. +Arguments FiniteModule.actrKV {gT A abelA} x. + (* Still allow ring notations, but give priority to groups now. *) Import FiniteModule GroupScope. diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index 6f46832..57b585e 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -141,6 +141,9 @@ Proof. by case. Qed. End OtherEncodings. +Prenex Implicits seq_of_opt tag_of_pair pair_of_tag opair_of_sum sum_of_opair. +Prenex Implicits seq_of_optK tag_of_pairK pair_of_tagK opair_of_sumK. + (* Generic variable-arity tree type, providing an encoding target for *) (* miscellaneous user datatypes. The GenTree.tree type can be combined with *) (* a sigT type to model multi-sorted concrete datatypes. *) @@ -562,8 +565,8 @@ Export Countable.Exports. Definition unpickle T := Countable.unpickle (Countable.class T). Definition pickle T := Countable.pickle (Countable.class T). -Arguments unpickle {T}. -Prenex Implicits pickle. +Arguments unpickle {T} n. +Arguments pickle {T} x. Section CountableTheory. @@ -609,6 +612,11 @@ Notation "[ 'countMixin' 'of' T 'by' <: ]" := (sub_countMixin _ : Countable.mixin_of T) (at level 0, format "[ 'countMixin' 'of' T 'by' <: ]") : form_scope. +Arguments pickle_inv {T} n. +Arguments pickleK {T} x. +Arguments pickleK_inv {T} x. +Arguments pickle_invK {T} n : rename. + Section SubCountType. Variables (T : choiceType) (P : pred T). diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index dc3daf0..58ef844 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -514,7 +514,8 @@ Structure subType : Type := SubType { _ : forall x Px, val (@Sub x Px) = x }. -Arguments Sub [s]. +(* Generic proof that the second property holds by conversion. *) +(* The vrefl_rect alias is used to flag generic proofs of the first property. *) Lemma vrefl : forall x, P x -> x = x. Proof. by []. Qed. Definition vrefl_rect := vrefl. @@ -522,18 +523,21 @@ Definition clone_subType U v := fun sT & sub_sort sT -> U => fun c Urec cK (sT' := @SubType U v c Urec cK) & phant_id sT' sT => sT'. +Section Theory. + Variable sT : subType. +Local Notation val := (@val sT). +Local Notation Sub x Px := (@Sub sT x Px). + Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px). Lemma SubP u : Sub_spec u. -Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed. +Proof. by case: sT Sub_spec SubSpec u => /= U _ mkU rec _. Qed. -Lemma SubK x Px : @val sT (Sub x Px) = x. -Proof. by case: sT. Qed. +Lemma SubK x Px : val (Sub x Px) = x. Proof. by case: sT. Qed. -Definition insub x := - if @idP (P x) is ReflectT Px then @Some sT (Sub x Px) else None. +Definition insub x := if idP is ReflectT Px then Some (Sub x Px) else None. Definition insubd u0 x := odflt u0 (insub x). @@ -561,49 +565,55 @@ Proof. by move/negPf/insubF. Qed. Lemma isSome_insub : ([eta insub] : pred T) =1 P. Proof. by apply: fsym => x; case: insubP => // /negPf. Qed. -Lemma insubK : ocancel insub (@val _). +Lemma insubK : ocancel insub val. Proof. by move=> x; case: insubP. Qed. -Lemma valP (u : sT) : P (val u). +Lemma valP u : P (val u). Proof. by case/SubP: u => x Px; rewrite SubK. Qed. -Lemma valK : pcancel (@val _) insub. +Lemma valK : pcancel val insub. Proof. by case/SubP=> x Px; rewrite SubK; apply: insubT. Qed. -Lemma val_inj : injective (@val sT). +Lemma val_inj : injective val. Proof. exact: pcan_inj valK. Qed. -Lemma valKd u0 : cancel (@val _) (insubd u0). +Lemma valKd u0 : cancel val (insubd u0). Proof. by move=> u; rewrite /insubd valK. Qed. Lemma val_insubd u0 x : val (insubd u0 x) = if P x then x else val u0. Proof. by rewrite /insubd; case: insubP => [u -> | /negPf->]. Qed. -Lemma insubdK u0 : {in P, cancel (insubd u0) (@val _)}. +Lemma insubdK u0 : {in P, cancel (insubd u0) val}. Proof. by move=> x Px; rewrite /= val_insubd [P x]Px. Qed. -Definition insub_eq x := - let Some_sub Px := Some (Sub x Px : sT) in - let None_sub _ := None in - (if P x as Px return P x = Px -> _ then Some_sub else None_sub) (erefl _). +Let insub_eq_aux x isPx : P x = isPx -> option sT := + if isPx as b return _ = b -> _ then fun Px => Some (Sub x Px) else fun=> None. +Definition insub_eq x := insub_eq_aux (erefl (P x)). Lemma insub_eqE : insub_eq =1 insub. Proof. -rewrite /insub_eq /insub => x; case: {2 3}_ / idP (erefl _) => // Px Px'. -by congr (Some _); apply: val_inj; rewrite !SubK. +rewrite /insub_eq => x; set b := P x; rewrite [in LHS]/b in (Db := erefl b) *. +by case: b in Db *; [rewrite insubT | rewrite insubF]. Qed. +End Theory. + End SubType. -Arguments SubType [T P]. -Arguments Sub {T P s}. -Arguments vrefl {T P}. -Arguments vrefl_rect {T P}. +Arguments SubType {T P} sub_sort val Sub rec SubK. +Arguments val {T P sT} u : rename. +Arguments Sub {T P sT} x Px : rename. +Arguments vrefl {T P} x Px. +Arguments vrefl_rect {T P} x Px. Arguments clone_subType [T P] U v [sT] _ [c Urec cK]. -Arguments insub {T P sT}. +Arguments insub {T P sT} x. +Arguments insubd {T P sT} u0 x. Arguments insubT [T] P [sT x]. -Arguments val_inj {T P sT} [x1 x2]. -Prenex Implicits val insubd. +Arguments val_inj {T P sT} [u1 u2] eq_u12 : rename. +Arguments valK {T P sT} u : rename. +Arguments valKd {T P sT} u0 u : rename. +Arguments insubK {T P} sT x. +Arguments insubdK {T P sT} u0 [x] Px. Local Notation inlined_sub_rect := (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px). @@ -623,10 +633,6 @@ Notation "[ 'subType' 'for' v 'by' rec ]" := (SubType _ v _ rec vrefl) Notation "[ 'subType' 'of' U 'for' v ]" := (clone_subType U v id idfun) (at level 0, format "[ 'subType' 'of' U 'for' v ]") : form_scope. -(* -Notation "[ 'subType' 'for' v ]" := (clone_subType _ v id idfun) - (at level 0, format "[ 'subType' 'for' v ]") : form_scope. -*) Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id) (at level 0, format "[ 'subType' 'of' U ]") : form_scope. diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index 9929e82..db1a8e7 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -147,6 +147,7 @@ End PlainTheory. Notation family F := (family_mem (fun_of_simpl (fmem F))). Notation ffun_on R := (ffun_on_mem _ (mem R)). +Arguments ffunK {aT rT}. Arguments familyP {aT rT pT F f}. Arguments ffun_onP {aT rT R f}. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 9ca96c8..87d5da4 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -2206,6 +2206,7 @@ Qed. End MaxSetMinSet. +Arguments setCK {T}. Arguments minsetP {T P A}. Arguments maxsetP {T P A}. Prenex Implicits minset maxset. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 441fc12..06aca24 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1485,7 +1485,7 @@ Proof. by rewrite mem_undup mem_pmap -valK map_f ?ssvalP. Qed. Lemma val_seq_sub_enum : uniq s -> map val seq_sub_enum = s. Proof. move=> Us; rewrite /seq_sub_enum undup_id ?pmap_sub_uniq //. -rewrite (pmap_filter (@insubK _ _ _)); apply/all_filterP. +rewrite (pmap_filter (insubK _)); apply/all_filterP. by apply/allP => x; rewrite isSome_insub. Qed. @@ -1646,13 +1646,13 @@ Lemma rev_ord_proof n (i : 'I_n) : n - i.+1 < n. Proof. by case: n i => [|n] [i lt_i_n] //; rewrite ltnS subSS leq_subr. Qed. Definition rev_ord n i := Ordinal (@rev_ord_proof n i). -Lemma rev_ordK n : involutive (@rev_ord n). +Lemma rev_ordK {n} : involutive (@rev_ord n). Proof. by case: n => [|n] [i lti] //; apply: val_inj; rewrite /= !subSS subKn. Qed. Lemma rev_ord_inj {n} : injective (@rev_ord n). -Proof. exact: inv_inj (@rev_ordK n). Qed. +Proof. exact: inv_inj rev_ordK. Qed. (* bijection between any finType T and the Ordinal finType of its cardinal *) Section EnumRank. @@ -1762,7 +1762,7 @@ End EnumRank. Arguments enum_val_inj {T A} [i1 i2] : rename. Arguments enum_rank_inj {T} [x1 x2]. -Prenex Implicits enum_val enum_rank. +Prenex Implicits enum_val enum_rank enum_valK enum_rankK. Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i. Proof. @@ -1800,8 +1800,8 @@ case: (ltngtP i h) => /= [-> | ltih | ->] //; last by rewrite ltnn. by rewrite subn1 /= leqNgt !(ltn_predK ltih, ltih, add1n). Qed. -Lemma unbumpK h : {in predC1 h, cancel (unbump h) (bump h)}. -Proof. by move=> i; move/negbTE=> neq_h_i; rewrite unbumpKcond neq_h_i. Qed. +Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}. +Proof. by move=> i /negbTE-neq_h_i; rewrite unbumpKcond neq_h_i. Qed. Lemma bump_addl h i k : bump (k + h) (k + i) = k + bump h i. Proof. by rewrite /bump leq_add2l addnCA. Qed. @@ -1882,15 +1882,11 @@ by case Dui: (unlift h i) / (unliftP h i) => [j Dh|//]; exists j. Qed. Lemma lift_inj n (h : 'I_n) : injective (lift h). -Proof. -move=> i1 i2; move/eqP; rewrite [_ == _](can_eq (@bumpK _)) => eq_i12. -exact/eqP. -Qed. +Proof. by move=> i1 i2 [/(can_inj (bumpK h))/val_inj]. Qed. +Arguments lift_inj {n h} [i1 i2] eq_i12h : rename. Lemma liftK n (h : 'I_n) : pcancel (lift h) (unlift h). -Proof. -by move=> i; case: (unlift_some (neq_lift h i)) => j; move/lift_inj->. -Qed. +Proof. by move=> i; case: (unlift_some (neq_lift h i)) => j /lift_inj->. Qed. (* Shifting and splitting indices, for cutting and pasting arrays *) @@ -1906,7 +1902,7 @@ Definition rshift m n (i : 'I_n) := Ordinal (rshift_subproof m i). Lemma split_subproof m n (i : 'I_(m + n)) : i >= m -> i - m < n. Proof. by move/subSn <-; rewrite leq_subLR. Qed. -Definition split m n (i : 'I_(m + n)) : 'I_m + 'I_n := +Definition split {m n} (i : 'I_(m + n)) : 'I_m + 'I_n := match ltnP (i) m with | LtnNotGeq lt_i_m => inl _ (Ordinal lt_i_m) | GeqNotLtn ge_i_m => inr _ (Ordinal (split_subproof ge_i_m)) @@ -1922,16 +1918,16 @@ rewrite /split {-3}/leq. by case: (@ltnP i m) => cmp_i_m //=; constructor; rewrite ?subnKC. Qed. -Definition unsplit m n (jk : 'I_m + 'I_n) := +Definition unsplit {m n} (jk : 'I_m + 'I_n) := match jk with inl j => lshift n j | inr k => rshift m k end. Lemma ltn_unsplit m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk. Proof. by case: jk => [j|k]; rewrite /= ?ltn_ord // ltnNge leq_addr. Qed. -Lemma splitK m n : cancel (@split m n) (@unsplit m n). +Lemma splitK {m n} : cancel (@split m n) unsplit. Proof. by move=> i; apply: val_inj; case: splitP. Qed. -Lemma unsplitK m n : cancel (@unsplit m n) (@split m n). +Lemma unsplitK {m n} : cancel (@unsplit m n) split. Proof. move=> jk; have:= ltn_unsplit jk. by do [case: splitP; case: jk => //= i j] => [|/addnI] => /ord_inj->. @@ -1979,6 +1975,8 @@ Arguments ord0 {n'}. Arguments ord_max {n'}. Arguments inord {n'}. Arguments sub_ord {n'}. +Arguments sub_ordK {n'}. +Arguments inord_val {n'}. (* Product of two fintypes which is a fintype *) Section ProdFinType. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index b7a8444..71fd10a 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -144,6 +144,8 @@ Definition QuotType_clone (Q : Type) qT cT End QuotientDef. +Arguments repr_ofK {T qT}. + (****************************) (* Protecting some symbols. *) (****************************) @@ -195,7 +197,7 @@ Notation QuotType Q m := (@QuotTypePack _ Q m). Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id) (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope. -Arguments repr {T qT}. +Arguments repr {T qT} x. (************************) (* Exporting the theory *) @@ -227,6 +229,8 @@ Proof. by move=> Py x; rewrite -[x]reprK; apply: Py; rewrite reprK. Qed. End QuotTypeTheory. +Arguments reprK {T qT} x. + (*******************) (* About morphisms *) (*******************) @@ -657,6 +661,8 @@ Canonical EquivQuot.eqType. Canonical EquivQuot.choiceType. Canonical EquivQuot.eqQuotType. +Arguments EquivQuot.ereprK {D C CD DC eD encD}. + Notation "{eq_quot e }" := (@EquivQuot.type_of _ _ _ _ _ _ (Phantom (rel _) e)) : quotient_scope. Notation "x == y %[mod_eq r ]" := (x == y %[mod {eq_quot r}]) : quotient_scope. @@ -690,7 +696,7 @@ Variables (eD : equiv_rel D) (encD : encModRel CD DC eD). Notation eC := (encoded_equiv encD). Fact eq_quot_countMixin : Countable.mixin_of {eq_quot encD}. -Proof. exact: CanCountMixin (@EquivQuot.ereprK _ _ _ _ _ _). Qed. +Proof. exact: CanCountMixin EquivQuot.ereprK. Qed. Canonical eq_quot_countType := CountType {eq_quot encD} eq_quot_countMixin. End CountEncodingModuloRel. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 9154eb5..8f81155 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -336,7 +336,7 @@ Definition enum : seq (n.-tuple T) := Lemma enumP : Finite.axiom enum. Proof. -case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (@insubK _ _ _)). +case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (insubK _)). rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first. by rewrite isSome_insub; case: eqP=> // ->. elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm. |