WIP: Try x2s2x1s1_r2_indep

smc/smc_interpreter.v

@@ -454,14 +454,18 @@ Let x1x2s2x1'r2_y2_indepP :=
   x1x2s2x1'r2_y2_indep (x2s2x1s1r2_y2_indep (x2s2x1s1r1_y2_indep inputs)).
 
 Let x2s2x1s1_r2_indep :
-  P |= [% s1, s2] _|_ [% x1, x2, r1] ->
   P |= [% x2, s2, x1, s1] _|_ [%s1, s2, r1].
 Proof.
-Check RV2_indeC .
+rewrite inde_rv_events'.
+rewrite /inde_rv_ev => E F.
+rewrite (reasoning_by_cases [%s1, s2, r1] [% x2, s2, x1, s1]).
+under eq_bigr do rewrite pr_in_pairC.
+rewrite (reasoning_by_cases [% x2, s2, x1, s1] [%s1, s2, r1]).
+rewrite pr_eq_setE /Pr.
 Abort.
 
 Let x2s2x1'_r2_indep :
-  P |= [% x2, s2, x1, s1] _|_ [%s1, s2, r1] ->
+  P |= [% x2, s2, x1, s1] _|_ [%s1, s2, r1] -> (* r2 = s1 *d s2 - r1 *)
   P |= [% x2, s2, x1'] _|_ r2.
 Proof.
 pose f := fun (vs : (VX * VX * VX * VX)) =>
@@ -471,6 +475,12 @@ pose g := fun (ws : (VX * VX * TX)) =>
 by apply_inde_rv_comp f g.
 Qed.
 
+Let  x2s2x1'_r2_indep_2 :
+  P |= [% x2, s2, x1'] _|_ r2.  (* r2 is uniformly distributed (proved) *)
+Proof.
+rewrite /x1' /r2.
+
+
 (*
 P |= [% x2, s2, x1 \+ s1] _|_ (s1 \*d s2 \- r1) .
 P |= [% x1, [% x2, s2, x1 \+ s1]] _|_ (s1 \*d s2 \- r1).

smc/smc_proba.v

@@ -38,26 +38,17 @@ Local Notation "f × g" :=
 
 
 Lemma RV2_indeC :
-  P |= [% X, X] _|_ [% Y, Z] ->
+  P |= [% X, X] _|_ [% Z, Y] ->
   P |= [% X, Y] _|_ [% X, Z].
 Proof.
 rewrite /inde_rv => H [x1 y] [x2 z].
-rewrite pr_eq_pairA.
-transitivity (`Pr[ [% X, X, Y, Z] = (x1, x2, y, z) ]).
-  admit.
-(* TODO: spliting events and changing order of RVs are kinda difficult *)
-Admitted.
-
-Lemma RV2_inde_reduce :
-  P |= X _|_ Y ->
-  P |= [% X, X] _|_ Y.
-Proof.
-move => H.
-rewrite /inde_rv => [[x1 x2] y].
-rewrite coqRE !pr_eqE'.
-(* TODO: [% X, X] = (x1, x2) but x1 could be different from x2 for all x1, x2? *)
-Admitted.
-
+rewrite coqRE.
+rewrite [LHS]pr_eq_pairAC.
+rewrite -[LHS]pr_eq_pairA.
+have H1 := H (x1, x2) (z, y).
+rewrite coqRE in H1.
+rewrite -[LHS]pr_eq_pairA in H1.
+Abort.
 
 (* Information-Theoretically Secure Number Protocol*)
 (* Lemma 3.1 *)