diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec index 271b22b931..0f06dec806 100644 --- a/examples/ChaChaPoly/chacha_poly.ec +++ b/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 /= => *. diff --git a/examples/PRG.ec b/examples/PRG.ec index 870a3ce0eb..d65a0153fb 100644 --- a/examples/PRG.ec +++ b/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 *) diff --git a/examples/Pedersen.ec b/examples/Pedersen.ec index bf42f25c96..d34e015d7c 100644 --- a/examples/Pedersen.ec +++ b/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: diff --git a/examples/UC/RndO.ec b/examples/UC/RndO.ec index e7b3c09838..4fc8823ddb 100644 --- a/examples/UC/RndO.ec +++ b/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 diff --git a/examples/br93.ec b/examples/br93.ec index 8a7c0fb851..167d8caf82 100644 --- a/examples/br93.ec +++ b/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 *) diff --git a/examples/ehoare/qselect/qselect.ec b/examples/ehoare/qselect/qselect.ec index d065a3174a..67a716361e 100644 --- a/examples/ehoare/qselect/qselect.ec +++ b/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)) = diff --git a/examples/hashed_elgamal_std.ec b/examples/hashed_elgamal_std.ec index 03bfa02a86..d8b8fb127c 100644 --- a/examples/hashed_elgamal_std.ec +++ b/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. diff --git a/src/ecScope.ml b/src/ecScope.ml index 1b1a3a97e9..8bc709c3d2 100644 --- a/src/ecScope.ml +++ b/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 diff --git a/theories/algebra/Bigalg.ec b/theories/algebra/Bigalg.ec index a56bc14135..fdf1a71ab7 100644 --- a/theories/algebra/Bigalg.ec +++ b/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 : diff --git a/theories/algebra/Bigop.eca b/theories/algebra/Bigop.eca index 3d1e1a8272..f616d9a0b3 100644 --- a/theories/algebra/Bigop.eca +++ b/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. (* -------------------------------------------------------------------- *) diff --git a/theories/algebra/Binomial.ec b/theories/algebra/Binomial.ec index d250a593af..9efa8007c5 100644 --- a/theories/algebra/Binomial.ec +++ b/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. diff --git a/theories/algebra/DynMatrix.eca b/theories/algebra/DynMatrix.eca index 8338e31700..5265b60baa 100644 --- a/theories/algebra/DynMatrix.eca +++ b/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. diff --git a/theories/algebra/Ideal.ec b/theories/algebra/Ideal.ec index d938c383bd..f232a4a46b 100644 --- a/theories/algebra/Ideal.ec +++ b/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. diff --git a/theories/algebra/Matrix.eca b/theories/algebra/Matrix.eca index 336ecd3f24..7116f6951e 100644 --- a/theories/algebra/Matrix.eca +++ b/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. diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec index c6632537b7..750e62e7a9 100644 --- a/theories/algebra/Poly.ec +++ b/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. diff --git a/theories/algebra/StdBigop.ec b/theories/algebra/StdBigop.ec index c3c9821ddf..ead4993094 100644 --- a/theories/algebra/StdBigop.ec +++ b/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. diff --git a/theories/analysis/RealSeries.ec b/theories/analysis/RealSeries.ec index ac61c29b7d..cc797b511d 100644 --- a/theories/analysis/RealSeries.ec +++ b/theories/analysis/RealSeries.ec @@ -75,7 +75,7 @@ move=> K uqK; rewrite (@BRA.bigID _ _ (mem J)) addrC BRA.big1 /=. + by move=> x [_ @/predC] /=; apply: contraR; rewrite normr0P &(hfin). rewrite -BRA.big_filter (@BRA.bigID _ _ (mem K) (undup J)). rewrite -!(@BRA.big_filter (predI _ _)) /= ler_paddr. -+ by apply: Bigreal.sumr_ge0 => /= a _; rewrite normr_ge0. ++ by apply: Bigreal.sumr_ge0 => /= a; rewrite normr_ge0. apply/lerr_eq/BRA.eq_big_perm. rewrite uniq_perm_eq ?filter_uniq ?undup_uniq //. by move=> x; rewrite !mem_filter mem_undup andbC. @@ -97,7 +97,7 @@ rewrite (@partition_big (fun x => x) _ predT _ _ I). + apply: pmap_inj_in_uniq; last by apply range_uniq. by move=> i j v _ _; case: enm => h _; apply/h. + by move=> a hin hs /=; rewrite /predT /=; apply /hn. -apply: sub_ler_sum => // a /= _. +apply: sub_ler_sum => // a /=. by rewrite (@bigD1_cond_if _ _ _ a) //= big1 /#. qed. @@ -181,7 +181,7 @@ lemma summableZ (s : 'a -> real) (c : real) : proof. case=> M h; exists (`|c| * M) => J /h leM. rewrite -(@eq_bigr _ (fun x => `|c| * `|s x|)) /=. -+ by move=> x _; rewrite normrM. ++ by move=> x; rewrite normrM. by rewrite -mulr_sumr ler_wpmul2l 1:normr_ge0. qed. @@ -209,12 +209,12 @@ proof. case=> [Mf smf] [Mg smg]; exists (Mf * Mg) => J uqJ. pose J1 := undup (unzip1 J). pose F (ab : 'a * 'b) := `|f ab.`1| * `|g ab.`1 ab.`2|. -rewrite (@eq_bigr _ _ F) /= => [ab _|]; 1: by rewrite normrM. +rewrite (@eq_bigr _ _ F) /= => [ab|]; 1: by rewrite normrM. rewrite /F (@sum_pair_dep ("`|_|"%Real \o f) ("`|_|"%Real \o2 g)) //=. apply: (@ler_trans (big predT (fun i => `|f i| * Mg) J1)); last first. + rewrite -mulr_suml ler_wpmul2r; 1: by apply: (@smg witness [] _). by apply/smf/undup_uniq. -apply: ler_sum => /= a _; rewrite ler_wpmul2l 1:normr_ge0. +apply: ler_sum => /= a; rewrite ler_wpmul2l 1:normr_ge0. pose G (b : 'b) := `|g a b|. rewrite big_filter (@eq_bigr _ _ (G \o snd)) => [[a' b] /= ->>//|]. rewrite -big_filter -(@big_map snd predT) &(smg). @@ -371,7 +371,7 @@ lemma eq_psum ['a] (s1 s2 : 'a -> real) : (forall x, `|s1 x| = `|s2 x|) => psum s1 = psum s2. proof. move=> eq; apply: eq_lub => x; split; case=> J [uqJ ->]; - by exists J; split=> //; apply: eq_bigr => /= i _; rewrite eq. + by exists J; split=> //; apply: eq_bigr => /= i; rewrite eq. qed. (* -------------------------------------------------------------------- *) @@ -406,7 +406,7 @@ have uqJ: forall n, uniq (pmap J (range 0 n)). by move=> x y v _ _; case: enm => + _; apply. have mono_u: forall n1 n2, (0 <= n1 <= n2)%Int => u n1 <= u n2. + move=> n1 n2 len; rewrite /u (@range_cat n1 _ n2); 1..2: by case: len. - by rewrite pmap_cat big_cat ler_addl sumr_ge0 => x /= _; apply/normr_ge0. + by rewrite pmap_cat big_cat ler_addl sumr_ge0 => x /=; apply/normr_ge0. case: (sbl) => M sblM; have := cnvto_lub_bmono_from _ M 0 mono_u _. + by move=> n ge0_n; apply/sblM/uqJ. pose l := lub _; suff ->//: l = psum s; rewrite eqr_le; split. @@ -457,7 +457,7 @@ have: perm_eq (F1 ++ F2) (pmap J (range 0 N)). rewrite pmap_map; apply/mapP; exists (Some v'). by rewrite mem_filter. move/eq_big_perm=> <-; rewrite big_cat ler_addl. -by apply/sumr_ge0=> y /= _; apply/normr_ge0. +by apply/sumr_ge0=> y /=; apply/normr_ge0. qed. (* -------------------------------------------------------------------- *) @@ -823,7 +823,7 @@ proof. move=> sms; rewrite psum_sum. + by apply/summable_big=> b bs /=; apply/summable_norm/sms. rewrite sum_norm /= -1:sum_big. -+ by move=> a; apply: sumr_ge0 => /= b _; apply: normr_ge0. ++ by move=> a; apply: sumr_ge0 => /= b; apply: normr_ge0. + by move=> b bs /=; apply/summable_norm/sms. by rewrite !big_seq &(eq_bigr) => /= b bs; rewrite psum_sum 1:&(sms). qed. @@ -898,14 +898,14 @@ move=> sm; rewrite eqr_le; split => [|_]. by apply: eq_psum => a /= @/v /#. rewrite /G /F (@partition_big f predT predT _ J L) /=. - by apply/undup_uniq. - - by move=> x xJ _ @/L; rewrite mem_undup map_f. + - by move=> x xJ @/L; rewrite mem_undup map_f. apply: ler_sum_seq => b bL _ /= @/predT /=; rewrite big_mkcond /=. rewrite ger0_norm; first by rewrite ge0_psum summable_cond. have smc := summable_cond _ (fun x => b = f x) sms. apply: (ler_trans _ _ (ler_big_psum smc uqJ)) => {smc}. - by rewrite lerr_eq &(eq_bigr) => a /= _ /#. + by rewrite lerr_eq &(eq_bigr) => a /= /#. + apply: ler_psum_lub => J uqJ; rewrite sumr_norm /=. - - by move=> ? _; apply/ge0_psum/summable_cond. + - by move=> ?; apply/ge0_psum/summable_cond. rewrite -psum_big /=. - by move=> b _; apply/summable_cond. apply: ler_psum => //= a; case: (f a \in J) => faJ; last first. @@ -929,10 +929,10 @@ rewrite (@psum_partition f (pos s)) 1:&summable_pos //. rewrite (@psum_partition f (neg s)) 1:&summable_neg //. rewrite psumB /=; last apply: eq_sum => b /=. + exists (psum (pos s)) => J uqJ; rewrite sumr_norm /=. - by move=> b _; apply/ge0_psum/hp. + by move=> b; apply/ge0_psum/hp. by apply: summable_psum_partition => //; apply/summable_pos. + exists (psum (neg s)) => J uqJ; rewrite sumr_norm /=. - by move=> b _; apply/ge0_psum/hn. + by move=> b; apply/ge0_psum/hn. by apply: summable_psum_partition => //; apply/summable_neg. rewrite ger0_norm; 1: by apply/ge0_psum/hp. rewrite ger0_norm; 1: by apply/ge0_psum/hn. @@ -956,7 +956,7 @@ lemma summable_partition ['a 'b] (f : 'a -> 'b) s : summable s => proof. move=> sms; exists (psum s) => J uqJ. have h := summable_psum_partition f s sms J uqJ. -apply/(ler_trans _ _ h)/Bigreal.ler_sum => /= b _. +apply/(ler_trans _ _ h)/Bigreal.ler_sum => /= b. by apply/norm_sum/summable_cond. qed. @@ -1073,7 +1073,7 @@ exists (sum S) => J uqJ. pose G y x := fa x * (F x y * fb y). have ge0_G: forall x y, 0%r <= G y x. - by move=> x y; rewrite mulr_ge0 1?ge0_fa mulr_ge0 (ge0_fb, ge0_F). rewrite (@BRA.eq_bigr _ _ (fun x => sum (fun y => G y x))) /=. -- move=> x _ @/G; rewrite ger0_norm. +- move=> x @/G; rewrite ger0_norm. - apply: mulr_ge0; [exact/ge0_fa | apply: ge0_sum => y /=]. by apply: mulr_ge0; [exact/ge0_F | exact/ge0_fb]. by rewrite -sumZ /= &(eq_sum) => y /=. @@ -1085,7 +1085,7 @@ apply: ler_sum_pos => /= [y|]; [split | exact/smb]. move=> _ @/S @/G; case: (fb y = 0%r) => [-> /= | nz_fb_y]. - by rewrite BRA.big1_eq. rewrite -sumZr -(@BRA.eq_bigr _ (fun x => (fa x * F x y) * fb y)) /=. -- by move=> x _; ring. +- by move=> x; ring. rewrite -BRA.mulr_suml sumZr &(ler_wpmul2r) 1:&ge0_fb. apply: ler_big_sum => //=. - by move=> x; apply: mulr_ge0; [exact/ge0_fa | exact/ge0_F]. diff --git a/theories/crypto/PRP.eca b/theories/crypto/PRP.eca index e2dc9d289f..9c3355ef2e 100644 --- a/theories/crypto/PRP.eca +++ b/theories/crypto/PRP.eca @@ -474,7 +474,7 @@ section Upto. by move=> &hr x_notin_m r_in_rng_m; apply excepted_lossless; exists x{hr}. move=> &1; conseq (_: collision PRFi.m ==> collision PRFi.m: =1%r)=> //=. proc; if; auto=> />; rewrite dD_ll //=. - move=> &0 x x' x'_neq_x x_in_m x'_in_m x_coll_x' x0_notin_m v _ _. + move=> &0 x x' x'_neq_x x_in_m x'_in_m x_coll_x' x0_notin_m v _. by exists x x'=> />; rewrite !mem_set x_in_m x'_in_m /= !get_set_neqE 1,2:/#. inline *; auto=> />; split=> [|_]. + by rewrite no_collision=> x x'; rewrite mem_empty. diff --git a/theories/crypto/RndExcept.eca b/theories/crypto/RndExcept.eca index e33034133d..56ac553c12 100644 --- a/theories/crypto/RndExcept.eca +++ b/theories/crypto/RndExcept.eca @@ -283,7 +283,7 @@ abstract theory AdversaryN. rnd;auto => &hr /> ??? Hs. apply (ler_trans (BRA.big predT (fun (x : t) => 1%r/n%r) X{hr})). + apply (ler_trans _ _ _ (mu_mem_le (d i{hr}) X{hr})). - by apply ler_sum_seq => /= ???;rewrite d_uni. + by apply ler_sum_seq => /= ??;rewrite d_uni. rewrite BRA.sumr_const RField.intmulr count_predT. by have /# : 0%r < inv n%r; apply invr_gt0; rewrite lt_fromint n_pos. + move=> c;proc;sp;inline *. diff --git a/theories/distributions/DList.ec b/theories/distributions/DList.ec index da0ba6d614..78e53bc8a8 100644 --- a/theories/distributions/DList.ec +++ b/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 : @@ -273,9 +273,9 @@ rewrite -big_filter (eq_big_perm _ _ _ (elems I ++ elems J)) ?big_cat. + rewrite cat_uniq !uniq_elems => />; apply/hasPn; smt(). + by rewrite mem_filter mem_range mem_cat -!memE in_fsetU /#. rewrite big_seq_cond (eq_bigr _ _ (fun _ => mu d p)) -?big_seq_cond. - move => i; rewrite /= /q -memE => -[iI _]; apply mu_eq => /#. + move => i; rewrite /= /q -memE => iI; apply mu_eq => /#. rewrite mulr_const big_seq_cond (eq_bigr _ _ (fun _ => mu d (predC p))) -?big_seq_cond. - move => i; rewrite /= /q -memE => -[iI _]; apply mu_eq => /#. + move => i; rewrite /= /q -memE => iI; apply mu_eq => /#. by rewrite mulr_const /card. qed. diff --git a/theories/distributions/Distr.ec b/theories/distributions/Distr.ec index f4c8ddf94e..2633d8ee74 100644 --- a/theories/distributions/Distr.ec +++ b/theories/distributions/Distr.ec @@ -133,7 +133,7 @@ hint exact : ge0_mu. lemma summable_mu1 ['a] (d : 'a distr) : summable (mu1 d). proof. exists 1%r=> s eq_s; rewrite (@eq_bigr _ _ (mu1 d)) => /=. - by move=> i _; rewrite ger0_norm //. + by move=> i; rewrite ger0_norm //. by apply/le1_mu1_fin. qed. @@ -154,7 +154,7 @@ lemma le1_mu (d : 'a distr) p : mu d p <= 1%r. proof. rewrite muE &(lerfin_sum) 1:&(summable_mu1_cond) => J uqJ. apply: (@ler_trans (big predT (mu1 d) J)). -+ by apply: ler_sum => /= a _; case: (p a). ++ by apply: ler_sum => /= a; case: (p a). + by apply: le1_mu1_fin. qed. @@ -707,7 +707,7 @@ rewrite BIA.big_cat IntID.addrC BIA.big_seq BIA.big1 /=. by rewrite -count_eq0 has_pred1. have /BIA.eq_big_perm <- := perm_filterC (mem J) (undup s). rewrite BIA.big_cat ler_paddr ?sumr_ge0 /=. -+ by move=> x _; rewrite count_ge0. ++ by move=> x; rewrite count_ge0. rewrite lerr_eq &(BIA.eq_big_perm) uniq_perm_eq //. + by rewrite filter_uniq. + by rewrite filter_uniq undup_uniq. @@ -1457,7 +1457,7 @@ rewrite -ler_pdivl_mull // mulr1 => le; move: (le_k_Vm). have gt0_Vm := ltr_le_trans _ _ _ lt0_k le_k_Vm. rewrite -ler_pinv 1?gtr_eqF // invrK => h; apply/(ler_trans _ _ h). apply/(ler_trans _ _ le) => {h le}; apply/lerr_eq. -by rewrite undup_id //; apply/eq_bigr=> /= x _; rewrite muK. +by rewrite undup_id //; apply/eq_bigr=> /= x; rewrite muK. qed. op dscalar (k : real) (d : 'a distr) = mk (mscalar k (mu1 d)). @@ -1487,7 +1487,7 @@ apply/eq_distr=> a; rewrite muK; last by rewrite /mscalar !dnull1E. split => /=. - by move=> {a}a @/mscalar; rewrite dnull1E. - move=> s _; rewrite (@BRA.eq_bigr _ _ (fun _ => 0%r)). - - by move=> a' /= _ @/mscalar; rewrite dnull1E. + - by move=> a' /= @/mscalar; rewrite dnull1E. - by rewrite Bigreal.sumr_const. qed. @@ -1630,7 +1630,7 @@ lemma isdistr_mrestrict ['a] d p : isdistr (mrestrict<:'a> d p). proof. split. + by move=> a; rewrite /mrestrict; case: (p a). + move=> J uqJ @/mrestrict; have h := le1_mu1_fin d _ uqJ. - by apply/(ler_trans _ _ h)/ler_sum=> /= a _; case: (p a). + by apply/(ler_trans _ _ h)/ler_sum=> /= a; case: (p a). qed. lemma drestrict1E ['a] d p x : @@ -1776,7 +1776,7 @@ rewrite (@partition_big ofst _ predT _ _ (undup (unzip1 s))). + by case=> a b ab_in_s _; rewrite mem_undup map_f. pose P := fun x ab => ofst<:'a, 'b> ab = x. pose F := fun (ab : 'a * 'b) => mb ab.`2. -rewrite -(@eq_bigr _ (fun x => ma x * big (P x) F s)) => /= [x _|]. +rewrite -(@eq_bigr _ (fun x => ma x * big (P x) F s)) => /= [x|]. + by rewrite mulr_sumr; apply/eq_bigr=> -[a b] /= @/P <-. pose s' := undup _; apply/(@ler_trans (big predT (fun x => ma x) s')). + apply/ler_sum=> a _ /=; apply/ler_pimulr; first by apply/ge0_isdistr. @@ -2215,7 +2215,7 @@ lemma djoin_fu (ds : 'a distr list) (xs : 'a list): proof. move=> eq_sz hfu; rewrite supportP djoin1E eq_sz /=. rewrite RealOrder.gtr_eqF // Bigreal.prodr_gt0_seq. -case=> d x /= /mem_zip [d_ds x_xs] _. +case=> d x /= /mem_zip [d_ds x_xs]. by rewrite -/(_ \in _) supportP -supportPn /=; apply: hfu. qed. @@ -2605,7 +2605,7 @@ lemma dfun_prod1E ['u 'v] (df : t -> 'u distr) (dg : t -> 'v distr) f g : proof. pose F x := mu1 (df x) (f x) * mu1 (dg x) (g x). rewrite dfun1E /= -(@BRM.eq_bigr _ F) //= /F => {F}. -- by move=> x _; rewrite dprod1E. +- by move=> x; rewrite dprod1E. - by rewrite BRM.big_split -!dfun1E. qed. @@ -2668,10 +2668,10 @@ pose p (x : t) := mu1 (dX x) true * mu1 (dt x) (f x) + mu1 (dX x) false * mu1 (df x) (f x). rewrite dfun1E /= -(@BRM.eq_bigr _ p) //=. -- by move=> x _; rewrite dletE_bool. +- by move=> x; rewrite dletE_bool. rewrite dlet1E prodrDl2; first by apply: FinT.is_finite_for. apply: eq_sum => X /=; rewrite !dfun1E -BRM.big_split /=. -by apply: BRM.eq_bigr => /= x _; case: (X x). +by apply: BRM.eq_bigr => /= x; case: (X x). qed. lemma dfun_dcondE ['u] (dX : t -> bool distr) (dt df : t -> 'u distr) : @@ -2928,7 +2928,7 @@ qed. lemma hasEC (d : 'a distr) (c : real) : hasE d (fun _ => c). proof. exists `|c| => J uqJ; pose f := fun i => `|c| * mu1 d i. -rewrite -(@eq_bigr _ f) /= => [i _|]. +rewrite -(@eq_bigr _ f) /= => [i|]. + by rewrite normrM (@ger0_norm (mu1 _ _)). rewrite /f -mulr_sumr ler_pimulr 1:normr_ge0. by apply/(@le1_mu1_fin d). @@ -3133,7 +3133,7 @@ rewrite (@sum_swap (fun ab : _ * _ => s ab.`1 ab.`2)). - apply: uniq_perm_eq; 1,2: by apply/undup_uniq. by move=> x @/K; rewrite !mem_undup -map_comp -(@eq_map snd). move/BRA.eq_big_perm=> ->; apply: Bigreal.ler_sum => /=. - move=> b _ @/s => {s}; pose s a := `|f b| * (mu1 (df a) b * mu1 d a). + move=> b @/s => {s}; pose s a := `|f b| * (mu1 (df a) b * mu1 d a). rewrite BRA.big_filter -(@BRA.eq_bigr _ (fun ba : _ * _ => s ba.`2)) /=. - case=> b' a' /= ->> @/pswap /= @/s. by rewrite -!mulrA !normrM; congr; rewrite !ger0_norm. @@ -3160,7 +3160,7 @@ rewrite (@sum_swap (fun ab : _ * _ => s ab.`1 ab.`2)). rewrite -psum_sum; 1: by apply: eq_summable sm_s => /= a; rewrite /s mulrC. apply: (ler_trans _ _ (ler_big_psum _ uqJ)) => //=; last first. - by apply: eq_summable sm_s => /= a @/s; rewrite mulrC. - apply/lerr_eq/BRA.eq_bigr=> /= a _ @/s. + apply/lerr_eq/BRA.eq_bigr=> /= a @/s. by rewrite normrM !ger0_norm // mulrC. apply: eq_sum=> /= b @/s; rewrite dlet1E -sumZ /=. by apply: eq_sum=> /= a; rewrite mulrAC mulrA. diff --git a/theories/prelude/Logic.ec b/theories/prelude/Logic.ec index c4b133b7ff..3399b3ac9e 100644 --- a/theories/prelude/Logic.ec +++ b/theories/prelude/Logic.ec @@ -53,7 +53,7 @@ op unwrap (w : 'a wrapped) = with w = Wrap x => x. (* -------------------------------------------------------------------- *) -op idfun ['a] (x:'a) = x. +op idfun ['a] (x:'a) / = x. (* -------------------------------------------------------------------- *) pred (== ) (f g : 'a -> 'b) = forall x, f x = g x. @@ -98,11 +98,10 @@ op [opaque] eta_ (f : 'a -> 'b) = fun x => f x. lemma etaE (f : 'a -> 'b): eta_ f = fun x => f x by rewrite/eta_. (* -------------------------------------------------------------------- *) -op (\o) ['a 'b 'c] (g : 'b -> 'c) (f : 'a -> 'b) = - fun x => g (f x). +op (\o) ['a 'b 'c] (g : 'b -> 'c) (f : 'a -> 'b) (x : 'a) / = g (f x). -op (\o2) ['a 'b 'c 'd] (f : 'c -> 'd) (g : 'a -> 'b -> 'c) = - fun a b => f (g a b). +op (\o2) ['a 'b 'c 'd] (f : 'c -> 'd) (g : 'a -> 'b -> 'c) (a : 'a) (b : 'b) / = + f (g a b). (* -------------------------------------------------------------------- *) pred morphism_1 (f : 'a -> 'b) aF rF = @@ -242,26 +241,26 @@ lemma bij_pswap ['a 'b] : bijective pswap<:'a, 'b>. proof. by exists pswap; rewrite !pswapK. qed. (* -------------------------------------------------------------------- *) -op pred0 ['a] = fun (x : 'a) => false. -op predT ['a] = fun (x : 'a) => true. +op pred0 ['a] (x : 'a) / = false. +op predT ['a] (x : 'a) / = true. op predI ['a] = fun (p1 p2 : 'a -> bool) x => p1 x /\ p2 x. op predU ['a] = fun (p1 p2 : 'a -> bool) x => p1 x \/ p2 x. -op predC ['a] = fun (p : 'a -> bool) x => ! (p x). +op predC ['a] (p : 'a -> bool) x / = ! (p x). op predD ['a] = fun (p1 p2 : 'a -> bool) x => !p2 x /\ p1 x. -op pred1 ['a] = fun (c x : 'a) => x = c. +op pred1 ['a] (c x : 'a) / = x = c. op predU1 ['a] = fun (c : 'a) (p : 'a -> bool) (x : 'a) => x = c \/ p x. -op predC1 ['a] = fun (c : 'a) (x : 'a) => x <> c. +op predC1 ['a] (c : 'a) (x : 'a) / = x <> c. op predD1 ['a] = fun (p : 'a -> bool) (c : 'a) (x : 'a) => x <> c /\ p x. (* -------------------------------------------------------------------- *) type 'a rel = 'a -> 'a -> bool. -op rel0 ['a 'b] = fun (x : 'a) (y : 'b) => false. -op relT ['a 'b] = fun (x : 'a) (y : 'b) => true. +op rel0 ['a 'b] (x : 'a) (y : 'b) / = false. +op relT ['a 'b] (x : 'a) (y : 'b) / = true. op relI ['a 'b] = fun (p1 p2 : 'a -> 'b -> bool) a b => p1 a b /\ p2 a b. op relU ['a 'b] = fun (p1 p2 : 'a -> 'b -> bool) a b => p1 a b \/ p2 a b. -op relC ['a 'b] = fun (p : 'a -> 'b -> bool) a b => ! (p a b). +op relC ['a 'b] (p : 'a -> 'b -> bool) a b / = ! (p a b). op relD ['a 'b] = fun (p1 p2 : 'a -> 'b -> bool) a b => !p2 a b /\ p1 a b. op rel1 ['a 'b] = fun (ca : 'a) (cb : 'b) a b => ca = a /\ cb = b. @@ -513,18 +512,18 @@ by smt(). (* -------------------------------------------------------------------- *) lemma addFb : left_id false (^) by []. lemma addbF : right_id false (^) by []. -lemma addbb : self_inverse false (^) by smt(). -lemma addbC : commutative (^) by smt(). -lemma addbA : associative (^) by smt(). -lemma addbCA : left_commutative (^) by smt(). -lemma addbAC : right_commutative (^) by smt(). -lemma addbACA : interchange (^) (^) by smt(). -lemma andb_addl : left_distributive (/\) (^) by smt(). -lemma andb_addr : right_distributive (/\) (^) by smt(). -lemma addKb : left_loop idfun (^) by smt(). -lemma addbK : right_loop idfun (^) by smt(). -lemma addIb : left_injective (^) by smt(). -lemma addbI : right_injective (^) by smt(). +lemma addbb : self_inverse false (^) by case. +lemma addbC : commutative (^) by case. +lemma addbA : associative (^) by case; case. +lemma addbCA : left_commutative (^) by case; case. +lemma addbAC : right_commutative (^) by case; case. +lemma addbACA : interchange (^) (^) by case; case; case. +lemma andb_addl : left_distributive (/\) (^) by case; case; case. +lemma andb_addr : right_distributive (/\) (^) by case; case; case. +lemma addKb : left_loop idfun (^) by case. +lemma addbK : right_loop idfun (^) by case. +lemma addIb : left_injective (^) by case; case; case. +lemma addbI : right_injective (^) by case; case; case. lemma addTb b : true ^ b <=> !b by []. lemma addbT b : b ^ true <=> !b by [].