convex_equiv.v needs to be fixed

probability/convex.v

@@ -307,7 +307,7 @@ HB.mixin Record isConvexSpace0 T of Choice T := {
       conv p a (conv q b c) = conv [s_of p, q] (conv [r_of p, q] a b) c }.
 
 #[short(type=convType)]
-HB.structure Definition ConvexSpace := {T of isConvexSpace0 T }.
+HB.structure Definition ConvexSpace := {T of isConvexSpace0 T & }.
 
 Notation "a <| p |> b" := (conv p a b) : convex_scope.
 Local Open Scope convex_scope.
@@ -485,7 +485,7 @@ HB.mixin Record isQuasiRealCone A of Choice A := {
     scalept p (scalept q x) = scalept (p * q)%coqR x }.
 
 #[short(type=quasiRealCone)]
-HB.structure Definition QuasiRealCone := { A & isQuasiRealCone A}.
+HB.structure Definition QuasiRealCone := { A of isQuasiRealCone A & }.
 
 Section quasireal_cone_theory.
 Variable A : quasiRealCone.
@@ -543,7 +543,7 @@ HB.mixin Record isRealCone A of QuasiRealCone A := {
 }.
 
 #[short(type=realCone)]
-HB.structure Definition RealCone := { A of isQuasiRealCone A & isRealCone A }.
+HB.structure Definition RealCone := { A of isRealCone A & }.
 
 Section real_cone_theory.
 Variable A : realCone.
@@ -2958,9 +2958,9 @@ TODO: see convex_type.v
 
 Section convex_set_R.
 
-Let pos := (fun x => 0 < x)%coqR.
+Definition Rpos_interval : set R := (fun x => 0 < x)%coqR.
 
-Lemma Rpos_convex : is_convex_set pos.
+Lemma Rpos_convex : is_convex_set Rpos_interval.
 Proof.
 apply/asboolP => x y t Hx Hy.
 have [->|Ht0] := eqVneq t 0%:pr; first by rewrite conv0.
