swap total_prob parameter, simplify proofs

Author: fdupress

theories/modules/TotalProb.ec

@@ -75,7 +75,7 @@ local lemma RandAux_partition_eq (dt' : t distr) (i' : input) (x' : t) &m :
   mu1 dt' x' * Pr[M.main(i', x') @ &m : res].
 proof.
 byphoare
-  (_ :
+  (:
    dt = dt' /\ i = i' /\ (glob M) = (glob M){m} ==>
    res /\ x_of_glob_RA (glob RandAux) = x') => //.
 proc; rewrite /x_of_glob_RA /=.
@@ -86,53 +86,53 @@ seq 1 :
   (1%r - mu1 dt x')
   0%r
   (i = i' /\ (glob M) = (glob M){m}) => //.
-+ auto.
-+ rnd (pred1 x'); auto.
-+ call (_ : i = i' /\ x = x' /\ glob M = (glob M){m} ==> res).
++ by auto.
++ by rnd (pred1 x'); auto.
++ call (: i = i' /\ x = x' /\ glob M = (glob M){m} ==> res).
   + bypr => &hr [#] -> -> glob_eq.
-    byequiv (_ : ={i, x, glob M} ==> ={res}) => //; sim.
-+ auto.
-hoare; call (_ : true); auto; smt().
+    by byequiv (: ={i, x, glob M} ==> ={res}) => //; sim.
++ by auto.
+by hoare; call (: true); auto; smt().
 qed.
 
-lemma total_prob' (dt' : t distr) (supp : t list) (i' : input) &m :
+lemma total_prob' (supp : t list) (dt' : t distr) (i' : input) &m :
   is_finite_for (support dt') supp =>
   Pr[Rand(M).f(dt', i') @ &m : res] =
   big predT
   (fun x' => mu1 dt' x' * Pr[M.main(i', x') @ &m : res])
   supp.
 proof.
 move => [uniq_supp supp_iff]. 
-have -> :
+have ->:
   Pr[Rand(M).f(dt', i') @ &m : res] = Pr[RandAux.f(dt', i') @ &m : res].
-  + byequiv (_ : ={dt, i, glob M} ==> ={res}) => //; proc; sim.
+  + by byequiv (_ : ={dt, i, glob M} ==> ={res}) => //; proc; sim.
 rewrite (EPL.list_partitioning RandAux (dt', i') E phi supp &m) //.
 have -> /= :
   Pr[RandAux.f(dt', i') @ &m: res /\ ! (x_of_glob_RA (glob RandAux) \in supp)] =
   0%r.
-  + byphoare (_ : dt = dt' /\ i = i' ==> _) => //; proc.
-    seq 1 :
-      (RandAux.x \in supp)
-      1%r
-      0%r
-      0%r
-      1%r => //.
-    + by hoare; call (_ : true); auto; smt().
-    by rnd pred0; auto; smt(mu0).
++ byphoare (: dt = dt' /\ i = i' ==> _) => //; proc.
+  seq 1 :
+    (RandAux.x \in supp)
+    1%r
+    0%r
+    0%r
+    1%r => //.
+  + by hoare; call (: true); auto; smt().
+  by rnd pred0; auto; smt(mu0).
 by congr; apply fun_ext => x'; rewrite RandAux_partition_eq.
 qed.
 
 end section.
 
 (*& total probability lemma for distributions with finite support &*)
 
-lemma total_prob (M <: T) (dt : t distr) (supp : t list) (i : input) &m :
+lemma total_prob (M <: T) (supp : t list) (dt : t distr) (i : input) &m :
   is_finite_for (support dt) supp =>
   Pr[Rand(M).f(dt, i) @ &m : res] =
   big predT
   (fun (x : t) => mu1 dt x * Pr[M.main(i, x) @ &m : res])
   supp.
-proof. move => iff_supp_dt_supp; by apply (total_prob' M). qed.
+proof. exact: (total_prob' M). qed.
 
 end TotalGeneral.
 
@@ -151,9 +151,9 @@ lemma total_prob_bool (M <: T) (i : input) &m :
   Pr[M.main(i, true) @ &m : res]  / 2%r +
   Pr[M.main(i, false) @ &m : res] / 2%r.
 proof.
-rewrite (total_prob M DBool.dbool [true; false]) //.
-+ by smt(supp_dbool).
-by rewrite 2!big_cons big_nil /= /predT /predF /= 2!dbool1E.
+rewrite (total_prob M [true; false]) //.
++ smt(supp_dbool).
+by rewrite 2!big_cons big_nil /= 2!dbool1E.
 qed.
 
 end TotalBool.
@@ -168,18 +168,16 @@ proof *.
 
 (*& total probability lemma for `drange` &*)
 
-lemma total_prob_drange (M <: T) (m n : int, i : input) &m :
+lemma total_prob_drange (M <: T) (m n : int) (i : input) &m :
   m < n =>
   Pr[Rand(M).f(drange m n, i) @ &m : res] =
   bigi predT
   (fun (j : int) => Pr[M.main(i, j) @ &m : res] / (n - m)%r)
   m n.
 proof.
-move => lt_m_n.
-rewrite (total_prob M (drange m n) (range m n)).
+move => lt_m_n; rewrite (total_prob M (range m n)).
 + by rewrite /is_finite_for; smt(range_uniq mem_range supp_drange).
-apply eq_big_seq => x x_in_range_m_n /=.
-by rewrite drange1E (_ : m <= x < n) 1:-mem_range.
+by apply: eq_big_seq=> |> y; rewrite drange1E mem_range=> ->.
 qed.
 
 end TotalRange.
@@ -198,18 +196,16 @@ proof *.
 
 (*& total probability lemma for `duniform` &*)
 
-lemma total_prob_uniform (M <: T) (xs : t list, i : input) &m :
+lemma total_prob_uniform (M <: T) (xs : t list) (i : input) &m :
   uniq xs => xs <> [] =>
   Pr[Rand(M).f(duniform xs, i) @ &m : res] =
   big predT
   (fun (x : t) => Pr[M.main(i, x) @ &m : res] / (size xs)%r)
   xs.
 proof.
-move => uniq_xs xs_ne_nil.
-rewrite (total_prob M (duniform xs) xs).
-+ by smt(supp_duniform).
-apply eq_big_seq => y y_in_xs /=.
-by rewrite duniform1E_uniq // (_ : y \in xs).
+move => uniq_xs xs_ne_nil; rewrite (total_prob M xs).
++ smt(supp_duniform).
+by apply: eq_big_seq=> |> x; rewrite duniform1E_uniq=> // ->.
 qed.
 
 end TotalUniform.