Simplify the pHL while rule further

The rule is now simpler, but a bit harder to use.
It does avoid doubling up reasoning when the loop condition itself is probabilistic.

examples/PIR.ec

@@ -209,9 +209,7 @@ proof.
       + auto => /> &hr H0j ???? b ?.    
         rewrite restrS //= oflist_cons. 
         smt (is_restr_addS is_restrS is_restr_Ueq  is_restr_diff fset0U is_restr_restr).
-      + if.
-        + by conseq H=> /#.
-        by hoare.
+        by conseq H=> /#.
       + by hoare;auto.
       smt().      
     conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
@@ -221,21 +219,14 @@ proof.
          is_restr (oflist s0) j0 /\ oflist s0 = restr x j0).
     + by auto => /> /#.
     + by wp => /=;rnd (pred1 (j0 \in x));skip => /> &hr;rewrite dbool1E.
-    + if.
-      + conseq H=> />.
-        + case: (j0 \in x) => Hjx ?? His Hof.
-          + by rewrite oflist_cons restrS 1:/# Hjx Hof.
-          by rewrite restrS 1:/# Hjx Hof /= fset0U.
-        smt (is_restrS is_restr_addS oflist_cons).
-      skip=> [/> ge1_Sj0 ge_Sj_N s0_j0 s0_x_j0 Sj0_N|].
-      + have ->: j0 + 1 = N by smt().
-        by rewrite expr0.
-      smt(restrS oflist_cons fset0U).
-    + if.
-      + conseq H=> /> &0 />.
-        + smt(restrS oflist_cons fset0U in_fsetU in_fset1 nin_is_restr).
-        smt(is_restr_addS oflist_cons is_restrS fset0U).
-      by hoare; skip; smt(restrS oflist_cons fset0U in_fsetU in_fset1 nin_is_restr).
+    + conseq H=> />.
+      + case: (j0 \in x) => Hjx ?? His Hof.
+        + by rewrite oflist_cons restrS 1:/# Hjx Hof.
+        by rewrite restrS 1:/# Hjx Hof /= fset0U.
+      smt (is_restrS is_restr_addS oflist_cons).
+    + conseq H=> /> &0 />.
+      + smt(restrS oflist_cons fset0U in_fsetU in_fset1 nin_is_restr).
+      smt(is_restr_addS oflist_cons is_restrS fset0U).
     move=> &hr /> ?????; rewrite -exprS 1:/#; congr;congr;ring.
 
   + wp;rnd predT;skip => /> &hr.
@@ -268,10 +259,8 @@ proof.
       + auto => /> &hr 5? b _.
         case: (j{hr}=i{hr}) => />; rewrite restrS //= oflist_cons;
           smt (is_restr_addS is_restrS is_restr_Ueq  is_restr_diff fset0U is_restr_restr).
-        if.
-        + by conseq H => /#.
-        by hoare; auto.
-      + by hoare;auto.
+        by conseq H => /#.
+      + by hoare; auto.
       smt().      
     conseq (_ : _ : = (1%r / 2%r ^ (N - j))) => [/#|].
     exists * j, PIR.s';elim * => j0 s0.    
@@ -280,37 +269,29 @@ proof.
          is_restr (oflist s0) j0 /\ oflist s0 = restr x j0).
     + by auto => /#.
     + by wp => /=;rnd (pred1 ((j0 = i) ^^ (j0 \in x)));skip => /> &hr;rewrite dbool1E.
-    + if.
-      + conseq H => />.
-        + move=> &hr ?? His Hof;case: (j0 = i{hr}) => /=. 
-          + rewrite xorC xor_true => <<-.
-            case: (j0 \in x) => Hjx.
-            + by rewrite restrS 1:/# Hjx /= oflist_cons Hof.
-            by rewrite /= restrS 1:/# Hjx /= fset0U Hof.
-          rewrite xorC xor_false => ?.
+    + conseq H => />.
+      + move=> &hr ?? His Hof;case: (j0 = i{hr}) => /=. 
+        + rewrite xorC xor_true => <<-.
           case: (j0 \in x) => Hjx.
