More results on lists (take/drop) and bit-encoding (bs2int/chunk)

Author: strub

theories/datatypes/BitEncoding.ec

@@ -235,7 +235,6 @@ proof.
   by rewrite addrAC.
 qed.
 
-(*-----------------------------------------------------------------------------*)
 lemma bs2int_cat s1 s2 :
   bs2int (s1 ++ s2) = bs2int s1 + (2 ^ (size s1)) * bs2int s2.
 proof.
@@ -244,6 +243,47 @@ proof.
   by rewrite exprD_nneg ?size_ge0.
 qed.
 
+lemma bs2intD (s1 s2 : bool list) (i : int) :
+  i = size s1 => bs2int s1 + (2 ^ i) * bs2int s2 = bs2int (s1 ++ s2).
+proof. by move=> ->; apply/eq_sym/bs2int_cat. qed.
+
+lemma bs2int_take_drop (i : int)  (s : bool list) :
+  0 <= i => bs2int s = bs2int (take i s) + 2 ^ i * bs2int (drop i s).
+proof.
+move=> ge0_i; case: (i < size s); last first.
+- move=> /lezNgt lei; rewrite drop_oversize //.
+  by rewrite bs2int_nil /= take_oversize.
+move=> ltis; rewrite -{1}[s](@cat_take_drop i) bs2int_cat.
+by rewrite size_take 1?ltis.
+qed.
+
+lemma bs2int_div (i : int) (s : bool list) :
+  0 <= i => bs2int s %/ 2^i = bs2int (drop i s).
+proof.
+move=> ge0_i; rewrite (@bs2int_take_drop i) //.
+rewrite mulrC divzMDr 1:expf_eq0 // pdiv_small //.
+rewrite bs2int_ge0 /= &(ltr_le_trans (2 ^ (size (take i s)))).
+- by apply/bs2int_le2Xs.
+- by rewrite &(ler_weexpn2l) //= size_ge0 /= &(size_take_le).
+qed.
+
+lemma bs2int_mod (s : bool list) (i : int) :
+  0 <= i => bs2int s %% 2^i = bs2int (take i s).
+proof.
+move=> ge0_i; rewrite (@bs2int_take_drop i) //.
+rewrite mulrC modzMDr pmod_small // bs2int_ge0 /=.
+apply/(ltr_le_trans (2 ^ (size (take i s)))).
+- by apply/bs2int_le2Xs.
+- by rewrite &(ler_weexpn2l) //= size_ge0 /= &(size_take_le).
+qed.
+
+lemma inj_bs2int_eqsize (s1 s2 : bool list) :
+  size s1 = size s2 => bs2int s1 = bs2int s2 => s1 = s2.
+proof.
+elim: s1 s2 => [|x1 s1 ih] [|x2 s2] //=; ~-1:smt(size_ge0).
+by move/addzI => eq_sz /=; rewrite !bs2int_cons /#.
+qed.
+
 lemma bs2int_range s :
   bs2int s \in range 0 (2 ^ size s).
 proof. by apply/mem_range; split; [apply bs2int_ge0|move => _; apply bs2int_le2Xs]. qed.
@@ -276,7 +316,6 @@ proof. by rewrite bs2int_cat bs2int_nseq_false size_nseq. qed.
 lemma bs2int_pow2 K N :
   bs2int (nseq K false ++ true :: nseq N false) = 2 ^ max 0 K.
 proof. by rewrite bs2int_mulr_pow2 bs2int1. qed.
-
 end BS2Int.
 
 
@@ -611,6 +650,14 @@ rewrite ler_maxr 1:subr_ge0 1:-subr_ge0 1:(ler_trans r) ?ge0_r //.
 by move/ler_eqVlt: ler=> [<-|->].
 qed.
 
