From 0b1ea03dafcf36880657ba910eec28ab78ccd018 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Thu, 13 Dec 2018 12:55:43 +0100 Subject: 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. --- mathcomp/algebra/ssrint.v | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'mathcomp/algebra/ssrint.v') 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. -- cgit v1.2.3