Use auto unfold for some Logic operators

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

@@ -1338,7 +1338,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.
 
 (* -------------------------------------------------------------------- *)

theories/algebra/Binomial.ec

@@ -213,6 +213,6 @@ lemma binomial (x y : real) n : 0 <= n => (x + y) ^ n =
   Bigreal.BRA.bigi predT (fun i => (bin n i)%r * (x ^ i * y ^ (n - i))) 0 (n + 1).
 proof.
 move=> ge0_n; have := binomial_r x y n ge0_n => ->.
-by apply: Bigreal.BRA.eq_bigr=> /= k _; rewrite intmulr mulrC mulrA.
+by apply: Bigreal.BRA.eq_bigr=> /= k; rewrite intmulr mulrC mulrA.
 qed.
 end BCR.

theories/algebra/DynMatrix.eca

@@ -296,7 +296,7 @@ rewrite !dotpE size_addv; pose m := max _ (max _ _).
 (* FIXME: (max _ _) should be precise enough, but this matches m! *)
 rewrite -[bigi _ _ 0 (max _ (size v2))](big_range0r _ m); 1,2: smt(getv0E mul0r).
 rewrite -[bigi _ _ 0 (max _ (size v3))](big_range0r _ m); 1,2: smt(getv0E mul0r).
-by rewrite sumrD /= &(eq_bigr) /= => i _; rewrite get_addv mulrDr.
+by rewrite sumrD /= &(eq_bigr) /= => i; rewrite get_addv mulrDr.
 qed.
 
 lemma dotpDl v1 v2 v3: dotp (v1 + v2) v3 = dotp v1 v3 + dotp v2 v3.
@@ -482,7 +482,7 @@ qed.
 lemma dotp_scalarv (v1 v2: vector) (s1 s2: t):
   dotp (s1 ** v1) (s2 ** v2) = (s1 * s2) * (dotp v1 v2).
 proof.
-rewrite 2!dotpE 2!size_scalarv !mulr_sumr &(eq_bigr) /= => i _.
+rewrite 2!dotpE 2!size_scalarv !mulr_sumr &(eq_bigr) /= => i.
 rewrite 2!get_scalarv; smt(mulrA mulrC).
 qed.
 
@@ -1154,7 +1154,7 @@ rewrite !get_mulmx dotpE /= (big_range0r (rows m2)) 1:/#.
 - smt(getm0E mulr0 mul0r rows_mulmx cols_mulmx row0E).
 rewrite (eq_bigr _ _ (fun k =>
     bigi predT (fun (l : int) => m1.[i,k] * (m2.[k,l] * m3.[l,j])) 0 (rows m3))).
-- move => k /= _.
+- move => k /=.
   rewrite get_mulmx dotpE mulr_sumr /= (big_range0r (rows m3)) // 1:/#.
   smt(getm0E mulr0 mul0r).
 rewrite exchange_big /= dotpE /=.
@@ -1664,10 +1664,10 @@ lemma catmr_subm m n: 0 <= n < cols m =>
 proof.
 move => n_bound; rewrite eq_matrixP /=.
 split => [| i j bound]. 
-- smt(rows_catmr cols_catmr size_subm).
+- rewrite rows_catmr cols_catmr; smt(size_subm).
 rewrite get_catmr // cols_subm /=.
 case (j < n) => j_bound.
-- rewrite get_subm /=; first 2 smt(size_catmr size_subm).
+- rewrite get_subm /=; first 2 rewrite rows_catmr cols_catmr 2!rows_subm 2!cols_subm /# in bound.
   rewrite (getm0E (subm _ _ _ _ _)).
   + smt(size_catmr size_subm).
   by rewrite addr0.

theories/algebra/Ideal.ec

@@ -204,7 +204,7 @@ qed.
 
 lemma ideal_idgen (xs : t list) : ideal (idgen xs).
 proof. do! split.
