start porting proba.v

_CoqProject

@@ -4,12 +4,10 @@
 -arg -w -arg -ambiguous-paths
 -arg -w -arg -notation-incompatible-format
 
-lib/ssrZ.v
-lib/ssrR.v
+lib/coqRE.v
 lib/realType_ext.v
-lib/Reals_ext.v
-lib/logb.v
-lib/Ranalysis_ext.v
+lib/realType_ln.v
+lib/derive_ext.v
 lib/ssr_ext.v
 lib/f2.v
 lib/ssralg_ext.v
@@ -31,7 +29,6 @@ probability/convex_stone.v
 probability/jfdist_cond.v
 probability/graphoid.v
 probability/jensen.v
-probability/ln_facts.v
 probability/divergence.v
 probability/variation_dist.v
 probability/log_sum.v

changelog.txt

@@ -1,3 +1,24 @@
+--------------------
+from 0.7.7 to master
+--------------------
+
+* changed:
+  almost no stdlib R anymore
+
+* added:
+- in bigop_ext.v
+  + lemmas morphs_oppr, morph_mulRDr, bigmax_le_seq, bigmax_leP_seq,
+           bigmax_gt0P_seq, big_union_nondisj
+- in derive_ext.v
+  + lemmas open_norm_subball,
+           near_eq_derive, near_eq_derivable, near_eq_is_derive
+- in realType_ext.v
+  + lemmas wpmulr_lgt0, wpmulr_rgt0
+- in ssr_ext.v
+  + lemma eqW
+  + setY* (symmetric difference for finite sets), notation: "A :*: B"
+
+
 -------------------
 from 0.7.6 to 0.7.7
 -------------------
@@ -25,6 +46,16 @@ from 0.7.3 to 0.7.4
 -------------------
 from 0.7.2 to 0.7.3
 -------------------
+* added:
+- in ssralg_ext.v
+  + lemmas mulr_regl, mulr_regr
+- in realType_ext.v
+  + lemmas x_x2_eq, x_x2_max, x_x2_pos, x_x2_nneg, expR1_gt2
+- new file derive_ext.v
+  + lemmas differentiable_{ln, Log}
+  + lemmas is_derive{D, B, N, M, V, Z, X, _sum}_eq
+  + lemmas is_derive1_{lnf, lnf_eq, Logf, Logf_eq, LogfM, LogfM_eq, LogfV, LogfV_eq}
+  + lemmas derivable1_mono, derivable1_homo
 
 - lemma `conv_pt_cset_is_convex` changed into a `Let`
 

ecc_classic/bch.v

@@ -43,9 +43,7 @@ Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
 Local Open Scope ring_scope.
-
 Local Open Scope vec_ext_scope.
-
 Local Open Scope dft_scope.
 
 Module BCH.
@@ -114,7 +112,7 @@ have j2t : (j.-1)./2 < t.*2.
   destruct j => //.
   by rewrite /= (ltn_trans i1) // ltnS muln2 -[in X in _ <= X]addnn leq_addl.
 move/(_ j2t)/(congr1 (fun x => x ^+ 2)).
-rewrite expr0n /= sum_char2 ?char_GFqm // => H'.
+rewrite expr0n /= sum_sqr ?char_GFqm // => H'.
 rewrite -[RHS]H'; apply eq_bigr => k _.
 rewrite exprMn_comm; last by rewrite /GRing.comm mulrC.
 congr (_ * _); last first.
@@ -140,31 +138,27 @@ apply/idP/idP.
   apply BCH_PCM_altP1 => i.
   move/eqP/rowP : H => /(_ i).
   rewrite !mxE => H; rewrite -[RHS]H.
-  apply eq_bigr => /= k _; by rewrite !mxE /= mulrC.
+  by apply eq_bigr => /= k _; rewrite !mxE /= mulrC.
 - rewrite /BCH.PCM_alt /BCH.PCM /syndrome => H.
   apply/eqP/rowP => i.
   have @j : 'I_t.*2.
-    refine (@Ordinal _ i.*2 _); by rewrite -!muln2 ltn_pmul2r.
+    by refine (@Ordinal _ i.*2 _); rewrite -!muln2 ltn_pmul2r.
   move/eqP : H => /matrixP/(_ ord0 j).
   rewrite !mxE => {2}<-.
-  apply eq_bigr => k _.
-  by rewrite !mxE.
+  by apply eq_bigr => k _; rewrite !mxE.
 Qed.
 
 End BCH_PCM_alt.
 
 Section BCH_def.
-
 Variables (n : nat) (m : nat).
 
