From 181e9e94e04f45e0deb231246e1783c48be4f99d Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Wed, 21 Feb 2018 23:07:25 -0800 Subject: Change Implicit Arguments to Arguments in fingroup --- mathcomp/fingroup/action.v | 38 +++++++++---------- mathcomp/fingroup/automorphism.v | 2 +- mathcomp/fingroup/fingroup.v | 80 ++++++++++++++++++++-------------------- mathcomp/fingroup/gproduct.v | 20 +++++----- mathcomp/fingroup/morphism.v | 26 ++++++------- mathcomp/fingroup/perm.v | 6 +-- mathcomp/fingroup/quotient.v | 4 +- 7 files changed, 88 insertions(+), 88 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index ecfa6ea..6478c81 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -287,7 +287,7 @@ Variables (aT : finGroupType) (D : {set aT}) (rT : finType) (to : action D rT). Implicit Types (a : aT) (x y : rT) (A B : {set aT}) (S T : {set rT}). Lemma act_inj : left_injective to. Proof. by case: to => ? []. Qed. -Implicit Arguments act_inj []. +Arguments act_inj : clear implicits. Lemma actMin x : {in D &, act_morph to x}. Proof. by case: to => ? []. Qed. @@ -486,17 +486,17 @@ End RawAction. (* Warning: this directive depends on names of bound variables in the *) (* definition of injective, in ssrfun.v. *) -Implicit Arguments act_inj [[aT] [D] [rT] x1 x2]. +Arguments act_inj {aT D rT} to _ [x1 x2]. Notation "to ^*" := (set_action to) : action_scope. -Implicit Arguments orbitP [aT D rT to A x y]. -Implicit Arguments afixP [aT D rT to A x]. -Implicit Arguments afix1P [aT D rT to a x]. +Arguments orbitP [aT D rT to A x y]. +Arguments afixP [aT D rT to A x]. +Arguments afix1P [aT D rT to a x]. Prenex Implicits orbitP afixP afix1P. -Implicit Arguments reindex_astabs [aT D rT vT idx op S F]. -Implicit Arguments reindex_acts [aT D rT vT idx op S A a F]. +Arguments reindex_astabs [aT D rT] to [vT idx op S] a [F]. +Arguments reindex_acts [aT D rT] to [vT idx op S A a F]. Section PartialAction. (* Lemmas that require a (partial) group domain. *) @@ -879,9 +879,9 @@ End PartialAction. Arguments Scope orbit_transversal [_ group_scope _ action_scope group_scope group_scope]. -Implicit Arguments orbit_in_eqP [aT D rT to G x y]. -Implicit Arguments orbit1P [aT D rT to G x]. -Implicit Arguments contra_orbit [aT D rT x y]. +Arguments orbit_in_eqP [aT D rT to G x y]. +Arguments orbit1P [aT D rT to G x]. +Arguments contra_orbit [aT D rT] to G [x y]. Prenex Implicits orbit_in_eqP orbit1P. Notation "''C' ( S | to )" := (astab_group to S) : Group_scope. @@ -1008,7 +1008,7 @@ Proof. apply: (iffP idP) => [nSA x|nSA]; first exact: acts_act. by apply/subsetP=> a Aa; rewrite !inE; apply/subsetP=> x; rewrite inE nSA. Qed. -Implicit Arguments actsP [A S]. +Arguments actsP [A S]. Lemma setact_orbit A x b : to^* (orbit to A x) b = orbit to (A :^ b) (to x b). Proof. @@ -1137,13 +1137,13 @@ Qed. End TotalActions. -Implicit Arguments astabP [aT rT to S a]. -Implicit Arguments orbit_eqP [aT rT to G x y]. -Implicit Arguments astab1P [aT rT to x a]. -Implicit Arguments astabsP [aT rT to S a]. -Implicit Arguments atransP [aT rT to G S]. -Implicit Arguments actsP [aT rT to A S]. -Implicit Arguments faithfulP [aT rT to A S]. +Arguments astabP [aT rT to S a]. +Arguments orbit_eqP [aT rT to G x y]. +Arguments astab1P [aT rT to x a]. +Arguments astabsP [aT rT to S a]. +Arguments atransP [aT rT to G S]. +Arguments actsP [aT rT to A S]. +Arguments faithfulP [aT rT to A S]. Prenex Implicits astabP orbit_eqP astab1P astabsP atransP actsP faithfulP. Section Restrict. @@ -1637,7 +1637,7 @@ Proof. by apply/permP=> x; rewrite permE. Qed. End PermAction. -Implicit Arguments perm_act1P [rT a]. +Arguments perm_act1P [rT a]. Prenex Implicits perm_act1P. Notation "'P" := (perm_action _) (at level 8) : action_scope. diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index 8813b45..e727aba 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -198,7 +198,7 @@ Qed. End MakeAut. -Implicit Arguments morphim_fixP [gT G f]. +Arguments morphim_fixP [gT G f]. Prenex Implicits aut morphim_fixP. Section AutIsom. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index dd57af4..5afc3c7 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -493,7 +493,7 @@ Qed. End PreGroupIdentities. Hint Resolve commute1. -Implicit Arguments invg_inj [T]. +Arguments invg_inj [T]. Prenex Implicits commute invgK invg_inj. Section GroupIdentities. @@ -641,11 +641,11 @@ Ltac gsimpl := autorewrite with gsimpl; try done. Definition gsimp := (mulg1 , mul1g, (invg1, @invgK), (mulgV, mulVg)). Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))). -Implicit Arguments mulgI [T]. -Implicit Arguments mulIg [T]. -Implicit Arguments conjg_inj [T]. -Implicit Arguments commgP [T x y]. -Implicit Arguments conjg_fixP [T x y]. +Arguments mulgI [T]. +Arguments mulIg [T]. +Arguments conjg_inj [T]. +Arguments commgP [T x y]. +Arguments conjg_fixP [T x y]. Prenex Implicits conjg_fixP commgP. Section Repr. @@ -672,7 +672,7 @@ Proof. by rewrite /repr; case: pickP => [x|_]; rewrite !inE. Qed. End Repr. -Implicit Arguments mem_repr [gT A]. +Arguments mem_repr [gT A]. Section BaseSetMulDef. (* We only assume a baseFinGroupType to allow this construct to be iterated. *) @@ -946,9 +946,9 @@ Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed. End BaseSetMulProp. -Implicit Arguments set1gP [gT x]. -Implicit Arguments mulsgP [gT A B x]. -Implicit Arguments prodsgP [gT I P A x]. +Arguments set1gP [gT x]. +Arguments mulsgP [gT A B x]. +Arguments prodsgP [gT I P A x]. Section GroupSetMulProp. (* Constructs that need a finGroupType *) @@ -1304,11 +1304,11 @@ Definition order x := #|cycle x|. End GroupSetMulProp. -Implicit Arguments lcosetP [gT A x y]. -Implicit Arguments lcosetsP [gT A B C]. -Implicit Arguments rcosetP [gT A x y]. -Implicit Arguments rcosetsP [gT A B C]. -Implicit Arguments group_setP [gT A]. +Arguments lcosetP [gT A x y]. +Arguments lcosetsP [gT A B C]. +Arguments rcosetP [gT A x y]. +Arguments rcosetsP [gT A B C]. +Arguments group_setP [gT A]. Prenex Implicits group_set mulsgP set1gP. Prenex Implicits lcosetP lcosetsP rcosetP rcosetsP group_setP. @@ -1858,15 +1858,15 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope. Prenex Implicits subg sgval subg_of. Bind Scope group_scope with subg_of. -Implicit Arguments trivgP [gT G]. -Implicit Arguments trivGP [gT G]. -Implicit Arguments lcoset_eqP [gT G x y]. -Implicit Arguments rcoset_eqP [gT G x y]. -Implicit Arguments mulGidPl [gT G H]. -Implicit Arguments mulGidPr [gT G H]. -Implicit Arguments comm_group_setP [gT G H]. -Implicit Arguments class_eqP [gT G x y]. -Implicit Arguments repr_classesP [gT G xG]. +Arguments trivgP [gT G]. +Arguments trivGP [gT G]. +Arguments lcoset_eqP [gT G x y]. +Arguments rcoset_eqP [gT G x y]. +Arguments mulGidPl [gT G H]. +Arguments mulGidPr [gT G H]. +Arguments comm_group_setP [gT G H]. +Arguments class_eqP [gT G x y]. +Arguments repr_classesP [gT G xG]. Prenex Implicits trivgP trivGP lcoset_eqP rcoset_eqP comm_group_setP class_eqP. Section GroupInter. @@ -2396,11 +2396,11 @@ Qed. End GeneratedGroup. -Implicit Arguments gen_prodgP [gT A x]. -Implicit Arguments joing_idPl [gT G A]. -Implicit Arguments joing_idPr [gT A G]. -Implicit Arguments mulGsubP [gT K H G]. -Implicit Arguments joing_subP [gT A B G]. +Arguments gen_prodgP [gT A x]. +Arguments joing_idPl [gT G A]. +Arguments joing_idPr [gT A G]. +Arguments mulGsubP [gT K H G]. +Arguments joing_subP [gT A B G]. Section Cycles. @@ -2524,7 +2524,7 @@ Proof. suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP. by rewrite eqEcard cardJg leqnn andbT inE. Qed. -Implicit Arguments normP [x A]. +Arguments normP [x A]. Lemma group_set_normaliser A : group_set 'N(A). Proof. @@ -2539,7 +2539,7 @@ Proof. apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //. by apply/normP; apply: nBA. Qed. -Implicit Arguments normsP [A B]. +Arguments normsP [A B]. Lemma memJ_norm x y A : x \in 'N(A) -> (y ^ x \in A) = (y \in A). Proof. by move=> Nx; rewrite -{1}(normP Nx) memJ_conjg. Qed. @@ -2987,13 +2987,13 @@ End SubAbelian. End Normaliser. -Implicit Arguments normP [gT x A]. -Implicit Arguments centP [gT x A]. -Implicit Arguments normsP [gT A B]. -Implicit Arguments cent1P [gT x y]. -Implicit Arguments normalP [gT A B]. -Implicit Arguments centsP [gT A B]. -Implicit Arguments commG1P [gT A B]. +Arguments normP [gT x A]. +Arguments centP [gT A x]. +Arguments normsP [gT A B]. +Arguments cent1P [gT x y]. +Arguments normalP [gT A B]. +Arguments centsP [gT A B]. +Arguments commG1P [gT A B]. Prenex Implicits normP normsP cent1P normalP centP centsP commG1P. @@ -3091,6 +3091,6 @@ Notation "[ 'min' A 'of' G | gP & gQ ]" := [min A of G | gP && gQ] : group_scope. Notation "[ 'min' G | gP & gQ ]" := [min G | gP && gQ] : group_scope. -Implicit Arguments mingroupP [gT gP G]. -Implicit Arguments maxgroupP [gT gP G]. +Arguments mingroupP [gT gP G]. +Arguments maxgroupP [gT gP G]. Prenex Implicits mingroupP maxgroupP. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index cd129f2..dc16021 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -96,10 +96,10 @@ Arguments Scope complements_to_in [_ group_scope group_scope]. Arguments Scope splits_over [_ group_scope group_scope]. Arguments Scope remgr [_ group_scope group_scope group_scope]. Arguments Scope divgr [_ group_scope group_scope group_scope]. -Implicit Arguments partial_product []. -Implicit Arguments semidirect_product []. -Implicit Arguments central_product []. -Implicit Arguments direct_product []. +Arguments partial_product : clear implicits. +Arguments semidirect_product : clear implicits. +Arguments central_product : clear implicits. +Arguments direct_product : clear implicits. Notation pprod := (partial_product _). Notation sdprod := (semidirect_product _). Notation cprod := (central_product _). @@ -870,11 +870,11 @@ Qed. End InternalProd. -Implicit Arguments complP [gT H A B]. -Implicit Arguments splitsP [gT A B]. -Implicit Arguments sdprod_normal_complP [gT K H G]. -Implicit Arguments dprodYP [gT K H]. -Implicit Arguments bigdprodYP [gT I P F]. +Arguments complP [gT H A B]. +Arguments splitsP [gT B A]. +Arguments sdprod_normal_complP [gT G K H]. +Arguments dprodYP [gT K H]. +Arguments bigdprodYP [gT I P F]. Section MorphimInternalProd. @@ -1703,5 +1703,5 @@ Qed. End DirprodIsom. -Implicit Arguments mulgmP [gT H1 H2 G]. +Arguments mulgmP [gT H1 H2 G]. Prenex Implicits mulgm mulgmP. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 2a70706..315358b 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -118,8 +118,8 @@ Notation "[ 'morphism' D 'of' f ]" := Notation "[ 'morphism' 'of' f ]" := (clone_morphism (@Morphism _ _ _ f)) (at level 0, format "[ 'morphism' 'of' f ]") : form_scope. -Implicit Arguments morphimP [aT rT D A f y]. -Implicit Arguments morphpreP [aT rT D R f x]. +Arguments morphimP [aT rT D A y f]. +Arguments morphpreP [aT rT D R x f]. Prenex Implicits morphimP morphpreP. (* Domain, image, preimage, kernel, using phantom types to infer the domain. *) @@ -873,7 +873,7 @@ Notation "f @* G" := (morphim_group (MorPhantom f) G) : Group_scope. Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope. Notation "f @: D" := (morph_dom_group f D) : Group_scope. -Implicit Arguments injmP [aT rT D f]. +Arguments injmP [aT rT D f]. Section IdentityMorphism. @@ -969,8 +969,8 @@ End RestrictedMorphism. Arguments Scope restrm [_ _ group_scope group_scope _ group_scope]. Prenex Implicits restrm. -Implicit Arguments restrmP [aT rT D A]. -Implicit Arguments domP [aT rT D A]. +Arguments restrmP [aT rT A D]. +Arguments domP [aT rT A D]. Section TrivMorphism. @@ -995,7 +995,7 @@ Proof. by apply/setIidPl/subsetP=> x _; rewrite !inE /=. Qed. End TrivMorphism. Arguments Scope trivm [_ _ group_scope group_scope]. -Implicit Arguments trivm [[aT] [rT]]. +Arguments trivm {aT rT}. (* The composition of two morphisms is a Canonical morphism instance. *) Section MorphismComposition. @@ -1259,7 +1259,7 @@ End Defs. Infix "\isog" := isog. -Implicit Arguments isom_isog [A B D]. +Arguments isom_isog [A B D]. (* The real reflection properties only hold for true groups and morphisms. *) @@ -1330,11 +1330,11 @@ Arguments Scope morphic [_ _ group_scope _]. Arguments Scope misom [_ _ group_scope group_scope _]. Arguments Scope isog [_ _ group_scope group_scope]. -Implicit Arguments morphicP [aT rT A f]. -Implicit Arguments misomP [aT rT A B f]. -Implicit Arguments isom_isog [aT rT A B D]. -Implicit Arguments isomP [aT rT G H f]. -Implicit Arguments isogP [aT rT G H]. +Arguments morphicP [aT rT A f]. +Arguments misomP [aT rT A B f]. +Arguments isom_isog [aT rT A B D]. +Arguments isomP [aT rT G H f]. +Arguments isogP [aT rT G H]. Prenex Implicits morphic morphicP morphm isom isog isomP misomP isogP. Notation "x \isog y":= (isog x y). @@ -1483,7 +1483,7 @@ Arguments Scope homg [_ _ group_scope group_scope]. Notation "G \homg H" := (homg G H) (at level 70, no associativity) : group_scope. -Implicit Arguments homgP [rT aT C D]. +Arguments homgP [rT aT C D]. (* Isomorphism between a group and its subtype. *) diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 6d9abdc..bbf4363 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -128,7 +128,7 @@ Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed. Lemma perm_inj s : injective s. Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed. -Implicit Arguments perm_inj []. +Arguments perm_inj : clear implicits. Hint Resolve perm_inj. Lemma perm_onto s : codom s =i predT. @@ -461,7 +461,7 @@ Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y). Proof. by rewrite -[_ y]mulg1 odd_mul_tperm odd_perm1 addbF. Qed. Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT]. -Implicit Arguments dpair [eT]. +Arguments dpair [eT]. Lemma prod_tpermP s : {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}. @@ -503,7 +503,7 @@ Proof. by rewrite !odd_permM odd_permV addbC addbK. Qed. End PermutationParity. Coercion odd_perm : perm_type >-> bool. -Implicit Arguments dpair [eT]. +Arguments dpair [eT]. Prenex Implicits pcycle dpair pcycles aperm. Section LiftPerm. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 242b4b7..99d1aef 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -751,8 +751,8 @@ Qed. End EqIso. -Implicit Arguments qisom_inj [gT G H]. -Implicit Arguments morphim_qisom_inj [gT G H]. +Arguments qisom_inj [gT G H]. +Arguments morphim_qisom_inj [gT G H]. Section FirstIsomorphism. -- cgit v1.2.3