Library mathcomp.ssreflect.seq

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

The seq type is the ssreflect type for sequences; it is an alias for the standard Coq list type. The ssreflect library equips it with many operations, as well as eqType and predType (and, later, choiceType) structures. The operations are geared towards reflection: 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. 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 of 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 an 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 when the head of s is x. 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 copies 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:

nilp s <=> s is [:: ]. := (size s == 0). 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 a s <=> a holds for some item in s, where a is an applicative bool predicate. all a s <=> a holds for all items in s. 'has_aP <-> the view reflect (exists2 x, x \in s & A x) (has a s), where aP x : reflect (A x) (a x). 'all_aP <=> the view for reflect {in s, forall x, A x} (all a s). all2 r s t <=> the (bool) relation r holds for all respective items in s and t, which must also have the same size, i.e., for s := [:: x1; ...; x_m] and t := [:: y1; ...; y_n], the condition [&& r x_1 y_1, ..., r x_n y_n & m == n]. find p s == the index of the first item in s for which p holds, or size s if no such item is found. count p s == the number of items of s for which p holds. count_mem x s == the multiplicity of x in s, i.e., count (pred1 x) s. tally s == a tally of s, i.e., a sequence of (item, multiplicity) pairs for all items in sequence s (without duplicates). incr_tally bs x == increment the multiplicity of x in the tally bs, or add x with multiplicity 1 at then end if x is not in bs. bs \is a wf_tally <=> bs is well-formed tally, with no duplicate items or null multiplicities. tally_seq bs == the expansion of a tally bs into a sequence where each (x, n) pair expands into a sequence of n x's. constant s <=> all items in s are identical (trivial if s = [:: ]). uniq s <=> all the items in s are pairwise different. subseq s1 s2 <=> s1 is a subsequence of s2, i.e., s1 = mask m s2 for some m : bitseq (see below). 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 right of perm_eq. > These left/right transitive versions of perm_eq make it easier to chain a sequence of equivalences. permutations s == a duplicate-free list of all permutations of s.

Filtering:

filter p s == the subsequence of s consisting of all the items for which the (boolean) predicate p holds. rem x s == the subsequence of s, where the first occurrence of x has been removed (compare filter (predC1 x) s where ALL occurrences of x are removed). 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 s1 s2 == the reversal of s1 followed by s2 (this is the recursive form of rev).

Dependent iterator: for s : seq S and t : S -> seq T

[seq E | x <- s, y <- t] := flatten [seq [seq E | x <- t] | y <- s] == the sequence of all the f x y, with x and y drawn from s and t, respectively, in row-major order, and where t is possibly dependent in elements of s allpairs_dep f s t := self expanding definition for [seq f x y | x <- s, y <- t i]

Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m],

