fix wrt MathComp 1.11

- give up on Coq 8.10 for travis - update readme
affeldt-aist · Jun 11, 2020 · 01f7379 · 01f7379
1 parent 7362531
commit 01f7379
Show file tree

Hide file tree

Showing 11 changed files with 74 additions and 73 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -14,7 +14,6 @@ env:
   - NJOBS="2"
   - CONTRIB_NAME="infotheo"
   matrix:
-  - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.10"
   - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11"
 
 install: |

diff --git a/README.org b/README.org
@@ -13,16 +13,16 @@
 
 *** Last stable version:
 
-Version 0.1:
+Version 0.1.1:
 3. ~opam install coq-infotheo~
 
 **** Requirements
 
-- [[https://coq.inria.fr][Coq]] 8.10.2 or 8.11
-- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.10.0
-- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.2.3
+- [[https://coq.inria.fr][Coq]] 8.11
+- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.11.0
+- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.3.1
   which requires
-  + [[https://github.com/math-comp/finmap][finmap]] 1.2.0 or greater
+  + [[https://github.com/math-comp/finmap][finmap]] 1.5.0 or greater
 
 All versions available from opam.
 

diff --git a/_CoqProject b/_CoqProject
@@ -94,4 +94,3 @@ toy_examples/expected_value_variance_tuple.v
 toy_examples/conditional_entropy.v
 
 -R . infotheo
-
diff --git a/ecc_classic/decoding.v b/ecc_classic/decoding.v
@@ -85,10 +85,10 @@ Proof.
 split => [H /= y x yx x' x'C | H /= y x yx].
 - move: {H}(H _ _ yx) => H.
   rewrite dH_sym H dH_sym.
-  case: arg_minP; first by case: c_not_empty.
+  case: arg_minnP; first by case: c_not_empty.
   move=> /= i ic ij; by rewrite dH_sym (dH_sym x') ij.
 - move: {H}(H _ _ yx) => H.
-  case: arg_minP; first by case: c_not_empty.
+  case: arg_minnP; first by case: c_not_empty.
   move=> /= i Hi /(_ x) Ki.
   apply/eqP; rewrite eqn_leq; apply/andP; split.
   - by rewrite dH_sym (dH_sym y) H.

diff --git a/ecc_classic/hamming_code.v b/ecc_classic/hamming_code.v
@@ -331,13 +331,13 @@ have syndrome_not_0 : syndrome (Hamming.PCM m) y != 0.
   by rewrite /hamming_err syndrome_is_0 nat_of_rV_0 addr0 dHE subrr wH0.
 move=> dHy.
 suff : dH y x != O.
-  move: dHy; rewrite leq_eqVlt => /orP[/eqP //|]; by rewrite ltnS leqn0 => ->.
+  by move: dHy; rewrite leq_eqVlt => /orP[/eqP //|]; rewrite ltnS leqn0 => ->.
 apply/negP => abs.
 have : y = x by move: abs; rewrite dHE wH_eq0 subr_eq0 => /eqP.
-rewrite /x; case: arg_minP => [|/=]; first by case: C_not_empty.
+rewrite /x; case: arg_minnP => [|/=]; first by case: C_not_empty.
 move=> y' Hy' _ yy'; rewrite -{}yy' in Hy'.
 move/negP : syndrome_not_0; apply.
-rewrite -mem_kernel_syndrome0; by rewrite inE in Hy'.
+by rewrite -mem_kernel_syndrome0; rewrite inE in Hy'.
 Qed.
 
 Lemma hamming_repair_img : oimg hamming_repair \subset Hamming.code m.
@@ -380,14 +380,14 @@ case Hi : (0 < wH i^T).
   exists (Ordinal H0) => //.
   apply/trmx_inj.
   rewrite col_matrix /= trmxK -{1}(nat_of_rVK i^T) subn1 prednK // lt0n nat_of_rV_eq0.
-  apply/eqP => abs; by rewrite abs lt0n wH0 eqxx in Hi.
+  by apply/eqP => abs; rewrite abs lt0n wH0 eqxx in Hi.
 apply/esym/negbTE; move/negbT : Hi; apply contra.
 case/imsetP => j Hj ->.
 case HwH : (wH (col j (Hamming.PCM m))^T); last by [].
 exfalso.
 move/eqP: HwH.
 rewrite col_matrix wH_eq0 trmxK => /eqP.
-apply rV_of_nat_neq0 => //; by apply Hamming.len_two_m.
+by apply rV_of_nat_neq0 => //; apply Hamming.len_two_m.
 Qed.
 
 Lemma col_PCM_inj : injective (fun i => col i (Hamming.PCM m)).
@@ -421,7 +421,7 @@ case HwH : (wH i^T == _).
   rewrite !mxE /=.
   move/setP/(_ j): Hx.
   rewrite in_set1 in_set tnth_mktuple mxE => <-.
-  rewrite F2_eq1; by case: F2P.
+  by rewrite F2_eq1; case: F2P.
 apply/negbTE; move/negbT: HwH; apply contra.
 case/imsetP => x Hx ->.
 by apply/eqP/wH_col_1.
@@ -431,7 +431,7 @@ Lemma cols_1_inj : injective (fun i => col i 1 : 'cV['F_2]_m).
 Proof.
 move=> i j /= /matrixP/(_ j 0).
 rewrite !mxE eqxx /=.
-case Hji : (j == i) => // _. by apply/esym/eqP.
+by case Hji : (j == i) => // _; apply/esym/eqP.
 Qed.
 
 Definition non_unit_cols := [set c : 'cV['F_2]_m | wH c^T > 1].
@@ -443,12 +443,12 @@ Proof.
 rewrite /non_unit_cols /unit_cols.
 transitivity #|[set c : 'cV['F_2]_m | wH c^T >= 1%nat]|.
   apply eq_card=> c; by rewrite !in_set orbC eq_sym -leq_eqVlt.
-rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj.
+by rewrite cols_PCM card_imset ?card_ord //; exact: col_PCM_inj.
 Qed.
 
 Lemma card_unit_cols : #|unit_cols| = m.
 Proof.
-rewrite /unit_cols cols_1 card_imset; by [apply card_ord | apply cols_1_inj].
+by rewrite /unit_cols cols_1 card_imset; [apply card_ord | apply cols_1_inj].
 Qed.
 
 Lemma card_non_unit : #|non_unit_cols| = (n - m)%nat.
@@ -475,11 +475,11 @@ have Hin : col i 1 \in image (fun j => col j (Hamming.PCM m)) 'I_n.
     rewrite -cols_PCM inE.
     have : col i 1 \in [set c : 'cV['F_2]_m | wH c^T == 1%nat].
       rewrite cols_1.
-      apply/imsetP; by exists i.
+      by apply/imsetP; exists i.
     by rewrite inE => /eqP ->.
   case/imsetP : Hi => j Hj Hj'.
-  exists j => //; by rewrite mem_enum.
-exists (iinv Hin); by apply (f_iinv Hin).
+  by exists j => //; rewrite mem_enum.
+by exists (iinv Hin); apply (f_iinv Hin).
 Defined.
 
 Definition ord_split (i : 'I_n) : 'I_(n - m + m) :=
@@ -509,7 +509,7 @@ have Hcols x : x \in non_unit_cols -> x \in [set col i (Hamming.PCM m) | i : 'I_
 case Hc : (c \in non_unit_cols).
   apply/imsetP.
   case/imsetP: (Hcols _ Hc) => x Hx Hx'.
-  exists x => //; by rewrite inE -Hx'.
+  by exists x => //; rewrite inE -Hx'.
 apply/negbTE.
 move/negbT: Hc; apply contra.
 case/imsetP => x Hx Hx'.
@@ -555,7 +555,7 @@ have Hij : i' = j'.
   apply cols_1_inj.
   by rewrite -(proj2_sig (ids1 i')) -(proj2_sig (ids1 j')) Htmp.
 rewrite Hij -Hj' /= in Hi'.
-by apply val_inj.
+exact: val_inj.
 Qed.
 
 Definition systematic : 'S_n := perm perm_ids_inj.
@@ -576,7 +576,7 @@ case/boolP : (j < n - m) => Hcond.
   rewrite castmxE /=.
   rewrite /PCM 2!cast_ord_id.
   rewrite esymK [in X in _ = X]mxE.
-  congr (Hamming.PCM m _ (systematic _)); by apply val_inj.
+  by congr (Hamming.PCM m _ (systematic _)); exact: val_inj.
 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 [].
@@ -901,9 +901,9 @@ move=> /= y c Hy c'.
 rewrite !(dH_sym _ y).
 move: (@hamming_MD_alt r' y c).
 move=> ->.
-- case: arg_minP.
+- case: arg_minnP.
     by destruct C_not_empty.
-  move => /= i Hi; by apply.
+  by move => /= i Hi; apply.
 - by rewrite -Hy /Decoder.repair /= /hamming_repair ffunE.
 Defined.
 

diff --git a/ecc_classic/linearcode.v b/ecc_classic/linearcode.v
@@ -244,7 +244,7 @@ Proof.
 apply: sigW.
 case: C_not_trivial => g /andP[gC g0].
 have := erefl [arg min_(g' < g | (g' \in C) && (g' != 0)) (size (rVpoly g'))].
-case: arg_minP => /=; [by apply/andP | move=> g'].
+case: arg_minnP => /=; [by apply/andP | move=> g'].
 case/andP=> g'C g'0 g_min _.
 exists g'.
 rewrite /non0_codeword_lowest_deg g'C g'0 /= /codeword_lowest_deg.
@@ -293,36 +293,34 @@ Proof. by rewrite /non_0_cw; case/andP: (xchooseP C_not_trivial). Qed.
 
 Lemma wH_non_0_cw : wH non_0_cw != O.
 Proof.
-rewrite /non_0_cw; case/andP: (xchooseP C_not_trivial); by rewrite wH_eq0.
+by rewrite /non_0_cw; case/andP: (xchooseP C_not_trivial); rewrite wH_eq0.
 Qed.
 
-Definition min_wH_cw := arg_min non_0_cw [pred cw | (cw \in C) && (wH cw != O)] (@wH F n).
-
-(*Definition min_wH_cw := arg_min non_0_cw [pred cw in C | wH cw != O] (@wH F n).*)
+Definition min_wH_cw :=
+  arg_min non_0_cw [pred cw | (cw \in C) && (wH cw != O)] (@wH F n).
 
 Definition min_dist := wH min_wH_cw.
 
 Lemma min_dist_is_min c : c \in C -> c != 0 -> min_dist <= wH c.
 Proof.
-move=> cC c0.
-rewrite /min_dist /min_wH_cw.
-case: arg_minP => /= [|c1 /andP [] Hc1 wHc1].
+move=> cC c0; rewrite /min_dist /min_wH_cw.
+case: arg_minnP => /= [|c1 /andP [] Hc1 wHc1].
   by rewrite non_0_cw_mem wH_non_0_cw.
-apply; by rewrite cC /= wH_eq0.
+by apply; rewrite cC /= wH_eq0.
 Qed.
 
 Lemma min_dist_achieved : exists c, c \in C /\ c <> 0 /\ wH c = min_dist.
 Proof.
 exists min_wH_cw; split.
   rewrite /min_wH_cw /=.
-  case: arg_minP => /=.
+  case: arg_minnP => /=.
     by rewrite non_0_cw_mem wH_non_0_cw.
   by move=> /= c /andP[].
 split; last reflexivity.
 rewrite /min_wH_cw /=.
-case: arg_minP => /=.
+case: arg_minnP => /=.
   by rewrite non_0_cw_mem wH_non_0_cw.
-move=> /= c /andP[_ /negP]; by rewrite wH_eq0 => /negP/eqP.
+by move=> /= c /andP[_ /negP]; rewrite wH_eq0 => /negP/eqP.
 Qed.
 
 Lemma min_dist_neq0 : min_dist <> O.
@@ -339,7 +337,7 @@ Lemma min_distP d :
 Proof.
 case=> H1 [y [yC [y0 yd]]].
 rewrite /min_dist /min_wH_cw.
-case: arg_minP => /=.
+case: arg_minnP => /=.
   by rewrite non_0_cw_mem wH_non_0_cw.
 move=> x /andP[xC x0] H.
 apply/eqP.
@@ -371,25 +369,25 @@ move=> even_d.
 rewrite /mdd_err_cor (_ : min_dist.-1./2 = min_dist./2 - 1)%N //.
 move Hd : min_dist => d.
 case: d Hd even_d => //= d -> /=.
-rewrite negbK uphalf_half => ->; by rewrite add1n subn1.
+by rewrite negbK uphalf_half => ->; rewrite add1n subn1.
 Qed.
 
 Definition sbound_f' k (H : k.-1 <= n) :=
   fun c : 'rV[F]_n => \row_(i < k.-1) c ord0 (widen_ord H i).
 
 Lemma sbound_f'Z k (H : k.-1 <= n) a y :
   sbound_f' H (a *: y) = a *: sbound_f' H y.
-Proof. apply/rowP => i; by rewrite !mxE. Qed.
+Proof. by apply/rowP => i; rewrite !mxE. Qed.
 
 Lemma sbound_f'D k (H : k.-1 <= n) y y' :
   sbound_f' H (y + y') = sbound_f' H y + sbound_f' H y'.
 Proof. by apply/rowP => i; rewrite !mxE. Qed.
 
 Lemma sbound_f'N k (H : k.-1 <= n) y : sbound_f' H (- y) = - sbound_f' H y.
-Proof. apply/rowP => i; by rewrite !mxE. Qed.
+Proof. by apply/rowP => i; rewrite !mxE. Qed.
 
 Lemma additive_sbound_f' k (H : k.-1 <= n) : additive (sbound_f' H).
-Proof. move=> x y; by rewrite sbound_f'D sbound_f'N. Qed.
+Proof. by move=> x y; rewrite sbound_f'D sbound_f'N. Qed.
 
 Definition sbound_f_linear k (H : k.-1 <= n) :
   {linear 'rV[F]_n -> 'rV[F]_k.-1} :=
@@ -439,9 +437,8 @@ have Kcw : wH cw <= n - k + 1.
     move/rowP => /= /(_ (Ordinal Hi)).
     rewrite !mxE /=.
     set x := widen_ord _ _.
-    suff -> : x = i.
-      by move/eqP.
-    by apply val_inj.
+    suff -> : x = i by move/eqP.
+    exact: val_inj.
   have X : forall i : 'I_n, ~~ (i < k.-1) -> (cw ord0 i != 0) <= 1.
     move=> i Hi.
     by case: (_ != _).
@@ -471,8 +468,7 @@ have Kcw : wH cw <= n - k + 1.
     move: dimCn.
     by rewrite prednK // not_trivial_dim.
   by rewrite addn1.
-apply: (leq_trans _ Kcw).
-by apply min_dist_is_min.
+exact/(leq_trans _ Kcw)/min_dist_is_min.
 Qed.
 
 Definition maximum_distance_separable := (min_dist == n - \dim C + 1)%N.
@@ -502,15 +498,16 @@ have gk : size (rVpoly g) <= size (rVpoly k).
   - apply: contra j0.
     by rewrite /k subr_eq addrC -subr_eq subrr eq_sym.
   - 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.
+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.
 - 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 *)
   have sz_g1 : size (rVpoly g) = 1%N.
     have : size (rVpoly g) != O by rewrite size_poly_eq0 rVpoly0.
-    case: (size _) size_1g => //; by case.
+    by case: (size _) size_1g => //; case.
   rewrite (@size1_polyC_F2 _ sz_g1).
   rewrite gj in sz_g1.
   by rewrite (@size1_polyC_F2 _ sz_g1) size_polyC subrr size_poly0.
@@ -549,24 +546,26 @@ case/boolP : (odd (min_dist C_not_trivial)) => [odd_d | even_d].
   have : min_dist C_not_trivial <= (min_dist C_not_trivial)./2.*2.
     move: abs.
     rewrite eq_sym => /(min_dist_prop C_not_trivial)/leq_trans; apply => //.
-    move/subsetP : f_img; apply.
-    rewrite inE; apply/existsP; exists y; by apply/eqP.
+      move/subsetP : f_img; apply.
+      by rewrite inE; apply/existsP; exists y; apply/eqP.
     by rewrite (@min_dist_double y).
   by rewrite -{1}(odd_double_half (min_dist C_not_trivial)) odd_d ltnNge leqnn.
 - rewrite (mdd_evenE even_d) in enc_m_v.
   apply/eqP/negPn/negP => abs.
   have {}abs : m0 != x by apply: contra abs; rewrite Hm0 => /eqP ->.
   have : (min_dist C_not_trivial)./2 <= (min_dist C_not_trivial)./2 - 1.
-    move: (odd_double_half (min_dist C_not_trivial)); rewrite -leq_double (negbTE even_d) /= add0n => ->.
+    move: (odd_double_half (min_dist C_not_trivial)).
+    rewrite -leq_double (negbTE even_d) /= add0n => ->.
     move: abs.
     rewrite eq_sym.
     move/(min_dist_prop C_not_trivial)/leq_trans; apply => //.
-    move/subsetP: f_img; apply.
-    rewrite inE; apply/existsP; exists y; by apply/eqP.
+      move/subsetP: f_img; apply.
+      by rewrite inE; apply/existsP; exists y; apply/eqP.
     by rewrite (@min_dist_double y).
   apply/negP.
   rewrite -ltnNge subn1 prednK // half_gt0 ltnNge; apply: contra even_d.
-  rewrite leq_eqVlt => /orP[/eqP->//|]; by rewrite ltnS leqn0 => /eqP/min_dist_neq0.
+  rewrite leq_eqVlt => /orP[/eqP->//|].
+  by rewrite ltnS leqn0 => /eqP/min_dist_neq0.
 Qed.
 
 (* see for example [F.J. MacWilliams and N.J.A. Sloane, The

diff --git a/ecc_classic/repcode.v b/ecc_classic/repcode.v
@@ -37,10 +37,10 @@ Lemma seq_block_inv A : forall r (l : seq A) k,
 Proof.
 elim=> [l r | r IH l [ | k H] ].
 - rewrite !mul0n => Hl.
-  exists l, nil; by rewrite cats0.
+  by exists l, nil; rewrite cats0.
 - rewrite muln1 => H.
   exists (take (r.+1) l), nil.
-  rewrite cats0 take_oversize; by [rewrite muln0 | rewrite H].
+  by rewrite cats0 take_oversize; [rewrite muln0 | rewrite H].
 - exists (take (r.+1) l), (drop (r.+1) l).
   rewrite cat_take_drop size_drop H size_take H ltn_Pmulr //.
   repeat (split => //).
@@ -210,7 +210,7 @@ Lemma min_dist_repcode (Hr : odd r.+1) : min_dist not_trivial_replcode = r.+1.
 Proof.
 rewrite /min_dist /= (_ : min_wH_cw _ = const_mx 1) ?wH_const_mx //.
 rewrite /min_wH_cw.
-case: arg_minP => /=.
+case: arg_minnP => /=.
   rewrite non_0_codeword_replcode (Rep.const_mx_in_code r 1) /= wH_eq0 /=.
   by apply/eqP => /matrixP/(_ 0 0); rewrite !mxE.
 move=> i Hi _.

diff --git a/lib/Rbigop.v b/lib/Rbigop.v
@@ -776,11 +776,7 @@ Local Open Scope min_scope.
 Lemma bigminn_min (A : finType) (C : {set A}) (cnot0 : {c0 | c0 \in C})
   a (Ha : a \in C) (h : A -> nat) :
   (\min^ (sval cnot0) _(c in C) h c <= h a)%nat.
-Proof.
-case: arg_minP.
-by destruct cnot0.
-move=> a0 a0C; exact.
-Qed.
+Proof. by case: arg_minnP; [case: cnot0|move=> a0 a0C; exact]. Qed.
 
 (* TODO: useless ? *)
 Lemma big_rmax_bigminn_helper (A : finType) n (g : nat -> R) :