graphoid

affeldt-aist · Jul 17, 2024 · 548d795 · 548d795
1 parent b16e4b8
commit 548d795
Showing 1 changed file with 53 additions and 39 deletions.
diff --git a/probability/graphoid.v b/probability/graphoid.v
@@ -1,9 +1,8 @@
 (* 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 ssrnum matrix.
-Require Import Reals.
-From mathcomp Require Import Rstruct.
-Require Import ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist.
+From mathcomp Require Import reals.
+Require Import realType_ext logb ssr_ext ssralg_ext bigop_ext fdist.
 Require Import proba jfdist_cond.
 
 (******************************************************************************)
@@ -18,15 +17,18 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
 
-Local Open Scope R_scope.
+Local Open Scope ring_scope.
 Local Open Scope proba_scope.
 Local Open Scope fdist_scope.
 
+Import GRing.Theory.
+
 (* TODO: rename *)
 Module Proj124.
 Section proj124.
-Variables (A B D C : finType) (P : {fdist A * B * D * C}).
-Definition d : {fdist A * B * C} := fdistX (fdistA (fdistX (fdistA P)))`2.
+Context {R : realType}.
+Variables (A B D C : finType) (P : R.-fdist (A * B * D * C)).
+Definition d : R.-fdist (A * B * C) := fdistX (fdistA (fdistX (fdistA P)))`2.
 Lemma dE abc : d abc = \sum_(x in D) P (abc.1.1, abc.1.2, x, abc.2).
 Proof.
 case: abc => [[a b] c] /=.
@@ -38,33 +40,37 @@ Proof. by rewrite /fdist_snd /d !fdistmap_comp. Qed.
 End proj124.
 End Proj124.
 
-Definition Proj14d (A B C D : finType) (d : {fdist A * B * D * C}) : {fdist A * C} :=
+Definition Proj14d {R : realType} (A B C D : finType) (d : R.-fdist (A * B * D * C)) :
+  R.-fdist (A * C) :=
   fdist_proj13 (Proj124.d d).
 
 (* TODO: rename *)
 Module QuadA23.
 Section def.
-Variables (A B C D : finType) (P : {fdist A * B * D * C}).
+Context {R : realType}.
+Variables (A B C D : finType) (P : R.-fdist (A * B * D * C)).
 Definition f (x : A * B * D * C) : A * (B * D) * C :=
   (x.1.1.1, (x.1.1.2, x.1.2), x.2).
 Lemma inj_f : injective f.
 Proof. by rewrite /f => -[[[? ?] ?] ?] [[[? ?] ?] ?] /= [-> -> -> ->]. Qed.
-Definition d : {fdist A * (B * D) * C} := fdistmap f P.
+Definition d : R.-fdist (A * (B * D) * C) := fdistmap f P.
 Lemma dE x : d x = P (x.1.1, x.1.2.1, x.1.2.2, x.2).
 Proof.
 case: x => -[a [b d] c]; rewrite /def.d fdistmapE /= -/(f (a, b, d, c)).
 by rewrite (big_pred1_inj inj_f).
 Qed.
 End def.
 Section prop.
-Variables (A B C D : finType) (P : {fdist A * B * D * C}).
+Context {R : realType}.
+Variables (A B C D : finType) (P : R.-fdist (A * B * D * C)).
 Lemma snd : (QuadA23.d P)`2 = P`2.
 Proof. by rewrite /fdist_snd /d fdistmap_comp. Qed.
 End prop.
 End QuadA23.
 
 Section cinde_rv_prop.
-Variables (U : finType) (P : {fdist U}) (A B C D : finType).
+Context {R : realType}.
+Variables (U : finType) (P : R.-fdist U) (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 
 Lemma cinde_drv_2C : P |= X _|_ [% Y, W] | Z -> P |= X _|_ [% W, Y] | Z.
@@ -83,7 +89,8 @@ End cinde_rv_prop.
 
 Section symmetry.
 
-Variable (U : finType) (P : {fdist U}).
+Context {R : realType}.
+Variable (U : finType) (P : R.-fdist U).
 Variables (A B C : finType) (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}).
 
 Lemma symmetry : P |= X _|_ Y | Z -> P |= Y _|_ X | Z.
@@ -92,14 +99,15 @@ move=> H b a c.
 rewrite /cinde_rv in H.
 rewrite cpr_eq_pairC.
 rewrite H.
-by rewrite mulRC.
+by rewrite mulrC.
 Qed.
 
 End symmetry.
 
 Section decomposition.
 
-Variables (U : finType) (P : {fdist U}) (A B C D : finType).
+Context {R : realType}.
+Variables (U : finType) (P : R.-fdist U) (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 
 Lemma decomposition : P |= X _|_ [% Y, W] | Z -> P |= X _|_ Y | Z.
@@ -121,7 +129,8 @@ End decomposition.
 
 Section weak_union.
 
-Variables (U : finType) (P : {fdist U}) (A B C D : finType).
+Context {R : realType}.
+Variables (U : finType) (P : R.-fdist U) (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 
 Lemma weak_union : P |= X _|_ [% Y, W] | Z -> P |= X _|_ Y | [% Z, W].
@@ -133,10 +142,10 @@ transitivity (`Pr[ X = a | [% Y, Z, W] = (b, c, d)] *
 transitivity (`Pr[ X = a | Z = c] * `Pr[ Y = b | [% Z, W] = (c, d)]).
   rewrite cpr_eq_pairACr.
   case/boolP : (`Pr[ [% Y, W, Z] = (b, d, c)] == 0) => [/eqP|] H0.
-  - by rewrite [X in _ * X = _ * X]cpr_eqE pr_eq_pairA pr_eq_pairAC H0 div0R !mulR0.
+  - by rewrite [X in _ * X = _ * X]cpr_eqE pr_eq_pairA pr_eq_pairAC H0 mul0r !mulr0.
   - by rewrite (cinde_alt _ H).
 case/boolP : (`Pr[ [% Z, W] = (c, d) ] == 0) => [/eqP|] ?.
-- by rewrite [X in _ * X = _ * X]cpr_eqE (pr_eq_pairC _ Y) (pr_eq_domin_RV2 Y) ?(div0R,mulR0).
+- by rewrite [X in _ * X = _ * X]cpr_eqE (pr_eq_pairC _ Y) (pr_eq_domin_RV2 Y) ?(mul0r,mulr0).
 - have {}H : P |= X _|_ W | Z by move/cinde_drv_2C : H; apply decomposition.
   by rewrite [in X in _ = X * _]cpr_eq_pairCr (cinde_alt _ H) // pr_eq_pairC.
 Qed.
@@ -145,7 +154,8 @@ End weak_union.
 
 Section contraction.
 
-Variables (U : finType) (P : {fdist U}) (A B C D : finType).
+Context {R : realType}.
+Variables (U : finType) (P : R.-fdist U) (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 
 Lemma contraction : P |= X _|_ W | [% Z, Y] -> P |= X _|_ Y | Z -> P |= X _|_ [% Y, W] | Z.
@@ -156,11 +166,11 @@ transitivity (`Pr[X = a | [% Y, Z] = (b, c)] * `Pr[[% Y, W] = (b, d) | Z = c]).
   rewrite -cpr_eq_pairAr [in X in X * _ = _]cpr_eq_pairCr -cpr_eq_pairAr.
   case/boolP : (`Pr[ [% W, [% Z, Y]] = (d, (c, b))] == 0) => [/eqP|] H0.
     rewrite [in X in _ * X = _ * X]cpr_eqE.
-    by rewrite -pr_eq_pairA pr_eq_pairC -pr_eq_pairA H0 div0R !mulR0.
+    by rewrite -pr_eq_pairA pr_eq_pairC -pr_eq_pairA H0 mul0r !mulr0.
   by rewrite (cinde_alt _ H1) // cpr_eq_pairCr.
 case/boolP : (`Pr[ [% Y, Z] = (b, c) ] == 0) => [/eqP|] H0.
 - rewrite [X in _ * X = _ * X]cpr_eqE.
-  by rewrite pr_eq_pairAC pr_eq_domin_RV2 ?div0R ?mulR0.
+  by rewrite pr_eq_pairAC pr_eq_domin_RV2 ?mul0r ?mulr0.
 - by rewrite (cinde_alt _ H2).
 Qed.
 
@@ -169,7 +179,8 @@ End contraction.
 (* Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference, Pearl, p.88 *)
 Section derived_rules.
 
-Variables (U : finType) (P : {fdist U}) (A B C D : finType).
+Context {R : realType}.
+Variables (U : finType) (P : R.-fdist U) (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 
 Lemma chaining_rule : P |= X _|_ Z | Y /\ P |= [% X, Y] _|_ W | Z -> P |= X _|_ W | Y.
@@ -191,7 +202,8 @@ End derived_rules.
 
 Section intersection.
 
-Variables (U : finType) (P : {fdist U}) (A B C D : finType).
+Context {R : realType}.
+Variables (U : finType) (P : R.-fdist U) (A B C D : finType).
 Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}) (W : {RV P -> D}).
 
 Hypothesis P0 : forall b c d, `Pr[ [% Y, Z, W] = (b, c, d) ] != 0.
@@ -213,13 +225,14 @@ have <- : \sum_(d <- fin_img W)
   suff H : forall d, `Pr[ [% X, Y] = (a, b) | Z = c] / `Pr[ Y = b | Z = c ] =
                 `Pr[ [% X, W] = (a, d) | Z = c] / `Pr[ W = d | Z = c ].
     apply eq_bigr => d _.
-    rewrite -eqR_divr_mulr; last first.
-      rewrite cpr_eqE divR_neq0' //.
+    rewrite -eqr_divr_mulr; last first.
+      rewrite cpr_eqE mulf_neq0 //.
       - by move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 W d) ->.
-      - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)).
+      - move: (P0 b c d); apply: contra.
+        rewrite invr_eq0;  move/eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)).
         by rewrite pr_eq_pairCA pr_eq_pairA => ->.
