Formalization for SMC protocols

_CoqProject

@@ -94,5 +94,9 @@ toy_examples/expected_value_variance.v
 toy_examples/expected_value_variance_ordn.v
 toy_examples/expected_value_variance_tuple.v
 toy_examples/conditional_entropy.v
+smc/smc_proba.v
+smc/smc_entropy.v
+smc/smc_interpreter.v
+smc/smc_tactics.v
 
 -R . infotheo

changelog.txt

@@ -27,6 +27,18 @@ from 0.6.0 to 0.6.1
 
 compatibility release
 
+-------------------
+from 0.6.1 to 0.7.0
+-------------------
+
+Port to MathComp 2
+
+-------------------
+from 0.6.0 to 0.6.1
+-------------------
+
+compatibility release
+
 -------------------
 from 0.5.2 to 0.6.0
 -------------------

information_theory/entropy.v

@@ -187,6 +187,25 @@ rewrite -(pair_bigA _ (fun a1 a2 => P (a1, a2) * log (P (a1, a2)))) /=.
 by rewrite exchange_big pair_big; apply eq_bigr => -[a b] _; rewrite fdistXE.
 Qed.
 
+Variables (C: finType) (P' : {fdist A * B * C}).
+
+About fdistA.
+
+Lemma joint_entropyA : `H P' = `H (fdistA P').
+Proof.
+congr (- _) => /=.
+rewrite (eq_bigr (fun a => P' (a.1.1, a.1.2, a.2) * log (P' (a.1.1, a.1.2, a.2)))); last by case => -[].
+rewrite -(pair_bigA _ (fun a1 a2 => P' (a1.1, a1.2, a2) * log (P' (a1.1, a1.2, a2)))) /=.
+rewrite -(pair_bigA _ (fun a1 a2 => \sum_j P' (a1, a2, j) * log (P' (a1, a2, j)))) /=.
+rewrite [RHS](eq_bigr (fun a => fdistA P' (a.1, (a.2.1, a.2.2)) * log (fdistA P' (a.1, (a.2.1, a.2.2))))); last by case => i [].
+rewrite -(pair_bigA _ (fun a1 a2 => fdistA P' (a1, (a2.1, a2.2)) * log (fdistA P' (a1, (a2.1, a2.2))))) /=.
+apply: eq_bigr => i _.
+rewrite -(pair_bigA _ (fun a1 a2 => fdistA P' (i, (a1, a2)) * log (fdistA P' (i, (a1, a2))))) /=.
+apply: eq_bigr => j _.
+apply: eq_bigr => k _.
+rewrite fdistAE //.
+Qed.
+
 End joint_entropy.
 
 Lemma entropy_rV (A : finType) n (P : {fdist 'rV[A]_n.+1}) :

probability/proba.v

@@ -514,7 +514,7 @@ Local Notation "{ 'RV' P -> V }" := (RV_of P (Phant _) (Phant V)).
 Definition ambient_dist (P : {fdist U}) (X : {RV P -> T}) : {fdist U} := P.
 
 End random_variable.
-Notation "{ 'RV' P -> T }" := (RV_of P (Phant _) (Phant T)) : proba_scope.
+Notation "{ 'RV' P -> T }" := (@RV _ T%type P ) : proba_scope.
 
 Section random_variable_eqType.
 Variables (U : finType) (A : eqType) (P : R.-fdist U).
@@ -1822,6 +1822,16 @@ End conditionnally_independent_discrete_random_variables.
 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 conditionnally_independent_discrete_random_variables_extra.
+
+Variables (U: finType) (P : R.-fdist U) (A B C: finType).
+Variables (X : {RV P -> A}) (Y : {RV P -> B}) (Z : {RV P -> C}).
+
+Lemma cinde_rv_sym :  X _|_  Y | Z -> Y _|_  X | Z.
+Proof. move=>H a b c. by rewrite mulRC cpr_eq_pairC. Qed.
+
+End conditionnally_independent_discrete_random_variables_extra.
+
 Section independent_rv.
 Variables (A : finType) (P : R.-fdist A) (TA TB : eqType).
 Variables (X : {RV P -> TA}) (Y : {RV P -> TB}).
@@ -2231,3 +2241,99 @@ rewrite big_ord_recr /=.
 Abort.
 
 End prob_chain_rule.
+
+
+
+Section more_rv_lemmas.
+Variables (U : finType) (P : R.-fdist U).
+Variables (TA TB TC UA UB UC : eqType) (f : TA -> UA) (g : TB -> UB) (h: TC -> UC).
+Variables (X : {RV P -> TA}) (Y : {RV P -> TB}) (Z : {RV P -> TC}).
+
+Local Notation "f × g" :=
+  (fun xy => (f xy.1, g xy.2)) (at level 10).
+
+Lemma comp_RV2_ACA : RV2 (f `o X) (g `o Y) = f × g `o RV2 X Y.
+Proof. by []. Qed.
+
+Lemma comp_RV3_ACA : [%h `o Z, [% (f `o X), (g `o Y)]] = h × (f × g) `o [%Z, [%X, Y]].
+Proof. by []. Qed.
+End more_rv_lemmas.
+
+Section more_preimset.
+Variables (aT1 aT2 aT3 rT1 rT2 rT3: finType).
+Variables (f : aT1 -> rT1)  (g : aT2 -> rT2) (h : aT3 -> rT3).
+Variables (A : {set rT1}) (B : {set rT2}) (C : {set rT3}).
+
+Local Notation "f × g" :=
+  (fun xy => (f xy.1, g xy.2)) (at level 10).
+
+Lemma preimsetX :
+  f × g @^-1: (A `* B) = f @^-1: A `* g @^-1: B.
+Proof. by apply/setP=> -[] a b /=; rewrite !inE. Qed.
+
+Lemma preimsetX2 :
+  h × (f × g) @^-1: (C `* (A `* B)) = h @^-1: C `* (f @^-1: A `* g @^-1: B).
+Proof. by apply/setP=> -[] a b /=; rewrite !inE. Qed.
+
+Lemma in_preimset x (Y : {set rT1}) : (x \in f @^-1: Y) = (f x \in Y).
+Proof. by rewrite !inE. Qed.
+Lemma in_preimset1 x y : (x \in f @^-1: [set y]) = (f x == y).
+Proof. by rewrite !inE. Qed.
+End more_preimset.
+
+
+Section more_pr_lemmas.
+Variables (U : finType) (P : R.-fdist U).
+Variables (TA UA : finType) (f : TA -> UA) (X : {RV P -> TA}).
+
+Lemma pr_in_comp' E :
+  `Pr[ (f `o X) \in E ]  = `Pr[ X \in f @^-1: E ].
+Proof.
+rewrite !pr_inE' /Pr.
+rewrite partition_big_preimset /=.
+apply: eq_bigr=> i iE.
+under [RHS]eq_bigr=> j ?.
+  rewrite fdistmapE -ssrR.sumRE.
+  under eq_bigl do rewrite /= inE /=.
+  over.
+under eq_bigl do rewrite -in_preimset1.
+rewrite -partition_big_preimset /= fdistmapE -ssrR.sumRE.
+apply: eq_bigl=> j.
+by rewrite !inE.
+Qed.
+End more_pr_lemmas.
+
+
+Section more_fdist.
+Lemma fdistmapE' (R : realType) (A B : finType) (g : A -> B)
+  (p : fdist R A) (b : B):
+  fdistmap g p b = (\sum_(a in g @^-1: [set b]) p a)%mcR.
+Proof. by rewrite fdistmapE; apply: eq_bigl=> ?; rewrite !inE. Qed.
+End more_fdist.
+
+
+Section more_inde_rv.
+Variables (A : finType) (P : R.-fdist A) (TA TB : finType).
+Variables (X : {RV P -> TA}) (Y : {RV P -> TB}).
+
+Definition inde_rv_ev :=
+  forall E F,
+    `Pr[ [% X, Y] \in E `* F] = `Pr[ X \in E ] * `Pr[ Y \in F ].
+
+Lemma inde_rv_events' : inde_rv X Y <-> inde_rv_ev.
+Proof.
+split=> H; last by move=> *; rewrite -!pr_eq_set1 -H setX1.
+move=> E F; rewrite !pr_inE'.
+rewrite [LHS]/Pr; under eq_bigr=> *.
+  rewrite fdistmapE.
+  under eq_bigl do rewrite !inE /=.
+  over.
+rewrite [in RHS]/Pr big_distrl /=.
+under [RHS]eq_bigr=> i ?.
+  rewrite big_distrr /=.
+  under eq_bigr do rewrite -!pr_eqE' -H pr_eqE'.
+  over.
+rewrite -big_setX; apply: eq_bigr=> *.
+by rewrite fdistmapE.
+Qed.
+End more_inde_rv.