@@ -2969,15 +2969,15 @@ apply mulR_ge0 => //; exact: ltRW.
 Qed.
 
 (*#[local]*)
-HB.instance Definition Rpos_interval := isConvexSet.Build R pos Rpos_convex.
+HB.instance Definition _ := isConvexSet.Build R Rpos_interval Rpos_convex.
 
-Let nneg := (fun x => 0 <= x)%coqR.
+Definition Rnonneg_interval : set R := (fun x => 0 <= x)%coqR.
 
-Lemma Rnonneg_convex : is_convex_set nneg.
+Lemma Rnonneg_convex : is_convex_set Rnonneg_interval.
 Proof. apply/asboolP=> x y t Hx Hy; apply addR_ge0; exact/mulR_ge0. Qed.
 
 (*#[local]*)
-HB.instance Definition Rnonneg_interval := isConvexSet.Build R nneg Rnonneg_convex.
+HB.instance Definition _ := isConvexSet.Build R Rnonneg_interval Rnonneg_convex.
 
 Lemma open_interval_convex a b (Hab : (a < b)%coqR) :
   is_convex_set (fun x => a < x < b)%coqR.
@@ -2996,7 +2996,7 @@ rewrite mulrDl.
   apply ltR_add; rewrite ltR_pmul2l //; [exact/RltP/prob_gt0 | exact/RltP/onem_gt0/prob_lt1].
 Qed.
 
-Let uniti := (fun x => 0 < x < 1)%coqR.
+Let uniti : set R := (fun x => 0 < x < 1)%coqR.
 
 Lemma open_unit_interval_convex : is_convex_set uniti.
 Proof. exact: open_interval_convex. Qed.

probability/convex_equiv.v

@@ -179,7 +179,7 @@ Module Type ConvSpace. Axiom T : convType. End ConvSpace.
 Module BinToNary(C : ConvSpace) <: NaryConvSpace.
 Import NaryConvexSpace.
 
-HB.instance Definition _ := @isNaryConv.Build C.T (@Convn C.T).
+HB.instance Definition _ := @isNaryConv.Build C.T (@Convn C.T conv).
 
 (* NB: is that ok? *)
 Definition T : naryConvType := C.T.
@@ -295,7 +295,7 @@ Lemma binconvmm p a : binconv p a a = a.
 Proof. by apply axidem => i; case: ifP. Qed.
 
 #[export]
-HB.instance Definition _ := @isConvexSpace.Build A.T binconv
+HB.instance Definition nary_to_bin := @isConvexSpace.Build A.T binconv
   binconv1 binconvmm binconvC binconvA.
 
 End NaryToBin.
@@ -307,21 +307,6 @@ Please report at http://coq.inria.fr/bugs/.
 (* Then prove BinToN and NToBin cancel each other:
    operations should coincide on both sides *)
 
-Module Equiv1(C : ConvSpace).
-Module A := BinToNary(C).
-Module B := NaryToBin(A).
-Import A B.
-
-Lemma equiv_conv p (a b : T) : a <| p |> b = a <& p &> b.
-Proof.
-apply: S1_inj.
-rewrite [LHS](@affine_conv (*NaryConv_sort__canonical__isConvexSpace__ConvexSpace*))/=.
-rewrite (_ : a <&p&> b = a <|p|> b)//.
-  by rewrite [RHS](@affine_conv (*NaryConv_sort__canonical__isConvexSpace__ConvexSpace*)_).
-Admitted.
-
-End Equiv1.
-
 Module Equiv2(A : NaryConvSpace).
 Module B := NaryToBin(A).
 Import A B.
@@ -353,8 +338,55 @@ apply/eqP => /(congr1 (Rplus (d ord0))).
 rewrite addRCA addRN !addR0 => b'.
 by elim b; rewrite -b' eqxx.
 Qed.
+
+(*
+Lemma equiv_conv p x y : x <& p &> y = x <| p |> y.
+Proof.
+rewrite /binconv.
+set g := fun (o : 'I_2) => if o == ord0 then x else y.
+set d := fdistI2 p.
+change x with (g ord0).
+change y with (g (lift ord0 ord0)).
+have -> : p = probfdist d ord0 by apply: val_inj=> /=; rewrite fdistI2E eqxx.
+by rewrite -ConvnI2E -equiv_convn.
+Qed.
+*)
+
 End Equiv2.
 
+Lemma convnE (s : convType) (n : nat) (d : R.-fdist 'I_n) (g : 'I_n -> s) :
+  convex.convn n d g = <|>_d g.
+Proof. Abort.
+
+Module Equiv1(C : ConvSpace).
+Module A := BinToNary(C).
+Module B := NaryToBin(A).
+Module EA := Equiv2(A).
+Import A B.
+
+Let equiv_convn n (d : {fdist 'I_n}) (g : 'I_n -> A.T) : <&>_d g = <|>_d g.
+Proof. by []. Qed.
+
+Let T' := NaryConv_sort__canonical__convex_ConvexSpace.
+
+Lemma equiv_conv p (a b : C.T) : a <| p |> b = a <& p &> b.
+Proof.
+change (a <& p &> b) with (@conv T' p a b).
+pose g := fun (x : 'I_2) => if x == ord0 then a else b.
+change a with (g ord0).
+change b with (g (lift ord0 ord0)).
+pose d := fdistI2 p.
+have -> : p = probfdist d ord0 by apply: val_inj=> /=; rewrite fdistI2E eqxx.
+rewrite -!ConvnI2E.
+
+STOP
+
+rewrite -equiv_convn.
+by rewrite EA.equiv_convn.
+Qed.
+
+End Equiv1.
+
 Module Type MapConst.
 Parameter T : naryConvType.
 Parameter axmap : ax_map T.

probability/partition_inequality.v

@@ -1,6 +1,6 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
-From mathcomp Require Import all_ssreflect ssrnum.
+From mathcomp Require Import all_ssreflect ssralg ssrnum.
 Require Import Reals Lra.
 From mathcomp Require Import Rstruct.
 Require Import ssrR realType_ext Reals_ext Ranalysis_ext ssr_ext logb ln_facts.
@@ -36,7 +36,7 @@ Variable P : {fdist A}.
 
 Definition bipart_pmf := [ffun i => \sum_(a in A_ i) P a].
 
-Definition bipart : {fdist [finType of bool]}.
+Definition bipart : {fdist bool}.
 apply (@FDist.make _ _ bipart_pmf).
 - by move=> a; rewrite ffunE; apply: sumr_ge0.
 - rewrite big_bool /= /bipart_pmf /= !ffunE.