cleaning

ecc_classic/cyclic_code.v

@@ -142,7 +142,7 @@ case: ifPn => [/eqP ->|i0]; last rewrite subr0.
   case: insubP => //= j _ j0.
   rewrite mxE unlock ffunE /= -val_eqE j0 /= j0 eqxx; congr (- x _ _).
   by apply val_inj => /=; rewrite inordK.
-case/boolP : (i == n.+1) => [/eqP ->|in0].
+have [->|in0] := eqVneq i n.+1.
   rewrite mulr1 2!coef_rVpoly /=.
   case: insubP => /= [j _ j0|]; last by rewrite ltnS leqnn.
   case: insubP => /= [?|_]; first by rewrite ltnn.
@@ -416,16 +416,16 @@ Lemma scale_cgen (g' : 'rV[F]_n) (HC : not_trivial C) :
 Proof.
 move=> Hg'.
 set g := canonical_cgen HC.
-case/boolP : (g == g') => [/eqP ->|gg'].
-  exists 1; by rewrite scale1r oner_neq0 eqxx.
+have [->|gg'] := eqVneq g g'.
+  by exists 1; rewrite scale1r oner_neq0 eqxx.
 have size_g := canonical_cgen_lowest_size HC.
 rewrite -/g in size_g.
 pose k := lead_coef (rVpoly g') / lead_coef (rVpoly g).
 pose g'' : {poly F} := rVpoly g' - k *: rVpoly g.
 have size_g' : size (rVpoly g') = size (rVpoly g) by rewrite size_g; apply size_lowest.
-case/boolP : (k == 0) => k0.
+have [k0|k0] := eqVneq k 0.
   exfalso.
-  move: k0.
+  move/eqP: k0.
   rewrite /k mulf_eq0 invr_eq0 2!lead_coef_eq0.
   case/orP; rewrite rVpoly0; apply/negP.
   by case/and3P : Hg'.
@@ -434,10 +434,11 @@ have size_g'' : size g'' < size (rVpoly g).
   rewrite /g'' -size_g'; apply size_sub => //.
   apply/eqP; rewrite rVpoly0; by case/and3P : Hg'.
   rewrite lreg_size ?size_g' //; by apply/GRing.lregP.
-  rewrite lead_coefZ /k -mulrA mulVr ?mulr1 // unitfE lead_coef_eq0 rVpoly0; by case/and3P : (canonical_cgenP HC).
+  rewrite lead_coefZ /k -mulrA mulVr ?mulr1 // unitfE lead_coef_eq0 rVpoly0.
+  by case/and3P : (canonical_cgenP HC).
 have g''C : poly_rV g'' \in C.
   rewrite /g'' linearD /= linearN /= linearZ /= (proj2 (Lcode0.aclosed C)) // ?rVpolyK; first by case/and3P : Hg'.
-  rewrite Lcode0.oclosed // Lcode0.sclosed //; by case/and3P : (canonical_cgenP HC).
+  by rewrite Lcode0.oclosed // Lcode0.sclosed //; case/and3P : (canonical_cgenP HC).
 have g''0 : g'' = 0.
   apply/eqP/negPn/negP => abs.
   case/and3P: (canonical_cgenP HC) => _ _ /forallP/(_ (poly_rV g'')).
@@ -467,8 +468,7 @@ Lemma divide_codeword (p : {poly F}) : poly_rV (`[ p ]_n) \in C ->
   forall g, g \in 'cgen[C] -> rVpoly g %| p.
 Proof.
 move=> pC g Hg.
-case/boolP : (p == 0) => [/eqP -> | p0].
-  by rewrite dvdp0.
+have [->|p0] := eqVneq p 0; first by rewrite dvdp0.
 move/eqP: (divp_eq p (rVpoly g)); rewrite addrC -subr_eq => /eqP.
 move/(congr1 (fun x => `[ x ]_n))/esym.
 have size_rem : size (p %% rVpoly g) < size (rVpoly g).