-    rewrite {1}/Rdiv mulRAC -/(Rdiv _ _) (H d) mulRAC eqR_divr_mulr //.
-    rewrite cpr_eqE divR_neq0' //.
+    rewrite mulrAC (H d) -mulrA mulVf ?mulr1 //.
+    rewrite cpr_eqE mulf_eq0 negb_or invr_eq0 pr_eq_pairC; apply/andP; split.
     - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 Y b).
       by rewrite pr_eq_pairC pr_eq_pairA pr_eq_pairAC => ->.
     - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)).
@@ -229,12 +242,12 @@ have <- : \sum_(d <- fin_img W)
     move=> d.
     rewrite cpr_eq_product_rule (H d).
     rewrite [in RHS]cpr_eq_product_rule.
-    rewrite {1}/Rdiv -mulRA mulRV; last first.
-      rewrite cpr_eqE divR_neq0' //.
+    rewrite -mulrA mulfV; last first.
+      rewrite cpr_eqE mulf_eq0 negb_or invr_eq0; apply/andP; split.
       - by move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 W d) ->.
       - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)).
         by rewrite pr_eq_pairCA -pr_eq_pairA => ->.
-    rewrite {1}/Rdiv -[in RHS]mulRA mulRV // cpr_eqE divR_neq0' //.
+    rewrite -[in RHS]mulrA mulfV // cpr_eqE mulf_eq0 negb_or invr_eq0; apply/andP; split.
     - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 Y b).
       by rewrite pr_eq_pairC pr_eq_pairA pr_eq_pairAC => ->.
     - move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, d)).
