Merge pull request #443 from pi8027/eqVneq

Refactoring and linting proofs especially in polydiv.v

8 files changed, 19 insertions, 22 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 8bdbe60..53a933a 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1480,7 +1480,7 @@ Proof.
 move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *.
 case: (pickP P) => [i Pi | P0]; last first.
   by rewrite !big_pred0 // => j; rewrite P0.
-rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eq_refl //=; congr (_ * _).
+rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eqxx //=; congr (_ * _).
 rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. 
 apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK.
 by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K.
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.
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).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 6f7c5b5..cd1a1bb 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -243,7 +243,7 @@ Lemma in_setT x : x \in setTfor (Phant T).
 Proof. by rewrite in_set. Qed.
 
 Lemma eqsVneq A B : eq_xor_neq A B (B == A) (A == B).
-Proof. by apply: eqVneq. Qed.
+Proof. exact: eqVneq. Qed.
 
 Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB.
 Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed.
@@ -862,7 +862,7 @@ Proof. by case/orP; apply: subset_trans; rewrite (subsetIl, subsetIr). Qed.
 
 Lemma subsetI A B C : (A \subset B :&: C) = (A \subset B) && (A \subset C).
 Proof.
-rewrite !(sameP setIidPl eqP) setIA; have [-> //| ] := altP (A :&: B =P A).
+rewrite !(sameP setIidPl eqP) setIA; have [-> //|] := eqVneq (A :&: B) A.
 by apply: contraNF => /eqP <-; rewrite -setIA -setIIl setIAC.
 Qed.
 
@@ -1428,7 +1428,7 @@ Proof.
 move=> injh; pose hA := mem (image h A).
 have [x0 Ax0 | A0] := pickP A; last first.
   by rewrite !big_pred0 // => x; apply/imsetP=> [[i]]; rewrite unfold_in A0.
-rewrite (eq_bigl hA) => [|j]; last by apply/imsetP/imageP.
+rewrite (eq_bigl hA) => [|j]; last exact/imsetP/imageP.
 pose h' j := if insub j : {? j | hA j} is Some u then iinv (svalP u) else x0.
 rewrite (reindex_onto h h') => [|j hAj]; rewrite {}/h'; last first.
   by rewrite (insubT hA hAj) f_iinv.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 5a42c80..14d623f 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -694,7 +694,7 @@ Lemma eq_subxx A B : A =i B -> A \subset B.
 Proof. by move/eq_subset->. Qed.
 
 Lemma subset_predT A : A \subset T.
-Proof. by apply/subsetP. Qed.
+Proof. exact/subsetP. Qed.
 
 Lemma predT_subset A : T \subset A -> forall x, x \in A.
 Proof. by move/subsetP=> allA x; apply: allA. Qed.
@@ -1240,7 +1240,7 @@ Lemma image_f A x : x \in A -> f x \in image f A.
 Proof. by move=> Ax; apply/imageP; exists x. Qed.
 
 Lemma codom_f x : f x \in codom f.
-Proof. by apply: image_f. Qed.
+Proof. exact: image_f. Qed.
 
 Lemma image_codom A : {subset image f A <= codom f}.
 Proof. by move=> _ /imageP[x _ ->]; apply: codom_f. Qed.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 718eea5..797dd0d 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -2404,7 +2404,7 @@ Lemma comparable_ltgtP x y : x >=< y ->
   compare x y (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
 Proof.
 rewrite />=<%O !le_eqVlt [y == x]eq_sym.
-have := (altP (x =P y), (boolP (x < y), boolP (y < x))).
+have := (eqVneq x y, (boolP (x < y), boolP (y < x))).
 move=> [[->//|neq_xy /=] [[] xy [] //=]] ; do ?by rewrite ?ltxx; constructor.
   by rewrite ltxx in xy.
 by rewrite le_gtF // ltW.
@@ -3065,7 +3065,7 @@ Variant eq0_xor_gt0 x : bool -> bool -> Set :=
   | POsNotEq0 : 0 < x -> eq0_xor_gt0 x false true.
 
 Lemma posxP x : eq0_xor_gt0 x (x == 0) (0 < x).
-Proof. by rewrite lt0x; have [] := altP eqP; constructor; rewrite ?lt0x. Qed.
+Proof. by rewrite lt0x; have [] := eqVneq; constructor; rewrite ?lt0x. Qed.
 
 Canonical join_monoid := Monoid.Law (@joinA _ _) join0x joinx0.
 Canonical join_comoid := Monoid.ComLaw (@joinC _ _).
@@ -3430,7 +3430,7 @@ Proof. by rewrite subUx subxx join0x. Qed.
 
 Lemma disj_le x y : x `&` y == 0 -> x <= y = (x == 0).
 Proof.
-have [->|x_neq0] := altP (x =P 0); first by rewrite le0x.
+have [->|x_neq0] := eqVneq x 0; first by rewrite le0x.
 by apply: contraTF => lexy; rewrite (meet_idPl _).
 Qed.
 
@@ -3826,10 +3826,7 @@ Let T_total_porderType : porderType tt :=
   POrderType tt T (LtPOrderMixin (le_def m) (lt_irr m) (@lt_trans _ m)).
 
 Fact le_total : total (le m).
-Proof.
-move=> x y; rewrite !le_def (eq_sym y).
-by case: (altP eqP); last exact: lt_total.
-Qed.
+Proof. by move=> x y; rewrite !le_def; case: eqVneq; last exact: lt_total. Qed.
 
 Let T_total_distrLatticeType : distrLatticeType tt :=
   DistrLatticeType T_total_porderType
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index d9ab11c..2790aa8 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -368,7 +368,7 @@ Proof.
 elim: s => [| h s]; first by case: ifP.
 rewrite mem2_cons => ->.
 do 2 rewrite inE (fun_if subseq) !if_arg !sub1seq /=.
-by case: eqVneq => [->|]; case: eqVneq.
+by have [->|] := eqVneq; case: eqVneq.
 Qed.
 
 Variant split2r x y : seq T -> Type :=
@@ -916,7 +916,7 @@ Let le_lex_transitive x sT : transitive (le_lex x sT).
 Proof.
 move=> ? ? ? /andP [xy /implyP xy'] /andP [yz /implyP yz'].
 rewrite /= (leT_tr xy yz) /=; apply/implyP => zx.
-by apply/ltn_trans: (xy' (leT_tr yz zx)) (yz' (leT_tr zx xy)).
+exact: ltn_trans (xy' (leT_tr yz zx)) (yz' (leT_tr zx xy)).
 Qed.
 
 Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 0ddd382..5b9d047 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -429,7 +429,7 @@ Qed.
 Lemma set_set_nth s n1 y1 n2 y2 (s2 := set_nth s n2 y2) :
   set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1.
 Proof.
-have [-> | ne_n12] := altP eqP.
+have [-> | ne_n12] := eqVneq.
   apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn.
   by do 2!rewrite !nth_set_nth /=; case: eqP.
 apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA.
@@ -2239,7 +2239,7 @@ Lemma nth_index_map s x0 x :
   {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x.
 Proof.
 elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //.
-move: s_x; rewrite inE; case: eqVneq => [-> | _] //=; apply: IHs.
+move: s_x; rewrite inE; have [-> // | _] := eqVneq; apply: IHs.
 by apply: sub_in2 inj_f => z; apply: predU1r.
 Qed.