@@ -585,7 +585,7 @@ case/dvdpP => /= i ig.
 split.
   by rewrite inE linear0 dvdp0.
 move=> k a b; rewrite !inE => ga gb.
-case/boolP : (k == 0) => [/eqP ->|k0]; first by rewrite scale0r add0r.
+have [->|k0] := eqVneq k 0; first by rewrite scale0r add0r.
 by rewrite linearD linearZ /= dvdp_addr // dvdpZr.
 Qed.
 

ecc_classic/decoding.v

@@ -3,10 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm.
 From mathcomp Require Import zmodp matrix vector order.
 From mathcomp Require Import lra ring mathcomp_extra Rstruct reals.
-From mathcomp Require ssrnum.
-(*Require Import Reals.*)
-Require Import (*ssrR*) realType_ext (*Reals_ext*) ssr_ext ssralg_ext f2 fdist bigop_ext.
-Require Import proba.
+Require Import realType_ext ssr_ext ssralg_ext f2 bigop_ext fdist proba.
 Require Import channel_code channel binary_symmetric_channel hamming pproba.
 
 (******************************************************************************)
@@ -243,7 +240,7 @@ Lemma ML_err_rate x1 x2 y : repair y = Some x1 ->
   x2 \in C -> W ``(y | x2) <= W ``(y | x1).
 Proof.
 move=> Hx1 Hx2.
