Merge pull request #79 from affeldt-aist/update_wrt_mca_040

compatibility with mca 0.4.0 and greater

changelog.txt

@@ -1,3 +1,13 @@
+-------------------
+from 0.3.6 to 0.3.7
+-------------------
+compatibility release
+
+-------------------
+from 0.3.5 to 0.3.6
+-------------------
+compatibility release
+
 -------------------
 from 0.3.4 to 0.3.5
 -------------------

coq-infotheo.opam

@@ -27,7 +27,7 @@ depends: [
   "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
   "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
   "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "0.3.11") & (< "0.4~")}
+  "coq-mathcomp-analysis" { (>= "0.3.13") & (< "0.6~")}
 ]
 
 tags: [

ecc_classic/decoding.v

@@ -281,7 +281,7 @@ pose g : nat -> R := fun d : nat => (1 - p) ^ (n - d) * p ^ d.
 have -> : W ``(y | c) = g (dH_y c).
   move: (DMC_BSC_prop p enc (discard c) y).
   set cast_card := eq_ind_r _ _ _.
-  rewrite (_ : cast_card = card_F2) //; last by apply eq_irrelevance.
+  rewrite (_ : cast_card = card_F2) //.
   clear cast_card.
   rewrite -/W compatible //.
   move/subsetP : f_img; apply.
@@ -290,7 +290,7 @@ transitivity (\big[Rmax/R0]_(c in C) (g (dH_y c))); last first.
   apply eq_bigr => /= c' Hc'.
   move: (DMC_BSC_prop p enc (discard c') y).
   set cast_card := eq_ind_r _ _ _.
-  rewrite (_ : cast_card = card_F2) //; last by apply eq_irrelevance.
+  rewrite (_ : cast_card = card_F2) //.
   by rewrite -/W compatible.
 (* the function maxed over is decreasing so we may look for its minimizer,
    which is given by minimum distance decoding *)

information_theory/convex_fdist.v

@@ -94,7 +94,7 @@ Definition avg_dom_pair p (x y : dom_pair) : dom_pair :=
 Definition uncurry_dom_pair U (f : fdist A -> fdist A -> U) (x : dom_pair) :=
   f (sval x).1 (sval x).2.
 
-Let dom_pair_choiceType := boolp.choice_of_Type dom_pair.
+Let dom_pair_choiceType := choice_of_Type dom_pair.
 Let avg := avg_dom_pair.
 Let avg1 (x y : dom_pair_choiceType) : avg 1%:pr x y = x.
 Proof. rewrite /avg; case x => x0 H /=; exact/boolp.eq_exist/conv1. Qed.
@@ -383,7 +383,7 @@ Variables (A B : finType) (P : fdist A).
 Local Open Scope divergence_scope.
 
 Lemma mutual_information_convex :
-  convex_function (fun Q : classical_sets.dep_arrow_choiceType (fun _ : A => fdist_convType B) =>
+  convex_function (fun Q : boolp.dep_arrow_choiceType (fun _ : A => fdist_convType B) =>
     MutualInfo.mi (CJFDist.make_joint P Q)).
 Proof.
 move=> p1yx p2yx t.

meta.yml

@@ -86,7 +86,7 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.3.11") & (< "0.4~")}'
+    version: '{ (>= "0.3.13") & (< "0.6~")}'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 namespace: infotheo

probability/bayes.v

@@ -50,7 +50,8 @@ Proof.
 destruct boolP.
 - congr T.
   case: p => // in H i *.
-  by rewrite (Eqdep_dec.UIP_refl_bool true i) (Eqdep_dec.UIP_refl_bool true H).
+  exfalso.
+  rewrite H in i.
 - by elim: (negP i).
 Qed.
 
@@ -62,9 +63,7 @@ Lemma boolPF  (H : is_true (~~ p)) :
 Proof.
 destruct boolP.
 - by elim: (negP H).
-- congr F.
-  case: p => // in H i *.
-  by rewrite (Eqdep_dec.UIP_refl_bool true i) (Eqdep_dec.UIP_refl_bool true H).
+- by congr F.
 Qed.
 End boolP.
 End ssr_ext.

probability/convex.v

@@ -1091,11 +1091,15 @@ Definition convex_set_of (A : convType) :=
   fun phT : phant (ConvexSpace.sort A) => convex_set A.
 Notation "{ 'convex_set' T }" := (convex_set_of (Phant T)) : convex_scope.
 
+(* kludge 2022-04-14 *)
+Definition choice_of_Type (T : Type) : choiceType :=
+  Choice.Pack (Choice.Class (@gen_eqMixin T) gen_choiceMixin).
+
 Section cset_canonical.
 Variable (A : convType).
 Canonical cset_predType := Eval hnf in
   PredType (fun t : convex_set A => (fun x => x \in CSet.car t)).
-Canonical cset_eqType := Equality.Pack (equality_mixin_of_Type (convex_set A)).
+Canonical cset_eqType := Equality.Pack (@gen_eqMixin (convex_set A)).
 Canonical cset_choiceType := choice_of_Type (convex_set A).
 End cset_canonical.
 
@@ -1770,15 +1774,15 @@ End convex_function_prop'.
 Section convex_in_both.
 Local Open Scope ordered_convex_scope.
 Variables (T U : convType) (V : orderedConvType) (f : T -> U -> V).
-Definition convex_in_both := convex_function (prod_curry f).
+Definition convex_in_both := convex_function (uncurry f).
 Lemma convex_in_bothP :
   convex_in_both
   <->
   forall a0 a1 b0 b1 t,
     f (a0 <| t |> a1) (b0 <| t |> b1) <= f a0 b0 <| t |> f a1 b1.
 Proof.
 split => [H a0 a1 b0 b1 t | H];
-  first by move: (H (a0,b0) (a1,b1) t); rewrite /convex_function_at /prod_curry.
+  first by move: (H (a0,b0) (a1,b1) t); rewrite /convex_function_at /uncurry.
 by case => a0 b0 [a1 b1] t; move:(H a0 a1 b0 b1 t).
 Qed.
 End convex_in_both.

probability/necset.v

@@ -106,7 +106,7 @@ Section neset_canonical.
 Variable A : Type.
 Canonical neset_predType :=
   Eval hnf in PredType (fun t : neset A => (fun x => x \in (t : set _))).
-Canonical neset_eqType := Equality.Pack (equality_mixin_of_Type (neset A)).
+Canonical neset_eqType := Equality.Pack (@gen_eqMixin (neset A)).
 Canonical neset_choiceType := choice_of_Type (neset A).
 End neset_canonical.
 
@@ -1016,7 +1016,7 @@ Section necset_canonical.
 Variable (A : convType).
 Canonical necset_predType :=
   Eval hnf in PredType (fun t : necset A => (fun x => x \in (t : set _))).
-Canonical necset_eqType := Equality.Pack (equality_mixin_of_Type (necset A)).
+Canonical necset_eqType := Equality.Pack (@gen_eqMixin (necset A)).
 Canonical necset_choiceType := choice_of_Type (necset A).
 (* NB(rei): redundant *)
 (*Canonical necset_neset (t : necset A) : neset A := NESet.mk (NECSet.mixin (NECSet.H t)).*)