allpairs f s t := same as allpairs_dep but where t is non dependent, i.e. self expanding definition for [seq f x y | x <- s, y <- t] := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] map f s == the sequence [:: f x_1, ..., f x_n]. pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik, pf x_i = Some y_i, and pf x_j = None iff j is not in {i1, ..., ik}. foldr f a s == the right fold of s by f (i.e., the natural iterator). := f x_1 (f x_2 ... (f x_n a)) sumn s == x_1 + (x_2 + ... + (x_n + 0)) (when s : seq nat). foldl f a s == the left fold of s by f. := f (f ... (f a x_1) ... x_n-1) x_n scanl f a s == the sequence of partial accumulators of foldl f a s. := [:: f a x_1; ...; foldl f a s] pairmap f a s == the sequence of f applied to consecutive items in a :: s. := [:: f a x_1; f x_1 x_2; ...; f x_n-1 x_n] zip s t == itemwise pairing of s and t (dropping any extra items). := [:: (x_1, y_1); ...; (x_mn, y_mn) ] with mn = minn n m. unzip1 s == [:: (x_1).1; ...; (x_n).1] when s : seq (S * T). unzip2 s == [:: (x_1).2; ...; (x_n).2] when s : seq (S * T). flatten s == x_1 ++ ... ++ x_n ++ [:: ] when s : seq (seq T). reshape r s == s reshaped into a sequence of sequences whose sizes are given by r (truncating if s is too long or too short). := [:: [:: x_1; ...; x_r1]; [:: x(r1 + 1); ...; x(r0 + r1) ]; ...; [:: x(r1 + ... + r(k-1) + 1); ...; x(r0 + ... rk) ]#] flatten_index sh r c == the index, in flatten ss, of the item of indexes (r, c) in any sequence of sequences ss of shape sh := sh_1 + sh_2 + ... + sh_r + c reshape_index sh i == the index, in reshape sh s, of the sequence containing the i-th item of s. reshape_offset sh i == the offset, in the (reshape_index sh i)-th sequence of reshape sh s of the i-th item of s

Notation for manifest comprehensions:

[seq x <- s | C] := filter (fun x => C) s. [seq E | x <- s] := map (fun x => E) s. [seq x <- s | C1 & C2] := [seq x <- s | C1 && C2]. [seq E | x <- s & C] := [seq E | x <- [seq x | C] ]. > The above allow optional type casts on the eigenvariables, as in [seq x : T <- s | C] or [seq E | x : T <- s, y : U <- t]. The cast may be needed as type inference considers E or C before s. We are quite systematic in providing lemmas to rewrite any composition of two operations. "rev", whose simplifications are not natural, is protected with nosimpl.

The following are equivalent:

[<-> P0; P1; ..; Pn] <-> P0, P1, ..., Pn are all equivalent. := P0 -> P1 -> ... -> Pn -> P0 if T : [<-> P0; P1; ..; Pn] is such an equivalence, and i, j are in nat then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj; when i (resp. j) is out of bounds, Pi (resp. Pj) defaults to P0. The tactic tfae splits the goal into n+1 implications to prove. An example of use can be found in fingraph theorem orbitPcycle.

Set Implicit Arguments.

Reserved Notation "[ '<->' P0 ; P1 ; .. ; Pn ]"
  (at level 0, format "[ '<->' '[' P0 ; '/' P1 ; '/' .. ; '/' Pn ']' ]").

Delimit Scope seq_scope with SEQ.
Open Scope seq_scope.

Inductive seq (T : Type) : Type := Nil | Cons of T & seq T.
Notation seq := list.
Notation Cons T := (@cons T) (only parsing).
Notation Nil T := (@nil T) (only parsing).

As :: and ++ are (improperly) declared in Init.datatypes, we only rebind them here.
Infix "::" := cons : seq_scope.

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

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

Notation "[ :: x & s ]" := (x :: s) (at level 0, only parsing) : seq_scope.

Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
  (at level 0, format
  "'[hv' [ :: '[' x1 , '/' x2 , '/' .. , '/' xn ']' '/ ' & s ] ']'"
  ) : seq_scope.

Notation "[ :: x1 ; x2 ; .. ; xn ]" := (x1 :: x2 :: .. [:: xn] ..)
  (at level 0, format "[ :: '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]"
  ) : seq_scope.

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 s : size s = 0 s = [::].

Definition nilp s := size s == 0.

Lemma nilP s : reflect (s = [::]) (nilp 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 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 n x s : size (ncons n x s) = n + size s.

Lemma size_nseq 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 : seqn_type n :=
  if n is n'.+1 return seqn_type n then
    fun xseqn_rec (fun sf (x :: s)) n'
  else f [::].
Definition seqn := seqn_rec id.

Sequence catenation "cat".

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

Lemma cat0s s : [::] ++ s = s.
Lemma cat1s x s : [:: x] ++ s = x :: s.
Lemma cat_cons x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2.

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

Lemma nseq_addn n1 n2 x :
  nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x.

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

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

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

last, belast, rcons, and last induction.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma lastP s : last_spec s.

Lemma last_ind P :
  P [::] ( s x, P s P (rcons s x)) 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 s : nth s 0 = head s.

Lemma nth_default s n : size s n nth s n = x0.

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

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

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

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

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

Lemma nth_rcons 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_rcons_default s i : nth (rcons s x0) i = nth s i.

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

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

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

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

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

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

Lemma set_set_nth s n1 y1 n2 y2 (s2 := set_nth s n2 y2) :
  set_nth (set_nth s n1 y1) n2 y2 = 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 size_filter s : size (filter s) = count s.

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

Lemma count_size s : count s size s.

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

Lemma filter_all s : all (filter s).

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

Lemma filter_id s : filter (filter s) = filter s.

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

Lemma find_size s : find s size s.

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

Lemma has_nil : has [::] = false.

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

Lemma has_nseq n x : has (nseq n x) = (0 < n) && a x.

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

Lemma all_nil : all [::] = true.

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

Lemma all_nseq n x : all (nseq n x) = (n == 0) || a x.

Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x.

Lemma filter_nseq n x : filter (nseq n x) = nseq (a x × n) x.

Lemma count_nseq n x : count (nseq n x) = a x × n.

Lemma find_nseq n x : find (nseq n x) = ~~ a x × n.

Lemma nth_find s : has s a (nth s (find s)).

Lemma before_find s i : i < find s a (nth s i) = false.

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

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

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

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

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

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

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

End SeqFind.

Lemma eq_find a1 a2 : a1 =1 a2 find a1 =1 find a2.

Lemma eq_filter a1 a2 : a1 =1 a2 filter a1 =1 filter a2.

Lemma eq_count a1 a2 : a1 =1 a2 count a1 =1 count a2.

Lemma eq_has a1 a2 : a1 =1 a2 has a1 =1 has a2.

Lemma eq_all a1 a2 : a1 =1 a2 all a1 =1 all a2.

Lemma all_filter (p q : pred T) xs :
  all p (filter q xs) = all [pred i | q i ==> p i] xs.

Section SubPred.

Variable (a1 a2 : pred T).
Hypothesis s12 : subpred a1 a2.

Lemma sub_find s : find a2 s find a1 s.

Lemma sub_has s : has a1 s has a2 s.

Lemma sub_count s : count a1 s count a2 s.

Lemma sub_all s : all a1 s all a2 s.

End SubPred.

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

Lemma filter_predT s : filter predT s = s.

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

Lemma count_pred0 s : count pred0 s = 0.

Lemma count_predT s : count predT s = size s.

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

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

Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s.

Lemma has_pred0 s : has pred0 s = false.

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

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

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

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

Lemma all_predT s : all predT s.

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

Lemma all_predI 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'.+1drop n' s'
  | _, _s
  end.

Lemma drop_behead : drop n0 =1 iter n0 behead.

Lemma drop0 s : drop 0 s = s.

Lemma drop1 : drop 1 =1 behead.

Lemma drop_oversize n s : size s n drop n s = [::].

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

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

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

Lemma drop_cat 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 n s1 s2 : size s1 = n drop n (s1 ++ s2) = s2.

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

Lemma drop_drop s n1 n2 : drop n1 (drop n2 s) = drop (n1 + n2) s.

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

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

Lemma take_oversize n s : size s n take n s = s.

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

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

Lemma drop_rcons s : n0 size s
   x, drop n0 (rcons s x) = rcons (drop n0 s) x.

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

Lemma size_takel s : n0 size s size (take n0 s) = n0.

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

Lemma take_cat 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 n s1 s2 : size s1 = n take n (s1 ++ s2) = s1.

Lemma takel_cat s1 s2 : n0 size s1 take n0 (s1 ++ s2) = take n0 s1.

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

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

Lemma take_take i j : i j s, take i (take j s) = take i s.

Lemma take_drop i j s : take i (drop j s) = drop j (take (i + j) s).

Lemma take_addn i j s : take (i + j) s = take i s ++ take j (drop i s).

Lemma takeC i j s : take i (take j s) = take j (take i s).

Lemma take_nseq i j x : i j take i (nseq j x) = nseq i x.

Lemma drop_nseq i j x : drop i (nseq j x) = nseq (j - i) x.

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 n s : n < size s drop n s = nth s n :: drop n.+1 s.

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

Rotation

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

Lemma rot0 s : rot 0 s = s.

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

Lemma rot_oversize n s : size s n rot n s = s.

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

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

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

(efficient) reversal

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

Definition rev s := catrev s [::].

Lemma catrev_catl s t u : catrev (s ++ t) u = catrev t (catrev s u).

Lemma catrev_catr s t u : catrev s (t ++ u) = catrev s t ++ u.

Lemma catrevE s t : catrev s t = rev s ++ t.

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

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

Lemma rev_cat s t : rev (s ++ t) = rev t ++ rev s.

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

Lemma revK : involutive rev.

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

Lemma filter_rev a s : filter a (rev s) = rev (filter a s).

Lemma count_rev a s : count a (rev s) = count a s.

Lemma has_rev a s : has a (rev s) = has a s.

Lemma all_rev a s : all a (rev s) = all a s.

Lemma rev_nseq n x : rev (nseq n x) = nseq n x.

End Sequences.



Notation count_mem x := (count (pred_of_simpl (pred1 x))).

Infix "++" := cat : seq_scope.

Notation "[ 'seq' x <- s | C ]" := (filter (fun xC%B) s)
 (at level 0, x at level 99,
  format "[ '[hv' 'seq' x <- s '/ ' | C ] ']'") : seq_scope.
Notation "[ 'seq' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
 (at level 0, x at level 99,
  format "[ '[hv' 'seq' x <- s '/ ' | C1 '/ ' & C2 ] ']'") : seq_scope.
Notation "[ 'seq' x : T <- s | C ]" := (filter (fun x : TC%B) s)
 (at level 0, x at level 99, only parsing).
Notation "[ 'seq' x : T <- s | C1 & C2 ]" := [seq x : T <- s | C1 && C2]
 (at level 0, x at level 99, only parsing).

Double induction/recursion.
Lemma seq_ind2 {S T} (P : seq S seq T Type) :
    P [::] [::]
    ( x y s t, size s = size t P s t P (x :: s) (y :: t))
   s t, size s = size t P s t.

Section RotRcons.

Variable T : Type.
Implicit Types (x : T) (s : seq T).

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

Lemma rcons_inj s1 s2 x1 x2 :
  rcons s1 x1 = rcons s2 x2 :> seq T (s1, x1) = (s2, x2).

Lemma rcons_injl x : injective (rcons^~ x).

Lemma rcons_injr s : injective (rcons s).

End RotRcons.


Equality and eqType for seq.

Section EqSeq.

Variables (n0 : nat) (T : eqType) (x0 : T).
Implicit Types (x y z : T) (s : seq 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 seq_eqMixin := EqMixin eqseqP.
Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.

Lemma eqseqE : eqseq = eq_op.

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

Lemma eqseq_cat s1 s2 s3 s4 :
  size s1 = size s2 (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).

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

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

Lemma has_filter a s : has a s = (filter a 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 seq_eqclass := seq T.
Identity Coercion seq_of_eqclass : seq_eqclass >-> seq.
Coercion pred_of_seq (s : seq_eqclass) : {pred T} := mem_seq s.

Canonical seq_predType := PredType (pred_of_seq : seq T pred T).
The line below makes mem_seq a canonical instance of topred.
Canonical mem_seq_predType := PredType mem_seq.

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

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

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

 (* to be repeated after the Section discharge. *)
Let inE := (mem_seq1, in_cons, inE).

Lemma mem_seq2 x y z : (x \in [:: y; z]) = xpred2 y z x.

Lemma mem_seq3 x y z t : (x \in [:: y; z; t]) = xpred3 y z t x.

Lemma mem_seq4 x y z t u : (x \in [:: y; z; t; u]) = xpred4 y z t u x.

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

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

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

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

Lemma mem_behead s : {subset behead s s}.

Lemma mem_belast s y : {subset belast y s y :: s}.

Lemma mem_nth s n : n < size s nth s n \in s.

Lemma mem_take s x : x \in take n0 s x \in s.

Lemma mem_drop s x : x \in drop n0 s x \in s.

Lemma last_eq s z x y : x != y z != y (last x s == y) = (last z s == y).

Section Filters.

Implicit Type a : pred T.

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

Lemma allP {a s} : reflect {in s, x, a x} (all a s).

Lemma hasPn a s : reflect {in s, x, ~~ a x} (~~ has a s).

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

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

Variables (a : pred T) (s : seq T) (A : T Prop).
Hypothesis aP : x, reflect (A x) (a x).

Lemma hasPP : reflect (exists2 x, x \in s & A x) (has a s).

Lemma allPP : reflect {in s, x, A x} (all a s).

End Filters.

Notation "'has_ view" := (hasPP _ (fun _view))
  (at level 4, right associativity, format "''has_' view").
Notation "'all_ view" := (allPP _ (fun _view))
  (at level 4, right associativity, format "''all_' view").

Section EqIn.

Variables a1 a2 : pred T.

Lemma eq_in_filter s : {in s, a1 =1 a2} filter a1 s = filter a2 s.

Lemma eq_in_find s : {in s, a1 =1 a2} find a1 s = find a2 s.

Lemma eq_in_count s : {in s, a1 =1 a2} count a1 s = count a2 s.

Lemma eq_in_all s : {in s, a1 =1 a2} all a1 s = all a2 s.

Lemma eq_in_has s : {in s, a1 =1 a2} has a1 s = has a2 s.

End EqIn.

Lemma eq_has_r s1 s2 : s1 =i s2 has^~ s1 =1 has^~ s2.

Lemma eq_all_r s1 s2 : s1 =i s2 all^~ s1 =1 all^~ s2.

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

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

Lemma mem_rev s : rev s =i 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 x s : reflect (s = nseq (size s) x) (all (pred1 x) s).

Lemma all_pred1_constant x s : all (pred1 x) s constant s.

Lemma all_pred1_nseq x n : all (pred1 x) (nseq n x).

Lemma mem_nseq n x y : (y \in nseq n x) = (0 < n) && (y == x).

Lemma nseqP n x y : reflect (y = x n > 0) (y \in nseq n x).

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

Uses x0
Lemma constantP s : reflect ( 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 x s : uniq (x :: s) = (x \notin s) && uniq s.

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

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

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

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

Lemma filter_uniq s a : uniq s uniq (filter a s).

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

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

Lemma count_memPn x s : reflect (count_mem x s = 0) (x \notin s).

Lemma count_uniq_mem s x : uniq s count_mem x s = (x \in s).

Lemma filter_pred1_uniq s x : uniq s x \in s filter (pred1 x) s = [:: x].

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 s : size (undup s) size s.

Lemma mem_undup s : undup s =i s.

Lemma undup_uniq s : uniq (undup s).

Lemma undup_id s : uniq s undup s = s.

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

Lemma filter_undup p s : filter p (undup s) = undup (filter p s).

Lemma undup_nil s : undup s = [::] s = [::].

Lemma undup_cat s t :
  undup (s ++ t) = [seq x <- undup s | x \notin t] ++ undup t.

Lemma undup_rcons s x : undup (rcons s x) = rcons [seq y <- undup s | y != x] x.

Lookup

Definition index x := find (pred1 x).

Lemma index_size x s : index x s size s.

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

Lemma nth_index x s : x \in s nth s (index x s) = x.

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

Lemma nthK s: uniq s {in gtn (size s), cancel (nth s) (index^~ s)}.

Lemma index_uniq i s : i < size s uniq s index (nth s i) s = i.

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

Lemma index_last x s : uniq (x :: s) index (last x s) (x :: s) = size s.

Lemma nth_uniq s i j :
  i < size s j < size s uniq s (nth s i == nth s j) = (i == j).

Lemma uniqPn s :
  reflect ( i j, [/\ i < j, j < size s & nth s i = nth s j]) (~~ uniq s).

Lemma uniqP s : reflect {in gtn (size s) &, injective (nth s)} (uniq s).

Lemma mem_rot s : rot n0 s =i s.

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

End EqSeq.

Section RotIndex.
Variables (T : eqType).
Implicit Types x y z : T.

Lemma rot_index s x (i := index x s) : x \in s
  rot i s = x :: (drop i.+1 s ++ take i s).

Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.

Lemma rot_to s x : x \in s rot_to_spec s x.

End RotIndex.

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



Section NthTheory.

Lemma nthP (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 (a : pred T) s x0 :
  reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).

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

End NthTheory.

Lemma set_nth_default T s (y0 x0 : T) n : n < size s nth x0 s n = nth y0 s n.

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


Definition bitseq := seq bool.
Canonical bitseq_eqType := Eval hnf in [eqType of bitseq].
Canonical 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 i {struct i} :=
  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 v i j : nth 0 (incr_nth v i) j = (i == j) + nth 0 v j.

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

Lemma incr_nth_inj v : injective (incr_nth v).

Lemma incr_nthC v i j :
  incr_nth (incr_nth v i) j = incr_nth (incr_nth v j) i.

Equality up to permutation

Section PermSeq.

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

Definition perm_eq s1 s2 :=
  all [pred x | count_mem x s1 == count_mem x s2] (s1 ++ s2).

Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).

Lemma perm_refl s : perm_eq s s.
Hint Resolve perm_refl : core.

Lemma perm_sym : symmetric perm_eq.

Lemma perm_trans : transitive perm_eq.

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

Lemma permEl s1 s2 : perm_eql s1 s2 perm_eq s1 s2.

Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).

Lemma permPr s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2).

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

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

Lemma perm_catl s t1 t2 : perm_eq t1 t2 perm_eql (s ++ t1) (s ++ t2).

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

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

Lemma perm_catr s1 s2 t : perm_eq s1 s2 perm_eql (s1 ++ t) (s2 ++ t).

Lemma perm_cat s1 s2 t1 t2 :
  perm_eq s1 s2 perm_eq t1 t2 perm_eq (s1 ++ t1) (s2 ++ t2).

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

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

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

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

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

Lemma perm_rev s : perm_eql (rev s) s.

Lemma perm_filter s1 s2 a :
  perm_eq s1 s2 perm_eq (filter a s1) (filter a s2).

Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.

Lemma perm_size s1 s2 : perm_eq s1 s2 size s1 = size s2.

Lemma perm_mem s1 s2 : perm_eq s1 s2 s1 =i s2.

Lemma perm_nilP s : reflect (s = [::]) (perm_eq s [::]).

Lemma perm_consP x s t :
  reflect ( i u, rot i t = x :: u perm_eq u s)
          (perm_eq t (x :: s)).

Lemma perm_has s1 s2 a : perm_eq s1 s2 has a s1 = has a s2.

Lemma perm_all s1 s2 a : perm_eq s1 s2 all a s1 = all a s2.

Lemma perm_small_eq s1 s2 : size s2 1 perm_eq s1 s2 s1 = s2.

Lemma uniq_leq_size s1 s2 : uniq s1 {subset s1 s2} size s1 size s2.

Lemma leq_size_uniq s1 s2 :
  uniq s1 {subset s1 s2} size s2 size s1 uniq s2.

Lemma uniq_size_uniq s1 s2 :
  uniq s1 s1 =i s2 uniq s2 = (size s2 == size s1).

Lemma uniq_min_size s1 s2 :
    uniq s1 {subset s1 s2} size s2 size s1
  (size s1 = size s2) × (s1 =i s2).

Lemma eq_uniq s1 s2 : size s1 = size s2 s1 =i s2 uniq s1 = uniq s2.

Lemma perm_uniq s1 s2 : perm_eq s1 s2 uniq s1 = uniq s2.

Lemma uniq_perm s1 s2 : uniq s1 uniq s2 s1 =i s2 perm_eq s1 s2.

Lemma perm_undup s1 s2 : s1 =i s2 perm_eq (undup s1) (undup s2).

Lemma count_mem_uniq s : ( x, count_mem x s = (x \in s)) uniq s.

Lemma catCA_perm_ind P :
    ( s1 s2 s3, P (s1 ++ s2 ++ s3) P (s2 ++ s1 ++ s3))
  ( s1 s2, perm_eq s1 s2 P s1 P s2).

Lemma catCA_perm_subst R F :
    ( s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R)
  ( s1 s2, perm_eq s1 s2 F s1 = F s2).

End PermSeq.

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

Hint Resolve perm_refl : core.

Section RotrLemmas.

Variables (n0 : nat) (T : Type) (T' : eqType).
Implicit Types (x : T) (s : seq T).

Lemma size_rotr s : size (rotr n0 s) = size s.

Lemma mem_rotr (s : seq T') : rotr n0 s =i s.

Lemma rotr_size_cat s1 s2 : rotr (size s2) (s1 ++ s2) = s2 ++ s1.

Lemma rotr1_rcons x s : rotr 1 (rcons s x) = x :: s.

Lemma has_rotr a s : has a (rotr n0 s) = has a s.

Lemma rotr_uniq (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 take_rev s : take n0 (rev s) = rev (drop (size s - n0) s).

Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).

Lemma rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).

Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).

End RotrLemmas.


Section RotCompLemmas.

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

Lemma rot_addn m n s : m + n size s rot (m + n) s = rot m (rot n s).

Lemma rotS n s : n < size s rot n.+1 s = rot 1 (rot n s).

Lemma rot_add_mod m n s : 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 m n s : rot m (rot n s) = rot n (rot m s).

Lemma rot_rotr m n s : rot m (rotr n s) = rotr n (rot m s).

Lemma rotr_rotr m n s : rotr m (rotr n s) = rotr n (rotr m s).

End RotCompLemmas.

Section Mask.

Variables (n0 : nat) (T : Type).
Implicit Types (m : bitseq) (s : seq T).

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

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

Lemma mask_true s n : size s n mask (nseq n true) s = s.

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

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

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

Lemma size_mask m s : size m = size s size (mask m s) = count id m.

Lemma mask_cat m1 m2 s1 s2 :
  size m1 = size s1 mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.

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

Lemma has_mask a m s : has a (mask m s) has a s.

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

Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s}.

End Mask.

Section EqMask.

Variables (n0 : nat) (T : eqType).
Implicit Types (s : seq T) (m : bitseq).

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

Lemma mem_mask x m s : x \in mask m s x \in s.

Lemma mask_uniq s : uniq s m, uniq (mask m s).

Lemma mem_mask_rot m s :
  size m = size s mask (rot n0 m) (rot n0 s) =i mask m s.

End EqMask.

Section Subseq.

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

Fixpoint subseq s1 s2 :=
  if s2 is y :: s2' then
    if s1 is x :: s1' then subseq (if x == y then s1' else s1) s2' else true
  else s1 == [::].

