From 9cd5b1762edb0780a7c702ae80f5cbc32c9c7b85 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 10 Apr 2024 12:42:26 +0900
Subject: [PATCH] wip

---
 lib/Reals_ext.v            |  1 -
 probability/convex.v       | 13 ++++---
 probability/convex_equiv.v | 14 +++-----
 probability/convex_stone.v | 12 +++++--
 probability/fsdist.v       | 49 +++++++++++++-------------
 probability/graphoid.v     |  2 +-
 probability/jensen.v       |  2 +-
 probability/jfdist_cond.v  |  8 +++--
 probability/ln_facts.v     |  3 +-
 probability/proba.v        | 72 ++++----------------------------------
 10 files changed, 62 insertions(+), 114 deletions(-)

diff --git a/lib/Reals_ext.v b/lib/Reals_ext.v
index 581a4344..2430364b 100644
--- a/lib/Reals_ext.v
+++ b/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).
 
diff --git a/probability/convex.v b/probability/convex.v
index e795021e..c0f9d04c 100644
--- a/probability/convex.v
+++ b/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.
diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v
index 01ebc90a..409ba1fe 100644
--- a/probability/convex_equiv.v
+++ b/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.
diff --git a/probability/convex_stone.v b/probability/convex_stone.v
index dbe54591..2dec32f0 100644
--- a/probability/convex_stone.v
+++ b/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.
diff --git a/probability/fsdist.v b/probability/fsdist.v
index 29554ed3..5a68b562 100644
--- a/probability/fsdist.v
+++ b/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.
diff --git a/probability/graphoid.v b/probability/graphoid.v
index 5df9e479..9a41c2d9 100644
--- a/probability/graphoid.v
+++ b/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.
diff --git a/probability/jensen.v b/probability/jensen.v
index 425c6d90..abfb7a52 100644
--- a/probability/jensen.v
+++ b/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.
diff --git a/probability/jfdist_cond.v b/probability/jfdist_cond.v
index bb2e58e1..8d0c146b 100644
--- a/probability/jfdist_cond.v
+++ b/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.
diff --git a/probability/ln_facts.v b/probability/ln_facts.v
index 2fc4870a..c5038fc9 100644
--- a/probability/ln_facts.v
+++ b/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.
 
diff --git a/probability/proba.v b/probability/proba.v
index 31b05d88..34f88e15 100644
--- a/probability/proba.v
+++ b/probability/proba.v
@@ -177,7 +177,6 @@ End TsetT.
   solve [apply/RleP; exact: FDist.le1] : core.
 
 Section probability.
-Notation R := Rstruct.real_realType.
 
 Variables (A : finType) (P : R.-fdist A).
 Implicit Types E : {set A}.
@@ -345,7 +344,6 @@ by move=> /(_ a); rewrite mem_index_enum => /(_ isT); rewrite aE implyTb.
 Qed.
 
 Section Pr_extra.
-Notation R := real_realType.
 
 Variables (A B : finType) (P : R.-fdist (A * B)).
 Implicit Types (E : {set A}) (F : {set B}).
