Library seq

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

The seq type is the ssreflect type for sequences; it is identical to the   
 standard Coq list type, but supports a larger set of operations, as well   
 as eqType and predType (and, later, choiceType) structures. The operations 
 are geared towards reflection, e.g., they generally expect and provide     
 boolean predicates, e.g., the membership predicate expects an eqType. To   
 avoid any confusion we do not Import the Coq List module, which forces us  
 to define our own Type since list is not defined in the pervasives.        
   As there is no true subtyping in Coq, we don't use a type for non-empty  
 sequences; rather, we pass explicitly the head and tail of the sequence.   
   The empty sequence is especially bothersome for subscripting, since it   
 forces us to pass a default value. This default value can often be hidden  
 by a notation.                                                             
   Here is the list of seq operations:                                      
constructors:

                        seq T == the type of sequences with items of type T 
                       bitseq == seq bool                                   
             [::], nil, Nil T == the empty sequence (of type T)             
 x :: s, cons x s, Cons T x s == the sequence x followed by s (of type T)   
                       [:: x] == the singleton sequence                     
           [:: x_0; ...; x_n] == the explicit sequence of the x_i           
       [:: x_0, ..., x_n & s] == the sequence of the x_i, followed by s     
                    rcons s x == the sequence s, followed by x              
  All of the above, except rcons, can be used in patterns. We define a view 
 lastP and and induction principle last_ind that can be used to decompose   
 or traverse a sequence in a right to left order. The view lemma lastP has  
 a dependent family type, so the ssreflect tactic case/lastP: p => [|p' x]  
 will generate two subgoals in which p has been replaced by [::] and by     
 rcons p' x, respectively.                                                  
factories:

             nseq n x == a sequence of n x's                                
          ncons n x s == a sequence of n x's, followed by s                 
 seqn n x_0 ... x_n-1 == the sequence of the x_i (can be partially applied) 
             iota m n == the sequence m, m + 1, ..., m + n - 1              
            mkseq f n == the sequence f 0, f 1, ..., f (n - 1)              
sequential access:

      head x0 s == the head (zero'th item) of s if s is non-empty, else x0  
        ohead s == None if s is empty, else Some x where x is the head of s 
       behead s == s minus its head, i.e., s' if s = x :: s', else [::]     
       last x s == the last element of x :: s (which is non-empty)          
     belast x s == x :: s minus its last item                               
dimensions:

         size s == the number of items (length) in s                        
       shape ss == the sequence of sizes of the items of the sequence of    
                   sequences ss                                             
random access:

         nth x0 s i == the item i of s (numbered from 0), or x0 if s does   
                       not have at least i+1 items (i.e., size x <= i)      
               s`_i == standard notation for nth x0 s i for a default x0,   
                       e.g., 0 for rings.                                   
   set_nth x0 s i y == s where item i has been changed to y; if s does not  
                       have an item i it is first padded with copieds of x0 
                       to size i+1.                                         
       incr_nth s i == the nat sequence s with item i incremented (s is     
                       first padded with 0's to size i+1, if needed).       
predicates:

         x \in s == x appears in s (this requires an eqType for T)          
       index x s == the first index at which x appears in s, or size s if   
                    x \notin s                                              
         has p s == the (applicative, boolean) predicate p holds for some   
                    item in s                                               
         all p s == p holds for all items in s                              
        find p s == the number of items of s for which p holds              
      constant s == all items in s are identical (trivial if s = [::])      
          uniq s == all the items in s are pairwise different               
   perm_eq s1 s2 == s2 is a permutation of s1, i.e., s1 and s2 have the     
                    items (with the same repetitions), but possibly in a    
                    different order.                                        
  perm_eql s1 s2 <-> s1 and s2 behave identically on the left of perm_eq    
  perm_eqr s1 s2 <-> s1 and s2 behave identically on the rightt of perm_eq  
    These left/right transitive versions of perm_eq make it easier to chain 
 a sequence of equivalences.                                                
filtering:

           filter p s == the subsequence of s consisting of all the items   
                         for which the (boolean) predicate p holds          
 subfilter s : seq sT == when sT has a subType p structure, the sequence    
                         of items of type sT corresponding to items of s    
                         for which p holds                                  
              undup s == the subsequence of s containing only the first     
                         occurrence of each item in s, i.e., s with all     
                         duplicates removed.                                
             mask m s == the subsequence of s selected by m : bitseq, with  
                         item i of s selected by bit i in m (extra items or 
                         bits are ignored.                                  
surgery:

 s1 ++ s2, cat s1 s2 == the concatenation of s1 and s2                      
            take n s == the sequence containing only the first n items of s 
                        (or all of s if size s <= n)                        
            drop n s == s minus its first n items ([::] if size s <= n)     
             rot n s == s rotated left n times (or s if size s <= n)        
                     := drop n s ++ take n s                                
            rotr n s == s rotated right n times (or s if size s <= n)       
               rev s == the (linear time) reversal of s                     
        catrev s2 s1 == the reversal of s1 followed by s2 (this is the      
                        recursive form of rev)                              
iterators: for s == [:: x_0, ..., x_n],

        map f s == the sequence [:: f x_0, ..., f x_n]                      
      pmap pf s == the sequence [:: y_i0, ..., y_ik] where i0 < ... < ik,   
                   pf x_i = Some y_i, and pf x_j = None iff j is not in     
                   {i0, ..., ik}.                                           
   foldr f a s == the right fold of s by f (i.e., the natural iterator)     
               := f x_0 (f x_1 ... (f x_n a))                               
        sumn s == x_0 + (x_1 + ... + (x_n + 0)) (when s : seq nat)          
   foldl f a s == the left fold of s by f                                   
               := f (f ... (f a x_0) ... x_n-1) x_n                         
   scanl f a s == the sequence of partial accumulators of foldl f a s       
               := [:: f a x_0; ...; foldl f a s]                            
 pairmap f a s == the sequence of f applied to consecutie items in a :: s   
               := [:: f a x_0; f x_0 x_1; ...; f x_n-1 x_n]                 
     zip s1 s2 == itemwise pairing of s1 and s2 (dropping any extra items)  
               := [:: (x1_0, x2_0); ...; (x1_n, x2_n)]                      
      unzip1 s == [:: (x_0).1; ...; (x_n).1] when s : seq (T1 * T2)         
      unzip2 s == [:: (x_0).2; ...; (x_n).2] when s : seq (T1 * T2)         
     flatten s == x_0 ++ ... ++ x_n ++ [::] when s : seq (seq T)            
   reshape r s == s reshaped into a sequence of sequences whose sizes are   
                  given by r (trucating if s is too long or too short)      
               := [:: [:: x_0; ...; x_(r0 - 1)];                            
                      [:: x_r0; ...; x_(r0 + r1 - 1)];                      
                      ...;                                                  
                      [:: x_(r0 + ... + r(k-1)); ...; x_(r0 + ... rk - 1)]] 
   We are quite systematic in providing lemmas to rewrite any composition   
 of two operations. "rev", whose simplifications are not natural, is        
 protected with nosimpl.

Import Prenex Implicits.

Delimit Scope seq_scope with SEQ.
Open Scope seq_scope.

Inductive seq (T : Type) : Type := Nil | Cons of T & seq T.
Implicit Arguments Cons [].
Notation nil := (Nil _) (only parsing).
Notation cons := (Cons _).

Notation "x :: s" := (Cons _ x s)
  (at level 60, right associativity, format "x :: s") : seq_scope.

Reserved Notation "s1 ++ s2"
  (at level 60, right associativity, format "s1 ++ s2").

Notation "[ :: ]" := nil (at level 0, format "[ :: ]") : seq_scope.

Notation "[ :: x1 ]" := (x1 :: [::])
  (at level 0, format "[ :: x1 ]") : seq_scope.

Notation "[ :: x & s ]" := (x :: s) (only parsing) : seq_scope.

Notation "[ :: x1 ; x2 ; .. ; xn ]" := (x1 :: x2 :: ..
Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: ..
Section Sequences.

Variable n0 : nat. Variable T : Type. Variable x0 : T.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Type s : (seq T).

Fixpoint size s := if s is _ :: s' then (size s').+1 else 0.

Lemma size0nil : forall s, size s = 0 -> s = [::].

Definition ohead s := if s is x :: _ then Some x else None.
Definition head s := if s is x :: _ then x else x0.

Definition behead s := if s is _ :: s' then s' else [::].

Lemma size_behead : forall s, size (behead s) = (size s).-1.

Factories

Definition ncons n x := iter n (cons x).
Definition nseq n x := ncons n x [::].

Lemma size_ncons : forall n x s, size (ncons n x s) = n + size s.

Lemma size_nseq : forall n x, size (nseq n x) = n.

n-ary, dependently typed constructor.

Fixpoint seqn_type n := if n is n'.+1 then T -> seqn_type n' else seq T.

Fixpoint seqn_rec f n {struct n} : seqn_type n :=
  if n is n'.+1 return seqn_type n then
    fun x => seqn_rec (fun s => f (x :: s)) n'
  else f [::].
Definition seqn := seqn_rec id.

Sequence catenation "cat".

Fixpoint cat s1 s2 {struct s1} := if s1 is x :: s1' then x :: s1' ++ s2 else s2
where "s1 ++ s2" := (cat s1 s2) : seq_scope.

Lemma cat0s : forall s, [::] ++ s = s.

Lemma cat1s : forall x s, [:: x] ++ s = x :: s.

Lemma cat_cons : forall x s1 s2, (x :: s1) ++ s2 = x :: s1 ++ s2.

Lemma cat_nseq : forall n x s, nseq n x ++ s = ncons n x s.

Lemma cats0 : forall s, s ++ [::] = s.

Lemma catA : forall s1 s2 s3, s1 ++ s2 ++ s3 = (s1 ++ s2) ++ s3.

Lemma size_cat : forall s1 s2, size (s1 ++ s2) = size s1 + size s2.

last, belast, rcons, and last induction.

Fixpoint rcons s z {struct s} :=
  if s is x :: s' then x :: rcons s' z else [:: z].

Lemma rcons_cons : forall x s z, rcons (x :: s) z = x :: rcons s z.

Lemma cats1 : forall s z, s ++ [:: z] = rcons s z.

Fixpoint last x s {struct s} := if s is x' :: s' then last x' s' else x.

Fixpoint belast x s {struct s} :=
  if s is x' :: s' then x :: (belast x' s') else [::].

Lemma lastI : forall x s, x :: s = rcons (belast x s) (last x s).

Lemma last_cons : forall x y s, last x (y :: s) = last y s.

Lemma size_rcons : forall s x, size (rcons s x) = (size s).+1.

Lemma size_belast : forall x s, size (belast x s) = size s.

Lemma last_cat : forall x s1 s2, last x (s1 ++ s2) = last (last x s1) s2.

Lemma last_rcons : forall x s z, last x (rcons s z) = z.

Lemma belast_cat : forall x s1 s2,
  belast x (s1 ++ s2) = belast x s1 ++ belast (last x s1) s2.

Lemma belast_rcons : forall x s z, belast x (rcons s z) = x :: s.

Lemma cat_rcons : forall x s1 s2, rcons s1 x ++ s2 = s1 ++ x :: s2.

Lemma rcons_cat : forall x s1 s2,
  rcons (s1 ++ s2) x = s1 ++ rcons s2 x.

CoInductive last_spec : seq T -> Type :=
  | LastNil : last_spec [::]
  | LastRcons s x : last_spec (rcons s x).

Lemma lastP : forall s, last_spec s.

Lemma last_ind : forall P,
  P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s.

Sequence indexing.

Fixpoint nth s n {struct n} :=
  if s is x :: s' then if n is n'.+1 then @nth s' n' else x else x0.

Fixpoint set_nth s n y {struct n} :=
  if s is x :: s' then
    if n is n'.+1 then x :: @set_nth s' n' y else y :: s'
  else ncons n x0 [:: y].

Lemma nth0 : forall s, nth s 0 = head s.

Lemma nth_default : forall s n, size s <= n -> nth s n = x0.

Lemma nth_nil : forall n, nth [::] n = x0.

Lemma last_nth : forall x s, last x s = nth (x :: s) (size s).

Lemma nth_last : forall s, nth s (size s).-1 = last x0 s.

Lemma nth_behead : forall s n, nth (behead s) n = nth s n.+1.

Lemma nth_cat : forall s1 s2 n,
nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1).

Lemma nth_rcons : forall s x n,
  nth (rcons s x) n =
    (if n < size s then nth s n else if n == size s then x else x0).

Lemma nth_ncons : forall m x s n,
  nth (ncons m x s) n = (if n < m then x else nth s (n - m)).

Lemma nth_nseq : forall m x n, nth (nseq m x) n = (if n < m then x else x0).

Lemma eq_from_nth : forall s1 s2, size s1 = size s2 ->
  (forall i, i < size s1 -> nth s1 i = nth s2 i) -> s1 = s2.

Lemma size_set_nth : forall s n y, size (set_nth s n y) = maxn n.+1 (size s).

Lemma set_nth_nil : forall n y, set_nth [::] n y = ncons n x0 [:: y].

Lemma nth_set_nth : forall s n y,
  nth (set_nth s n y) =1 [eta nth s with n |-> y].

Lemma set_set_nth : forall s n1 y1 n2 y2,
  set_nth (set_nth s n1 y1) n2 y2 =
   let s2 := set_nth s n2 y2 in if n1 == n2 then s2 else set_nth s2 n1 y1.

find, count, has, all.

Section SeqFind.

Variable a : pred T.

Fixpoint find s := if s is x :: s' then if a x then 0 else (find s').+1 else 0.

Fixpoint filter s :=
  if s is x :: s' then if a x then x :: filter s' else filter s' else [::].

Fixpoint count s := if s is x :: s' then a x + count s' else 0.

Fixpoint has s := if s is x :: s' then a x || has s' else false.

Fixpoint all s := if s is x :: s' then a x && all s' else true.

Lemma count_filter : forall s, count s = size (filter s).

Lemma has_count : forall s, has s = (0 < count s).

Lemma count_size : forall s, count s <= size s.

Lemma all_count : forall s, all s = (count s == size s).

Lemma all_filterP : forall s, reflect (filter s = s) (all s).

Lemma has_find : forall s, has s = (find s < size s).

Lemma find_size : forall s, find s <= size s.

Lemma find_cat : forall s1 s2,
  find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2.

Lemma has_nil : has [::] = false.

Lemma has_seq1 : forall x, has [:: x] = a x.

Lemma has_seqb : forall (b : bool) x, has (nseq b x) = b && a x.

Lemma all_nil : all [::] = true.

Lemma all_seq1 : forall x, all [:: x] = a x.

Lemma nth_find : forall s, has s -> a (nth s (find s)).

Lemma before_find : forall s i, i < find s -> a (nth s i) = false.

Lemma filter_cat : forall s1 s2, filter (s1 ++ s2) = filter s1 ++ filter s2.

Lemma filter_rcons : forall s x,
  filter (rcons s x) = if a x then rcons (filter s) x else filter s.

Lemma count_cat : forall s1 s2, count (s1 ++ s2) = count s1 + count s2.

Lemma has_cat : forall s1 s2, has (s1 ++ s2) = has s1 || has s2.

Lemma has_rcons : forall s x, has (rcons s x) = a x || has s.

Lemma all_cat : forall s1 s2, all (s1 ++ s2) = all s1 && all s2.

Lemma all_rcons : forall s x, all (rcons s x) = a x && all s.

End SeqFind.

Lemma eq_find : forall a1 a2, a1 =1 a2 -> find a1 =1 find a2.

Lemma eq_filter : forall a1 a2, a1 =1 a2 -> filter a1 =1 filter a2.

Lemma eq_count : forall a1 a2, a1 =1 a2 -> count a1 =1 count a2.

Lemma eq_has : forall a1 a2, a1 =1 a2 -> has a1 =1 has a2.

Lemma eq_all : forall a1 a2, a1 =1 a2 -> all a1 =1 all a2.

Lemma filter_pred0 : forall s, filter pred0 s = [::].

Lemma filter_predT : forall s, filter predT s = s.

Lemma filter_predI : forall a1 a2 s,
  filter (predI a1 a2) s = filter a1 (filter a2 s).

Lemma count_pred0 : forall s, count pred0 s = 0.

Lemma count_predT : forall s, count predT s = size s.

Lemma count_predUI : forall a1 a2 s,
count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.

Lemma count_predC : forall a s, count a s + count (predC a) s = size s.

Lemma has_pred0 : forall s, has pred0 s = false.

Lemma has_predT : forall s, has predT s = (0 < size s).

Lemma has_predC : forall a s, has (predC a) s = ~~ all a s.

Lemma has_predU : forall a1 a2 s, has (predU a1 a2) s = has a1 s || has a2 s.

Lemma all_pred0 : forall s, all pred0 s = (size s == 0).

Lemma all_predT : forall s, all predT s = true.

Lemma all_predC : forall a s, all (predC a) s = ~~ has a s.

Lemma all_predI : forall a1 a2 s, all (predI a1 a2) s = all a1 s && all a2 s.

Surgery: drop, take, rot, rotr.

Fixpoint drop n s {struct s} :=
  match s, n with
  | _ :: s', n'.+1 => drop n' s'
  | _, _ => s
  end.

Lemma drop_behead : drop n0 =1 iter n0 behead.

Lemma drop0 : forall s, drop 0 s = s.

Lemma drop1 : drop 1 =1 behead.

Lemma drop_oversize : forall n s, size s <= n -> drop n s = [::].

Lemma drop_size : forall s, drop (size s) s = [::].

Lemma drop_cons : forall x s,
  drop n0 (x :: s) = if n0 is n.+1 then drop n s else x :: s.

Lemma size_drop : forall s, size (drop n0 s) = size s - n0.

Lemma drop_cat : forall s1 s2,
drop n0 (s1 ++ s2) =
   if n0 < size s1 then drop n0 s1 ++ s2 else drop (n0 - size s1) s2.

Lemma drop_size_cat : forall n s1 s2, size s1 = n -> drop n (s1 ++ s2) = s2.

Lemma nconsK : forall n x, cancel (ncons n x) (drop n).

Fixpoint take n s {struct s} :=
  match s, n with
  | x :: s', n'.+1 => x :: take n' s'
  | _, _ => [::]
  end.

Lemma take0 : forall s, take 0 s = [::].

Lemma take_oversize : forall n s, size s <= n -> take n s = s.

Lemma take_size : forall s, take (size s) s = s.

Lemma take_cons : forall x s,
  take n0 (x :: s) = if n0 is n.+1 then x :: (take n s) else [::].

Lemma drop_rcons : forall s, n0 <= size s ->
  forall x, drop n0 (rcons s x) = rcons (drop n0 s) x.

Lemma cat_take_drop : forall s, take n0 s ++ drop n0 s = s.

Lemma size_takel : forall s, n0 <= size s -> size (take n0 s) = n0.

Lemma size_take : forall s,
  size (take n0 s) = if n0 < size s then n0 else size s.

Lemma take_cat : forall s1 s2,
take n0 (s1 ++ s2) =
   if n0 < size s1 then take n0 s1 else s1 ++ take (n0 - size s1) s2.

Lemma take_size_cat : forall n s1 s2, size s1 = n -> take n (s1 ++ s2) = s1.

Lemma takel_cat : forall s1, n0 <= size s1 ->
  forall s2, take n0 (s1 ++ s2) = take n0 s1.

Lemma nth_drop : forall s i, nth (drop n0 s) i = nth s (n0 + i).

Lemma nth_take : forall i, i < n0 -> forall s, nth (take n0 s) i = nth s i.

drop_nth and take_nth below do NOT use the default n0, because the "n"  
 can be inferred from the condition, whereas the nth default value x0    
 will have to be given explicitly (and this will provide "d" as well).

Lemma drop_nth : forall n s, n < size s -> drop n s = nth s n :: drop n.+1 s.

Lemma take_nth : forall n s, n < size s ->
take n.+1 s = rcons (take n s) (nth s n).

Definition rot n s := drop n s ++ take n s.

Lemma rot0 : forall s, rot 0 s = s.

Lemma size_rot : forall s, size (rot n0 s) = size s.

Lemma rot_oversize : forall n s, size s <= n -> rot n s = s.

Lemma rot_size : forall s, rot (size s) s = s.

Lemma has_rot : forall s a, has a (rot n0 s) = has a s.

Lemma rot_size_cat : forall s1 s2, rot (size s1) (s1 ++ s2) = s2 ++ s1.

Definition rotr n s := rot (size s - n) s.

Lemma rotK : cancel (rot n0) (rotr n0).

Lemma rot_inj : injective (rot n0).

Lemma rot1_cons : forall x s, rot 1 (x :: s) = rcons s x.

(efficient) reversal

Fixpoint catrev s2 s1 {struct s1} :=
if s1 is x :: s1' then catrev (x :: s2) s1' else s2.

End Sequences.

rev must be defined outside a Section because Coq's end of section 
 "cooking" removes the nosimpl guard.

Definition rev T s := nosimpl catrev T (Nil T) s.

Notation "s1 ++ s2" := (cat s1 s2) : seq_scope.

Section Rev.

Variable T : Type.
Implicit Type s : seq T.

Lemma rev_rcons : forall s x, rev (rcons s x) = x :: (rev s).

Lemma rev_cons : forall x s, rev (x :: s) = rcons (rev s) x.

Lemma size_rev : forall s, size (rev s) = size s.

Lemma rev_cat : forall s1 s2, rev (s1 ++ s2) = rev s2 ++ rev s1.

Lemma revK : involutive (@rev T).

Lemma nth_rev : forall x0 n s,
n < size s -> nth x0 (rev s) n = nth x0 s (size s - n.+1).

End Rev.

Equality and eqType for seq.

Section EqSeq.

Variables (n0 : nat) (T : eqType) (x0 : T).
Notation Local nth := (nth x0).
Implicit Type s : seq T.
Implicit Types x y z : T.

Fixpoint eqseq s1 s2 {struct s2} :=
  match s1, s2 with
  | [::], [::] => true
  | x1 :: s1', x2 :: s2' => (x1 == x2) && eqseq s1' s2'
  | _, _ => false
  end.

Lemma eqseqP : Equality.axiom eqseq.

Canonical Structure seq_eqMixin := EqMixin eqseqP.
Canonical Structure seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.

Lemma eqseqE : eqseq = eq_op.

Lemma eqseq_cons : forall x1 x2 s1 s2,
  (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).

Lemma eqseq_cat : forall s1 s2 s3 s4,
  size s1 = size s2 -> (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).

Lemma eqseq_rcons : forall s1 s2 x1 x2,
  (rcons s1 x1 == rcons s2 x2) = (s1 == s2) && (x1 == x2).

Lemma has_filter : forall a s, has a s = (filter a s != [::]).

Lemma size_eq0 : forall s, (size s == 0) = (s == [::]).

mem_seq and index. 
 mem_seq defines a predType for seq.

Fixpoint mem_seq (s : seq T) :=
if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.

Definition eqseq_class := seq T.
Identity Coercion seq_of_eqseq : eqseq_class >-> seq.

Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].

Canonical Structure seq_predType := @mkPredType T (seq T) pred_of_eq_seq.

The line below makes mem_seq a canonical instance of topred.

Canonical Structure mem_seq_predType := mkPredType mem_seq.

Lemma in_cons : forall y s x, (x \in y :: s) = (x == y) || (x \in s).

Lemma in_nil : forall x, (x \in [::]) = false.

Lemma mem_seq1 : forall x y, (x \in [:: y]) = (x == y).

Let inE := (mem_seq1, in_cons, inE).

Lemma mem_seq2 : forall x y1 y2, (x \in [:: y1; y2]) = xpred2 y1 y2 x.

Lemma mem_seq3 : forall x y1 y2 y3,
  (x \in [:: y1; y2; y3]) = xpred3 y1 y2 y3 x.

Lemma mem_seq4 : forall x y1 y2 y3 y4,
  (x \in [:: y1; y2; y3; y4]) = xpred4 y1 y2 y3 y4 x.

Lemma mem_cat : forall x s1 s2, (x \in s1 ++ s2) = (x \in s1) || (x \in s2).

Lemma mem_rcons : forall s y, rcons s y =i y :: s.

Lemma mem_head : forall x s, x \in x :: s.

Lemma mem_last : forall x s, last x s \in x :: s.

Lemma mem_behead : forall s, {subset behead s <= s}.

Lemma mem_belast : forall s y, {subset belast y s <= y :: s}.

Lemma mem_nth : forall s n, n < size s -> nth s n \in s.

Lemma mem_take : forall s x, x \in take n0 s -> x \in s.

Lemma mem_drop : forall s x, x \in drop n0 s -> x \in s.

Lemma mem_rev : forall s, rev s =i s.

Section Filters.

Variable a : pred T.

Lemma hasP : forall s, reflect (exists2 x, x \in s & a x) (has a s).

Lemma hasPn : forall s, reflect (forall x, x \in s -> ~~ a x) (~~ has a s).

Lemma allP : forall s, reflect (forall x, x \in s -> a x) (all a s).

Lemma allPn : forall s, reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).

Lemma mem_filter : forall x s, (x \in filter a s) = a x && (x \in s).

End Filters.

Lemma eq_in_filter : forall (a1 a2 : pred T) s,
  {in s, a1 =1 a2} -> filter a1 s = filter a2 s.

Lemma eq_has_r : forall s1 s2, s1 =i s2 -> has^~ s1 =1 has^~ s2.

Lemma eq_all_r : forall s1 s2, s1 =i s2 -> all^~ s1 =1 all^~ s2.

Lemma has_sym : forall s1 s2, has (mem s1) s2 = has (mem s2) s1.

Lemma has_pred1 : forall x s, has (pred1 x) s = (x \in s).

Constant sequences, i.e., the image of nseq.

Definition constant s := if s is x :: s' then all (pred1 x) s' else true.

Lemma all_pred1P : forall x s, reflect (s = nseq (size s) x) (all (pred1 x) s).

Lemma all_pred1_constant : forall x s, all (pred1 x) s -> constant s.

Lemma all_pred1_nseq : forall x y n,
all (pred1 x) (nseq n y) = (n == 0) || (x == y).

Lemma constant_nseq : forall n x, constant (nseq n x).

Uses x0

Lemma constantP : forall s,
reflect (exists x, s = nseq (size s) x) (constant s).

Duplicate-freenes.

Fixpoint uniq s :=
  if s is x :: s' then (x \notin s') && uniq s' else true.

Lemma cons_uniq : forall x s, uniq (x :: s) = (x \notin s) && uniq s.

Lemma cat_uniq : forall s1 s2,
  uniq (s1 ++ s2) = [&& uniq s1, ~~ has (mem s1) s2 & uniq s2].

Lemma uniq_catC : forall s1 s2, uniq (s1 ++ s2) = uniq (s2 ++ s1).

Lemma uniq_catCA : forall s1 s2 s3,
  uniq (s1 ++ s2 ++ s3) = uniq (s2 ++ s1 ++ s3).

Lemma rcons_uniq : forall s x, uniq (rcons s x) = (x \notin s) && uniq s.

Lemma filter_uniq : forall s a, uniq s -> uniq (filter a s).

Lemma rot_uniq : forall s, uniq (rot n0 s) = uniq s.

Lemma rev_uniq : forall s, uniq (rev s) = uniq s.

Lemma count_uniq_mem : forall s x, uniq s -> count (pred1 x) s = (x \in s).

Removing duplicates

Fixpoint undup s :=
if s is x :: s' then if x \in s' then undup s' else x :: undup s' else [::].

Lemma size_undup : forall s, size (undup s) <= size s.

Lemma mem_undup : forall s, undup s =i s.

Lemma undup_uniq : forall s, uniq (undup s).

Lemma undup_id : forall s, uniq s -> undup s = s.

Lemma ltn_size_undup : forall s, (size (undup s) < size s) = ~~ uniq s.

Lookup

Definition index x := find (pred1 x).

Lemma index_size : forall x s, index x s <= size s.

Lemma index_mem : forall x s, (index x s < size s) = (x \in s).

Lemma nth_index : forall x s, x \in s -> nth s (index x s) = x.

Lemma index_cat : forall x s1 s2,
index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2.

Lemma index_uniq : forall i s, i < size s -> uniq s -> index (nth s i) s = i.

Lemma index_head : forall x s, index x (x :: s) = 0.

Lemma index_last : forall x s,
  uniq (x :: s) -> index (last x s) (x :: s) = size s.

Lemma nth_uniq : forall s i j,
   i < size s -> j < size s -> uniq s -> (nth s i == nth s j) = (i == j).

Lemma mem_rot : forall s, rot n0 s =i s.

Lemma eqseq_rot : forall s1 s2, (rot n0 s1 == rot n0 s2) = (s1 == s2).

CoInductive rot_to_spec (s : seq T) (x : T) : Type :=
  RotToSpec i s' of rot i s = x :: s'.

Lemma rot_to : forall s x, x \in s -> rot_to_spec s x.

End EqSeq.

Definition inE := (mem_seq1, in_cons, inE).

Implicit Arguments eqseqP [T x y].
Implicit Arguments all_filterP [T a s].
Implicit Arguments hasP [T a s].
Implicit Arguments hasPn [T a s].
Implicit Arguments allP [T a s].
Implicit Arguments allPn [T a s].

Section NseqthTheory.

Lemma nthP : forall (T : eqType) (s : seq T) x x0,
  reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s).

Variable T : Type.

Lemma has_nthP : forall (a : pred T) s x0,
  reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).

Lemma all_nthP : forall (a : pred T) s x0,
  reflect (forall i, i < size s -> a (nth x0 s i)) (all a s).

End NseqthTheory.

Lemma set_nth_default : forall T s (y0 x0 : T) n,
  n < size s -> nth x0 s n = nth y0 s n.

Lemma headI : forall T s (x : T),
  rcons s x = head x s :: behead (rcons s x).

Implicit Arguments nthP [T s x].
Implicit Arguments has_nthP [T a s].
Implicit Arguments all_nthP [T a s].

Definition bitseq := seq bool.
Canonical Structure bitseq_eqType := Eval hnf in [eqType of bitseq].
Canonical Structure bitseq_predType := Eval hnf in [predType of bitseq].

Incrementing the ith nat in a seq nat, padding with 0's if needed. This  
 allows us to use nat seqs as bags of nats.

Fixpoint incr_nth (v : seq nat) (i : nat) {struct i} : seq nat :=
  if v is n :: v' then
    if i is i'.+1 then n :: incr_nth v' i' else n.+1 :: v'
  else
    ncons i 0 [:: 1].

Lemma nth_incr_nth : forall v i j,
  nth 0 (incr_nth v i) j = (i == j) + nth 0 v j.

Lemma size_incr_nth : forall v i,
  size (incr_nth v i) = if i < size v then size v else i.+1.

equality up to permutation

Section PermSeq.

Variable T : eqType.

Definition same_count1 (s1 s2 : seq T) x :=
   count (pred1 x) s1 == count (pred1 x) s2.

Definition perm_eq (s1 s2 : seq T) := all (same_count1 s1 s2) (s1 ++ s2).

Lemma perm_eqP : forall s1 s2,
  reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).

Lemma perm_eq_refl : forall s, perm_eq s s.
Hint Resolve perm_eq_refl.

Lemma perm_eq_sym : symmetric perm_eq.

Lemma perm_eq_trans : transitive perm_eq.

Notation perm_eql := (fun s1 s2 => perm_eq s1 =1 perm_eq s2).
Notation perm_eqr := (fun s1 s2 => perm_eq^~ s1 =1 perm_eq^~ s2).

Lemma perm_eqlP : forall s1 s2, reflect (perm_eql s1 s2) (perm_eq s1 s2).

Lemma perm_eqrP : forall s1 s2, reflect (perm_eqr s1 s2) (perm_eq s1 s2).

Lemma perm_catC : forall s1 s2, perm_eql (s1 ++ s2) (s2 ++ s1).

Lemma perm_cat2l : forall s1 s2 s3,
  perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.

Lemma perm_cons : forall x s1 s2, perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.

Lemma perm_cat2r : forall s1 s2 s3,
  perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.

Lemma perm_catAC : forall s1 s2 s3,
  perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).

Lemma perm_catCA : forall s1 s2 s3,
  perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).

Lemma perm_rcons : forall x s, perm_eql (rcons s x) (x :: s).

Lemma perm_rot : forall n s, perm_eql (rot n s) s.

Lemma perm_rotr : forall n s, perm_eql (rotr n s) s.

Lemma perm_eq_mem : forall s1 s2, perm_eq s1 s2 -> s1 =i s2.

Lemma perm_eq_size : forall s1 s2, perm_eq s1 s2 -> size s1 = size s2.

Lemma uniq_leq_size : forall s1 s2 : seq T,
  uniq s1 -> {subset s1 <= s2} -> size s1 <= size s2.

Lemma leq_size_uniq : forall s1 s2 : seq T,
  uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> uniq s2.

Lemma uniq_size_uniq : forall s1 s2 : seq T,
  uniq s1 -> s1 =i s2 -> uniq s2 = (size s2 == size s1).

Lemma leq_size_perm : forall s1 s2 : seq T,
  uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 ->
    s1 =i s2 /\ size s1 = size s2.

Lemma perm_uniq : forall s1 s2 : seq T,
  s1 =i s2 -> size s1 = size s2 -> uniq s1 = uniq s2.

Lemma perm_eq_uniq : forall s1 s2, perm_eq s1 s2 -> uniq s1 = uniq s2.

Lemma uniq_perm_eq : forall s1 s2,
  uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2.

Lemma count_mem_uniq : forall s : seq T,
  (forall x, count (pred1 x) s = (x \in s)) -> uniq s.

End PermSeq.

Notation perm_eql := (fun s1 s2 => perm_eq s1 =1 perm_eq s2).
Notation perm_eqr := (fun s1 s2 => perm_eq^~ s1 =1 perm_eq^~ s2).

Implicit Arguments perm_eqP [T s1 s2].
Implicit Arguments perm_eqlP [T s1 s2].
Implicit Arguments perm_eqrP [T s1 s2].
Hint Resolve perm_eq_refl.

Section RotrLemmas.

Variables (n0 : nat) (T : Type) (T' : eqType).

Lemma size_rotr : forall s : seq T, size (rotr n0 s) = size s.

Lemma mem_rotr : forall s : seq T', rotr n0 s =i s.

Lemma rotr_size_cat : forall s1 s2 : seq T,
  rotr (size s2) (s1 ++ s2) = s2 ++ s1.

Lemma rotr1_rcons : forall x (s : seq T), rotr 1 (rcons s x) = x :: s.

Lemma has_rotr : forall (a : pred T) s, has a (rotr n0 s) = has a s.

Lemma rotr_uniq : forall s : seq T', uniq (rotr n0 s) = uniq s.

Lemma rotrK : cancel (@rotr T n0) (rot n0).

Lemma rotr_inj : injective (@rotr T n0).

Lemma rev_rot : forall s : seq T, rev (rot n0 s) = rotr n0 (rev s).

Lemma rev_rotr : forall s : seq T, rev (rotr n0 s) = rot n0 (rev s).

End RotrLemmas.

Section RotCompLemmas.

Variable T : Type.

Lemma rot_addn : forall m n (s : seq T), m + n <= size s ->
  rot (m + n) s = rot m (rot n s).

Lemma rotS : forall n (s : seq T), n < size s -> rot n.+1 s = rot 1 (rot n s).

Lemma rot_add_mod : forall m n (s : seq T), n <= size s -> m <= size s ->
  rot m (rot n s) = rot (if m + n <= size s then m + n else m + n - size s) s.

Lemma rot_rot : forall m n (s : seq T), rot m (rot n s) = rot n (rot m s).

Lemma rot_rotr : forall m n (s : seq T), rot m (rotr n s) = rotr n (rot m s).

Lemma rotr_rotr : forall m n (s : seq T),
  rotr m (rotr n s) = rotr n (rotr m s).

End RotCompLemmas.

Section Mask.

Variables (n0 : nat) (T : Type).

Fixpoint mask (m : bitseq) (s : seq T) {struct m} : seq T :=
  match m, s with
  | b :: m', x :: s' => if b then x :: mask m' s' else mask m' s'
  | _, _ => [::]
  end.

Lemma mask_false : forall s n, mask (nseq n false) s = [::].

Lemma mask_true : forall s n, size s <= n -> mask (nseq n true) s = s.

Lemma mask0 : forall m, mask m [::] = [::].

Lemma mask1 : forall b x, mask [:: b] [:: x] = nseq b x.

Lemma mask_cons : forall b m x s,
  mask (b :: m) (x :: s) = nseq b x ++ mask m s.

Lemma size_mask : forall m s,
  size m = size s -> size (mask m s) = count id m.

Lemma mask_cat : forall m1 s1, size m1 = size s1 ->
  forall m2 s2, mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.

Lemma has_mask_cons : forall a b m x s,
  has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).

Lemma mask_rot : forall m s, size m = size s ->
   mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s).

End Mask.

Section EqMask.

Variables (n0 : nat) (T : eqType).

Lemma mem_mask_cons : forall x b m y (s : seq T),
  (x \in mask (b :: m) (y :: s)) = b && (x == y) || (x \in mask m s).

Lemma mem_mask : forall x m (s : seq T), (x \in mask m s) -> (x \in s).

Lemma mask_uniq : forall s : seq T, uniq s -> forall m, uniq (mask m s).

Lemma mem_mask_rot : forall m (s : seq T), size m = size s ->
  mask (rot n0 m) (rot n0 s) =i mask m s.

End EqMask.

Section Map.

Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2) (f : T1 -> T2).

Fixpoint map (s : seq T1) : seq T2 :=
  if s is x :: s' then f x :: map s' else [::].

Lemma map_cons : forall x s, map (x :: s) = f x :: map s.

Lemma map_nseq : forall x, map (nseq n0 x) = nseq n0 (f x).

Lemma map_cat : forall s1 s2, map (s1 ++ s2) = map s1 ++ map s2.

Lemma size_map : forall s, size (map s) = size s.

Lemma behead_map : forall s, behead (map s) = map (behead s).

Lemma nth_map : forall n s, n < size s -> nth x2 (map s) n = f (nth x1 s n).

Lemma map_rcons : forall s x,
  map (rcons s x) = rcons (map s) (f x).

Lemma last_map : forall s x, last (f x) (map s) = f (last x s).

Lemma belast_map : forall s x, belast (f x) (map s) = map (belast x s).

Lemma filter_map : forall a s,
  filter a (map s) = map (filter (preim f a) s).

Lemma find_map : forall a s, find a (map s) = find (preim f a) s.

Lemma has_map : forall a s, has a (map s) = has (preim f a) s.

Lemma count_map : forall a s, count a (map s) = count (preim f a) s.

Lemma map_take : forall s, map (take n0 s) = take n0 (map s).

Lemma map_drop : forall s, map (drop n0 s) = drop n0 (map s).

Lemma map_rot : forall s, map (rot n0 s) = rot n0 (map s).

Lemma map_rotr : forall s, map (rotr n0 s) = rotr n0 (map s).

Lemma map_rev : forall s, map (rev s) = rev (map s).

Lemma map_mask : forall m s, map (mask m s) = mask m (map s).

Hypothesis Hf : injective f.

Lemma inj_map : injective map.

End Map.

Section EqMap.

Variables (n0 : nat) (T1 : eqType) (x1 : T1).
Variables (T2 : eqType) (x2 : T2) (f : T1 -> T2).

Lemma map_f : forall (s : seq T1) x, x \in s -> f x \in map f s.

Lemma mapP : forall (s : seq T1) y,
  reflect (exists2 x, x \in s & y = f x) (y \in map f s).

Lemma map_uniq : forall s, uniq (map f s) -> uniq s.

Lemma map_inj_in_uniq : forall s : seq T1,
  {in s &, injective f} -> uniq (map f s) = uniq s.

Hypothesis Hf : injective f.

Lemma mem_map : forall s x, (f x \in map f s) = (x \in s).

Lemma index_map : forall s x, index (f x) (map f s) = index x s.

Lemma map_inj_uniq : forall s, uniq (map f s) = uniq s.

End EqMap.

Implicit Arguments mapP [T1 T2 f s y].

Lemma filter_mask : forall T a (s : seq T), filter a s = mask (map a s) s.

Section MapComp.

Variable T1 T2 T3 : Type.

Lemma map_id : forall s : seq T1, map id s = s.

Lemma eq_map : forall f1 f2 : T1 -> T2, f1 =1 f2 -> map f1 =1 map f2.

Lemma map_comp : forall (f1 : T2 -> T3) (f2 : T1 -> T2) s,
  map (f1 \o f2) s = map f1 (map f2 s).

Lemma mapK : forall (f1 : T1 -> T2) (f2 : T2 -> T1),
  cancel f1 f2 -> cancel (map f1) (map f2).

End MapComp.

Lemma eq_in_map : forall (T1 : eqType) T2 (f1 f2 : T1 -> T2) (s : seq T1),
  {in s, f1 =1 f2} -> map f1 s = map f2 s.

Lemma map_id_in : forall (T : eqType) f (s : seq T),
  {in s, f =1 id} -> map f s = s.

Map a partial function

Section Pmap.

Variables (aT rT : Type) (f : aT -> option rT) (g : rT -> aT).

Fixpoint pmap s :=
  if s is x :: s' then oapp (cons^~ (pmap s')) (pmap s') (f x) else [::].

Lemma map_pK : pcancel g f -> cancel (map g) pmap.

Lemma size_pmap : forall s, size (pmap s) = count [eta f] s.

Lemma pmapS_filter : forall s, map some (pmap s) = map f (filter [eta f] s).

Hypothesis fK : ocancel f g.

Lemma pmap_filter : forall s, map g (pmap s) = filter [eta f] s.

End Pmap.

Section EqPmap.

Variables (aT rT : eqType) (f : aT -> option rT) (g : rT -> aT).

Lemma eq_pmap : forall (f1 f2 : aT -> option rT),
f1 =1 f2 -> pmap f1 =1 pmap f2.

Lemma mem_pmap : forall s u, (u \in pmap f s) = (Some u \in map f s).

Hypothesis fK : ocancel f g.

Lemma can2_mem_pmap : pcancel g f ->
  forall s u, (u \in pmap f s) = (g u \in s).

Lemma pmap_uniq : forall s, uniq s -> uniq (pmap f s).

End EqPmap.

Section Pmapub.

Variables (T : Type) (p : pred T) (sT : subType p).

Let insT : T -> option sT := insub.

Lemma size_pmap_sub : forall s, size (pmap insT s) = count p s.

End Pmapub.

Section EqPmapSub.

Variables (T : eqType) (p : pred T) (sT : subType p).

Let insT : T -> option sT := insub.

Lemma mem_pmap_sub : forall (s : seq T) u,
  (u \in pmap insT s) = (val u \in s).

Lemma pmap_sub_uniq : forall s : seq T, uniq s -> uniq (pmap insT s).

End EqPmapSub.

Index sequence

Fixpoint iota (m n : nat) {struct n} : seq nat :=
  if n is n'.+1 then m :: iota m.+1 n' else [::].

Lemma size_iota : forall m n, size (iota m n) = n.

Lemma iota_add : forall m n1 n2,
  iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.

Lemma iota_addl : forall m1 m2 n,
  iota (m1 + m2) n = map (addn m1) (iota m2 n).

Lemma nth_iota : forall m n i, i < n -> nth 0 (iota m n) i = m + i.

Lemma mem_iota : forall m n i, (i \in iota m n) = (m <= i) && (i < m + n).

Lemma iota_uniq : forall m n, uniq (iota m n).

Making a sequence of a specific length, using indexes to compute items.

Section MakeSeq.

Variables (T : Type) (x0 : T).

Definition mkseq f n : seq T := map f (iota 0 n).

Lemma size_mkseq : forall f n, size (mkseq f n) = n.

Lemma eq_mkseq : forall f g, f =1 g -> mkseq f =1 mkseq g.

Lemma nth_mkseq : forall f n i, i < n -> nth x0 (mkseq f n) i = f i.

Lemma mkseq_nth : forall s, mkseq (nth x0 s) (size s) = s.

End MakeSeq.

Lemma mkseq_uniq : forall (T : eqType) (f : nat -> T) n,
  injective f -> uniq (mkseq f n).

Section FoldRight.

Variables (T R : Type) (f : T -> R -> R) (z0 : R).

Fixpoint foldr (s : seq T) : R := if s is x :: s' then f x (foldr s') else z0.

End FoldRight.

Section FoldRightComp.

Variables (T1 T2 : Type) (h : T1 -> T2).
Variables (R : Type) (f : T2 -> R -> R) (z0 : R).

Lemma foldr_cat :
  forall s1 s2, foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.

Lemma foldr_map :
  forall s : seq T1, foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s.

End FoldRightComp.

Quick characterization of the null sequence.

Definition sumn := foldr addn 0.

Lemma sumn_nseq : forall x n : nat, sumn (nseq n x) = x * n.

Lemma sumn_cat : forall s1 s2, sumn (s1 ++ s2) = sumn s1 + sumn s2.

Lemma natnseq0P : forall s : seq nat,
  reflect (s = nseq (size s) 0) (sumn s == 0).

Section FoldLeft.

Variables (T R : Type) (f : R -> T -> R).

Fixpoint foldl z (s : seq T) {struct s} :=
  if s is x :: s' then foldl (f z x) s' else z.

Lemma foldl_rev : forall z s, foldl z (rev s) = foldr (fun x z => f z x) z s.

Lemma foldl_cat : forall z s1 s2, foldl z (s1 ++ s2) = foldl (foldl z s1) s2.

End FoldLeft.

Section Scan.

Variables (T1 : Type) (x1 : T1) (T2 : Type) (x2 : T2).
Variables (f : T1 -> T1 -> T2) (g : T1 -> T2 -> T1).

Fixpoint pairmap x (s : seq T1) {struct s} :=
  if s is y :: s' then f x y :: pairmap y s' else [::].

Lemma size_pairmap : forall x s, size (pairmap x s) = size s.

Lemma nth_pairmap : forall s n, n < size s ->
  forall x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n).

Fixpoint scanl x (s : seq T2) {struct s} :=
  if s is y :: s' then let x' := g x y in x' :: scanl x' s' else [::].

Lemma size_scanl : forall x s, size (scanl x s) = size s.

Lemma nth_scanl : forall s n, n < size s ->
  forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s).

Lemma scanlK :
  (forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x).

Lemma pairmapK :
  (forall x, cancel (f x) (g x)) -> forall x, cancel (pairmap x) (scanl x).

End Scan.

Section Zip.

Variables T1 T2 : Type.

Fixpoint zip (s1 : seq T1) (s2 : seq T2) {struct s2} :=
  match s1, s2 with
  | x1 :: s1', x2 :: s2' => (x1,x2) :: zip s1' s2'
  | _, _ => [::]
  end.

Definition unzip1 := map (@fst T1 T2).
Definition unzip2 := map (@snd T1 T2).

Lemma zip_unzip : forall s, zip (unzip1 s) (unzip2 s) = s.

Lemma unzip1_zip : forall s1 s2,
  size s1 <= size s2 -> unzip1 (zip s1 s2) = s1.

Lemma unzip2_zip : forall s1 s2,
  size s2 <= size s1 -> unzip2 (zip s1 s2) = s2.

Lemma size1_zip : forall s1 s2,
  size s1 <= size s2 -> size (zip s1 s2) = size s1.

Lemma size2_zip : forall s1 s2,
  size s2 <= size s1 -> size (zip s1 s2) = size s2.

End Zip.

Section Flatten.

Variable T : Type.

Definition flatten := foldr cat (Nil T).
Definition shape := map (@size T).
Fixpoint reshape (sh : seq nat) (s : seq T) {struct sh} :=
  if sh is n :: sh' then take n s :: reshape sh' (drop n s) else [::].

Lemma size_flatten : forall ss, size (flatten ss) = sumn (shape ss).

Lemma flattenK : forall ss, reshape (shape ss) (flatten ss) = ss.

Lemma reshapeKr : forall sh s, size s <= sumn sh -> flatten (reshape sh s) = s.

Lemma reshapeKl : forall sh s, size s >= sumn sh -> shape (reshape sh s) = sh.

End Flatten.