@@ -243,25 +256,26 @@ have <- : \sum_(d <- fin_img W)
                      `Pr[ X = a | [% W, Z, Y] = (d, c, b)].
     move=> d; move: {H2}(H2 a d (c, b)).
     rewrite cpr_eq_product_rule.
-    have /eqP H0 : `Pr[ W = d | [% Z, Y] = (c, b)] != 0.
+    have H0 : `Pr[ W = d | [% Z, Y] = (c, b)] != 0.
       rewrite cpr_eqE pr_eq_pairA pr_eq_pairAC -pr_eq_pairA.
-      rewrite pr_eq_pairC divR_neq0' //; first by rewrite pr_eq_pairC.
+      rewrite pr_eq_pairC mulf_eq0 negb_or invr_eq0.
+      apply/andP; split; first by rewrite pr_eq_pairC.
       by move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 W d) ->.
-    move/eqR_mul2r => /(_ H0){H0}/esym.
-    by rewrite [in LHS]cpr_eq_pairCr cpr_eq_pairAr.
+    move/mulIf => /(_ H0){H0}/esym.
+    by rewrite (cpr_eq_pairCr X Z) cpr_eq_pairAr.
   have {}H1 : forall d, `Pr[ X = a | [% W, Z] = (d, c)] =
                      `Pr[ X = a | [% Y, W, Z] = (b, d, c)].
     move=> d; move: {H1}(H1 a b (c, d)).
     rewrite cpr_eq_product_rule.
-    have /eqP H0 : `Pr[ Y = b | [% Z, W] = (c, d)] != 0.
-      rewrite cpr_eqE pr_eq_pairA divR_neq0' //.
+    have H0 : `Pr[ Y = b | [% Z, W] = (c, d)] != 0.
+      rewrite cpr_eqE pr_eq_pairA mulf_eq0 negb_or invr_eq0 P0 /=.
       move: (P0 b c d); apply: contra => /eqP/(pr_eq_domin_RV2 Y b).
       by rewrite pr_eq_pairC -pr_eq_pairA => ->.
-    move/eqR_mul2r => /(_ H0){H0}/esym.
-    by rewrite [in LHS]cpr_eq_pairCr cpr_eq_pairAr cpr_eq_pairACr.
+    move/mulIf => /(_ H0){H0}/esym.
+    by rewrite (cpr_eq_pairCr X Z) cpr_eq_pairAr cpr_eq_pairACr.
   by move=> d; rewrite {H2}(H2 d) {}H1 cpr_eq_pairCr cpr_eq_pairAr.
 rewrite -big_distrr /=.
-rewrite cPr_1 ?mulR1 //.
+rewrite cPr_1 ?mulr1 //.
 move: (P0 b c D_not_empty); apply: contra.
 rewrite pr_eq_pairAC => /eqP/(pr_eq_domin_RV2 [% Y, W] (b, D_not_empty)).
 by rewrite pr_eq_pairC => ->.