@@ -389,7 +387,7 @@ Lemma Pr_domin_setXN (A B : finType) (P : {fdist A * B}) E F :
   Pr P (E `* F) != 0 -> Pr P`1 E != 0.
 Proof. by apply/contra => /eqP/Pr_domin_setX => ?; exact/eqP. Qed.
 
-Lemma Pr_fdistmap (A B : finType) (f : A -> B) (d : real_realType.-fdist A) (E : {set A}) :
+Lemma Pr_fdistmap (A B : finType) (f : A -> B) (d : R.-fdist A) (E : {set A}) :
   injective f ->
   Pr d E = Pr (fdistmap f d) (f @: E).
 Proof.
@@ -485,7 +483,6 @@ Local Close Scope vec_ext_scope.
 
 Section random_variable.
 Variables (U : finType) (T : eqType).
-Notation R := real_realType.
 
 Definition RV (P : R.-fdist U) := U -> T.
 
@@ -500,7 +497,6 @@ End random_variable.
 Notation "{ 'RV' P -> T }" := (RV_of P (Phant _) (Phant T)) : proba_scope.
 
 Section random_variable_eqType.
-Notation R := real_realType.
 Variables (U : finType) (A : eqType) (P : R.-fdist U).
 
 Definition pr_eq (X : {RV P -> A}) (a : A) := locked (Pr P (finset (X @^-1 a))).
@@ -535,7 +531,6 @@ Notation "`Pr[ X = a ]" := (pr_eq X a) : proba_scope.
 Global Hint Resolve pr_eq_ge0 : core.
 
 Section random_variable_order.
-Notation R := real_realType.
 Variables (U : finType) (d : unit) (T : porderType d) (P : R.-fdist U).
 Variables (X : {RV P -> T}).
 
@@ -548,7 +543,6 @@ Notation "'`Pr[' X '>=' r ']'" := (pr_geq X r) : proba_scope.
 Notation "'`Pr[' X '<=' r ']'" := (pr_leq X r) : proba_scope.
 
 Section random_variable_finType.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U) (A : finType).
 
 Definition pr_eq_set (X : {RV P -> A}) (E : {set A}) :=
@@ -581,8 +575,6 @@ Notation "`Pr[ X '\in' E ]" := (pr_eq_set X E) : proba_scope.
 Notation "`p_ X" := (dist_of_RV X) : proba_scope.
 
 Section random_variables.
-Notation R := real_realType.
-
 Variables (U : finType) (P : R.-fdist U).
 
 Definition const_RV (T : eqType) cst : {RV P -> T} := fun=> cst.
@@ -617,7 +609,6 @@ Notation "'`--' P" := (neg_RV P) : proba_scope.
 Notation "'`log' P" := (log_RV P) : proba_scope.
 
 Section RV_lemmas.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U).
 Implicit Types X : {RV P -> R}.
 
@@ -636,7 +627,6 @@ Proof. by rewrite sq_RV_pow2; exact: pow2_ge_0. Qed.
 End RV_lemmas.
 
 Section pair_of_RVs.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U).
 Variables (A : eqType) (X : {RV P -> A}) (B : eqType) (Y : {RV P -> B}).
 Definition RV2 : {RV P -> A * B} := fun x => (X x, Y x).
@@ -645,7 +635,6 @@ End pair_of_RVs.
 Notation "'[%' x , y , .. , z ']'" := (RV2 .. (RV2 x y) .. z).
 
 Section RV2_prop.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U).
 Variables (A B : finType) (X : {RV P -> A}) (Y : {RV P -> B}).
 
@@ -667,7 +656,6 @@ Proof. by []. Qed.
 End RV2_prop.
 
 Section RV3_prop.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U).
 Variables (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
@@ -688,10 +676,10 @@ Proof. by rewrite /fdistC12 /dist_of_RV /fdistA fdistmap_comp. Qed.
 
 End RV3_prop.
 
-Lemma pr_eq_unit (U : finType) (P : real_realType.-fdist U) : `Pr[ (unit_RV P) = tt ] = 1.
+Lemma pr_eq_unit (U : finType) (P : R.-fdist U) : `Pr[ (unit_RV P) = tt ] = 1.
 Proof. by rewrite pr_eqE'; apply/eqP/fdist1P; case. Qed.
 
-Lemma Pr_fdistmap_RV2 (U : finType) (P : real_realType.-fdist U) (A B : finType)
+Lemma Pr_fdistmap_RV2 (U : finType) (P : R.-fdist U) (A B : finType)
   (E : {set A}) (F : {set B}) (X : {RV P -> A}) (Z : {RV P -> B}) :
   Pr `p_[% X, Z] (E `* F) =
   Pr P ([set x | preim X (mem E) x] :&: [set x | preim Z (mem F) x]).
@@ -705,7 +693,6 @@ by rewrite fdistmapE.
 Qed.
 
 Section pr_pair.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U).
 Variables (A B C : finType) (TA TB TC : eqType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}).
@@ -776,7 +763,6 @@ by apply/imsetP/idP => [[a aE [] ->//]|XuE]; exists (X u).
 Qed.
 
 Section RV_domin.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U) (A B : finType) (TA TB : eqType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}).
 Variables (TX : {RV P -> A}) (TY : {RV P -> B}).