-- by exists []; rewrite BAdd.big1 //= => i _; rewrite mul0r.
+- by exists []; rewrite BAdd.big1 //= => i; rewrite mul0r.
 - move=> x y /idgenP[cxs [szx ->]] /idgenP[cys [szy ->]].
   rewrite BAdd.sumrB /=; exists (mkseq (fun i => cxs.[i] - cys.[i]) (size xs)).
   rewrite !BAdd.big_seq &(BAdd.eq_bigr) /= => i /mem_range rg_i.

theories/algebra/Matrix.eca

@@ -343,7 +343,7 @@ lemma trmxD (m1 m2 : matrix) : trmx (m1 + m2) = trmx m1 + trmx m2.
 proof. by apply/eq_matrixP=> i j rg; rewrite /= !trmxE. qed.
 
 lemma trace_trmx m : trace (trmx m) = trace m.
-proof. by apply: eq_bigr=> /= i _; rewrite trmxE. qed.
+proof. by apply: eq_bigr=> /= i; rewrite trmxE. qed.
 
 op ( * ) (m1 m2 : matrix) =
   offunm (fun i j => bigi predT (fun k => m1.[i, k] * m2.[k, j]) 0 size).
@@ -352,7 +352,7 @@ lemma offunM (m1 m2 : matrix) i j :
   (m1 * m2).[i, j] = bigi predT (fun k => m1.[i, k] * m2.[k, j]) 0 size.
 proof.
 case: (mrange i j) => [rg_ij|Nrg_ij]; first by rewrite offunmE.
-rewrite getm_out // big1 // => /= k _; move: Nrg_ij.
+rewrite getm_out // big1 // => /= k; move: Nrg_ij.
 by rewrite negb_and => -[/getm_outL|/getm_outR] ->; rewrite ?(mulr0, mul0r).
 qed.
 
@@ -394,16 +394,16 @@ move=> m1 m2 m3; apply/eq_matrixP=> i j rg_ij.
 pose M k l := m1.[i, k] * m2.[k, l] * m3.[l, j].
 pose E := bigi predT (fun k => bigi predT (M k) 0 size) 0 size.
 apply: (@eq_trans _ E); rewrite offunM.
-+ apply: eq_bigr=> /= k _; rewrite mulr_sumr &(eq_bigr) /=.
-  by move=> l _; rewrite mulrA.
-+ rewrite /E exchange_big &(eq_bigr) => /= l _.
-  by rewrite mulr_suml &(eq_bigr) => /= k _.
++ apply: eq_bigr=> /= k; rewrite mulr_sumr &(eq_bigr) /=.
+  by move=> l; rewrite mulrA.
++ rewrite /E exchange_big &(eq_bigr) => /= l.
+  by rewrite mulr_suml &(eq_bigr) => /= k.
 qed.
 
 lemma trmxM (m1 m2 : matrix) : trmx (m1 * m2) = trmx m2 * trmx m1.
 proof.
 apply/eq_matrixP=> i j rg; rewrite trmxE /=.
-by apply: eq_bigr => /= k _; rewrite !trmxE mulrC.
+by apply: eq_bigr => /= k; rewrite !trmxE mulrC.
 qed.
 
 op ( *^ ) (m : matrix) (v : vector) : vector =
@@ -415,13 +415,13 @@ op ( ^* ) (v : vector) (m : matrix) : vector =
 lemma mulmxTv (m : matrix) (v : vector) : (trmx m) *^ v = v ^* m.
 proof.
 apply/eq_vectorP=> i rgi; rewrite !offunvE //= &(eq_bigr) /=.
-by move=> j _; rewrite mulrC trmxE.
+by move=> j; rewrite mulrC trmxE.
 qed.
 
 lemma mulmxv0 (m : matrix) : m *^ zerov = zerov.
 proof.
 apply/eq_vectorP => i rgi; rewrite !offunvE //=.
-by rewrite big1 // => /= j _; rewrite mulr0.
+by rewrite big1 // => /= j; rewrite mulr0.
 qed.
 
 lemma mulmx1v (v : vector) : onem *^ v = v.
@@ -436,14 +436,14 @@ lemma mulmxvDl (m1 m2 : matrix) (v : vector) :
   (m1 + m2) *^ v = m1 *^ v + m2 *^ v.
 proof.
 apply/eq_vectorP=> i rgi /=; rewrite !offunvE //=.
