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/binomial.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/ssreflect/binomial.v') diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 1649a89..3a484a1 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -31,7 +31,7 @@ Qed. Lemma fact_prod n : n`! = \prod_(1 <= i < n.+1) i. Proof. elim: n => [|n IHn] //; first by rewrite big_nil. -by apply sym_equal; rewrite factS IHn // !big_add1 big_nat_recr //= mulnC. +by apply/esym; rewrite factS IHn // !big_add1 big_nat_recr //= mulnC. Qed. Lemma logn_fact p n : prime p -> logn p n`! = \sum_(1 <= k < n.+1) n %/ p ^ k. @@ -114,7 +114,7 @@ rewrite [mFpM _ _]mFp1 (bigD1 Fpn1) -?mFpA -/mFpM; last first. rewrite (reindex_onto vFp vFp) -/mFpM => [|i]; last by do 3!case/andP; auto. rewrite (eq_bigl (xpredD1 ltv Fp0)) => [|i]; last first. rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt. - rewrite andbA -ltnNge; symmetry; case: (altP eqP) => [->|ni0]. + rewrite andbA -ltnNge; symmetry; have [->|ni0] := eqVneq. by case: eqP => // E; rewrite ?E !andbF. by rewrite vFpK //eqxx vFp0. rewrite -{2}[mFp]/mFpM -[mFpM _ _]big_split -/mFpM. -- cgit v1.2.3