[distributions] in programmatic list sampling, make the distribution dynamic

theories/distributions/DList.ec

@@ -174,7 +174,7 @@ lemma dlist_fu (d: 'a distr) (xs:'a list):
   xs \in dlist d (size xs).
 proof.
 move=> fu; rewrite /support dlist1E 1:size_ge0 /=.
-by apply Bigreal.prodr_gt0_seq => /= a Hin _;apply fu.
+by apply Bigreal.prodr_gt0_seq => /= a Hin _; apply fu.
 qed.
 
 lemma dlist_uni (d:'a distr) n :
@@ -331,12 +331,11 @@ have ->: k1 + (n - (k1 + 1)) = n - 1 by ring.
 by have := inrgf 0 _; smt().
 qed.
 
-abstract theory Program.
+abstract theory ParametricProgram.
   type t.
-  op d: t distr.
 
   module Sample = {
-    proc sample(n:int): t list = {
+    proc sample(d: t distr, n:int): t list = {
       var r;
 
       r <$ dlist d n;
@@ -345,7 +344,7 @@ abstract theory Program.
   }.
 
   module SampleCons = {
-    proc sample(n:int): t list = {
+    proc sample(d: t distr, n:int): t list = {
       var r, rs;
 
       rs <$ dlist d (n - 1);
@@ -355,7 +354,7 @@ abstract theory Program.
   }.
 
   module Loop = {
-    proc sample(n:int): t list = {
+    proc sample(d: t distr, n:int): t list = {
       var i, r, l;
 
       i <- 0;
@@ -370,7 +369,7 @@ abstract theory Program.
   }.
 
   module LoopSnoc = {
-    proc sample(n:int): t list = {
+    proc sample(d: t distr, n:int): t list = {
       var i, r, l;
 
       i <- 0;
@@ -384,63 +383,179 @@ abstract theory Program.
     }
   }.
 
-  lemma pr_Sample _n &m xs: Pr[Sample.sample(_n) @ &m: res = xs] = mu (dlist d _n) (pred1 xs).
-  proof. by byphoare (_: n = _n ==> res = xs)=> //=; proc; rnd. qed.
+  lemma pr_Sample _d _n &m xs:
+    Pr[Sample.sample(_d, _n) @ &m: res = xs] = mu (dlist _d _n) (pred1 xs).
+  proof. by byphoare (: d = _d /\ n = _n ==> res = xs)=> //=; proc; rnd. qed.
 
-  equiv Sample_SampleCons_eq: Sample.sample ~ SampleCons.sample: 0 < n{1} /\ ={n} ==> ={res}.
+  equiv Sample_SampleCons_eq: Sample.sample ~ SampleCons.sample: 0 < n{1} /\ ={d, n} ==> ={res}.
   proof.
-    bypr (res{1}) (res{2})=> //= &1 &2 xs [lt0_n] <-.
-    rewrite (pr_Sample n{1} &1 xs); case (size xs = n{1})=> [<<-|].
-      case xs lt0_n=> [|x xs lt0_n]; 1: smt().
+    bypr (res{1}) (res{2})=> //= &1 &2 xs [lt0_n] [] <- <-.
+    rewrite (pr_Sample d{1} n{1} &1 xs); move: lt0_n; case (size xs = n{1})=> [<-|].
+    + case: xs=> [|x xs lt0_n]; 1: smt().
       rewrite dlistS1E.
-      byphoare (_: n = size xs + 1 ==> x::xs = res)=> //=; 2: by rewrite addrC. 
-      proc; seq 1: (rs = xs) (mu (dlist d (size xs)) (pred1 xs)) (mu d (pred1 x)) _ 0%r => //.
-        by rnd (pred1 xs); skip; smt().
-        by rnd (pred1 x); skip; smt().
-        by hoare; auto; smt().
-        smt().
-    move=> len_xs; rewrite dlist1E 1:/# ifF 1:/#.
+      byphoare (: d = d{1} /\ n = size xs + 1 ==> x::xs = res)=> //=; 2: by rewrite addrC. 
+      proc; seq 1: (rs = xs) (mu (dlist d{1} (size xs)) (pred1 xs)) (mu d{1} (pred1 x)) _ 0%r (d = d{1}) => //.
+      + by auto.
+      + by rnd (pred1 xs); skip; smt().
+      + by rnd (pred1 x); skip; smt().
+      + by hoare; auto; smt().
+      + smt().
+    move=> len_xs gt0_n; rewrite dlist1E 1:/# ifF 1:/#.
     byphoare (_: n = n{1} ==> xs = res)=> //=; hoare.
     proc; auto=> />; smt(supp_dlist_size).
   qed.
 
-  equiv Sample_Loop_eq: Sample.sample ~ Loop.sample: ={n} ==> ={res}.
+  equiv Sample_Loop_eq: Sample.sample ~ Loop.sample: ={d, n} ==> ={res}.
   proof.
     proc*; exists* n{1}; elim* => _n.
     move: (eq_refl _n); case (_n <= 0)=> //= h.
-    + inline *;rcondf{2} 4;auto;smt (supp_dlist0 weight_dlist0).
+    + inline *;rcondf{2} 5;auto;smt (supp_dlist0 weight_dlist0).
     have {h} h: 0 <= _n by smt ().
-    call (_: _n = n{1} /\ ={n} ==> ={res})=> //=.
+    call (_: _n = n{1} /\ ={d, n} ==> ={res})=> //=.
     elim _n h=> //= [|_n le0_n ih].
-      proc; rcondf{2} 3; auto=> />. smt(supp_dlist0 weight_dlist0).
+    + by proc; rcondf{2} 3; auto=> />; smt(supp_dlist0 weight_dlist0).
     case (_n = 0)=> [-> | h].
-      proc; rcondt{2} 3; 1:(by auto); rcondf{2} 6; 1:by auto.
+    + proc; rcondt{2} 3; 1:(by auto); rcondf{2} 6; 1:by auto.
       wp; rnd (fun x => head witness x) (fun x => [x]).
-      auto => />;split => [ rR ? | _ rL ].
+      auto => /> &0;split => [ rR ? | _ rL ].
       + by rewrite dlist1E //= big_consT big_nil.
-      rewrite supp_dlist //;case rL => //=; smt (size_eq0).
+      by rewrite supp_dlist //;case rL => //=; smt (size_eq0).
     transitivity SampleCons.sample
-                 (={n} /\ 0 < n{1} ==> ={res})
-                 (_n + 1 = n{1} /\ ={n} /\ 0 < n{1} ==> ={res})=> //=; 1:smt().
-      by conseq Sample_SampleCons_eq.
+                 (={d, n} /\ 0 < n{1} ==> ={res})
+                 (_n + 1 = n{1} /\ ={d, n} /\ 0 < n{1} ==> ={res})=> //=; 1:smt().
+    + by conseq Sample_SampleCons_eq.
     proc; splitwhile{2} 3: (i < n - 1).
     rcondt{2} 4; 1:by auto; while (i < n); auto; smt().
     rcondf{2} 7; 1:by auto; while (i < n); auto; smt().
     wp; rnd.
     outline {1} 1 ~ Sample.sample.
     rewrite equiv[{1} 1 ih].
     inline.
-    by wp; while (={i} /\ ={l} /\ n0{1} = n{2} - 1); auto; smt().
+    by wp; while (={i, l} /\ d0{1} = d{2} /\ n0{1} = n{2} - 1); auto; smt().
   qed.
 
-  equiv Sample_LoopSnoc_eq: Sample.sample ~ LoopSnoc.sample: ={n} ==> ={res}.
+  equiv Sample_LoopSnoc_eq: Sample.sample ~ LoopSnoc.sample: ={d, n} ==> ={res}.
   proof.
     proc*. 
     replace* {1} { x } by { x; r <- rev r; }.
       inline *; wp; rnd rev; auto.
       smt(revK dlist_rev).
     rewrite equiv[{1} 1 Sample_Loop_eq].
-    inline *; wp; while (={i, n0} /\ rev l{1} = l{2}); auto => />.
+    inline *; wp; while (={i, n0, d0} /\ rev l{1} = l{2}); auto => />.
     smt(rev_cons cats1).
   qed.
+end ParametricProgram.
+
+abstract theory Program.
+  type t.
+  op d: t distr.
+
+  module Sample = {
+    proc sample(n:int): t list = {
+      var r;
+
+      r <$ dlist d n;
+      return r;
+    }
+  }.
+
+  module SampleCons = {
+    proc sample(n:int): t list = {
+      var r, rs;
+
+      rs <$ dlist d (n - 1);
+      r  <$ d;
+      return r::rs;
+    }
+  }.
+
+  module Loop = {
+    proc sample(n:int): t list = {
+      var i, r, l;
+
+      i <- 0;
+      l <- [];
+      while (i < n) {
+        r <$ d;
+        l <- r :: l;
+        i <- i + 1;
+      }
+      return l;
+    }
+  }.
+
+  module LoopSnoc = {
+    proc sample(n:int): t list = {
+      var i, r, l;
+
+      i <- 0;
+      l <- [];
+      while (i < n) {
+        r <$ d;
+        l <- l ++ [r];
+        i <- i + 1;
+      }
+      return l;
+    }
+  }.
+
+  section.
+
+  local clone ParametricProgram as PP with
+    type t <- t
+  proof *.
+
+  lemma pr_Sample _n &m xs:
+    Pr[Sample.sample(_n) @ &m: res = xs] = mu (dlist d _n) (pred1 xs).
+  proof.
+  rewrite -(PP.pr_Sample d _n &m xs).
+  byequiv (: ={n} /\ d{2} = d ==> ={res})=> //.
+  by proc; auto.
+  qed.
+
+  equiv Sample_SampleCons_eq: Sample.sample ~ SampleCons.sample: 0 < n{1} /\ ={n} ==> ={res}.
+  proof.
+  transitivity PP.Sample.sample
+    (={n} /\ d{2} = d ==> ={res})
+    (0 < n{1} /\ ={n} /\ d{1} = d ==> ={res})=> //.
+  + by move=> |> &2 gt0_arg2; exists (d, arg{2}).
+  + by proc; auto.
+  transitivity PP.SampleCons.sample
+    (0 < n{1} /\ ={d, n} ==> ={res})
+    (={n} /\ d{1} = d ==> ={res})=> //.
+  + by move=> |> &2 gt0_n2 <-; exists (d{2}, n{2}).
+  + exact: PP.Sample_SampleCons_eq.
+  by proc; auto.
+  qed.
+
+  equiv Sample_Loop_eq: Sample.sample ~ Loop.sample: ={n} ==> ={res}.
+  proof.
+  transitivity PP.Sample.sample
+    (={n} /\ d{2} = d ==> ={res})
+    (={n} /\ d{1} = d ==> ={res})=> //.
+  + by move=> |> &2; exists (d, arg{2}).
+  + by proc; auto.
+  transitivity PP.Loop.sample
+    (={d, n} ==> ={res})
+    (={n} /\ d{1} = d ==> ={res})=> //.
+  + by move=> |> &2 <-; exists (d{2}, n{2}).
+  + exact: PP.Sample_Loop_eq.
+  by proc; while (={i, n, l} /\ d{1} = d); auto.
+  qed.
+
+  equiv Sample_LoopSnoc_eq: Sample.sample ~ LoopSnoc.sample: ={n} ==> ={res}.
+  proof.
+  transitivity PP.Sample.sample
+    (={n} /\ d{2} = d ==> ={res})
+    (={n} /\ d{1} = d ==> ={res})=> //.
+  + by move=> |> &2; exists (d, arg{2}).
+  + by proc; auto.
+  transitivity PP.LoopSnoc.sample
+    (={d, n} ==> ={res})
+    (={n} /\ d{1} = d ==> ={res})=> //.
+  + by move=> |> &2 <-; exists (d{2}, n{2}).
+  + exact: PP.Sample_LoopSnoc_eq.
+  by proc; while (={i, n, l} /\ d{1} = d); auto.
+  qed.
+  end section.
 end Program.