Lemma sub0seq s : subseq [::] s.

Lemma subseq0 s : subseq s [::] = (s == [::]).

Lemma subseq_refl s : subseq s s.
Hint Resolve subseq_refl : core.

Lemma subseqP s1 s2 :
  reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2).

Lemma mask_subseq m s : subseq (mask m s) s.

Lemma subseq_trans : transitive subseq.

Lemma cat_subseq s1 s2 s3 s4 :
  subseq s1 s3 subseq s2 s4 subseq (s1 ++ s2) (s3 ++ s4).

Lemma prefix_subseq s1 s2 : subseq s1 (s1 ++ s2).

Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2).

Lemma take_subseq s i : subseq (take i s) s.

Lemma drop_subseq s i : subseq (drop i s) s.

Lemma mem_subseq s1 s2 : subseq s1 s2 {subset s1 s2}.

Lemma sub1seq x s : subseq [:: x] s = (x \in s).

Lemma size_subseq s1 s2 : subseq s1 s2 size s1 size s2.

Lemma size_subseq_leqif s1 s2 :
  subseq s1 s2 size s1 size s2 ?= iff (s1 == s2).

Lemma subseq_cons s x : subseq s (x :: s).

Lemma subseq_rcons s x : subseq s (rcons s x).

Lemma subseq_uniq s1 s2 : subseq s1 s2 uniq s2 uniq s1.

