wip

lib/Reals_ext.v

@@ -264,7 +264,6 @@ have [/RleP ? /RleP ?] : (0 <= / IZR (Zpos p) <= 1)%coqR.
   - exact/IZR_le/Pos2Z.pos_le_pos/Pos.le_1_l.
 exact/andP.
 Qed.
-HB.about GRing.isSemiRing.Build.
 
 Canonical probIZR (p : positive) := Eval hnf in Prob.mk (prob_IZR_subproof p).
 

probability/convex.v

@@ -1865,7 +1865,9 @@ Let avgA p q (d0 d1 d2 : R) :
   avg p d0 (avg q d1 d2) = avg [s_of p, q] (avg [r_of p, q] d0 d1) d2.
 Proof. by rewrite /avg convA. Qed.
 
-#[non_forgetful_inheritance] HB.instance Definition _ := @isConvexSpace.Build R _ avg1 avgI avgC avgA.
+#[export]
+(* TODO(rei): attributed needed? *)
+(*#[non_forgetful_inheritance]*) HB.instance Definition _ := @isConvexSpace.Build R _ avg1 avgI avgC avgA.
 
 Lemma avgRE p (x y : R) : x <| p |> y = (Prob.p p * x + (Prob.p p).~ * y)%coqR. Proof. by []. Qed.
 
@@ -1914,6 +1916,7 @@ Qed.
 
 End R_convex_space.
 End RConvex.
+HB.export RConvex.
 
 Section fun_convex_space.
 Variables (A : choiceType) (B : convType).
@@ -2252,7 +2255,7 @@ Section opposite_ordered_convex_space.
 Import OppositeOrderedConvexSpace.
 Variable A : orderedConvType.
 
-HB.instance Definition _ := isOrdered.Build (T A)(@leoppR A) (@leopp_trans A) (@eqopp_le A).
+HB.instance Definition _ := isOrdered.Build (T A) (@leoppR A) (@leopp_trans A) (@eqopp_le A).
 
 End opposite_ordered_convex_space.
 
@@ -2713,14 +2716,16 @@ apply addR_gt0wl; first by apply mulR_gt0 => //; exact/RltP/prob_gt0.
 apply mulR_ge0 => //; exact: ltRW.
 Qed.
 
-#[local] HB.instance Definition _ := isConvexSet.Build R pos Rpos_convex.
+(*#[local]*)
+HB.instance Definition Rpos_interval := isConvexSet.Build R pos Rpos_convex.
 
 Let nneg := (fun x => 0 <= x)%coqR.
 
 Lemma Rnonneg_convex : is_convex_set nneg.
 Proof. apply/asboolP=> x y t Hx Hy; apply addR_ge0; exact/mulR_ge0. Qed.
 
-#[local] HB.instance Definition _ := isConvexSet.Build R nneg Rnonneg_convex.
+(*#[local]*)
+HB.instance Definition Rnonneg_interval := isConvexSet.Build R nneg Rnonneg_convex.
 
 Lemma open_interval_convex a b (Hab : (a < b)%coqR) :
   is_convex_set (fun x => a < x < b)%coqR.

probability/convex_equiv.v

@@ -39,8 +39,7 @@ Local Open Scope convex_scope.
 
 Module NaryConvexSpace.
 
-HB.mixin Record isNaryConv (T : Type) := {
-  narychoice : Choice.class_of T ;
+HB.mixin Record isNaryConv (T : choiceType) := {
   convn : forall n, {fdist 'I_n} -> ('I_n -> T) -> T
 }.
 
@@ -49,9 +48,6 @@ HB.structure Definition NaryConv := {T & isNaryConv T}.
 
 Notation "'<&>_' d f" := (convn _ d f) : convex_scope.
 
-Canonical naryconv_eqType (T : naryConvType) := EqType T narychoice.
-Canonical conv_choiceType (T : naryConvType) := ChoiceType T narychoice.
-
 End NaryConvexSpace.
 
 Module NaryConvexSpaceEquiv.
@@ -183,10 +179,10 @@ Module Type ConvSpace. Axiom T : convType. End ConvSpace.
 Module BinToNary(C : ConvSpace) <: NaryConvSpace.
 Import NaryConvexSpace.
 
-HB.instance Definition _ := @isNaryConv.Build _ (Choice.class _) (@Convn C.T).
+HB.instance Definition _ := @isNaryConv.Build _ (@Convn C.T).
 
 (* NB: is that ok? *)
-Definition T : naryConvType := Choice_sort__canonical__NaryConvexSpace_NaryConv.
+Definition T : naryConvType := C.T.
 Definition axbary := @Convn_fdist_convn C.T.
 Definition axproj := @Convn_fdist1 C.T.
 End BinToNary.
@@ -264,7 +260,7 @@ rewrite /binconv.
 set g := fun i : 'I_3 => if i <= 0 then a else if i <= 1 then b else c.
 rewrite [X in <&>_(fdistI2 q) X](_ : _ = g \o lift ord0); last first.
   by apply funext => i; case/orP: (ord2 i) => /eqP ->.
-rewrite [X in <&>_(_ [r_of p, q]) X](_ : _ = g \o (widen_ord (leqnSn 2))); last first.
+rewrite [X in <&>_(fdistI2 [r_of p, q]) X](_ : _ = g \o (widen_ord (leqnSn 2))); last first.
   by apply funext => i; case/orP: (ord2 i) => /eqP ->.
 rewrite 2!axmap.
 set d1 := fdistmap _ _.
@@ -299,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 (Choice.class _) binconv
+HB.instance Definition _ := @isConvexSpace.Build A.T binconv
   binconv1 binconvmm binconvC binconvA.
 
 End NaryToBin.

probability/convex_stone.v

@@ -211,7 +211,7 @@ by move /(@perm_inj _ s)/lift_inj.
 Qed.
 
 Lemma swap_asaE n (s : 'S_n.+2) (K : s ord0 != ord0) :
-  s = (lift_perm ord0 ord0 (PermDef.perm (swap_asa_inj K)) * tperm (ord0) (s ord0))%g.
+  s = (lift_perm ord0 ord0 (perm (swap_asa_inj K)) * tperm (ord0) (s ord0))%g.
 Proof.
 apply/permP => i.
 rewrite [in RHS]permE /=.
@@ -707,6 +707,8 @@ congr (_ <| _ |> _).
   rewrite s_of_pqE /= /onem.
   rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj.
   rewrite -R1E -!RminusE -!RdivE'// -!RmultE.
+  set tmp1 := d _.
+  set tmp2 := d _.
   field.
   split; first by rewrite subR_eq0; exact/nesym.
   rewrite -addR_opp oppRB -addR_opp oppRB addRC addRA subRK.
@@ -719,6 +721,8 @@ congr (_ <| _ |> _).
     rewrite (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj.
     rewrite -[RHS]RdivE'.
     rewrite -R1E -!RminusE -!RdivE' // -!RmultE.
+    set tmp1 := d _.
+    set tmp2 := d _.
     field.
     split.
     rewrite subR_eq0.
@@ -879,7 +883,7 @@ Lemma Convn_perm_projection n (d : {fdist 'I_n.+2})
 Proof.
 transitivity (g ord0 <| probfdist d ord0 |> (<|>_(fdist_del dmax1) (fun x => g (fdist_del_idx ord0 x)))).
   by rewrite convnE.
-set s' : 'S_n.+1 := PermDef.perm (Sn.proj0_inj H).
+set s' : 'S_n.+1 := perm (Sn.proj0_inj H).
 transitivity (g ord0 <| probfdist d ord0 |> (<|>_(fdistI_perm (fdist_del dmax1) s') ((fun x => g (fdist_del_idx ord0 x)) \o s'))).
   by rewrite -IH.
 transitivity (g (s ord0) <| probfdist d ord0 |> (<|>_(fdistI_perm (fdist_del dmax1) s') ((fun x => g (fdist_del_idx ord0 x)) \o s'))).
@@ -1123,7 +1127,9 @@ apply/fdist_ext => a.
 rewrite fdist_convE fdist_convnE /= big_ord_recl; congr (_ + _)%coqR.
 rewrite IH fdist_convnE big_distrr /=; apply eq_bigr => i _.
 rewrite fdist_delE fdistD1E eq_sym (negbTE (neq_lift _ _)).
-by rewrite mulrAC mulrC !mulrA mulrV ?mul1r //; exact/onem_neq0.
+rewrite mulrAC mulrC -!mulrA; congr (_ * _)%mcR.
+rewrite /fdist_del_idx ltn0 /onem mulVr ?mulr1//.
+exact/onem_neq0.
 Qed.
 
 End convn_convnfdist.

probability/fsdist.v

@@ -57,10 +57,10 @@ Local Open Scope fdist_scope.
 
 Import Order.POrderTheory Num.Theory.
 
-Lemma fdist_Rgt0 (A : finType) (d : real_realType.-fdist A) a :
+Lemma fdist_Rgt0 (A : finType) (d : R.-fdist A) a :
   (d a != 0) <-> (0 < d a)%coqR.
 Proof. by rewrite fdist_gt0; split=> /RltP. Qed.
-Lemma fdist_Rge0 (A : finType) (d : real_realType.-fdist A) a :
+Lemma fdist_Rge0 (A : finType) (d : R.-fdist A) a :
   0 <= d a.
 Proof. by apply/RleP; rewrite FDist.ge0. Qed.
 
@@ -95,7 +95,7 @@ Section fsdist.
 Variable A : choiceType.
 
 Record t := mk {
-  f :> {fsfun A -> real_realType with 0} ;
+  f :> {fsfun A -> R with 0} ;
   _ : all (fun x => (0 < f x)%mcR) (finsupp f) &&
       \sum_(a <- finsupp f) f a == 1}.
 
@@ -145,16 +145,15 @@ Global Hint Resolve FSDist.ge0 : core.
 
 Section FSDist_canonical.
 Variable A : choiceType.
-Canonical FSDist_subType := Eval hnf in [subType for @FSDist.f A].
-Definition FSDist_eqMixin := [eqMixin of fsdist A by <:].
-Canonical FSDist_eqType := Eval hnf in EqType _ FSDist_eqMixin.
-Definition FSDist_choiceMixin := [choiceMixin of fsdist A by <:].
-Canonical FSDist_choiceType := Eval hnf in ChoiceType _ FSDist_choiceMixin.
+HB.instance Definition _ := [isSub for @FSDist.f A].
+HB.instance Definition _ := [Equality of fsdist A by <:].
+HB.instance Definition _ := [Choice of fsdist A by <:].
 End FSDist_canonical.
 
-Definition FSDist_to_Type (A : choiceType) :=
+(*Definition FSDist_to_Type (A : choiceType) :=
   fun phT : phant (Choice.sort A) => fsdist A.
-Local Notation "{ 'dist' T }" := (FSDist_to_Type (Phant T)).
+Local Notation "{ 'dist' T }" := (FSDist_to_Type (Phant T)).*)
+Local Notation "{ 'dist' T }" := (fsdist T).
 
 Section fsdist_prop.
 Variable A : choiceType.
@@ -416,14 +415,14 @@ Definition FSDist_prob (C : choiceType) (d : {dist C}) (x : C) : {prob R} :=
   Eval hnf in Prob.mk_ (andb_true_intro (conj (FSDist.ge0' d x) (FSDist.le1' d x))).
 Canonical FSDist_prob.
 
-Definition fsdistjoin A (D : {dist (FSDist_choiceType A)}) : {dist A} :=
+Definition fsdistjoin A (D : {dist {dist A}}) : {dist A} :=
   D >>= ssrfun.id.
 
-Lemma fsdistjoinE A (D : {dist (FSDist_choiceType A)}) x :
+Lemma fsdistjoinE A (D : {dist {dist A}}) x :
   fsdistjoin D x = \sum_(d <- finsupp D) D d * d x.
 Proof. by rewrite /fsdistjoin fsdistbindE. Qed.
 
-Lemma fsdistjoin1 (A : choiceType) (D : {dist (FSDist_choiceType A)}) :
+Lemma fsdistjoin1 (A : choiceType) (D : {dist {dist A}}) :
   fsdistjoin (fsdist1 D) = D.
 Proof.
 apply/fsdist_ext => d.
@@ -503,7 +502,7 @@ End FSDist_lift_supp.
 
 Module FSDist_of_fdist.
 Section def.
-Variable (A : finType) (P : real_realType.-fdist A).
+Variable (A : finType) (P : R.-fdist A).
 
 Let D := [fset a0 : A | P a0 != 0].
 Definition f : {fsfun A -> R with 0} := [fsfun a in D => P a | 0].
@@ -543,7 +542,7 @@ Qed.
 Lemma f0' b : (0 <= f b)%O. (* TODO: we shouldn't see %O *)
 Proof. exact/RleP/f0. Qed.
 
-Definition d : real_realType.-fdist D := locked (FDist.make f0' f1).
+Definition d : R.-fdist D := locked (FDist.make f0' f1).
 End def.
 Module Exports.
 Notation fdist_of_fs := d.
@@ -579,7 +578,7 @@ rewrite [X in (_ + X = _)%coqR](_ : _ = 0) ?addR0.
 by rewrite big1 // => a; rewrite mem_finsupp negbK ffunE => /eqP.
 Qed.
 
-Definition d : real_realType.-fdist A := locked (FDist.make f0' f1).
+Definition d : R.-fdist A := locked (FDist.make f0' f1).
 
 Lemma dE a : d a = P a.
 Proof. by rewrite /d; unlock; rewrite ffunE. Qed.
@@ -592,7 +591,7 @@ End fdist_of_finFSDist.
 Export fdist_of_finFSDist.Exports.
 
 Section fsdist_conv_def.
-Variables (A : choiceType) (p : {prob real_realType}) (d1 d2 : {dist A}).
+Variables (A : choiceType) (p : {prob R}) (d1 d2 : {dist A}).
 Local Open Scope reals_ext_scope.
 Local Open Scope convex_scope.
 
@@ -628,8 +627,7 @@ Proof.
 move => /[dup]; rewrite {1}supp => aD.
 rewrite /f ltR_neqAle mem_finsupp eq_sym => /eqP ?; split => //.
 rewrite /f fsfunE avgRE aD.
-by apply/RleP; rewrite RplusE !RmultE addr_ge0// mulr_ge0//;
-  [exact/RleP|exact/onem_ge0|exact/RleP].
+by apply/RleP; rewrite RplusE !RmultE addr_ge0// mulr_ge0//.
 Qed.
 
 Let f1 : \sum_(a <- finsupp f) f a = 1.
@@ -668,7 +666,7 @@ End fsdist_conv_def.
 
 Section fsdist_convType.
 Variables (A : choiceType).
-Implicit Types (p q : {prob real_realType}) (a b c : {dist A}).
+Implicit Types (p q : {prob R}) (a b c : {dist A}).
 Local Open Scope reals_ext_scope.
 
 Local Notation "x <| p |> y" := (fsdist_conv p x y) : fsdist_scope.
@@ -690,14 +688,14 @@ Let convA p q a b c :
 Proof. by apply/fsdist_ext=> ?; rewrite !fsdist_convE convA. Qed.
 
 HB.instance Definition _ :=
-  @isConvexSpace.Build (FSDist.t _) (Choice.class _) (@fsdist_conv A)
+  @isConvexSpace.Build (FSDist.t _) (@fsdist_conv A)
   conv1 convmm convC convA.
 
 End fsdist_convType.
 
 Section fsdist_conv_prop.
 Variables (A : choiceType).
-Implicit Types (p : {prob real_realType}) (a b c : {dist A}).
+Implicit Types (p : {prob R}) (a b c : {dist A}).
 Local Open Scope reals_ext_scope.
 Local Open Scope convex_scope.
 
@@ -734,15 +732,16 @@ Lemma supp_fsdist_conv p (p0 : p != 0%:pr) (p1 : p != 1%:pr) a b :
   finsupp (a <|p|> b) = finsupp a `|` finsupp b.
 Proof. by rewrite supp_fsdist_conv' (negPf p0) (negPf p1). Qed.
 
-Lemma fsdist_scalept_conv (C : convType) (x y : {dist C}) (p : {prob real_realType}) (i : C) :
+Lemma fsdist_scalept_conv (C : convType) (x y : {dist C}) (p : {prob R}) (i : C) :
   scalept ((x <|p|> y) i) (S1 i) = scalept (x i) (S1 i) <|p|> scalept (y i) (S1 i).
 Proof. by rewrite fsdist_convE scalept_conv. Qed.
 
 End fsdist_conv_prop.
 
-Definition FSDist_to_convType (A : choiceType) :=
+(*Definition FSDist_to_convType (A : choiceType) :=
   fun phT : phant (Choice.sort A) => conv_choiceType [the convType of FSDist.t A].
-Notation "{ 'dist' T }" := (FSDist_to_convType (Phant T)) : proba_scope.
+Notation "{ 'dist' T }" := (FSDist_to_convType (Phant T)) : proba_scope.*)
+Notation "{ 'dist' T }" := (FSDist.t T) : proba_scope.
 
 Local Open Scope reals_ext_scope.
 Local Open Scope proba_scope.

probability/graphoid.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 ssralg matrix.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 Require Import Reals.
 From mathcomp Require Import Rstruct.
 Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist.

probability/jensen.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 ssralg matrix.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 From mathcomp Require Import boolp Rstruct.
 Require Import Reals.
 Require Import ssrR Reals_ext ssr_ext realType_ext ssralg_ext logb.

probability/jfdist_cond.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 ssralg matrix.
+From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
 From mathcomp Require boolp.
 From mathcomp Require Import Rstruct.
 Require Import Reals.
@@ -220,7 +220,7 @@ Lemma jproduct_rule E F : Pr P (E `* F) = \Pr_P[E | F] * Pr (P`2) F.
 Proof.
 have [/eqP PF0|PF0] := boolP (Pr (P`2) F == 0).
   rewrite jcPrE /cPr -{1}(setIT E) -{1}(setIT F) -setIX.
-  rewrite Pr_domin_setI; last by rewrite -Pr_fdistX Pr_domin_setX // fdistX1.
+  rewrite [LHS]Pr_domin_setI; last by rewrite -Pr_fdistX Pr_domin_setX // fdistX1.
   by rewrite setIC Pr_domin_setI ?(div0R,mul0R) // setTE Pr_setTX.
 rewrite -{1}(setIT E) -{1}(setIT F) -setIX product_rule.
 rewrite -EsetT setTT cPrET Pr_setT mulR1 jcPrE.
@@ -267,7 +267,9 @@ Arguments jcPr_fdistmap_l [A] [A'] [B] [f] [d] [E] [F] _.
 Lemma Pr_jcPr_unit (A : finType) (E : {set A}) (P : {fdist A}) :
   Pr P E = \Pr_(fdistmap (fun a => (a, tt)) P) [E | setT].
 Proof.
-rewrite /jcPr (Pr_set1 _ tt).
+rewrite /jcPr/= (_ : [set: unit] = [set tt]); last first.
+  by apply/setP => -[]; rewrite !inE eqxx.
+rewrite (Pr_set1 _ tt).
 rewrite (_ : _`2 = fdist1 tt) ?fdist1xx ?divR1; last first.
   rewrite /fdist_snd fdistmap_comp; apply/fdist_ext; case.
   by rewrite fdistmapE fdist1xx (eq_bigl xpredT) // FDist.f1.

probability/ln_facts.v

@@ -1,8 +1,9 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require boolp.
-From mathcomp Require Import Rstruct.
+From mathcomp Require Import Rstruct reals.
 Require Import Reals Lra.
 Require Import ssrR realType_ext Reals_ext Ranalysis_ext logb convex.