-          + by rewrite oflist_cons restrS 1:/# Hjx Hof.
-          by rewrite restrS 1:/# Hjx Hof /= fset0U.
-        smt (is_restrS is_restr_addS oflist_cons).
-      skip=> /> &0 *.
-      + have ->: j0 + 1 = N by smt().
-        by rewrite expr0.
-      smt(oflist_cons restrS fset0U).
-    + if.      
-      + conseq H => />.
-        + move=> &hr ?? His Hof Hb.
-          rewrite restrS 1:/# (negbRL _ _ Hb);case: (j0 = i{hr}) => /= [<<- | ?].  
-          + rewrite xorC xor_true /=.
-            case (j0 \in x) => /= Hj0x /=.
-            + by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His). 
-            by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
-          rewrite xorC xor_false.
+          + by rewrite restrS 1:/# Hjx /= oflist_cons Hof.
+          by rewrite /= restrS 1:/# Hjx /= fset0U Hof.
+        rewrite xorC xor_false => ?.
+        case: (j0 \in x) => Hjx.
+        + by rewrite oflist_cons restrS 1:/# Hjx Hof.
+        by rewrite restrS 1:/# Hjx Hof /= fset0U.
+      smt (is_restrS is_restr_addS oflist_cons).
+    + conseq H => />.
+      + move=> &hr ?? His Hof Hb.
+        rewrite restrS 1:/# (negbRL _ _ Hb);case: (j0 = i{hr}) => /= [<<- | ?].  
+        + rewrite xorC xor_true /=.
           case (j0 \in x) => /= Hj0x /=.
           + by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His). 
           by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
-        smt (is_restrS is_restr_addS oflist_cons).
-      hoare; auto=> /> &0.
-      smt(oflist_cons restrS in_fsetU in_fset1 nin_is_restr fset0U).
+        rewrite xorC xor_false.
+        case (j0 \in x) => /= Hj0x /=.
+        + by rewrite (eq_sym (oflist s0)) (is_restr_diff j0 (restr x j0) _ His). 
+        by rewrite fset0U oflist_cons -Hof (is_restr_diff j0 (oflist s0) _ His).
+      smt (is_restrS is_restr_addS oflist_cons).
     by move=> &hr /> ?????;rewrite -exprS 1:/#;congr;congr;ring.
   + wp;rnd predT;skip => &hr.
     smt (dbool_ll oflist_cons is_restrS is_restr_addS).

examples/PRG.ec

@@ -527,22 +527,14 @@ section.
   while (n <= qP /\ card (fdom F.m) <= qF).
   + move=> Hw; exists* P.logP, F.m; elim* => logPw m.
     case: (Bad P.logP F.m).
-    + by conseq (_ : _ : <= (1%r))=> // /#.         
-    case: (n = size P.logP + 1).                    
-    + rcondf 3; first by auto=> /#.
-      wp; rnd; auto=> /> _ /le_fromint domF_le_qF _.
-      rewrite addzA big_int1=> /= /pr_newbad ->.
-      apply: ler_wpmul2r.
-      + by apply: invr_ge0; smt(Support.card_gt0).
-      by rewrite !fromintD ler_add2r.
-    rcondt 3; first by auto=> /#.
+    + by conseq (_ : _ : <= (1%r))=> // /#.
     seq 2: (Bad P.logP F.m)
            ((qF + size logPw)%r / Support.card%r) 1%r 1%r
            ((sumid (qF + (size logPw + 1)) (qF + n))%r / Support.card%r)
            (F.m = m /\ r::logPw = P.logP /\
             n <= qP /\ card (fdom F.m) <= qF)=> //.
     + by wp; rnd=> //.
-    + wp; rnd; auto=> /> &0 _ /le_fromint domF_le_qF _ + _ - /pr_newbad ->.
+    + wp; rnd; auto=> /> &0 _ /le_fromint domF_le_qF _ /pr_newbad ->.
       apply: ler_wpmul2r.
       + by apply: invr_ge0; smt(Support.card_gt0).
       by rewrite !fromintD ler_add2r.

examples/WhileSampling.ec

@@ -28,7 +28,6 @@ while true (if test r then 1 else 0) 1 (mu sample (predC test))=> //.
 + by move=> _ r; case: (test r).
 + move=> ih; seq  1: true=> //.
   by auto; rewrite sample_ll.
-+ by if=> //; conseq ih.
 + by auto; rewrite sample_ll.
 rewrite pr_ntest=> /= z; conseq (: true ==> !test r).
 + smt().

examples/vonNeumann.eca

@@ -89,6 +89,7 @@ have ->:
 + byphoare (_: true ==> res = x)=> //.
   by proc; rnd (pred1 x \o fst); skip=> />.
 byphoare (_: true ==> res = x)=> //; proc; sp.