End Subseq.


Hint Resolve subseq_refl : core.

Section Rem.

Variables (T : eqType) (x : T).

Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s.

Lemma rem_id s : x \notin s rem s = s.

Lemma perm_to_rem s : x \in s perm_eq s (x :: rem s).

Lemma size_rem s : x \in s size (rem s) = (size s).-1.

Lemma rem_subseq s : subseq (rem s) s.

Lemma rem_uniq s : uniq s uniq (rem s).

Lemma mem_rem s : {subset rem s s}.

Lemma rem_filter s : uniq s rem s = filter (predC1 x) s.

Lemma mem_rem_uniq s : uniq s rem s =i [predD1 s & x].

Lemma mem_rem_uniqF s : uniq s x \in rem s = false.

End Rem.

Section Map.

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

Fixpoint map s := if s is x :: s' then f x :: map s' else [::].

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

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

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

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

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

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

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

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

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

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

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

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

Lemma all_map a s : all a (map s) = all (preim f a) s.

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

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

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

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

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

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

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

Lemma inj_map : injective f injective map.

End Map.

Notation "[ 'seq' E | i <- s ]" := (map (fun iE) s)
  (at level 0, E at level 99, i ident,
   format "[ '[hv' 'seq' E '/ ' | i <- s ] ']'") : seq_scope.