@@ -797,11 +783,11 @@ End RV_domin.
 
 Local Open Scope vec_ext_scope.
 
-Definition cast_RV_fdist_rV1 (U : finType) (P : real_realType.-fdist U) (T : eqType) (X : {RV P -> T})
+Definition cast_RV_fdist_rV1 (U : finType) (P : R.-fdist U) (T : eqType) (X : {RV P -> T})
    : {RV (P `^ 1) -> T} :=
   fun x => X (x ``_ ord0).
 
-Definition cast_RV_fdist_rV10 (U : finType) (P : real_realType.-fdist U) (T : eqType)
+Definition cast_RV_fdist_rV10 (U : finType) (P : R.-fdist U) (T : eqType)
     (Xs : 'rV[{RV P -> T}]_1) : {RV (P `^ 1) -> T} :=
   cast_RV_fdist_rV1 (Xs ``_ ord0).
 
@@ -814,7 +800,6 @@ Definition cast_fun_rV10 U (T : eqType) (Xs : 'rV[U -> T]_1) : 'rV[U]_1 -> T :=
 Local Close Scope vec_ext_scope.
 
 Section expected_value_def.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}).
 
 Definition Ex := \sum_(u in U) X u * P u.
@@ -829,7 +814,6 @@ Notation "'`E'" := (@Ex _ _) : proba_scope.
 
 (* Alternative definition of the expected value: *)
 Section Ex_alt.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}).
 
 Definition Ex_alt := \sum_(r <- fin_img X) r * `Pr[ X = r ].
@@ -846,8 +830,6 @@ Qed.
 End Ex_alt.
 
 Section expected_value_prop.
-Notation R := real_realType.
-
 Variables (U : finType) (P : R.-fdist U) (X Y : {RV P -> R}).
 
 Lemma E_neg_RV : `E (`-- X) = - `E X.
@@ -919,7 +901,7 @@ Proof. move=> H; by rewrite /comp_RV /= H. Qed.
 
 End expected_value_prop.
 
-Lemma E_cast_RV_fdist_rV1 (A : finType) (P : real_realType.-fdist A) :
+Lemma E_cast_RV_fdist_rV1 (A : finType) (P : R.-fdist A) :
   forall (X : {RV P -> R}), `E (cast_RV_fdist_rV1 X) = `E X.
 Proof.
 move=> f; rewrite /cast_RV_fdist_rV1 /=; apply big_rV_1 => // m.
@@ -927,8 +909,6 @@ by rewrite -fdist_rV1.
 Qed.
 
 Section conditional_expectation_def.
-Notation R := real_realType.
-
 Variable (U : finType) (P : R.-fdist U) (X : {RV P -> R}) (F : {set U}).
 
 Definition cEx :=
@@ -938,8 +918,6 @@ End conditional_expectation_def.
 Notation "`E_[ X | F ]" := (cEx X F).
 
 Section conditional_expectation_prop.
-Notation R := real_realType.
-
 Variable (U I : finType) (P : R.-fdist U) (X : {RV P -> R}) (F : I -> {set U}).
 Hypothesis dis : forall i j, i != j -> [disjoint F i & F j].
 Hypothesis cov : cover [set F i | i in I] = [set: U].
@@ -1024,7 +1002,6 @@ End Ind.
     contributed by Erik Martin-Dorel: the corresponding theorem is named
     [Pr_bigcup_incl_excl] and is more general than lemma [Pr_bigcup]. *)
 Section probability_inclusion_exclusion.
-Notation R := real_realType.
 Variables (A : finType) (P : R.-fdist A).
 
 Let SumIndCap (n : nat) (S : 'I_n -> {set A}) (k : nat) (x : A) :=
@@ -1147,7 +1124,6 @@ Proof. by move=> r0; rewrite leR_pdivl_mulr // mulRC; exact/Ex_lb. Qed.
 End markov_inequality.
 
 Section thm61.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}) (phi : R -> R).
 
 Lemma Ex_comp_RV : `E (phi `o X) = \sum_(r <- fin_img X) phi r * `Pr[ X = r ].
@@ -1163,8 +1139,6 @@ Qed.
 End thm61.
 
 Section variance_def.
-Notation R := real_realType.
-
 Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}).
 
 (* Variance of a random variable (\sigma^2(X) = V(X) = E (X^2) - (E X)^2): *)
@@ -1184,8 +1158,6 @@ Arguments Var {U} _ _.
 Notation "'`V'" := (@Var _ _) : proba_scope.
 
 Section variance_prop.