-case/boolP : (W ``(y | x2) == 0) => [/eqP -> //| Hcase].
+have [->//|Hcase] := eqVneq (W ``(y | x2)) 0.
 have PWy : receivable_prop P W y.
   apply/existsP; exists x2.
   by rewrite Hcase andbT fdist_uniform_supp_neq0 inE.
@@ -284,7 +281,7 @@ apply ler_sum => /= tb _.
 rewrite (eq_bigl (fun m => phi tb == Some m)); last by move=> m; rewrite inE.
 rewrite [leRHS](eq_bigl (fun m => dec tb == Some m)); last by move=> m; rewrite inE.
 (* show that phi_ML succeeds more often than phi *)
-have [dectb_None|dectb_Some] := boolP (dec tb == None).
+have [dectb_None|dectb_Some] := eqVneq (dec tb) None.
   case/boolP : (receivable_prop P W tb) => [Hy|Htb].
     case: (ML_dec (mkReceivable Hy)) => [m' [tb_m']].
     by move: dectb_None; rewrite {1}/dec {1}ffunE tb_m'.
@@ -295,7 +292,7 @@ have [dectb_None|dectb_Some] := boolP (dec tb == None).
     move/subsetP : enc_img; apply; apply/imsetP; by exists m.
   rewrite (eq_bigr (fun=> 0)); last by move=> m _; rewrite W_tb.
   by rewrite big1 //; apply sumr_ge0.
-case/boolP : (phi tb == None) => [/eqP ->|phi_tb].
+have [->|phi_tb] := eqVneq (phi tb) None.
   by rewrite big_pred0 //; apply sumr_ge0.
 have [m1 Hm1] : exists m', dec tb = Some m' by destruct (dec tb) => //; exists s.
 have [m2 Hm2] : exists m', phi tb = Some m' by destruct (phi tb) => //; exists s.
@@ -374,7 +371,6 @@ Qed.
 End MD_ML_decoding.
 
 Section MAP_decoding.
-
 Variables (A : finFieldType) (B : finType) (W : `Ch(A, B)).
 Variables (n : nat) (C : {vspace 'rV[A]_n}).
 Variable dec : decT B ('rV[A]_n) n.
@@ -416,9 +412,7 @@ under [in X in _ = X / _ -> _]eq_bigr.
   rewrite fdist_uniform_supp_in; last by rewrite inE.
   over.
 move=> H.
-rewrite -bigmaxR_distrr in H; last first.
-  apply/ltW.
-  exact: Hunpos.
+rewrite -bigmaxR_distrr in H; last exact/ltW/Hunpos.
 exists m; split; first exact tbm.
 rewrite ffunE in H.
 set x := (X in _ * _ / X) in H.

ecc_classic/grs.v

@@ -26,8 +26,7 @@ Module GRS.
 
 Section GRS_def.
 
-Variables (n (*q*) : nat).
-(*Hypothesis nq : n <= q.*)
+Variables (n : nat).
 Variable (F : finFieldType).
 Variable a : 'rV[F]_n.
 Hypothesis a_inj : injective [ffun i => a``_i]. (* pairwise distinct *)
@@ -211,14 +210,14 @@ Definition GRS_mod r : {poly F} :=
 Lemma GRS_key_equation r :
   Sigma * GRS.syndromep a b r y = Omega + GRS_mod r * 'X^r.
 Proof.
-case/boolP : (r == O) => r0.
-  rewrite (eqP r0) mulr1.
+have [r0|r0] := eqVneq r 0.
+  rewrite r0 mulr1.
   rewrite /GRS.syndromep poly_def big_ord0 mulr0.
   apply/eqP; rewrite eq_sym addr_eq0; apply/eqP.
   rewrite /GRS_mod /Omega /erreval -sumrN; apply eq_bigr => j jy.
   rewrite expr0 mulr1 mulrN opprK [in RHS]mulrC mulrC -!scalerA.
   rewrite -scalerAl mulrC mul_polyC; congr (_ *: (_ *: _)).
-  apply eq_bigl => k; by rewrite in_setD1 andbC.
+  by apply eq_bigl => k; rewrite in_setD1 andbC.
 rewrite /GRS_mod big_distrl /= /Omega /erreval -big_split /=.
 rewrite GRS.syndromepE big_distrr /=.
 apply eq_bigr => i iy.

ecc_classic/hamming_code.v

@@ -1,7 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm zmodp.
-From mathcomp Require Import matrix mxalgebra vector ring.
+From mathcomp Require Import all_ssreflect ssralg ssrnum fingroup finalg perm.
+From mathcomp Require Import zmodp matrix mxalgebra vector ring.
 From mathcomp Require Import Rstruct reals.
 Require Import realType_ext ssr_ext ssralg_ext f2 linearcode natbin hamming.
 Require Import bigop_ext fdist proba channel channel_code decoding.
@@ -47,7 +47,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Import GRing.Theory.
+Import GRing.Theory Order.POrderTheory.
 Local Open Scope ring_scope.
 
 Module Hamming.
@@ -120,8 +120,8 @@ Proof.
 move=> /wH_2[i [j [Hij [Hi [Hj Hk]]]]].
 rewrite /syndrome mulmx_sum_col (bigID (pred1 i)) /= big_pred1_eq /=.
 rewrite (bigID (pred1 j)) /= (eq_bigl (pred1 j)) /=; last first.
-  move=> a /=; case/boolP : (a == j) => aj; last by rewrite andbC.
-  rewrite andbC /= (eqP aj) eq_sym; by apply/eqP.
+  move=> a /=; have [aj|aj] := eqVneq a j; last by rewrite andbC.
+  rewrite andbC /= aj eq_sym; by apply/eqP.
 rewrite big_pred1_eq /= (eq_bigr (fun=> 0)) /=; last first.
   move=> a /andP[X1 X2].
   rewrite mxE Hk ?scale0r //; (apply/eqP; by rewrite eq_sym).
@@ -272,21 +272,22 @@ rewrite /alt_hamming_err.
 destruct (nat_of_rV _); first by rewrite wH0.
 clearbody n; clear.
 rewrite wH_sum.
-case/boolP : (n0 < n)%N => n0n.
-  rewrite (bigD1 (Ordinal n0n)) //= mxE eqxx (eq_bigr (fun x => O)); last first.
+have [n0n|n0n] := ltnP n0 n.
+  rewrite (bigD1 (Ordinal n0n))//= mxE eqxx (eq_bigr (fun x => O)); last first.
     move=> i Hi; rewrite mxE ifF //.
     apply: contraNF Hi => /eqP Hi; by apply/eqP/val_inj.
   by rewrite big_const iter_addn mul0n.
 rewrite (eq_bigr (fun x => O)); first by rewrite big_const iter_addn.
-move=> i _; rewrite mxE ifF //=; by apply: contraNF n0n => /eqP ->.
+move=> i _; rewrite mxE ifF //=.
+by apply/negbTE; rewrite gtn_eqF// (leq_trans (ltn_ord i)).
 Qed.
 
 Lemma syndrome_hamming_err y :
   syndrome (Hamming.PCM m) (hamming_err y) = syndrome (Hamming.PCM m) y.
 Proof.
 rewrite /hamming_err.
 move Hs : (syndrome (Hamming.PCM m) y) => s.
-case/boolP : (s == 0) => [/eqP ->|s0].
+have [->|s0] := eqVneq s 0.
   by rewrite nat_of_rV_0 syndrome0.
 have [k ks] : exists k : 'I_n, nat_of_rV s = k.+1.
   move: s0; rewrite -nat_of_rV_eq0 -lt0n => s0.
@@ -571,7 +572,7 @@ Lemma PCM_A_1 : PCM = castmx (erefl, subnK (Hamming.dim_len m')) (row_mx CSM 1).
 Proof.
 apply/matrixP => i j.
 rewrite mxE castmxE /=.
-case/boolP : (j < n - m)%N => Hcond.
+have [Hcond|Hcond] := ltnP j (n - m)%N.
   have -> : cast_ord (esym (subnK (Hamming.dim_len m'))) j =
            lshift m (Ordinal Hcond) by apply val_inj.
   rewrite row_mxEl [in X in _  = X]mxE.
@@ -582,13 +583,13 @@ case/boolP : (j < n - m)%N => Hcond.
 rewrite [in X in _ = X]mxE.
 move: (splitP (cast_ord (esym (subnK (Hamming.dim_len m'))) j)) => [k Hk|k Hk].
   have jk : j = k :> nat by [].
-  by rewrite jk (ltn_ord k) in Hcond.
+  by rewrite leqNgt jk (ltn_ord k) in Hcond.
 rewrite permE /perm_ids.
 move Hj : (ord_split j) => l.
 move: (splitP l) => [p Hp|p Hlp].
   exfalso.
   move/negP : Hcond; apply.
-  suff -> : nat_of_ord j = nat_of_ord p by apply ltn_ord.
+  suff -> : nat_of_ord j = nat_of_ord p by apply/negP; rewrite -ltnNge ltn_ord.
   by rewrite -Hp -Hj.
 destruct ids1 as [x e] => /=.
 move/matrixP/(_ i 0) : e.

ecc_classic/linearcode.v

@@ -267,7 +267,7 @@ move=> xC x0.
 rewrite /lowest_size.
 case: exists_non0_codeword_lowest_deg => g /= /and3P[H1 H2 /forallP].
 move/(_ x); rewrite xC x0 /= andbT.
-case/boolP : (x == g) => [/eqP -> //| xg].
+have [->//|xg] := eqVneq x g.
 by rewrite implyTb.
 Qed.
 
@@ -277,7 +277,7 @@ Proof.
 case/and3P => gC g0 Hg.
 rewrite /lowest_size.
 case: exists_non0_codeword_lowest_deg => g' /= /and3P[g'C g'0 Hg'].
-case/boolP: (g == g') => [/eqP -> // | gg'].
+have [->//|gg'] := eqVneq g g'.
 apply/eqP; rewrite eqn_leq.
 move: Hg => /forallP/(_ g').
 rewrite g'C /= g'0 andbT eq_sym gg' implyTb => ->.
@@ -512,11 +512,10 @@ have gk : size (rVpoly g) <= size (rVpoly k).
   - rewrite /k; move: abs; apply contra; by rewrite subr_eq0.
 suff kg : size (rVpoly k) < size (rVpoly g).
   by move: (leq_ltn_trans gk kg); rewrite ltnn.
-rewrite /k linearB /=; case/boolP: (1 < size (rVpoly g)) => size_1g.
+rewrite /k linearB /=; have [size_1g|size_1g] := ltnP 1 (size (rVpoly g)).
 - apply: size_sub => //=; last by apply lead_coef_F2.
-  apply/eqP; apply: contra g0; by rewrite rVpoly0.
-- rewrite -leqNgt in size_1g.
-  (* this means that g is constant *)
+  by apply/eqP; apply: contra g0; rewrite rVpoly0.
+- (* this means that g is constant *)
   have sz_g1 : size (rVpoly g) = 1%N.
     have : size (rVpoly g) != O by rewrite size_poly_eq0 rVpoly0.
     by case: (size _) size_1g => //; case.
@@ -720,11 +719,11 @@ transitivity (\sum_(i < r.+1) #| [set y | dH x y == i] |)%N.
     apply: trivIimset.
     - move=> i j _ _ ji; rewrite -setI_eq0; apply/eqP/setP => /= y.
       rewrite !inE.
-      case/boolP : (dH x y == i) => //= /eqP ->.
-      apply/negbTE; by rewrite eq_sym.
+      have [->/=|//] := eqVneq (dH x y) i.
+      by apply/negbTE; rewrite eq_sym.
     - apply/negP; case/imsetP => /= i _ => /esym.
       apply/eqP/sphere_not_empty.
-      rewrite (leq_trans _ rn) //; move: (ltn_ord i); by rewrite ltnS.
+      by rewrite (leq_trans _ rn) //; move: (ltn_ord i); rewrite ltnS.
   have partD : partition (f @: enum 'I_r.+1) D.
     apply/and3P; split.
     - rewrite cover_imset //; apply/eqP/eq_bigl => i; by rewrite mem_enum.
@@ -767,11 +766,11 @@ have /card_partition : partition P (\bigcup_(c in C) ball c t).
   move/setP/(_ x); by rewrite !inE dHE subrr wH0 leq0n.
 rewrite big_imset /=; last first.
   move=> c1 c2 c1C c2C.
-  case/boolP : (c1 == c2) => [/eqP //|c1c2 abs].
+  have [//|c1c2 abs] := eqVneq c1 c2.
   move: (H _ _ c1C c2C c1c2).
   rewrite abs setIid => /setP/(_ c2).
   by rewrite !inE dHE subrr wH0 leq0n.
-move=> <-; apply subset_leq_card; apply/subsetP => x; by rewrite inE.
+by move=> <-; apply subset_leq_card; apply/subsetP => x; rewrite inE.
 Qed.
 
 Definition perfect n q (C : Lcode0.t 'F_q n)

ecc_classic/poly_decoding.v

@@ -147,7 +147,7 @@ apply (@leq_trans (#|E|.*2.+1 - #|E|)); last first.
 rewrite leq_sub // ltnS.
 apply (@leq_trans (\sum_(i in E) 2)); last by rewrite big_const iter_addn_0 mul2n.
 apply leq_sum => /= i iE.
-case/boolP : (a ``_ i == 0) => [/eqP ->|ai0].
+have [->|ai0] := eqVneq (a ``_ i) 0.
   by rewrite scale0r subr0 size_poly1.
 by rewrite size_one_minus_X.
 Qed.
@@ -393,7 +393,7 @@ Qed.
 Lemma size_syndromep y : size (syndromep u y t) <= t.
 Proof.
 rewrite /syndromep poly_def (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _.
-case/boolP : (fdcoor u y (inord i.+1) == 0) => [/eqP -> | ?].
+have [->|?] := eqVneq (fdcoor u y (inord i.+1)) 0.
 - by rewrite scale0r size_poly0.
 - by rewrite size_scale // size_polyXn.
 Qed.
@@ -447,7 +447,7 @@ Hypothesis tn : t < n.
 Lemma dft_syndromep (v : 'rV[F]_n) :
   rVpoly (dft (rVexp a n) t (twisted a v)) = syndromep (rVexp a n) v t.
 Proof.
-case/boolP : (a == 0) => [/eqP -> | a0].
+have [->|a0] := eqVneq a 0.
   apply/polyP => i.
   rewrite !coef_poly.
   case: ifPn => // it.