Notation "[ 'seq' E | i <- s & C ]" := [seq E | i <- [seq i <- s | C]]
(at level 0, E at level 99, i ident,
   format "[ '[hv' 'seq' E '/ ' | i <- s '/ ' & C ] ']'") : seq_scope.

Notation "[ 'seq' E | i : T <- s ]" := (map (fun i : TE) s)
  (at level 0, E at level 99, i ident, only parsing) : seq_scope.

Notation "[ 'seq' E | i : T <- s & C ]" :=
  [seq E | i : T <- [seq i : T <- s | C]]
(at level 0, E at level 99, i ident, only parsing) : seq_scope.

Notation "[ 'seq' E : R | i <- s ]" := (@map _ R (fun iE) s)
  (at level 0, E at level 99, i ident, only parsing) : seq_scope.

Notation "[ 'seq' E : R | i <- s & C ]" := [seq E : R | i <- [seq i <- s | C]]
(at level 0, E at level 99, i ident, only parsing) : seq_scope.

Notation "[ 'seq' E : R | i : T <- s ]" := (@map T R (fun i : TE) s)
  (at level 0, E at level 99, i ident, only parsing) : seq_scope.

Notation "[ 'seq' E : R | i : T <- s & C ]" :=
  [seq E : R | i : T <- [seq i : T <- s | C]]