-Notation R := real_realType.
-
 Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}).
 
 (* The variance is not linear V (k X) = k^2 V (X) \cite[Theorem 6.7]{probook}: *)
@@ -1218,8 +1190,6 @@ Qed.
  In any data sample, "nearly all" the values are "close to" the mean value:
  Pr[ |X - E X| \geq \epsilon] \leq V(X) / \epsilon^2 *)
 Section chebyshev.
-Notation R := real_realType.
-
 Variables (U : finType) (P : R.-fdist U) (X : {RV P -> R}).
 
 Lemma chebyshev_inequality epsilon : 0 < epsilon ->
@@ -1245,8 +1215,6 @@ Qed.
 End chebyshev.
 
 Section independent_events.
-Notation R := real_realType.
-
 Variables (A : finType) (d : R.-fdist A).
 
 Definition inde_events (E F : {set A}) := Pr d (E :&: F) = Pr d E * Pr d F.
@@ -1267,8 +1235,6 @@ Qed.
 End independent_events.
 
 Section k_wise_independence.
-Notation R := real_realType.
-
 Variables (A I : finType) (k : nat) (d : R.-fdist A) (E : I -> {set A}).
 
 Definition kwide_inde := forall (J : {set I}), (#|J| <= k)%nat ->
@@ -1277,8 +1243,6 @@ Definition kwide_inde := forall (J : {set I}), (#|J| <= k)%nat ->
 End k_wise_independence.
 
 Section pairwise_independence.
-Notation R := real_realType.
-
 Variables (A I : finType) (d : R.-fdist A) (E : I -> {set A}).
 
 Definition pairwise_inde := @kwide_inde A I 2%nat d E.
@@ -1306,8 +1270,6 @@ Qed.
 End pairwise_independence.
 
 Section mutual_independence.
-Notation R := real_realType.
-
 Variables (A I : finType) (d : R.-fdist A) (E : I -> {set A}).
 
 Definition mutual_inde := (forall k, @kwide_inde A I k.+1 d E).
@@ -1336,7 +1298,6 @@ Qed.
 End mutual_independence.
 
 Section conditional_probablity.
-Notation R := real_realType.
 Variables (A : finType) (d : R.-fdist A).
 Implicit Types E F : {set A}.
 
@@ -1457,7 +1418,6 @@ Notation "`Pr_ P [ E | F ]" := (cPr P E F) : proba_scope.
 Global Hint Resolve cPr_ge0 : core.
 
 Section fdist_cond.
-Notation R := real_realType.
 Variables (A : finType) (P : R.-fdist A) (E : {set A}).
 Hypothesis E0 : Pr P E != 0.
 
@@ -1483,7 +1443,6 @@ Definition fdist_cond : {fdist A} := locked (FDist.make f0 f1).
 End fdist_cond.
 
 Section fdist_cond_prop.
-Notation R := real_realType.
 Variables (A : finType) (P : R.-fdist A) (E : {set A}).
 
 Hypothesis E0 : Pr P E != 0.
@@ -1540,7 +1499,6 @@ by apply/fdist_proj23_domin/H; rewrite inE /= bF cG.
 Qed.
 
 Section conditionally_independent_events.
-Notation R := real_realType.
 Variables (A : finType) (d : R.-fdist A).
 
 Definition cinde_events (E F G : {set A}) :=
@@ -1565,7 +1523,6 @@ Proof. by split; rewrite /cinde_events /inde_events !cPrET. Qed.
 End conditionally_independent_events.
 
 Section crandom_variable_eqType.
-Notation R := real_realType.
 Variables (U : finType) (A B : eqType) (P : R.-fdist U).
 
 Definition cpr_eq (X : {RV P -> A}) (a : A) (Y : {RV P -> B}) (b : B) :=
@@ -1593,7 +1550,6 @@ by apply/setP => u; rewrite !inE xpair_eqE.
 Qed.
 
 Section crandom_variable_finType.
-Notation R := real_realType.
 Variables (U A B : finType) (P : R.-fdist U).
 Implicit Types X : {RV P -> A}.
 
@@ -1647,7 +1603,6 @@ by rewrite setTE Pr_fdistmap_RV2; congr Pr; apply/setP => u; rewrite !inE.
 Qed.
 
 Section cpr_pair.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U) (A B C D : finType) (TA TB TC TD : eqType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 Variables (TX : {RV P -> TA}) (TY : {RV P -> TB}) (TZ : {RV P -> TC}) (TW : {RV P -> TD}).
@@ -1810,8 +1765,6 @@ by apply eq_bigr => b _; rewrite pr_in_pairAC.
 Qed.
 
 Section conditionnally_independent_discrete_random_variables.
-Notation R := real_realType.
-
 Variables (U : finType) (P : R.-fdist U) (A B C : eqType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}).
 
@@ -1834,8 +1787,6 @@ Notation "P |= X _|_  Y | Z" := (@cinde_rv _ P _ _ _ X Y Z) : proba_scope.
 Notation "X _|_  Y | Z" := (cinde_rv X Y Z) : proba_scope.
 
 Section independent_rv.
-Notation R := real_realType.
-
 Variables (A : finType) (P : R.-fdist A) (TA TB : eqType).
 Variables (X : {RV P -> TA}) (Y : {RV P -> TB}).
 
@@ -2012,7 +1963,6 @@ End sum_two_rand_var.
 Section expected_value_of_the_product.
 
 Section thm64.
-Notation R := real_realType.
 Variables (A B : finType) (P : R.-fdist (A * B)).
 Variables (X : {RV (P`1) -> R}) (Y : {RV (P`2) -> R}).
 
@@ -2059,8 +2009,6 @@ End thm64.
 End expected_value_of_the_product.
 
 Section sum_n_rand_var_def.
-Notation R := real_realType.
-
 Variables (A : finType) (P : R.-fdist A).
 
 Inductive sum_n : forall n, {RV (P `^ n) -> R} -> 'rV[{RV P -> R}]_n -> Prop :=
@@ -2074,8 +2022,6 @@ End sum_n_rand_var_def.
 Notation "X '\=sum' Xs" := (sum_n X Xs) : proba_scope.
 
 Section independent_rv_lemma.
-Notation R := real_realType.
-
 Variables (A B : finType) (P1 : R.-fdist A) (P2 : R.-fdist B) (TA TB : eqType).
 Variable (X : {RV P1 -> TA}) (Y : {RV P2 -> TB}).
 Let P := P1 `x P2.
@@ -2121,8 +2067,6 @@ Qed.
 Local Close Scope vec_ext_scope.
 
 Section sum_n_rand_var.
-Notation R := real_realType.
-
 Variable (A : finType) (P : R.-fdist A).
 
 Local Open Scope vec_ext_scope.
@@ -2189,8 +2133,6 @@ Qed.
 End sum_n_rand_var.
 
 Section weak_law_of_large_numbers.
-Notation R := real_realType.
-
 Local Open Scope vec_ext_scope.
 
 Variables (A : finType) (P : R.-fdist A) (n : nat).
@@ -2222,7 +2164,6 @@ End weak_law_of_large_numbers.
 
 (* wip*)
 Section vector_of_RVs.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U).
 Variables (A : finType) (n : nat) (X : 'rV[{RV P -> A}]_n).
 Local Open Scope ring_scope.
@@ -2231,7 +2172,6 @@ Definition RVn : {RV P -> 'rV[A]_n} := fun x => \row_(i < n) (X ``_ i) x.
 End vector_of_RVs.
 
 Section prob_chain_rule.
-Notation R := real_realType.
 Variables (U : finType) (P : R.-fdist U) (A : finType).
 Local Open Scope vec_ext_scope.