various improvements, per feedback

Author: alleystoughton

theories/modules/TotalProb.ec

@@ -86,40 +86,39 @@ 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).
-bypr => &hr [#] -> -> glob_eq.
-byequiv (_ : ={i, x, glob M} ==> ={res}) => //; sim.
-auto.
++ auto.
++ 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().
 qed.
 
 lemma total_prob' (dt' : t distr) (supp : t list) (i' : input) &m :
-  is_lossless dt' => is_finite_for (support dt') supp =>
+  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 => dt'_ll [uniq_supp supp_iff]. 
+move => [uniq_supp supp_iff]. 
 have -> :
   Pr[Rand(M).f(dt', i') @ &m : res] = Pr[RandAux.f(dt', i') @ &m : res].
-  byequiv (_ : ={dt, i, glob M} ==> ={res}) => //; proc; sim.
+  + 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 => //.
-  auto.
-  hoare; call (_ : true); auto; smt().
-  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 => //.
+    + hoare; call (_ : true); auto; smt().
+    rnd pred0; auto; smt(mu0).
 congr; apply fun_ext => x'; by rewrite RandAux_partition_eq.
 qed.
 
@@ -128,15 +127,12 @@ end section.
 (*& total probability lemma for distributions with finite support &*)
 
 lemma total_prob (M <: T) (dt : t distr) (supp : t list) (i : input) &m :
-  is_lossless dt => is_finite_for (support dt) supp =>
+  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 => dt_ll iff_supp_dt_supp.
-by apply (total_prob' M).
-qed.
+proof. move => iff_supp_dt_supp; by apply (total_prob' M). qed.
 
 end TotalGeneral.
 
@@ -156,8 +152,7 @@ lemma total_prob_bool (M <: T) (i : input) &m :
   Pr[M.main(i, false) @ &m : res] / 2%r.
 proof.
 rewrite (total_prob M DBool.dbool [true; false]) //.
-rewrite dbool_ll.
-smt(supp_dbool).
++ smt(supp_dbool).
 by rewrite 2!big_cons big_nil /= /predT /predF /= 2!dbool1E.
 qed.
 
@@ -171,22 +166,6 @@ clone include TotalGeneral with
   type t <- int
 proof *.
 
-lemma big_weight_simp (M <: T) (m n : int, i : input, ys : int list) &m :
-  (forall y, y \in ys => m <= y < n) =>
-  big predT
-  (fun (x : int) => mu1 (drange m n) x * Pr[M.main(i, x) @ &m : res])
-  ys =
-  big predT
-  (fun (x : int) => Pr[M.main(i, x) @ &m : res] / (n - m)%r)
-  ys.
-proof.
-elim ys => [// | y ys IH mem_impl].
-rewrite 2!big_cons (_ : predT y) //=.
-rewrite drange1E (_ : m <= y < n) 1:mem_impl //=.
-rewrite IH => [z z_in_ys | //].
-by rewrite mem_impl /= z_in_ys.
-qed.
-
 (*& total probability lemma for `drange` &*)
 
 lemma total_prob_drange (M <: T) (m n : int, i : input) &m :
@@ -198,10 +177,9 @@ lemma total_prob_drange (M <: T) (m n : int, i : input) &m :
 proof.
 move => lt_m_n.
 rewrite (total_prob M (drange m n) (range m n)).
-by rewrite drange_ll.
-rewrite /is_finite_for.
-smt(range_uniq mem_range supp_drange).
-rewrite (big_weight_simp M) //; by move => j /mem_range.
++ 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.
 qed.
 
 end TotalRange.
@@ -218,23 +196,6 @@ clone include TotalGeneral with
   type t <- t
 proof *.
 
-lemma big_weight_simp (M <: T) (xs : t list, i : input, ys : t list) &m :
-  uniq xs =>
-  (forall y, y \in ys => y \in xs) =>
-  big predT
-  (fun (x : t) => mu1 (duniform xs) x * Pr[M.main(i, x) @ &m : res])
-  ys =
-  big predT
-  (fun (x : t) => Pr[M.main(i, x) @ &m : res] / (size xs)%r)
-  ys.
-proof.
-move => uniq_xs.
-elim ys => [// | y ys IH mem_impl].
-rewrite 2!big_cons (_ : predT true) //=.
-rewrite duniform1E_uniq // (_ : y \in xs) 1:mem_impl //=.
-rewrite IH => [z z_in_ys | //]; by rewrite mem_impl /= z_in_ys.
-qed.
-
 (*& total probability lemma for `duniform` &*)
 
 lemma total_prob_uniform (M <: T) (xs : t list, i : input) &m :
@@ -246,9 +207,9 @@ lemma total_prob_uniform (M <: T) (xs : t list, i : input) &m :
 proof.
 move => uniq_xs xs_ne_nil.
 rewrite (total_prob M (duniform xs) xs).
-by rewrite duniform_ll.
-smt(supp_duniform).
-by rewrite (big_weight_simp M).
++ smt(supp_duniform).
+apply eq_big_seq => y y_in_xs /=.
+by rewrite duniform1E_uniq // (_ : y \in xs).
 qed.
 
 end TotalUniform.