Files

  • infotheo

    • Module infotheo.probability.graphoid

    From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
    From mathcomp Require Import mathcomp_extra reals.
    Require Import ssr_ext ssralg_ext bigop_ext realType_ext fdist.
    Require Import proba jfdist_cond.

    # Graphoid axioms This file provides a formalization of the graphoid axioms (symmetry, decomposition, weak_union, contraction, and intersection) and derived rules. Reference: - R. Affeldt, J. Garrigue, T. Saikawa. Reasoning with Conditional Probabilities and Joint Distributions in Coq. Computer Software 37(3)

    Set Implicit Arguments.
    Set SsrOldRewriteGoalsOrder.
    Unset Strict Implicit.
    Import Prenex Implicits.

    Local Open Scope ring_scope.
    Local Open Scope proba_scope.
    Local Open Scope fdist_scope.

    Import GRing.Theory.



    Section cinde_rv_prop.
    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.
    Proof.
    move=> H a -[d b] c.
    by rewrite cpr_eq_pairA cpr_eq_pairAC -cpr_eq_pairA H cpr_eq_pairC.
    Qed.

    Lemma cinde_drv_3C : P |= X _|_ Y | [% Z, W] -> P |= X _|_ Y | [% W, Z].
    Proof.
    move=> H; move=> a b -[d c]; move: (H a b (c, d)) => {}H.
    by rewrite cpr_eq_pairCr H cpr_eq_pairCr; congr (_ * _); rewrite cpr_eq_pairCr.
    Qed.

    End cinde_rv_prop.

    Section symmetry.

    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.
    Proof.
    by move=> H b a c; rewrite cpr_eq_pairC H mulrC. Qed.

    End symmetry.

    Section decomposition.
    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.
    Proof.
    move=> H a b c.
    transitivity (\sum_(d <- fin_img W) `Pr[ [% X, [% Y, W]] = (a, (b, d)) | Z = c]).
      rewrite -cpr_in1 (creasoning_by_cases _ W); apply: eq_bigr => /= d _.
      by rewrite setX1 cpr_in1 cpr_eq_pairA.
    transitivity (\sum_(d <- fin_img W)
      `Pr[ X = a | Z = c] * `Pr[ [% Y, W] = (b, d) | Z = c]).
      by apply: eq_bigr => d _; rewrite H.
    rewrite -big_distrr /=; congr (_ * _).
    rewrite -cpr_in1 (creasoning_by_cases _ W); apply: eq_bigr => d _.
    by rewrite setX1 cpr_in1.
    Qed.

    End decomposition.

    Section weak_union.
    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].
    Proof.
    move=> H a b [c d].
    transitivity (`Pr[ X = a | [% Y, Z, W] = (b, c, d)] *
      `Pr[ Y = b | [% Z, W] = (c, d)]).
      by rewrite cpr_eq_product_rule cpr_eq_pairAr.
    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 pfwd1_pairA pfwd1_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 (pfwd1_pairC _ Y) (pfwd1_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) // pfwd1_pairC.
    Qed.

    End weak_union.

    Section contraction.
    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.
    Proof.
    move=> H1 H2 a [b d] c.
    rewrite cpr_eq_product_rule.
    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 -pfwd1_pairA pfwd1_pairC -pfwd1_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 pfwd1_pairAC pfwd1_domin_RV2 ?mul0r ?mulr0.
    - by rewrite (cinde_alt _ H2).
    Qed.

    End contraction.

    Section derived_rules.
    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.
    Proof.
    case=> ? ?.
    suff : P |= X _|_ [% W, Z] | Y by move/decomposition.
    apply/cinde_drv_2C/contraction => //.
    exact/cinde_drv_3C/symmetry/weak_union/symmetry.
    Qed.

    Lemma mixing_rule : P |= X _|_ [% Y, W] | Z /\ P |= Y _|_ W | Z -> P |= [% X, W] _|_ Y | Z.
    Proof.
    case=> ? ?.
    apply/symmetry/cinde_drv_2C/contraction; last by [].
    exact/symmetry/weak_union.
    Qed.

    End derived_rules.

    Section intersection.
    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.
    Hypothesis D_not_empty : D.

    Lemma intersection :
      P |= X _|_ Y | [% Z, W] -> P |= X _|_ W | [% Z, Y] -> P |= X _|_ [% Y, W] | Z.
    Proof.
    move=> H1 H2.
    suff : P |= X _|_ Y | Z by apply: contraction.
    move=> a b c; apply/esym.
    rewrite -[in X in X * _ = _]cpr_in1 [in X in X * _ = _](creasoning_by_cases _ W).
    under eq_bigr do rewrite setX1.
    under eq_bigr do rewrite cpr_in1.
    rewrite big_distrl /=.
    have <- : \sum_(d <- fin_img W)
               `Pr[ [% X, Y] = (a, b) | Z = c] * `Pr[ W = d | Z = c] =
             \sum_(d <- fin_img W)
               `Pr[ [% X, W] = (a, d) | Z = c] * `Pr[ Y = b | Z = c].
      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_divrMr; last first.
          rewrite cpr_eqE mulf_neq0 //.
          - by move: (P0 b c d); apply: contra => /eqP/(pfwd1_domin_RV2 W d) ->.
          - move: (P0 b c d); apply: contra.
            rewrite invr_eq0; move/eqP/(pfwd1_domin_RV2 [% Y, W] (b, d)).
            by rewrite pfwd1_pairCA pfwd1_pairA => ->.
        rewrite mulrAC (H d) -mulrA mulVf ?mulr1 //.
        rewrite cpr_eqE mulf_eq0 negb_or invr_eq0 pfwd1_pairC; apply/andP; split.
        - move: (P0 b c d); apply: contra => /eqP/(pfwd1_domin_RV2 Y b).
          by rewrite pfwd1_pairC pfwd1_pairA pfwd1_pairAC => ->.
        - move: (P0 b c d); apply: contra => /eqP/(pfwd1_domin_RV2 [% Y, W] (b, d)).
          by rewrite pfwd1_pairCA -pfwd1_pairA => ->.
      suff H : forall d, `Pr[ X = a | [% Y, Z] = (b, c)] =
                    `Pr[ X = a | [% W, Z] = (d, c)].
        move=> d.
        rewrite cpr_eq_product_rule (H d).
        rewrite [in RHS]cpr_eq_product_rule.
        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/(pfwd1_domin_RV2 W d) ->.
          - move: (P0 b c d); apply: contra => /eqP/(pfwd1_domin_RV2 [% Y, W] (b, d)).
            by rewrite pfwd1_pairCA -pfwd1_pairA => ->.
        rewrite -[in RHS]mulrA mulfV // cpr_eqE mulf_eq0 negb_or invr_eq0; apply/andP; split.
        - move: (P0 b c d); apply: contra => /eqP/(pfwd1_domin_RV2 Y b).
          by rewrite pfwd1_pairC pfwd1_pairA pfwd1_pairAC => ->.
        - move: (P0 b c d); apply: contra => /eqP/(pfwd1_domin_RV2 [% Y, W] (b, d)).
          by rewrite pfwd1_pairCA -pfwd1_pairA => ->.
      have {}H2 : forall d, `Pr[ X = a | [% Y, Z] = (b, c)] =
                         `Pr[ X = a | [% W, Z, Y] = (d, c, b)].
        move=> d; move: {H2}(H2 a d (c, b)).
        rewrite cpr_eq_product_rule.
        have H0 : `Pr[ W = d | [% Z, Y] = (c, b)] != 0.
          rewrite cpr_eqE pfwd1_pairA pfwd1_pairAC -pfwd1_pairA.
          rewrite pfwd1_pairC mulf_eq0 negb_or invr_eq0 P0/=.
          move: (P0 b c d); apply: contra => /eqP.
          by rewrite pfwd1_pairC/= => /(pfwd1_domin_RV2 W d) ->.
        move/mulIf => /(_ H0){H0}/esym.
        by rewrite (cpr_eq_pairCr X Z) cpr_eq_pairAr.
      have {}H1 d : `Pr[ X = a | [% W, Z] = (d, c)] =
                    `Pr[ X = a | [% Y, W, Z] = (b, d, c)].
        move: {H1}(H1 a b (c, d)).
        rewrite cpr_eq_product_rule.
        have H0 : `Pr[ Y = b | [% Z, W] = (c, d)] != 0.
          rewrite cpr_eqE pfwd1_pairA mulf_eq0 negb_or invr_eq0 P0 /=.
          move: (P0 b c d); apply: contra => /eqP/(pfwd1_domin_RV2 Y b).
          by rewrite pfwd1_pairC -pfwd1_pairA => ->.
        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 //.
    move: (P0 b c D_not_empty); apply: contra.
    rewrite pfwd1_pairAC => /eqP/(pfwd1_domin_RV2 [% Y, W] (b, D_not_empty)).
    by rewrite pfwd1_pairC => ->.
    Qed.

    End intersection.
    Generated by rocqnavi