-Definition code (a : 'rV_n) t :=
-  Rcode.t (@GF2_of_F2 m) (kernel (PCM a t)).
+Definition code (a : 'rV_n) t := Rcode.t (@GF2_of_F2 m) (kernel (PCM a t)).
 
 End BCH_def.
 
 Section BCH_syndromep.
-
-Variables (n' : nat).
+Variable n' : nat.
 Let n := n'.+1.
 Variable (m : nat).
 Let F : fieldType := GF2 m.
@@ -181,8 +175,7 @@ Notation "'\BCHsynp_(' a , e , t )" := (BCH.syndromep a e t) : bch_scope.
 Local Open Scope bch_scope.
 
 Section BCH_is_GRS.
-
-Variable (m : nat).
+Variable m : nat.
 Let F := GF2 m.
 Variable (n' : nat).
 Let n := n'.+1.
@@ -206,7 +199,7 @@ Lemma BCH_syndromep_is_GRS_syndromep y :
   GRS.syndromep (rVexp a n) (rVexp a n) t.*2 (F2_to_GF2 m y).
 Proof.
 apply/polyP => i.
-rewrite !coef_poly; case: ifPn => // it; by rewrite fdcoor_syndrome_coord.
+by rewrite !coef_poly; case: ifPn => // it; rewrite fdcoor_syndrome_coord.
 Qed.
 
 End BCH_is_GRS.
@@ -252,7 +245,7 @@ apply/idP/idP.
   rewrite -(@ltn_pmul2r 2) // !muln2 -(ltn_add2r 1) !addn1.
   move/leq_trans; apply.
   move: tn.
-  rewrite -divn2 leq_divRL // muln2 => /leq_ltn_trans; exact.
+  by rewrite -divn2 leq_divRL // muln2 => /leq_ltn_trans; exact.
 Qed.
 
 End BCH_PCM_checksum.
@@ -328,7 +321,7 @@ transitivity (\det (\matrix_(i, j) (h i j * g j))).
   apply/matrixP => i j.
   by rewrite !mxE /h /g /BCH.PCM_alt !mxE -!exprD /= -exprM mul1n addn1.
 rewrite det_mlinear; congr (_ * _).
-congr (\det _); apply/matrixP => i j; by rewrite !mxE /h -exprM.
+by congr (\det _); apply/matrixP => i j; rewrite !mxE /h -exprM.
 Qed.
 
 Hypothesis a_neq0 : distinct_non_zero a.
@@ -401,7 +394,7 @@ have Hf : \sum_(i < (wH x).-1.+1)
   case: ifPn => [_|]; first by rewrite!mxE mulrC.
   rewrite negb_and negbK.
   case/orP => [/eqP ->|abs']; first by rewrite rmorph0 scale0r mxE.
-  case/boolP : (x ``_ (f j) == 0) => [/eqP ->|abs''].
+  have [->|abs''] := eqVneq (x ``_ (f j)) 0.
     by rewrite rmorph0 scale0r mxE.
   exfalso.
   move/eqP: abs'; apply.
@@ -419,7 +412,7 @@ have {}Hf : \sum_(i < r'.+1) GF2_of_F2 x ``_ (f i) *:
   move/colP : Hf => /(_ (widen_ord (ltnW Hr') j)).
   rewrite !mxE summxE => Hf.
   rewrite -[RHS]Hf.
-  apply eq_bigr => /= i _; by rewrite !mxE.
+  by apply eq_bigr => /= i _; rewrite !mxE.
 have /negP := det_B_neq0 Hr' Hinj.
 rewrite -det_tr; apply.
 apply/det0P; exists (\row_i GF2_of_F2 x ``_ (f i)).
@@ -437,13 +430,12 @@ apply/det0P; exists (\row_i GF2_of_F2 x ``_ (f i)).
 apply/rowP => i; rewrite !mxE.
 move/colP : Hf => /(_ i).
 rewrite !mxE => Hf; rewrite -[RHS]Hf.
-rewrite summxE; apply eq_bigr=> k _; by rewrite !mxE.
+by rewrite summxE; apply eq_bigr=> k _; rewrite !mxE.
 Qed.
 
 End BCH_minimum_distance_lb.
 
 Section BCH_erreval.
-
 Variables (F : fieldType) (n : nat) (a : 'rV[F]_n).
 
 Definition BCH_erreval := erreval (const_mx 1) a.
@@ -453,7 +445,6 @@ End BCH_erreval.
 Notation "'\BCHomega_(' a , e )" := (BCH_erreval a e) : bch_scope.
 
 Section BCH_key_equation_old.
-
 Variables (F : fieldType) (n' : nat).
 Let n := n'.+1.
 Variable a : F.
@@ -471,7 +462,7 @@ under eq_bigr.
   rewrite (_ : \sigma_(rVexp a n, y) =
     \sigma_(rVexp a n, y, i) * (1 - ((rVexp a n) ``_ i) *: 'X)); last first.
     rewrite /errloc (bigD1 i) //= mulrC; congr (_ * _).
-    apply eq_bigl => ij; by rewrite in_setD1 andbC.
+    by apply eq_bigl => ij; rewrite in_setD1 andbC.
   over.
 transitivity (\sum_(i in supp y) y ``_ i *:
      (\sigma_(rVexp a n, y, i) * (1 - a ^+ (i * n) *: 'X^n))).
@@ -496,7 +487,6 @@ Qed.
 End BCH_key_equation_old.
 
 Section decoding_using_euclid.
-
 Variables (n' : nat) (m : nat).
 Let n := n'.+1.
 Let F := GF2 m.
@@ -650,10 +640,8 @@ Qed.
 End decoding_using_euclid.
 
 Section BCH_cyclic.
-
-Variables (n' : nat) (m : nat).
+Variables (n' m : nat).
 Let n := n'.+1.
-(*Hypothesis nm : (n %| (2 ^ m.-1))%N.*)
 Let F := GF2 m.
 Variable a : F.
 Variable t : nat.
@@ -676,9 +664,9 @@ have [M HM] : exists M, `[ 'X * rVpoly x' ]_ n = 'X * rVpoly x' + M * ('X^n - 1)
 rewrite HM /fdcoor poly_rV_K //; last first.
   rewrite -HM.
   move: (ltn_modp ('X * rVpoly x') ('X^n - 1)).
-  rewrite size_Xn_sub_1 // ltnS => ->.
-  by rewrite monic_neq0 // monic_Xn_sub_1.
-rewrite !(hornerE,hornerXn(*TODO(rei): not necessary since mc1.16.0*)).
+  rewrite size_XnsubC // ltnS => ->.
+  by rewrite monic_neq0 // monicXnsubC.
+rewrite !(hornerE,hornerXn).
 move: (Hx i); rewrite /fdcoor => /eqP ->; rewrite mulr0 add0r.
 by rewrite mxE exprAC a1 expr1n subrr mulr0.
 Qed.