From a06d61a8e226eeabc52f1a22e469dca1e6077065 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 29 Nov 2019 01:19:33 +0900 Subject: Refactoring and linting especially polydiv - Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`: The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and introduces a hypothesis in the form of `x != y` in the second case. Thus, `case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms can be replaced with `case: eqVneq`, `case: (eqVneq x)` and `case: (eqVneq x y)` respectively. This replacement slightly simplifies and reduces proof scripts. - use `have [] :=` rather than `case` if it is better. - `by apply:` -> `exact:`. - `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`. - `move/lem1; move/lem2` -> `move/lem1/lem2`. - Remove `GRing.` prefix if applicable. - `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`. --- mathcomp/solvable/cyclic.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/solvable/cyclic.v') diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index e6d3afb..d82009b 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -587,7 +587,7 @@ Variable u : {unit 'Z_#[a]}. Lemma injm_cyclem : 'injm (cyclem (val u) a). Proof. apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn. -case: (eqVneq a 1) => [a1 | nta]; first by rewrite a1 cycle1 inE in ax. +have [a1 | nta] := eqVneq a 1; first by rewrite a1 cycle1 inE in ax. rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-. by rewrite dvdn_gcd {2}Zp_cast ?order_gt1 // order_dvdG. Qed. @@ -616,7 +616,7 @@ Canonical Zp_unit_morphism := Morphism Zp_unitmM. Lemma injm_Zp_unitm : 'injm Zp_unitm. Proof. -case: (eqVneq a 1) => [a1 | nta]. +have [a1 | nta] := eqVneq a 1. by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1. apply/subsetP=> /= u /morphpreP[_ /set1P/= um1]. have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1. -- cgit v1.2.3