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/ssreflect/eqtype.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mathcomp/ssreflect/eqtype.v') diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index e9da3ec..f5d95e8 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -916,9 +916,9 @@ Hypothesis aR'E : forall x y, aR' x y = (x != y) && (aR x y). Hypothesis rR'E : forall x y, rR' x y = (x != y) && (rR x y). Let aRE x y : aR x y = (x == y) || (aR' x y). -Proof. by rewrite aR'E; case: (altP eqP) => //= ->; apply: aR_refl. Qed. +Proof. by rewrite aR'E; case: eqVneq => //= ->; apply: aR_refl. Qed. Let rRE x y : rR x y = (x == y) || (rR' x y). -Proof. by rewrite rR'E; case: (altP eqP) => //= ->; apply: rR_refl. Qed. +Proof. by rewrite rR'E; case: eqVneq => //= ->; apply: rR_refl. Qed. Section InDom. Variable D : pred aT. @@ -962,7 +962,7 @@ Lemma total_homo_mono_in : total aR -> {in D &, {mono f : x y / aR x y >-> rR x y}}. Proof. move=> aR_tot mf x y xD yD. -have [->|neq_xy] := altP (x =P y); first by rewrite ?eqxx ?aR_refl ?rR_refl. +have [->|neq_xy] := eqVneq x y; first by rewrite ?eqxx ?aR_refl ?rR_refl. have [xy|] := (boolP (aR x y)); first by rewrite rRE mf ?orbT// aR'E neq_xy. have /orP [->//|] := aR_tot x y. rewrite aRE eq_sym (negPf neq_xy) /= => /mf -/(_ yD xD). -- cgit v1.2.3