Library seq

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
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 structures. The operations are geared       
towards reflection, e.g., they generally expect and provide boolean     
predicates, and our membership predicates 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.        
  Since 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 have a default value. We use a combination of syntactic 
extensions/prettyprinting to hide it in most of the development.        
  Here is the list of seq operations :                                  
  - constructors : Nil, Cons (nil, cons if polymorphic), rcons          
  - factories : ncons, nseq (repeat sequence), seqn (n-ary).            
  - items from indexes : iota (index generation), mkseq.                
  - sequential access: ohead (option), head (w. default), behead,       
                       last, belast (non empty seqs)                    
  - random access: nth & set_nth (w. default), incr_nth (for seq nat)   
  - size: size (seq version of length), shape (= map size)              
  - elements lookup: index, mem_seq (implements the predType interface) 
  - set operations: find, count, has, all, constant                     
  - filtering : filter, subfilter (to subType), sieve (bitseq masking)  
  - "no duplicates" predicate & function: uniq, undup                   
  - permutation equivalence: perm_eq, perm_eql & r (left & right trans) 
  - surgery: cat, drop, take, rot, rotr, rev                            
  - iterators: map, pmap (partial funs), foldr (fold_right), foldl,     
               sumn, scanl, pairmap zip, unzip1 & 2, flatten, reshape   
The sieve operator uses a boolean sequence to select a subsequence; it  
is used heavily for the correctness of the config compilation.          
We are quite systematic in providing lemmas to rewrite any composition  
of two operations. "rev", whose simplifications are not natural, is     
protected with nosimpl.                                                 
 Notations:                                                             
   [::], x :: s, s1 ++ s2   nil, cons x s, cat s1 s2                    
   [:: x0; ... xn]          explicit seq                                
   [:: x0, ... xn & s]      multiple cons                               
   s`_i                     nth x0 s i for the appropriate x0           
                            (to be defined in the appropriate scope)    

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.
numerical parameter for take, drop et al 
Variable T : Type.
must come before the implicit Type     
Variable x0 : T.
default for head/nth 

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 = [::]. Qed.

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. Qed.

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

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. Qed.

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. Qed.

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. Qed.

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 = [::]. Qed.

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. Qed.

Lemma drop1 : drop 1 =1 behead. Qed.

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 = [::]. Qed.

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). Qed.

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_eqMixin.

Lemma eqseqE : eqseq = eq_op. Qed.

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).

to be repeated after the Section discharge. 
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 Sieve.

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

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

Lemma sieve_false : forall s n, sieve (nseq n false) s = [::].

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

Lemma sieve0 : forall m, sieve m [::] = [::].

Lemma sieve1 : forall b x, sieve [:: b] [:: x] = nseq b x.

Lemma sieve_cons : forall b m x s,
  sieve (b :: m) (x :: s) = nseq b x ++ sieve m s.

Lemma size_sieve : forall m s,
  size m = size s -> size (sieve m s) = count id m.

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

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

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

End Sieve.

Section EqSieve.

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

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

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

Lemma sieve_uniq : forall s : seq T, uniq s -> forall m, uniq (sieve m s).

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

End EqSieve.

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_sieve : forall m s, map (sieve m s) = sieve 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_sieve : forall T a (s : seq T), filter a s = sieve (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.