(at level 0, E at level 99, i ident, only parsing) : seq_scope.

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

Lemma mask_filter (T : eqType) (s : seq T) (m : bitseq) :
  uniq s mask m s = [seq i <- s | i \in mask m s].

Section FilterSubseq.

Variable T : eqType.
Implicit Types (s : seq T) (a : pred T).

Lemma filter_subseq a s : subseq (filter a s) s.

Lemma subseq_filter s1 s2 a :
  subseq s1 (filter a s2) = all a s1 && subseq s1 s2.

Lemma subseq_uniqP s1 s2 :
  uniq s2 reflect (s1 = filter (mem s1) s2) (subseq s1 s2).

Lemma perm_to_subseq s1 s2 :
  subseq s1 s2 {s3 | perm_eq s2 (s1 ++ s3)}.

End FilterSubseq.


Section EqMap.

Variables (n0 : nat) (T1 : eqType) (x1 : T1).
Variables (T2 : eqType) (x2 : T2) (f : T1 T2).
Implicit Type s : seq T1.

Lemma map_f s x : x \in s f x \in map f s.

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

Lemma map_uniq s : uniq (map f s) uniq s.

Lemma map_inj_in_uniq s : {in s &, injective f} uniq (map f s) = uniq s.

Lemma map_subseq s1 s2 : subseq s1 s2 subseq (map f s1) (map f s2).

Lemma nth_index_map s x0 x :
  {in s &, injective f} x \in s nth x0 s (index (f x) (map f s)) = x.

Lemma perm_map s t : perm_eq s t perm_eq (map f s) (map f t).

Hypothesis Hf : injective f.

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

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

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

Lemma perm_map_inj s t : perm_eq (map f s) (map f t) perm_eq s t.

End EqMap.


Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) :
  {f | uniq s size fs = size s map f s = fs}.

Section MapComp.

Variable T1 T2 T3 : Type.

Lemma map_id (s : seq T1) : map id s = s.

Lemma eq_map (f1 f2 : T1 T2) : f1 =1 f2 map f1 =1 map f2.

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

Lemma mapK (f1 : T1 T2) (f2 : T2 T1) :
  cancel f1 f2 cancel (map f1) (map f2).

End MapComp.