+lemma size_nth_chunk ['a] (x0 : 'a list) (s : 'a list) (i n : int) :
+  0 <= n => 0 <= i < (size s) %/ n => size (nth x0 (chunk n s) i) = n.
+proof.
+move/lez_eqVlt => [<<- //|]; first by rewrite divz0 /#.
+move=> gt0_n rgi; apply: (@in_chunk_size n s) => //.
+by rewrite mem_nth size_chunk.
+qed.
+
 lemma size_flatten_chunk r (bs : 'a list) : 0 < r =>
   size (flatten (chunk r bs)) = (size bs) %/ r * r.
 proof.
@@ -669,4 +716,30 @@ rewrite size_drop ?mulr_ge0 // 1:ltrW // szxs -mulrBl.
 rewrite ler_maxr ?mulr_ge0 1,2:ltrW ?subr_gt0 ?ler_pmull //.
 by rewrite ler_subr_addl -ltzE.
 qed.
+
+lemma inj_chunk ['a] (n : int) (s1 s2 : 'a list) :
+  0 < n => n %| size s1 => n %| size s2 => chunk n s1 = chunk n s2 => s1 = s2.
+proof.
+move=> gt0_n dvd1 dvd2 ^ /(congr1 List.size).
+rewrite !size_chunk //; move: dvd1 dvd2.
+move=> /dvdzP[q] ^sz1E -> /dvdzP[q'] ^sz2E ->.
+rewrite !mulzK ~-1:gtr_eqF // => <<- @/chunk.
+rewrite sz1E sz2E mulzK 1:gtr_eqF //.
+elim/natind: q s1 s2 sz1E sz2E => [q ge0_q|q ge0_q ih] /=.
+- smt(size_ge0 size_eq0).
+move=> s1 s2; rewrite mulzDl /= [_ + n]addrC => szE1 szE2.
+have := size_eqD _ _ _ _ _ szE1; ~-1: move=> //#.
+have := size_eqD _ _ _ _ _ szE2; ~-1: move=> //#.
+case=> [s1a s1b] [# sz1a sz1b ->] [s2a s2b] [# sz2a sz2b ->].
+rewrite !mkseqSr /(\o) //= !drop0 !take_catl ?(sz1a, sz2a) //.
+rewrite !take_oversize ?(sz1a, sz2a) // => -[<-].
+move=> eq_tl; congr; apply: ih => //.
+apply: (eq_trans _ _ (eq_trans _ eq_tl _)).
+- apply: eq_in_mkseq => i rgi /=; rewrite mulzDr /=.
+  rewrite [n+_]addrC -drop_drop ~-1://#.
+  by rewrite drop_catr ?sz2a //= drop0.
+- apply: eq_in_mkseq => i rgi /=; rewrite mulzDr /=.
+  rewrite [n+_]addrC -drop_drop ~-1://#.
+  by rewrite drop_catr ?sz2a //= drop0.
+qed.
 end BitChunking.

theories/datatypes/List.ec

@@ -827,6 +827,14 @@ rewrite drop_cat lez_eqVlt; case: (n = size s1) => [->|] //=.
 by rewrite drop0 drop_size.
 qed.
 
+lemma drop_catl ['a] (s1 s2 : 'a list) (i : int) :
+  i <= size s1 => drop i (s1 ++ s2) = drop i s1 ++ s2.
+proof. by move=> ?; rewrite drop_cat_le iftrue. qed.
+
+lemma drop_catr ['a] (s1 s2 : 'a list) (i : int) :
+  size s1 <= i => drop i (s1 ++ s2) = drop (i - size s1) s2.
+proof. by move=> ?; rewrite drop_cat iffalse // ltzNge. qed.
+
 lemma drop_size_cat n (s1 s2 : 'a list):
   size s1 = n => drop n (s1 ++ s2) = s2.
 proof. by move=> <-; rewrite drop_cat subzz ltzz drop0. qed.
@@ -902,6 +910,14 @@ rewrite take_cat lez_eqVlt; case: (n = size s1) => [->|] //=.
 by rewrite take0 take_size cats0.
 qed.
 
+lemma take_catl ['a] (s1 s2 : 'a list) (i : int) :
+  i <= size s1 => take i (s1 ++ s2) = take i s1.
+proof. by move=> ?; rewrite take_cat_le iftrue. qed.
+
+lemma take_catr ['a] (s1 s2 : 'a list) (i : int) :
+  size s1 <= i => take i (s1 ++ s2) = s1 ++ take (i - size s1) s2.
+proof. by move=> ?; rewrite take_cat iffalse // ltzNge. qed.
+
 lemma take_size_cat n (s1 s2 : 'a list):
   size s1 = n => take n (s1 ++ s2) = s1.
 proof. by move=> <-; rewrite take_cat subzz ltzz take0 cats0. qed.
@@ -916,6 +932,37 @@ qed.
 lemma cat_take_drop n (s : 'a list): take n s ++ drop n s = s.
 proof. by elim: s n=> /#. qed.
 
+lemma takeD ['a] (s : 'a list) (i j : int) :
+  0 <= i => 0 <= j => take (i + j) s = take i s ++ take j (drop i s).
+proof.
+move=> ge0_i ge0_j; case: (size s <= i) => [sz_le|/ltzNge sz_lt].
+- by rewrite drop_oversize //= cats0 !take_oversize //#.
+rewrite -{1}[s](cat_take_drop i) take_cat.
+by rewrite size_take // sz_lt /= iffalse 1:/# addrAC.
+qed.
+
+lemma size_eqD ['a] (m n : int) (s : 'a list) :
+  0 <= m => 0 <= n => size s = m + n =>
+    exists s1 s2, (size s1 = m /\ size s2 = n) /\ s = s1 ++ s2.
+proof.
+move=> ge0_m ge0_n szs; exists (take m s) (drop m s).
+by rewrite cat_take_drop /= !(size_take, size_drop) //#.
+qed.
+
+lemma drop_take ['a] (s : 'a list) (i j : int) :
+  0 <= i => 0 <= j => drop i (take j s) = take (j-i) (drop i s).
+proof.
+move=> ge0_i ge0_j; case: (j < i) => [lt_ji|/lezNgt le_ij].
+- rewrite (take_le0 (j-i)) 1:/# drop_oversize //.
+  by apply/(lez_trans j)/ltzW => //; apply/size_take_le.
+case: (i < size s) => [lti|]; last first.
+- move=> /lezNgt lei; rewrite !drop_oversize //=.
+  by rewrite &(lez_trans _ _ _ _ lei) size_take //#.
+rewrite {1}(_ : j = i + (j - i)) 1:addzCA //.
+rewrite takeD ~-1://# drop_catr // 1:&(size_take_le) //.
+by rewrite drop_le0 // size_take // lti.
+qed.
+
 lemma mem_drop n (s:'a list) x: mem (drop n s) x => mem s x.
 proof. by rewrite -{2}[s](cat_take_drop n) mem_cat=>->. qed.
 
@@ -951,6 +998,14 @@ move=> i [ge0_i lti]; rewrite nth_cat size_take //= lt_n_s /=.
 smt(nth_take nth_drop).
 qed.
 
+lemma drop_take1_nth ['a] (x0 : 'a) (s : 'a list) (i : int) :
+  0 <= i < size s => take 1 (drop i s) = [nth x0 s i].
+proof.
+move=> [ge0_i lti]; rewrite -{1}[s](cat_take_insert_drop x0 i) //.
+rewrite drop_cat_le size_take // lti /=.
+by rewrite drop_oversize 1:size_take // 1:lti //= take0.
+qed.
+
 lemma splitPr (xs : 'a list) (x : 'a): mem xs x =>
   exists s1, exists s2, xs = s1 ++ x :: s2.
 proof.
@@ -2548,9 +2603,14 @@ lemma mkseqS f n : 0 <= n =>
   mkseq<:'a> f (n + 1) = rcons (mkseq f n) (f n).
 proof. by move=> ge0_n; rewrite /mkseq iotaSr //= map_rcons. qed.
 
-lemma mkseqSr ['a] (f : int -> 'a) n : 0 <= n => mkseq f (n + 1) = f 0 :: mkseq (f \o ((+)%Int 1)) n.
+lemma mkseqSr ['a] (f : int -> 'a) n : 0 <= n =>
+  mkseq f (n + 1) = f 0 :: mkseq (f \o ((+)%Int 1)) n.
 proof. by move => le0n; rewrite /mkseq iotaS //= map_comp -iota_addl. qed.
 
+lemma mkseqSr_minus ['a] (f : int -> 'a) (n : int) :
+  0 < n => mkseq f n = f 0 :: mkseq (f \o (+) 1) (n - 1).
+proof. by move=> gt0_n; rewrite (mkseqSr _ (n-1)) //#. qed.
+
 lemma mkseq_add (f : int -> 'a) n m : 0 <= n => 0 <= m =>
   mkseq f (n+m) = mkseq f n ++ mkseq (fun i => f (n+i)) m.
 proof.
@@ -2801,6 +2861,9 @@ proof.
   by rewrite !flatten_cons ih catA.
 qed.
 
+lemma flatten1 ['a] (x : 'a list) : flatten [x] = x.
+proof. by rewrite flatten_cons flatten_nil cats0. qed.
+
 lemma flatten_rcons (s : 'a list list) (x : 'a list)  :
   flatten (rcons s x) = flatten s ++ x.
 proof. by rewrite -cats1 flatten_cat flatten_seq1. qed.
@@ -2929,6 +2992,46 @@ rewrite (_ : max 0 k = k) 1:/#  //; elim: k ge0_k => [|k ge0_k ih].
 by rewrite nseqS // flatten_cons count_cat /#.
 qed.
 
+lemma size_flatten_ctt ['a] (n : int) (s : 'a list list) :
+     (forall x, x \in s => size x = n)
+  => size (flatten s) = n * (size s).
+proof.
+move=> sz_s; rewrite size_flatten (iffLR _ _ (eq_in_map _ (fun _ => n) _)) //.
+by elim: {sz_s} s => //= s @/sumz /= ->; rewrite mulzDr.
+qed.
+
+lemma drop_flatten_ctt ['a] (m n : int) (s : 'a list list) :
+     (forall x, x \in s => size x = m)
+  => drop (m * n) (flatten s) = flatten (drop n s).
+proof.
+move=> hsz; case: (m < 0) => [lt0_m|/lezNgt ge0_m].
+- have ->>//: s = []; apply: contraLR lt0_m.
+  case: s hsz => // x s /(_ x _) // <- _.
+  by rewrite ltzNge /= size_ge0.
+elim/natind: n s hsz => [n le0_n|n ge0_n ih] s hsz.
+- by rewrite !drop_le0 //#.
+rewrite mulzDr /=; case: s hsz => // x s hsz.
+rewrite flatten_cons drop_cat hsz // iffalse 1:/#.
+rewrite -addrA /=  iffalse 1:/# &(ih) => ??.
+by apply: hsz => /=; right.
+qed.
+
+lemma take_flatten_ctt ['a] (m n : int) (s : 'a list list) :
+     (forall x, x \in s => size x = m)
+  => take (m * n) (flatten s) = flatten (take n s).
+proof.
+move=> hsz; case: (m < 0) => [lt0_m|/lezNgt ge0_m].
+- have ->>//: s = []; apply: contraLR lt0_m.
+  case: s hsz => // x s /(_ x _) // <- _.
+  by rewrite ltzNge /= size_ge0.
+elim/natind: n s hsz => [n le0_n|n ge0_n ih] s hsz.
+- by rewrite !take_le0 //#.
+rewrite mulzDr /=; case: s hsz => // x s hsz.
+rewrite flatten_cons take_cat hsz // iffalse 1:/#.
+rewrite -addrA /=  iffalse 1:/# ih // => ??.
+by apply: hsz => /=; right.
+qed.
+
 lemma perm_eq_pair ['a 'b] (s : ('a * 'b) list) : uniq s => perm_eq s
   (flatten
      (map (fun a => filter (fun xy : _ * _ => xy.`1 = a) s)