-by rewrite -big_split &(eq_bigr) => /= j _; rewrite mulrDl.
+by rewrite -big_split &(eq_bigr) => /= j; rewrite mulrDl.
 qed.
 
 lemma mulmxvDr (m : matrix) (v1 v2 : vector) :
   m *^ (v1 + v2) = m *^ v1 + m *^ v2.
 proof.
 apply/eq_vectorP=> i rgi /=; rewrite !offunvE //=.
-by rewrite -big_split &(eq_bigr) => /= j _; rewrite mulrDr.
+by rewrite -big_split &(eq_bigr) => /= j; rewrite mulrDr.
 qed.
 
 lemma mulmxvA (m1 m2 : matrix) (v : vector) :
@@ -453,10 +453,10 @@ apply/eq_vectorP=> i rgi; rewrite !offunvE //=.
 pose F j k := m1.[i,k] * m2.[k,j] * v.[j].
 pose E := bigi predT (fun j => bigi predT (F j) 0 size) 0 size.
 apply: (@eq_trans _ E).
-+ by rewrite /E /F &(eq_bigr) => /= j _; rewrite mulr_suml.
++ by rewrite /E /F &(eq_bigr) => /= j; rewrite mulr_suml.
 rewrite /E /F exchange_big !big_seq &(eq_bigr) /= => j.
 move/mem_range => rgj; rewrite offunvE //= mulr_sumr. 
-by apply: eq_bigr => /= k _; rewrite mulrA.
+by apply: eq_bigr => /= k; rewrite mulrA.
 qed.
 
 lemma mulvmxT (v : vector) (m : matrix) : v ^* (trmx m) = m *^ v.
@@ -484,13 +484,13 @@ lemma mulmxvE (m : matrix) (v : vector) i :
   (m *^ v).[i] = bigi predT (fun j => m.[i, j] * v.[j]) 0 size.
 proof.
 case: (0 <= i < size) => [rg_i|rgN_i]; first by rewrite offunvE.
-by rewrite getv_out // big1 //= => j _; rewrite getm_outL // mul0r.
+by rewrite getv_out // big1 //= => j; rewrite getm_outL // mul0r.
 qed.
 
 lemma mulvmxE (m : matrix) (v : vector) j :
   (v ^* m).[j] = bigi predT (fun i => v.[i] * m.[i, j]) 0 size.
 proof.
-by rewrite -mulmxTv mulmxvE; apply: eq_bigr => /= i _; rewrite trmxE mulrC.
+by rewrite -mulmxTv mulmxvE; apply: eq_bigr => /= i; rewrite trmxE mulrC.
 qed.
 
 op colmx (v : vector) : matrix = offunm (fun i _ => v.[i]).
@@ -518,7 +518,7 @@ proof. by move=> rg_i; rewrite -colmxT trmxE colmxE. qed.
 lemma colmx_mulmxv (m : matrix) (v : vector) : colmx (m *^ v) = m * colmx v.
 proof.
 apply/eq_matrixP=> i j [rg_i rg_j]; rewrite colmxE // offunM.
-by rewrite mulmxvE; apply: eq_bigr => /= k _; rewrite colmxE.
+by rewrite mulmxvE; apply: eq_bigr => /= k; rewrite colmxE.
 qed.
 
 lemma rowmx_mulvmx (v : vector) (m : matrix) : rowmx (v ^* m) = rowmx v * m.
@@ -529,7 +529,7 @@ lemma mulmx_diag (v1 v2 : vector) :
 proof.
 apply: eq_matrixP=> i j [rg_i rg_j]; rewrite diagmxE /=.
 case: (i = j) => [<-|ne_ij]; last first.
-+ rewrite big1 // => /= k _; rewrite !diagmxE.
++ rewrite big1 // => /= k; rewrite !diagmxE.
   case: (i = k) => [->>|]; last by rewrite mul0r.
   by case: (k = j) => [<<-|]; last by rewrite mulr0.
 rewrite offunvE //= (bigD1 _ _ i) ?(mem_range, range_uniq) //=.