+conseq (: _: =(if b = b' then mu dvn (pred1 x \o fst) else b2r (b = x)))=> //.
 while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
 + by move=> /#.
 + move=> ih.
@@ -98,16 +99,16 @@ while true (b2i (b = b')) 1 (2%r * p * (1%r - p))=> />.
   + seq 1: (b' = !x) (mu1 dbiased (!x)) 1%r (mu1 dbiased x) (mu dvn (pred1 x \o fst)) (b = x)=> //.
     + by auto.
     + by rnd (pred1 (!x)); auto.
-    + by rcondf 1; auto; case: x.
+    + by conseq ih=> />; rewrite negbLR.
     + by rnd (pred1 x); auto=> /#.
-    by rcondt 1; [by auto=> /#|by conseq ih].
+    by conseq ih=> /> &0 /negbRL /=.
   + by rnd (pred1 (!x)); auto=> /#.
   + seq 1: (b' = x) _ 0%r (mu1 dbiased (!x)) (mu dvn (pred1 x \o fst)) (b <> x)=> //.
     + by auto.
-    + by rcondf 1; [by auto|by hoare].
+    + by conseq ih=> /> &0 /negbRL ->; rewrite negbLR.
     + by rnd (pred1 (!x)); auto=> /#.
-    by rcondt 1; [by auto=> /#|by conseq ih].
-  move=> {ih} _ _; rewrite !vnE /svn /(\o)/ pred1 /= /b2i /=.
+    by conseq ih=> /> &0 /negbRL -> /negbRL ->.
+  move=> {ih} _ -> /=; rewrite !vnE /svn /(\o)/ pred1 /= /b2i /=.
   by move: x=> [] /=; rewrite !dbiased1E /#.
 + by auto=> />; rewrite dbiased_ll.
 split => //= [|z]; first by smt w=(in01_p).

src/phl/ecPhlWhile.ml

@@ -189,9 +189,7 @@ let t_bdhoare_while_rev_r inv tc =
   (* 1. Sub-goal *)
   let body_concl =
     let while_s  = EcModules.stmt [EcModules.i_abstract w] in
-    let while_s' = EcModules.i_if (lp_guard_exp, while_s, EcModules.stmt []) in
-    let while_s' = EcModules.stmt [while_s'] in
-    let unfolded_while_s = EcModules.s_seq lp_body while_s' in
+    let unfolded_while_s = EcModules.s_seq lp_body while_s in
     let while_jgmt = f_bdHoareS_r {bhs with bhs_pr=inv ; bhs_s=while_s; } in
     let unfolded_while_jgmt = f_bdHoareS_r
       { bhs with bhs_pr = f_and inv lp_guard; bhs_s = unfolded_while_s; }
@@ -283,10 +281,8 @@ let t_bdhoare_while_rev_geq_r inv vrnt k eps tc =
 
   let body_concl =
     let while_s1 = EcModules.stmt [EcModules.i_abstract w] in
-    let while_s2 = EcModules.i_if (lp_guard_exp, while_s1, EcModules.stmt []) in
-    let while_s2 = EcModules.stmt [while_s2] in
 
-    let unfolded_while_s = EcModules.s_seq lp_body while_s2 in
+    let unfolded_while_s = EcModules.s_seq lp_body while_s1 in
     let while_jgmt = f_bdHoareS_r { bhs with bhs_pr=inv; bhs_s=while_s1; } in
     let unfolded_while_jgmt = f_bdHoareS_r
       { bhs with bhs_pr=f_and inv lp_guard; bhs_s=unfolded_while_s; }

theories/distributions/Dexcepted.ec

@@ -296,14 +296,16 @@ case @[ambient]: (mu (dt x) (X x) = weight (dt x))=> Hpt.
   while (X x r /\ i = x /\ test = X)=> //=.
   auto=> &m' [#] _ -> -> _ r; move: (mu_in_weight (X x) (dt x) r).
   by rewrite Hpt.
+conseq (: _: =(if X x r then mu (dt x \ X x) P else b2r (P r))).
++ by move=> />; rewrite y_in_Xx.
 while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x)))=> //=.
 + smt().
 + move=> ih. alias 2 r0 = r.
   (** TRANSITIVITY FOR PHOARE!! **)
   phoare split (mu (dt x) (predI P (predC (X x))))
                (mu (dt x) (X x) * mu (dt x \ X x) P)
                : (P r0 /\ !X x r0).
-  + move=> &m' [#] -> -> _ /=; rewrite dexceptedE.
+  + move=> &m' [#] -> -> -> /=; rewrite dexceptedE.
     rewrite -{1}(mulr1 (mu (dt x) (predI _ _))).
     rewrite -(@divrr (weight (dt x) - mu (dt x) (X x))).
     + smt().
@@ -315,16 +317,16 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x))
             (r0 = r /\ i = x /\ test = X)=> //=.
     + by auto.
     + by wp; rnd (predI P (predC (X x))); auto=> />.
-    + by rcondf 1.
+    + by conseq ih=> />.
     by hoare; conseq (: _ ==> true)=> // /#.
   seq 2: (!X x r0)
                          _ 0%r
          (mu (dt x) (X x)) (mu (dt x \ X x) P)
          (r0 = r /\ i = x /\ test = X)=> //=.
   + by auto.
-  + by hoare; rcondf 1=> //; auto=> /#.
+  + case: (P r0); last by conseq ih=> />.
+    by hoare; conseq (: true)=> />.
   + by wp; rnd.
-  rcondt 1; first by auto.
   by conseq ih=> &m' />; rewrite dexceptedE.
 + by auto.
 split.