Lemma eq_in_map (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 (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 let r := pmap s' in oapp (cons^~ r) r (f x) else [::].

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

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

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

Hypothesis fK : ocancel f g.

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

Lemma pmap_cat s t : pmap (s ++ t) = pmap s ++ pmap t.

Lemma all_pmap (p : pred rT) s :
  all p (pmap s) = all [pred i | oapp p true (f i)] s.

End Pmap.

Section EqPmap.

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

Lemma eq_pmap (f1 f2 : aT option rT) : f1 =1 f2 pmap f1 =1 pmap f2.

Lemma mem_pmap 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 s u, (u \in pmap f s) = (g u \in s).

Lemma pmap_uniq s : uniq s uniq (pmap f s).

Lemma perm_pmap s t : perm_eq s t perm_eq (pmap f s) (pmap f t).

End EqPmap.

Section PmapSub.

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

Lemma size_pmap_sub s : size (pmap (insub : T option sT) s) = count p s.

End PmapSub.

Section EqPmapSub.

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

Let insT : T option sT := insub.

Lemma mem_pmap_sub s u : (u \in pmap insT s) = (val u \in s).

Lemma pmap_sub_uniq s : uniq s uniq (pmap insT s).

End EqPmapSub.

Index sequence

Fixpoint iota m n := if n is n'.+1 then m :: iota m.+1 n' else [::].

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

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

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

Lemma nth_iota p m n i : i < n nth p (iota m n) i = m + i.

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

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

Lemma take_iota k m n : take k (iota m n) = iota m (minn k n).

Lemma drop_iota k m n : drop k (iota m n) = iota (m + k) (n - k).

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 f n : size (mkseq f n) = n.

Lemma eq_mkseq f g : f =1 g mkseq f =1 mkseq g.

Lemma nth_mkseq f n i : i < n nth x0 (mkseq f n) i = f i.

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

End MakeSeq.

Section MakeEqSeq.

Variable T : eqType.

Lemma mkseq_uniq (f : nat T) n : injective f uniq (mkseq f n).

Lemma perm_iotaP {s t : seq T} x0 (It := iota 0 (size t)) :
  reflect (exists2 Is, perm_eq Is It & s = map (nth x0 t) Is) (perm_eq s t).

End MakeEqSeq.


Section FoldRight.

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

Fixpoint foldr s := 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 s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.

Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x zf (h x) z) z0 s.

End FoldRightComp.

Quick characterization of the null sequence.

Definition sumn := foldr addn 0.

Lemma sumn_nseq x n : sumn (nseq n x) = x × n.

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

Lemma sumn_count T (a : pred T) s : sumn [seq a i : nat | i <- s] = count a s.

Lemma sumn_rcons s n : sumn (rcons s n) = sumn s + n.

Lemma perm_sumn s1 s2 : perm_eq s1 s2 sumn s1 = sumn s2.

Lemma sumn_rot s n : sumn (rot n s) = sumn s.

Lemma sumn_rev s : sumn (rev s) = sumn s.

Lemma natnseq0P s : reflect (s = nseq (size s) 0) (sumn s == 0).

Section FoldLeft.

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

Fixpoint foldl z s := if s is x :: s' then foldl (f z x) s' else z.

Lemma foldl_rev z s : foldl z (rev s) = foldr (fun x zf z x) z s.

Lemma foldl_cat 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 := if s is y :: s' then f x y :: pairmap y s' else [::].

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

Lemma pairmap_cat x s1 s2 :
  pairmap x (s1 ++ s2) = pairmap x s1 ++ pairmap (last x s1) s2.

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

Fixpoint scanl x s :=
  if s is y :: s' then let x' := g x y in x' :: scanl x' s' else [::].

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

Lemma scanl_cat x s1 s2 :
  scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2.

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

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

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

End Scan.


Section Zip.

Variables S T : Type.

Fixpoint zip (s : seq S) (t : seq T) {struct t} :=
  match s, t with
  | x :: s', y :: t'(x, y) :: zip s' t'
  | _, _[::]
  end.

Definition unzip1 := map (@fst S T).
Definition unzip2 := map (@snd S T).

Fixpoint all2 (r : S T bool) s t :=
  match s, t with
  | [::], [::]true
  | x :: s, y :: tr x y && all2 r s t
  | _, _false
  end.

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

Lemma unzip1_zip s t : size s size t unzip1 (zip s t) = s.

Lemma unzip2_zip s t : size t size s unzip2 (zip s t) = t.

Lemma size1_zip s t : size s size t size (zip s t) = size s.

Lemma size2_zip s t : size t size s size (zip s t) = size t.

Lemma size_zip s t : size (zip s t) = minn (size s) (size t).

Lemma zip_cat s1 s2 t1 t2 :
  size s1 = size t1 zip (s1 ++ s2) (t1 ++ t2) = zip s1 t1 ++ zip s2 t2.

Lemma nth_zip x y s t i :
  size s = size t nth (x, y) (zip s t) i = (nth x s i, nth y t i).

Lemma nth_zip_cond p s t i :
   nth p (zip s t) i
     = (if i < size (zip s t) then (nth p.1 s i, nth p.2 t i) else p).

Lemma zip_rcons s t x y :
  size s = size t zip (rcons s x) (rcons t y) = rcons (zip s t) (x, y).

Lemma rev_zip s t : size s = size t rev (zip s t) = zip (rev s) (rev t).

Lemma all2E r s t :
  all2 r s t = (size s == size t) && all [pred xy | r xy.1 xy.2] (zip s t).

End Zip.


Section Flatten.

Variable T : Type.
Implicit Types (s : seq T) (ss : seq (seq T)).

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

Definition flatten_index sh r c := sumn (take r sh) + c.
Definition reshape_index sh i := find (pred1 0) (scanl subn i.+1 sh).
Definition reshape_offset sh i := i - sumn (take (reshape_index sh i) sh).

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

Lemma flatten_cat ss1 ss2 : flatten (ss1 ++ ss2) = flatten ss1 ++ flatten ss2.

Lemma size_reshape sh s : size (reshape sh s) = size sh.

Lemma nth_reshape (sh : seq nat) l n :
  nth [::] (reshape sh l) n = take (nth 0 sh n) (drop (sumn (take n sh)) l).

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

Lemma reshapeKr sh s : size s sumn sh flatten (reshape sh s) = s.

Lemma reshapeKl sh s : size s sumn sh shape (reshape sh s) = sh.

Lemma flatten_rcons ss s : flatten (rcons ss s) = flatten ss ++ s.

Lemma flatten_seq1 s : flatten [seq [:: x] | x <- s] = s.

Lemma count_flatten ss P :
  count P (flatten ss) = sumn [seq count P x | x <- ss].

Lemma filter_flatten ss (P : pred T) :
  filter P (flatten ss) = flatten [seq filter P i | i <- ss].

Lemma rev_flatten ss :
  rev (flatten ss) = flatten (rev (map rev ss)).

Lemma nth_shape ss i : nth 0 (shape ss) i = size (nth [::] ss i).

Lemma shape_rev ss : shape (rev ss) = rev (shape ss).

Lemma eq_from_flatten_shape ss1 ss2 :
  flatten ss1 = flatten ss2 shape ss1 = shape ss2 ss1 = ss2.

Lemma rev_reshape sh s :
  size s = sumn sh rev (reshape sh s) = map rev (reshape (rev sh) (rev s)).

Lemma reshape_rcons s sh n (m := sumn sh) :
  m + n = size s
  reshape (rcons sh n) s = rcons (reshape sh (take m s)) (drop m s).

Lemma flatten_indexP sh r c :
  c < nth 0 sh r flatten_index sh r c < sumn sh.

Lemma reshape_indexP sh i : i < sumn sh reshape_index sh i < size sh.

Lemma reshape_offsetP sh i :
  i < sumn sh reshape_offset sh i < nth 0 sh (reshape_index sh i).

Lemma reshape_indexK sh i :
  flatten_index sh (reshape_index sh i) (reshape_offset sh i) = i.

Lemma flatten_indexKl sh r c :
  c < nth 0 sh r reshape_index sh (flatten_index sh r c) = r.

Lemma flatten_indexKr sh r c :
  c < nth 0 sh r reshape_offset sh (flatten_index sh r c) = c.

Lemma nth_flatten x0 ss i (r := reshape_index (shape ss) i) :
  nth x0 (flatten ss) i = nth x0 (nth [::] ss r) (reshape_offset (shape ss) i).

Lemma reshape_leq sh i1 i2
  (r1 := reshape_index sh i1) (c1 := reshape_offset sh i1)
  (r2 := reshape_index sh i2) (c2 := reshape_offset sh i2) :
  (i1 i2) = ((r1 < r2) || ((r1 == r2) && (c1 c2))).

End Flatten.


Lemma map_flatten S T (f : T S) ss :
  map f (flatten ss) = flatten (map (map f) ss).

Lemma flatten_map1 (S T : Type) (f : S T) s :
  flatten [seq [:: f x] | x <- s] = map f s.

Lemma undup_flatten_nseq n (T : eqType) (s : seq T) : 0 < n
  undup (flatten (nseq n s)) = undup s.

Lemma sumn_flatten (ss : seq (seq nat)) :
  sumn (flatten ss) = sumn (map sumn ss).

Lemma map_reshape T S (f : T S) sh s :
  map (map f) (reshape sh s) = reshape sh (map f s).

Section EqFlatten.

Variables S T : eqType.

Lemma flattenP (A : seq (seq T)) x :
  reflect (exists2 s, s \in A & x \in s) (x \in flatten A).

Lemma flatten_mapP (A : S seq T) s y :
  reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)).

