diff options
| author | Georges Gonthier | 2018-12-13 12:55:43 +0100 |
|---|---|---|
| committer | Georges Gonthier | 2018-12-13 12:55:43 +0100 |
| commit | 0b1ea03dafcf36880657ba910eec28ab78ccd018 (patch) | |
| tree | 60a84ff296299226d530dd0b495be24fd7675748 /mathcomp/fingroup/morphism.v | |
| parent | fa9b7b19fc0409f3fdfa680e08f40a84594e8307 (diff) | |
Adjust implicits of cancellation lemmas
Like injectivity lemmas, instances of cancellation lemmas (whose
conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or
`ocancel`) are passed to
generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should
not have trailing on-demand implicits _just before_ the `cancel`
conclusion, as these would be inconvenient to insert (requiring
essentially an explicit eta-expansion).
We therefore use `Arguments` or `Prenex Implicits` directives to make
all such arguments maximally inserted implicits. We don’t, however make
other arguments implicit, so as not to spoil direct instantiation of
the lemmas (in, e.g., `rewrite -[y](invmK injf)`).
We have also tried to do this with lemmas whose statement matches a
`cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern
unification will pick up `f = fun x => E[x]`).
We also adjusted implicits of a few stray injectivity
lemmas, and defined constants.
We provide a shorthand for reindexing a bigop with a permutation.
Finally we used the new implicit signatures to simplify proofs that
use injectivity or cancellation lemmas.
Diffstat (limited to 'mathcomp/fingroup/morphism.v')
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 8 |
1 files changed, 6 insertions, 2 deletions
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. + |