use auto unfold for some Logic operators

and fix bug with bindings for multiple variables and one type

Author: oskgo

examples/ChaChaPoly/chacha_poly.ec

@@ -2383,7 +2383,6 @@ section PROOFS.
   move=> n lenc Hrec [#] log lc c [] H1 H2.
   have/=:=Hrec log lc c H2.
   rewrite !size_flatten /= !sumzE /= !BIA.big_cons /=.
-  pose p1 := predT _; have->/={p1}:p1=true by done. 
   case: (c.`1 \in lenc) => ? H0 * /=.
   + rewrite H0 //=. 
     have-> /= :c.`1 <> n by smt().
@@ -2431,7 +2430,6 @@ section PROOFS.
   proof.
   move=> huniq hnin.
   rewrite !size_flatten /= !sumzE /= !BIA.big_cons /=.
-  pose p1 := predT _; have->/={p1}:p1=true by done. 
   rewrite !size_map; congr.
   rewrite !BIA.big_map /= !predTofV/(\o) /=.
   apply BIA.congr_big_seq  => />; rewrite {1}/predT /= => *.

examples/PRG.ec

@@ -270,7 +270,7 @@ section.
     by move=> _ _; islossless.
     (* Psample.prg preserves bad *)
     move=> *; proc; auto=> />; rewrite dseed_ll dout_ll /=.
-    move=> &hr + v1 _ _ v2 _ _; case=> [h|r r_in_log r_in_m].
+    move=> &hr + v1 _ v2 _; case=> [h|r r_in_log r_in_m].
     + by apply/Cycle; rewrite /= h.
     by apply/(@Collision _ _ r)=> /=; [rewrite r_in_log|rewrite r_in_m].
     (* [F.f ~ F.f: I] when Bad does not hold *)
@@ -290,7 +290,7 @@ section.
     case (x \in F.m).
     + by rcondf 3; auto=> />; rewrite dseed_ll dout_ll.
     rcondt 3; first by do !rnd; wp.
-    auto=> />; rewrite dseed_ll dout_ll //= => &hr bad_init x_notin_m v _ _ v0 _ _.
+    auto=> />; rewrite dseed_ll dout_ll //= => &hr bad_init x_notin_m v _ v0 _.
     case: bad_init=> [/(Cycle<:seed,seed * output>) -> //|r r_in_log r_in_m].
     by apply/(@Collision _ _ r)=> //=; rewrite mem_set r_in_m.
   (* Returning to main *)

examples/Pedersen.ec

@@ -108,7 +108,7 @@ section PedersenSecurity.
     proc; wp.
     swap 4 3.
     rnd (pred1 b'); call ug_ll; wp; rnd; call uc_ll; auto => />.
-    by rewrite dt_ll /= => v _ _ result; rewrite DBool.dbool1E.
+    by rewrite dt_ll /= => v _ result; rewrite DBool.dbool1E.
   qed.
 
   local lemma phi_hi (U<:Unhider) &m:

examples/UC/RndO.ec

@@ -318,7 +318,7 @@ module LRO : RO = {
 lemma RRO_resample_ll : islossless RRO.resample.
 proof. 
   proc; call (iter_ll RRO.I _)=> //; proc; auto=> /= ?;
-    by split; first apply sampleto_ll. 
+    by apply sampleto_ll. 
 qed.
 
 (* now we use the eager tactics to show a series of lemmas

examples/br93.ec

@@ -363,7 +363,7 @@ auto; call (_: true).
 + exact A_a1_ll. (* adversary *)
 + by proc; call (LRO_o_ll _); auto=> /=; apply: dptxt_ll. (* oracle *)
 auto=> />; rewrite dkeys_ll drand_ll dptxt_ll /predT /=.
-by move=> _ _ _ _ _ _ r; rewrite dbool1E pred1E.
+by move=> _ _ _ _ _ _ r; rewrite dbool1E.
 qed.
 
 (* Step 3: The reduction step -- if A queries the RO with the randomness *)

examples/ehoare/qselect/qselect.ec

@@ -251,7 +251,10 @@ proof.
     have -> : 4 * sumid (pos + 1)(hi + 1) = 2 * (2 * sumid (pos + 1)(hi + 1)) by ring.
     rewrite sumidE_rm 1:/#.
     apply RealOrder.ler_pdivr_mulr; 1: smt().
-    rewrite !to_pos_pos 1,3,4:/#.
+    rewrite !to_pos_pos 3,4:/#.
+    + rewrite le_fromint.
+      pose h1 := hi + 1; pose p1 := pos + 1. pose lo1 := 1+ lo.
+      by apply IntOrder.mulr_ge0 => /#.
     + rewrite le_fromint.
       pose h1 := hi + 1; pose p1 := pos + 1. pose lo1 := 1+ lo.
       have -> : 2 * ((h1 - p1) * (h1 + p1 - 1)) + 4 * ((- lo1) * (h1 - p1)) = 

examples/hashed_elgamal_std.ec

@@ -179,7 +179,7 @@ section Security.
   proof.
   byphoare=> //; proc.
   rnd (pred1 b')=> /=; conseq (_:_ ==> true).
-  + by move=> /> b; rewrite dbool1E pred1E.
+  + by move=> /> b; rewrite dbool1E.
   call Ag_ll; auto.
   by call Ac_ll; auto=> />; rewrite dhkey_ll dt_ll dbits_ll.
   qed.

src/ecScope.ml

@@ -1349,7 +1349,7 @@ module Op = struct
     } in
     let unfold =
       match op.po_args with
-      | (a, Some _) -> Some (List.length a)
+      | (a, Some _) -> Some (List.fold (fun acc (b, _) -> acc + List.length b) 0 a)
       | (_, None) -> None in
 
     let tyop   = EcDecl.mk_op ~opaque ?unfold tparams ty body lc in

theories/algebra/Bigalg.ec

@@ -122,7 +122,7 @@ lemma sum_pair_dep ['a 'b] u v J : uniq J =>
          (filter (fun ij : _ * _ => ij.`1 = i) J))
       (undup (unzip1 J)).
 proof.
-move=> uqJ; rewrite big_pair // &(eq_bigr) => /= a _.
+move=> uqJ; rewrite big_pair // &(eq_bigr) => /= a.
 by rewrite mulr_sumr !big_filter &(eq_bigr) => -[a' b] /= ->>.
 qed.
 
@@ -133,7 +133,7 @@ lemma sum_pair ['a 'b] u v J : uniq J =>
       (undup (unzip1 J)).
 proof.
 move=> uqJ; rewrite (@sum_pair_dep u (fun _ => v)) // &(eq_bigr) /=.
-by move=> a _ /=; congr; rewrite big_map predT_comp /(\o).
+by move=> a /=; congr; rewrite big_map predT_comp /(\o).
 qed.
 end BAdd.
 
@@ -357,7 +357,7 @@ case: (x = zeror) => [->>|nz_x].
 rewrite -subr_ge0 subrXX 1:ltzW // pmulr_lge0 ?subr_ge0 //=.
 rewrite {2}(_ : n = n - 1 + 1) 1:#ring BAdd.big_int_recr /= 1:/#.
 rewrite expr0 /= ltr_spaddr ?mul1r; 1: by rewrite expr_gt0 ltr_neqAle /#.
-by rewrite sumr_ge0 => /= i _; rewrite mulr_ge0 ?expr_ge0.
+by rewrite sumr_ge0 => /= i; rewrite mulr_ge0 ?expr_ge0.
 qed.
 
 lemma big_normr ['a] P F s :

theories/algebra/Bigop.eca

@@ -439,7 +439,7 @@ lemma big_undup ['a] (P : 'a -> bool) F s :
 proof.
 have <- := eq_big_perm P F _ _ (perm_undup_count s).
 rewrite big_flatten big_map (@big_mkcond P); apply/eq_big => //=.
-by move=> @/(\o) /= x _; apply/big_nseq_cond.
+by move=> @/(\o) /= x; apply/big_nseq_cond.
 qed.
 
 (* -------------------------------------------------------------------- *)