Lemma perm_flatten (ss1 ss2 : seq (seq T)) :
  perm_eq ss1 ss2 perm_eq (flatten ss1) (flatten ss2).

End EqFlatten.


Notation "[ 'seq' E | x <- s , y <- t ]" :=
  (flatten [seq [seq E | y <- t] | x <- s])
  (at level 0, E at level 99, x ident, y ident,
   format "[ '[hv' 'seq' E '/ ' | x <- s , '/ ' y <- t ] ']'")
   : seq_scope.
Notation "[ 'seq' E | x : S <- s , y : T <- t ]" :=
  (flatten [seq [seq E | y : T <- t] | x : S <- s])
  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
Notation "[ 'seq' E : R | x : S <- s , y : T <- t ]" :=
  (flatten [seq [seq E : R | y : T <- t] | x : S <- s])
  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
Notation "[ 'seq' E : R | x <- s , y <- t ]" :=
  (flatten [seq [seq E : R | y <- t] | x <- s])
  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.

Section AllPairsDep.

Variables (S S' : Type) (T T' : S Type) (R : Type).
Implicit Type f : x, T x R.

Definition allpairs_dep f s t := [seq f x y | x <- s, y <- t x].

Lemma size_allpairs_dep f s t :
  size [seq f x y | x <- s, y <- t x] = sumn [seq size (t x) | x <- s].

Lemma eq_allpairs (f1 f2 : x, T x R) s t :
    ( x, f1 x =1 f2 x)
  [seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].

Lemma allpairs_cat f s1 s2 t :
  [seq f x y | x <- s1 ++ s2, y <- t x] =
    [seq f x y | x <- s1, y <- t x] ++ [seq f x y | x <- s2, y <- t x].

Lemma allpairs_mapl f (g : S' S) s t :
  [seq f x y | x <- map g s, y <- t x] = [seq f (g x) y | x <- s, y <- t (g x)].

Lemma allpairs_mapr f (g : x, T' x T x) s t :
  [seq f x y | x <- s, y <- map (g x) (t x)] =
    [seq f x (g x y) | x <- s, y <- t x].

End AllPairsDep.


Lemma map_allpairs S T R R' (g : R' R) f s t :
  map g [seq f x y | x : S <- s, y : T x <- t x] =
    [seq g (f x y) | x <- s, y <- t x].

Section AllPairsNonDep.

Variables (S T R : Type) (f : S T R).
Implicit Types (s : seq S) (t : seq T).

Definition allpairs s t := [seq f x y | x <- s, y <- t].

Lemma size_allpairs s t : size [seq f x y | x <- s, y <- t] = size s × size t.

End AllPairsNonDep.


Section EqAllPairsDep.

Variables (S : eqType) (T : S eqType).
Implicit Types (R : eqType) (s : seq S) (t : x, seq (T x)).

Lemma allpairsPdep R (f : x, T x R) s t (z : R) :
  reflect ( x y, [/\ x \in s, y \in t x & z = f x y])
          (z \in [seq f x y | x <- s, y <- t x]).

Variable R : eqType.
Implicit Type f : x, T