Merge pull request #443 from pi8027/eqVneq

Refactoring and linting proofs especially in polydiv.v

5 files changed, 11 insertions, 11 deletions

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 0e3005d..4932148 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -166,7 +166,7 @@ have normD x y : le (norm (x + y)) (norm x + norm y).
     have [-> | nz_u u_ge0 v_ge0] := eqVneq u 0; first by rewrite add0r.
     by have /andP[]: lt 0 (u + v) by rewrite sposDl // /lt nz_u.
   have le_sqr u v: conj u = u -> le 0 v -> le (u ^+ 2) (v ^+ 2) -> le u v.
-    move=> Ru v_ge0; have [-> // | nz_u] := eqVneq u 0.
+    case: (eqVneq u 0) => [-> //|nz_u Ru v_ge0].
     have [u_gt0 | u_le0 _] := boolP (lt 0 u).
       by rewrite leB (leB u) subr_sqr mulrC addrC; apply: sposM; apply: sposDl.
     rewrite leB posD // posE normN -addr_eq0; apply/eqP.
@@ -931,7 +931,7 @@ Qed.
 
 Lemma dvdCP x y : reflect (exists2 z, z \in Cint & y = z * x) (x %| y)%C.
 Proof.
-rewrite unfold_in; have [-> | nz_x] := altP eqP.
+rewrite unfold_in; have [-> | nz_x] := eqVneq.
   by apply: (iffP eqP) => [-> | [z _ ->]]; first exists 0; rewrite ?mulr0.
 apply: (iffP idP) => [Zyx | [z Zz ->]]; last by rewrite mulfK.
 by exists (y / x); rewrite ?divfK.
@@ -990,7 +990,7 @@ Canonical dvdC_zmodPred x := ZmodPred (dvdC_zmod x).
 Lemma dvdC_nat (p n : nat) : (p %| n)%C = (p %| n)%N.
 Proof.
 rewrite unfold_in CintEge0 ?divr_ge0 ?invr_ge0 ?ler0n // !pnatr_eq0.
-have [-> | nz_p] := altP eqP; first by rewrite dvd0n.
+have [-> | nz_p] := eqVneq; first by rewrite dvd0n.
 apply/CnatP/dvdnP=> [[q def_q] | [q ->]]; exists q.
   by apply/eqP; rewrite -eqC_nat natrM -def_q divfK ?pnatr_eq0.
 by rewrite [num in num / _]natrM mulfK ?pnatr_eq0.
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 4824697..b41d5ec 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -582,7 +582,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
   pose abs v := if le 0 v then v else - v.
   have absN v: abs (- v) = abs v.
     rewrite /abs /le !(eq_sym 0) oppr_eq0 opprK posN.
-    have [-> | /posVneg/orP[v_gt0 | v_lt0]] := altP eqP; first by rewrite oppr0.
+    have [-> | /posVneg/orP[v_gt0 | v_lt0]] := eqVneq; first by rewrite oppr0.
       by rewrite v_gt0 /= -if_neg posNneg.
     by rewrite v_lt0 /= -if_neg -(opprK v) posN posNneg ?posN.
   have absE v: le 0 v -> abs v = v by rewrite /abs => ->.
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index be7dd6c..15d1d61 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -247,7 +247,7 @@ have: root (map_poly (nu \o QnC) (minPoly 1%AS x)) (nu (QnC x)).
   by rewrite fmorph_root root_minPoly.
 rewrite map_Qnum_poly ?minPolyOver // Hrs.
 rewrite [map_poly _ _](_:_ = \prod_(y <- map QnC rs) ('X - y%:P)); last first.
-  rewrite big_map rmorph_prod; apply eq_bigr => i _.
+  rewrite big_map rmorph_prod; apply: eq_bigr => i _.
   by rewrite rmorphB /= map_polyX map_polyC.
 rewrite root_prod_XsubC.
 by case/mapP => y _ ?; exists y.
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 86d3d39..b8acbd6 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -1311,7 +1311,7 @@ Definition subfx_poly_inv (q : {poly F}) : {poly F} :=
 Let subfx_poly_invE q : iotaPz (subfx_poly_inv q) = (iotaPz q)^-1.
 Proof.
 rewrite /subfx_poly_inv.
-have [-> | nzq] := altP eqP; first by rewrite rmorph0 invr0.
+have [-> | nzq] := eqVneq; first by rewrite rmorph0 invr0.
 rewrite [nth]lock -[_^-1]mul1r; apply: canRL (mulfK nzq) _; rewrite -rmorphM /=.
 have rz0: iotaPz (gdcop q p0) = 0.
   by apply/rootP; rewrite gdcop_map root_gdco ?map_poly_eq0 // p0z0 nzq.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 72cd0df..bbd6358 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -132,7 +132,7 @@ Qed.
 Lemma kHom_inv K E f : kHom K E f -> {in E, {morph f : x / x^-1}}.
 Proof.
 case/kHomP=> fM idKf x Ex.
-case (eqVneq x 0) => [-> | nz_x]; first by rewrite linear0 invr0 linear0.
+have [-> | nz_x] := eqVneq x 0; first by rewrite linear0 invr0 linear0.
 have fxV: f x * f x^-1 = 1 by rewrite -fM ?rpredV ?divff // idKf ?mem1v.
 have Ufx: f x \is a GRing.unit by apply/unitrPr; exists (f x^-1).
 by apply: (mulrI Ufx); rewrite divrr.
@@ -1014,8 +1014,8 @@ Lemma galois_connection K E (A : {set gal_of E}):
   (K <= E)%VS -> (A \subset 'Gal(E / K)) = (K <= fixedField A)%VS.
 Proof.
 move=> sKE; apply/idP/idP => [/fixedFieldS | /(galS E)].
-  by apply: subv_trans; apply galois_connection_subv.
-by apply: subset_trans; apply: galois_connection_subset.
+  exact/subv_trans/galois_connection_subv.
+exact/subset_trans/galois_connection_subset.
 Qed.
 
 Definition galTrace U V a := \sum_(x in 'Gal(V / U)) (x a).
@@ -1047,7 +1047,7 @@ Qed.
 
 Lemma galNormX n : {morph galNorm U V : a / a ^+ n}.
 Proof.
-move=> a; elim: n => [|n IHn]; first by apply: galNorm1.
+move=> a; elim: n => [|n IHn]; first exact: galNorm1.
 by rewrite !exprS galNormM IHn.
 Qed.
 
@@ -1309,7 +1309,7 @@ Qed.
 Lemma galois_fixedField K E :
   reflect (fixedField 'Gal(E / K) = K) (galois K E).
 Proof.
-apply (iffP idP) => [/and3P[sKE /separableP sepKE nKE] | fixedKE].
+apply: (iffP idP) => [/and3P[sKE /separableP sepKE nKE] | fixedKE].
   apply/eqP; rewrite eqEsubv galois_connection_subv ?andbT //.
   apply/subvP=> a /mem_fixedFieldP[Ea fixEa]; rewrite -adjoin_deg_eq1.
   have [r /allP Er splitKa] := normalFieldP nKE a Ea.