minor fix

affeldt-aist · Nov 9, 2019 · 77ed2a3 · 77ed2a3
1 parent de233d3
commit 77ed2a3
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 17 deletions.
diff --git a/ecc_modern/checksum.v b/ecc_modern/checksum.v
@@ -29,22 +29,17 @@ Notation "'\delta'" := (checksubsum).
 Lemma checksubsum_set1 n i (x : 'rV['F_2]_n) :
   \delta [set i] x = ~~ (bool_of_F2 x ``_ i).
 Proof.
-rewrite /checksubsum (big_pred1 i).
-  by rewrite /bool_of_F2 negbK.
-move=> /= n2; by rewrite in_set1.
+by rewrite /checksubsum (big_pred1 i) ?negbK // => n2; rewrite in_set1.
 Qed.
 
 Lemma checksubsum_set2 n n1 n2 (n1n2 : n1 != n2) (d : 'rV_n) :
   \delta [set n1; n2] d = (d ``_ n1 == d ``_ n2).
 Proof.
-rewrite /checksubsum.
-rewrite big_setU1 /=; last by rewrite inE.
-rewrite big_set1.
+rewrite /checksubsum big_setU1 ?inE //= big_set1.
 by rewrite -{1}(oppr_char2 (@char_Fp 2 erefl) (d ``_ n2)) subr_eq0.
 Qed.
 
 Section checksubsum_parity.
-
 Variables (n m : nat) (H : 'M['F_2]_(m, n)) (A : {set 'I_n}).
 
 Lemma checksubsum_D1 i x : i \in A ->
@@ -80,14 +75,14 @@ rewrite {1}(_ : (1 = (\prod_(m0 < m) 1)%:R)%R); [congr INR |
 apply eq_bigr => m0 _.
 rewrite /C mem_kernel_syndrome0 /syndrome in x_in_C.
 move/eqP in x_in_C.
-have {x_in_C}x_in_C : forall m0, \sum_i (H m0 i) * (x ``_ i) = 0.
+have {}x_in_C : forall m0, \sum_i (H m0 i) * (x ``_ i) = 0.
   move=> m1.
   move/rowP : x_in_C => /(_ m1).
   rewrite !mxE.
   move=> t_in_C; rewrite -[in X in _ = X]t_in_C.
   apply eq_bigr => // i _; congr (_ * _).
   by rewrite /row_of_tuple !mxE.
-have {x_in_C}x_in_C : forall m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) = 0.
+have {}x_in_C : forall m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) = 0.
   move=> m1.
   rewrite -[in X in _ = X](x_in_C m1); symmetry.
   rewrite (bigID [pred i | i \in 'V m1]) /=.
@@ -97,12 +92,12 @@ have {x_in_C}x_in_C : forall m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) = 0.
     by rewrite big_const /= iter_addr0.
   apply eq_big => // n0.
   rewrite VnextE tanner_relE -F2_eq0 => /eqP ->; by rewrite mul0r.
-have {x_in_C}x_in_C : forall m0, \sum_(i in 'V m0) x ``_ i = 0.
+have {}x_in_C : forall m0, \sum_(i in 'V m0) x ``_ i = 0.
   move=> m1.
   rewrite -[in X in _ = X](x_in_C m1).
   apply eq_bigr => // i.
   rewrite VnextE tanner_relE => /eqP ->; by rewrite mul1r.
-have {x_in_C}x_in_C : forall m0, \sum_(i in 'V m0) x ``_ i = 0.
+have {}x_in_C : forall m0, \sum_(i in 'V m0) x ``_ i = 0.
   move=> m1.
   by rewrite -{2}(x_in_C m1).
 by rewrite /checksubsum (x_in_C m0) eqxx.
@@ -113,11 +108,11 @@ Lemma kernel_checksubsum0 (x : 'rV['F_2]_n) : x \notin kernel H ->
 Proof.
 move=> x_notin_C.
 rewrite /C mem_kernel_syndrome0 /syndrome in x_notin_C.
-have {x_notin_C}x_notin_C : [exists m0, \sum_i (H m0 i) * (x ``_ i) != 0].
+have {}x_notin_C : [exists m0, \sum_i (H m0 i) * (x ``_ i) != 0].
   rewrite -negb_forall; apply: contra x_notin_C => /forallP x_notin_C.
   apply/eqP/rowP => a; rewrite !mxE /= -[RHS](eqP (x_notin_C a)).
   by apply eq_bigr => // i _; rewrite /row_of_tuple !mxE.
-have {x_notin_C}x_notin_C : [exists m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) != 0].
+have {}x_notin_C : [exists m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) != 0].
   case/existsP : x_notin_C => m0 Hm0.
   apply/existsP; exists m0.
   apply: contra Hm0 => /eqP Hm0.
@@ -127,12 +122,12 @@ have {x_notin_C}x_notin_C : [exists m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) !
     by rewrite big_const /= iter_addr0.
   apply eq_big => n0 //.
   rewrite VnextE tanner_relE -F2_eq0 => /eqP ->; by rewrite mul0r.
-have {x_notin_C}x_notin_C : [exists m0, \sum_(i in 'V m0) x ``_ i != 0].
+have {}x_notin_C : [exists m0, \sum_(i in 'V m0) x ``_ i != 0].
   case/existsP : x_notin_C => /= m0 x_notin_C.
   apply/existsP; exists m0; apply: contra x_notin_C => /eqP H0.
   apply/eqP; rewrite -[RHS]H0; apply eq_bigr => n0.
   rewrite VnextE tanner_relE => /eqP ->; by rewrite mul1r.
-have {x_notin_C}x_notin_C : [exists m0, \sum_(i in 'V m0) x ``_ i != 0].
+have {}x_notin_C : [exists m0, \sum_(i in 'V m0) x ``_ i != 0].
   case/existsP : x_notin_C => /= m0 x_notin_C.
   by apply/existsP; exists m0; apply: contra x_notin_C => /eqP ->.
 case/existsP : x_notin_C => m0 Hm0.

diff --git a/opam b/opam
@@ -26,7 +26,7 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.9.1" & < "8.11~"}
+  "coq" {>= "8.10" & < "8.11~"}
   "coq-mathcomp-field" {>= "1.9.0" & < "1.10~"}
   "coq-mathcomp-analysis"   {>= "0.2.0" & <= "0.2.2"}
 ]
@@ -40,5 +40,5 @@ tags: [
   "keyword: probability"
   "keyword: error-correcting codes"
   "logpath:infotheo"
-  "date:2019-09-17"
+  "date:2019-11-09"
 ]