@@ -549,9 +549,9 @@ lemma dotp_mulmxv m v1 v2 : dotp (m *^ v1) v2 = dotp v1 (v2 ^* m).
 proof.
 pose F i j := m.[i, j] * v1.[j] * v2.[i].
 rewrite /dotp -(eq_bigr _ (fun i => bigi predT (F i) 0 size)) /=.
-+ by move=> i _ @/F; rewrite -mulr_suml mulmxvE.
-rewrite exchange_big &(eq_bigr) => /= i _ @/F.
-rewrite mulvmxE mulr_sumr &(eq_bigr) => /= j _.
++ by move=> i @/F; rewrite -mulr_suml mulmxvE.
+rewrite exchange_big &(eq_bigr) => /= i @/F.
+rewrite mulvmxE mulr_sumr &(eq_bigr) => /= j.
 by rewrite mulrA (mulrC _ m.[_]) mulrA.
 qed.
 

theories/algebra/Poly.ec

@@ -438,7 +438,7 @@ apply: (eq_trans _ _ _ (BCA.eq_big_perm _ _ _ (range 0 (k+1)) _)).
   * move=> x; split => [/mapP[y []]|]; 1: by rewrite !mem_range /#.
     rewrite !mem_range => *; apply/mapP; exists (F x).
     by rewrite !mem_range /F /#.
-+ by apply: BCA.eq_bigr => /= i _ @/F; rewrite mulrC /#.
++ by apply: BCA.eq_bigr => /= i @/F; rewrite mulrC /#.
 qed.
 
 lemma polyMEwr M p q k : (k <= M)%Int => (p * q).[k] =
@@ -468,9 +468,9 @@ have ->: (p * (q * r)).[k] =
   ) 0 (k+1).
 + rewrite polyME !BCA.big_seq &(BCA.eq_bigr) => /= i.
   case/mem_range => g0_i lt_i_Sk; rewrite (@polyMEwr k) 1:/#.
-  by rewrite BCA.mulr_sumr &(BCA.eq_bigr) => /= j _; rewrite mulrA.
-rewrite BCA.exchange_big &(BCA.eq_bigr) => /= i _.
-by rewrite &(BCA.eq_bigr) => /= j _ /#.
+  by rewrite BCA.mulr_sumr &(BCA.eq_bigr) => /= j; rewrite mulrA.
+rewrite BCA.exchange_big &(BCA.eq_bigr) => /= i.
+by rewrite &(BCA.eq_bigr) => /= j /#.
 qed.
 
 lemma mul1p : left_id poly1 polyM.
@@ -485,13 +485,13 @@ qed.
 lemma mul0p : left_zero poly0 polyM.
 proof.
 move=> p; apply/poly_eqP=> c _; rewrite poly0E polyME.
-by rewrite BCA.big1 //= => i _; rewrite poly0E mul0r.
+by rewrite BCA.big1 //= => i; rewrite poly0E mul0r.
 qed.
 
 lemma mulpDl: left_distributive polyM polyD.
 proof.
 move=> p q r; apply: poly_eqP => c ge0_c; rewrite !(polyME, polyDE).
-by rewrite -BCA.big_split &(BCA.eq_bigr) => /= i _; rewrite polyDE mulrDl.
+by rewrite -BCA.big_split &(BCA.eq_bigr) => /= i; rewrite polyDE mulrDl.
 qed.
 
 lemma onep_neq0 : poly1 <> poly0.

theories/algebra/StdBigop.ec

@@ -215,7 +215,7 @@ move=> rg_p; have h := sum_iexpr_le p n rg_p.
 rewrite &(RealOrder.ler_pdivl_mulr) -1:mulrC //.
 - by rewrite RealOrder.expr_gt0 /#.
 rewrite &(RealOrder.ler_trans _ _ _ _ h) RealOrder.lerr_eq.
-by congr; apply: BRA.eq_bigr => /= i _; rewrite ofintR.
+by congr; apply: BRA.eq_bigr => /= i; rewrite ofintR.
 qed.
 
 end Bigreal.