before next release

.travis.yml

@@ -15,8 +15,7 @@ env:
   - CONTRIB_NAME="infotheo"
   matrix:
   - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.10"
-
-
+  - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.10"
 
 install: |
   # Prepare the COQ container

README.org

@@ -1,5 +1,7 @@
 * infotheo
 
+[[https://travis-ci.com/affeldt-aist/infotheo][file:https://travis-ci.com/affeldt-aist/infotheo.svg?branch=master]]
+
 ** Installation
 
    The preferred way to install infotheo is with opam because it takes
@@ -11,26 +13,21 @@
 
 *** Last stable version:
 
-Version 0.0.5:
+Version 0.0.6:
 3. ~opam install coq-infotheo~
 
 **** Requirements
 
 - [[https://coq.inria.fr][Coq]] 8.10
-- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.9.0
-- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.2.2
+- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.9.0 or 1.10.0
+- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.2.2 or 0.2.3
   which requires
-  + [[https://github.com/math-comp/bigenough/][bigenough]] first release
-  + [[https://github.com/math-comp/finmap][finmap]] 1.2.1
+  + [[https://github.com/math-comp/finmap][finmap]] 1.2.0 or greater
 
 All versions available from opam.
 
 *** Development version (git master):
 
-[[https://travis-ci.com/affeldt-aist/infotheo][file:https://travis-ci.com/affeldt-aist/infotheo.svg?branch=master]]
-
-With Coq 8.10.
-
 1. ~git clone [email protected]:affeldt-aist/infotheo.git~
 2. ~cd infotheo~
 

changelog.txt

@@ -1,5 +1,5 @@
-from 0.0.5 to 0.0.6 (wip):
---------------------------
+from 0.0.5 to 0.0.6 :
+---------------------
 renamings:
 - Pr_big_union_disj -> Boole_eq (generalization)
 - setX1' -> setX1r (direction change)

opam

@@ -25,9 +25,8 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.10" & < "8.11~"}
-  "coq-mathcomp-field" {>= "1.9.0" & < "1.10~"}
-  "coq-mathcomp-analysis"   {>= "0.2.0" & <= "0.2.2"}
+  "coq-mathcomp-field" {>= "1.9.0" & <= "1.10.0"}
+  "coq-mathcomp-analysis"   {(>= "0.2.0" & <= "0.2.3")}
 ]
 synopsis: "Infotheo"
 description: """

probability/convex_choice.v

@@ -640,15 +640,15 @@ Proof.
 elim: n points d => [|n IH] points d.
   move: (FDist.f1 d); rewrite /= big_ord0 => /Rlt_not_eq; elim.
   exact: Rlt_0_1.
-rewrite /=; case: Bool.bool_dec => [/eqP|]Hd.
+rewrite /=; case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb]Hd.
   rewrite (bigD1 ord0) //= Hd big1 /=.
     rewrite addpt0 (scalept_gt0 _ _ Rlt_0_1).
     by congr Scaled; apply val_inj; rewrite /= mulR1.
   move=> i Hi; have := FDist.f1 d.
   rewrite (bigD1 ord0) ?inE // Hd /= addRC => /(f_equal (Rminus^~ R1)).
   rewrite addRK subRR => /prsumr_eq0P -> //.
   by rewrite scalept0.
-set d' := DelFDist.d (Bool.eq_true_not_negb _ Hd).
+set d' := DelFDist.d Hd.
 set points' := fun i => points (DelFDist.f ord0 i).
 rewrite /index_enum -enumT (bigD1_seq ord0) ?enum_uniq ?mem_enum //=.
 rewrite -big_filter (perm_big (map (lift ord0) (enum 'I_n)));
@@ -659,7 +659,7 @@ rewrite /barycenter 2!big_map [in RHS]big_map.
 apply eq_bigr => i _.
 rewrite scalept_comp // DelFDist.dE D1FDist.dE /=.
 rewrite /Rdiv (mulRC (d _)) mulRA mulRV ?mul1R //.
-by move: (Bool.eq_true_not_negb _ Hd); apply contra => /eqP Hd'; rewrite -onem0 -Hd' onemK.
+by move: (Hd); apply contra => /eqP Hd'; rewrite -onem0 -Hd' onemK.
 Qed.
 End with_affine_projection.
 
@@ -688,16 +688,16 @@ Proof. by apply convn_proj; rewrite FDist1.dE eqxx. Qed.
 
 Lemma convn1E g (e : {fdist 'I_1}) : \Conv_ e g = g ord0.
 Proof.
-rewrite /=; case: Bool.bool_dec => // H; exfalso; move/eqP: (Bool.eq_true_not_negb _ H); apply.
+rewrite /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H; exfalso; move/eqP: H; apply.
 by apply/eqP; rewrite FDist1.dE1 (FDist1.I1 e).
 Qed.
 
 Lemma convnE n g (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%R) :
   \Conv_d g = g ord0 <| probfdist d ord0 |> \Conv_(DelFDist.d i1) (fun x => g (DelFDist.f ord0 x)).
 Proof.
-rewrite /=; case: Bool.bool_dec => /= H.
+rewrite /=; case: Bool.bool_dec => /= [|/Bool.eq_true_not_negb] H.
 exfalso; by rewrite (eqP H) eqxx in i1.
-by rewrite (eq_irrelevance (Bool.eq_true_not_negb _ H) i1).
+by rewrite (eq_irrelevance H i1).
 Qed.
 
 Lemma convn2E g (d : {fdist 'I_2}) :
@@ -842,7 +842,7 @@ exists 2, (fun i => if i == ord0 then a0 else a1), (I2FDist.d p); split => /=.
   move=> a2.
   case => i _ <-{a2} /=.
   case: ifPn => _; [by left | by right].
-case: Bool.bool_dec => [/eqP|H].
+case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb H].
   rewrite I2FDist.dE eqxx /= => p1.
   suff -> : p = `Pr 1 by rewrite conv1.
   exact/prob_ext.
@@ -851,7 +851,7 @@ case: Bool.bool_dec => // H'.
 exfalso.
 move: H'; rewrite DelFDist.dE D1FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)).
 rewrite I2FDist.dE (eq_sym (lift _ _)) (negbTE (neq_lift _ _)) I2FDist.dE eqxx divRR ?eqxx //.
-by move: (Bool.eq_true_not_negb _ H); rewrite I2FDist.dE eqxx onem_neq0.
+by move: H; rewrite I2FDist.dE eqxx onem_neq0.
 Qed.
 End hull_prop.