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). infix s1 s2 <=> s1 is a contiguous subsequence of s2, i.e., s ++ s1 ++ s' = s2 for some sequences s, s'. prefix s1 s2 <=> s1 is a subchain of s2 appearing at the beginning of s2. suffix s1 s2 <=> s1 is a subchain of s2 appearing at the end of s2. infix_index s1 s2 <=> the first index at which s1 appears in s2, or (size s2).+1 if infix s1 s2 is false. 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 y]

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] allrel r xs ys := all [pred x | all (r x) ys] xs <=> r x y holds whenever x is in xs and y is in ys all2rel r xs := allrel r xs xs <=> the proposition r x y holds for all possible x, y in xs. pairwise r xs <=> the relation r holds for any i-th and j-th element of xs such that i < j. 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.

Declare Scope seq_scope.

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.
Bind Scope seq_scope with list.
Arguments cons {T%type} x s%SEQ : rename.
Arguments nil {T%type} : rename.
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 nseqD 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.

Lemma cat_nilp s1 s2 : nilp (s1 ++ s2) = nilp s1 && nilp 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 if_nth s b n : b || (size s n)
  (if b then nth s n else x0) = nth s n.

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

Lemma nth_seq1 n x : nth [:: x] n = if n == 0 then x else 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 hasNfind s : ~~ has s find s = size s.

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 find_pred0 s : find pred0 s = size s.

Lemma find_predT s : find predT s = 0.

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 allT (a : pred T) s : ( x, a x) all a 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 size_take_min s : size (take n0 s) = minn n0 (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 find_ltn p s i : has p (take i s) find p s < i.

Lemma has_take p s i : has p s has p (take i s) = (find p s < i).

Lemma has_take_leq (p : pred T) (s : seq T) i : i size s
  has p (take i s) = (find p s < i).

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

Lemma take_min i j s : take (minn i j) s = take i (take j s).

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

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

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

Lemma takeD 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_nilp s : nilp (rev s) = nilp 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.

Arguments seqn {T} n.
Arguments rev {T} s : simpl never.
Arguments nth : simpl nomatch.
Arguments set_nth : simpl nomatch.
Arguments take : simpl nomatch.
Arguments drop : simpl nomatch.

Arguments nilP {T s}.
Arguments all_filterP {T a s}.
Arguments rotK n0 {T} s : rename.
Arguments rot_inj {n0 T} [s1 s2] eq_rot_s12 : rename.
Arguments revK {T} s : rename.

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 <- s | C ]" := (filter (fun xC%B) s)
 (at level 0, x strict pattern,
  format "[ '[hv' 'seq' ' x <- s '/ ' | C ] ']'") : seq_scope.
Notation "[ 'seq' ' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
 (at level 0, x strict pattern,
  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).

#[deprecated(since="mathcomp 1.16",
             note="Use take_takel or take_min instead")]
Notation take_take := take_takel.

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 FindSpec.
Variable (T : Type) (a : {pred T}) (s : seq T).

Variant find_spec : bool nat Type :=
| NotFound of ~~ has a s : find_spec false (size s)
| Found (i : nat) of i < size s & ( x0, a (nth x0 s i)) &
  ( x0 j, j < i a (nth x0 s j) = false) : find_spec true i.

Lemma findP : find_spec (has a s) (find a s).

End FindSpec.
Arguments findP {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.

Arguments rcons_inj {T s1 x1 s2 x2} eq_rcons : rename.
Arguments rcons_injl {T} x [s1 s2] eq_rcons : rename.
Arguments rcons_injr {T} s [x1 x2] eq_rcons : rename.

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 nilpE s : nilp s = (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 forall_cons {P : T Prop} {a s} :
  {in a::s, x, P x} P a {in s, x, P x}.

Lemma exists_cons {P : T Prop} {a s} :
  (exists2 x, x \in a::s & P x) P a exists2 x, x \in s & P x.

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 allss s : all [in s] 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 [in s1] s2 = has [in 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.
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.

Lemma count_undup s p : count p (undup s) count p s.

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 memNindex x s : x \notin s index x s = size 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 index_ltn x s i : x \in take i s index x s < i.

Lemma in_take x s i : x \in s (x \in take i s) = (index x s < i).

Lemma in_take_leq x s i : i size s (x \in take i s) = (index x s < i).

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

Lemma drop_index s (n := index x0 s) : x0 \in s drop n s = x0 :: drop n.+1 s.

lemmas about the pivot pattern [ ++ _ :: _ ]

Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1
  index x s = size s1.

Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1
  take (index x s) s = s1.

Lemma rev_pivot x s1 s2 : rev (s1 ++ x :: s2) = rev s2 ++ x :: rev s1.

Lemma eqseq_pivot2l x s1 s2 s3 s4 : x \notin s1 x \notin s3
  (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).

Lemma eqseq_pivot2r x s1 s2 s3 s4 : x \notin s2 x \notin s4
  (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).

Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 x \notin s2
  (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).

Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 x \notin s4
  (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).

Lemma uniq_eqseq_pivotl x s1 s2 s3 s4 : uniq (s1 ++ x :: s2)
  (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).

Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4)
  (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).

End EqSeq.
Arguments eqseq : simpl nomatch.

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


Arguments eqseq {T} !_ !_.
Arguments pred_of_seq {T} s x /.
Arguments eqseqP {T x y}.
Arguments hasP {T a s}.
Arguments hasPn {T a s}.
Arguments allP {T a s}.
Arguments allPn {T a s}.
Arguments nseqP {T n x y}.
Arguments count_memPn {T x s}.
Arguments uniqPn {T} x0 {s}.
Arguments uniqP {T} x0 {s}.
Arguments forall_cons {T P a s}.
Arguments exists_cons {T P a s}.

Since both `all [in s] s`, `all (mem s) s`, and `all (pred_of_seq s) s` may appear in goals, the following hint has to be declared using the `Hint Extern` command. Additionally, `mem` and `pred_of_seq` in the above terms do not reduce to each other; thus, stating `allss` in the form of one of them makes `apply: allss` fail for the other case. Since both `mem` and `pred_of_seq` reduce to `mem_seq`, the following explicit type annotation for `allss` makes it work for both cases.
#[export] Hint Extern 0 (is_true (all _ _)) ⇒
  apply: (allss : T s, all (mem_seq s) s) : core.

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.
Implicit Types (a : pred T) (x : T).

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

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

Lemma set_nthE s x0 n x :
  set_nth x0 s n x = if n < size s
    then take n s ++ x :: drop n.+1 s
    else s ++ ncons (n - size s) x0 [:: x].

Lemma count_set_nth a s x0 n x :
  count a (set_nth x0 s n x) =
    count a s + a x - a (nth x0 s n) × (n < size s) + (a x0) × (n - size s).

Lemma count_set_nth_ltn a s x0 n x : n < size s
  count a (set_nth x0 s n x) = count a s + a x - a (nth x0 s n).

Lemma count_set_nthF a s x0 n x : ~~ a x0
  count a (set_nth x0 s n x) = count a s + a x - a (nth x0 s n).

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

Arguments nthP {T s x}.
Arguments has_nthP {T a s}.
Arguments all_nthP {T a s}.

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

Generalizations of splitP (from path.v): split_find_nth and split_find
Section FindNth.
Variables (T : Type).
Implicit Types (x : T) (p : pred T) (s : seq T).

Variant split_find_nth_spec p : seq T seq T seq T T Type :=
  FindNth x s1 s2 of p x & ~~ has p s1 :
    split_find_nth_spec p (rcons s1 x ++ s2) s1 s2 x.

Lemma split_find_nth x0 p s (i := find p s) :
  has p s split_find_nth_spec p s (take i s) (drop i.+1 s) (nth x0 s i).

Variant split_find_spec p : seq T seq T seq T Type :=
  FindSplit x s1 s2 of p x & ~~ has p s1 :
    split_find_spec p (rcons s1 x ++ s2) s1 s2.

Lemma split_find p s (i := find p s) :
  has p s split_find_spec p s (take i s) (drop i.+1 s).

Lemma nth_rcons_cat_find x0 p s1 s2 x (s := rcons s1 x ++ s2) :
   p x ~~ has p s1 nth x0 s (find p s) = x.

End FindNth.

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].
Arguments incr_nth : simpl nomatch.

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_catACA s1 s2 s3 s4 :
  perm_eql ((s1 ++ s2) ++ (s3 ++ s4)) ((s1 ++ s3) ++ (s2 ++ s4)).

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 eq_count_undup a s1 s2 :
  {in a, s1 =i s2} count a (undup s1) = count a (undup s2).

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

Arguments permP {T s1 s2}.
Arguments permPl {T s1 s2}.
Arguments permPr {T s1 s2}.
#[global] 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 rev_take s : rev (take n0 s) = drop (size s - n0) (rev s).

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

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

Arguments rotrK n0 {T} s : rename.
Arguments rotr_inj {n0 T} [s1 s2] eq_rotr_s12 : rename.

Section RotCompLemmas.

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

Lemma rotD 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_minn n s : rot n s = rot (minn n (size s)) s.

Definition rot_add s n m (k := size s) (p := minn m k + minn n k) :=
  locked (if p k then p else p - k).

Lemma leq_rot_add n m s : rot_add s n m size s.

Lemma rot_addC n m s : rot_add s n m = rot_add s m n.

Lemma rot_rot_add n m s : rot m (rot n s) = rot (rot_add s n m) 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 mask0s s : mask [::] s = [::].

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 mask_rcons b m x s : size m = size s
  mask (rcons m b) (rcons s x) = mask m s ++ nseq b x.

Lemma all_mask a m s : all a s all a (mask m s).

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 rev_mask m s : size m = size s rev (mask m s) = mask (rev m) (rev 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}.

Lemma takeEmask i s : take i s = mask (nseq i true) s.

Lemma dropEmask i s :
  drop i s = mask (nseq i false ++ nseq (size s - i) true) s.

End Mask.
Arguments 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 in_mask x m s :
  uniq s x \in mask m s = (x \in s) && nth false m (index x 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_anti : antisymmetric subseq.

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

Lemma cons_subseq s1 s2 x : subseq (x :: s1) s2 subseq s1 s2.

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

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

Lemma take_uniq s n : uniq s uniq (take n s).

Lemma drop_uniq s n : uniq s uniq (drop n s).

Lemma undup_subseq s : subseq (undup s) s.

Lemma subseq_rev s1 s2 : subseq (rev s1) (rev s2) = subseq s1 s2.

Lemma subseq_cat2l s s1 s2 : subseq (s ++ s1) (s ++ s2) = subseq s1 s2.

Lemma subseq_cat2r s s1 s2 : subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2.

Lemma subseq_rot p s n :
  subseq p s exists2 k, k n & subseq (rot k p) (rot n s).

End Subseq.

Arguments subseqP {T s1 s2}.

#[global] 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_cons y s : rem (y :: s) = if y == x then s else y :: rem s.

Lemma remE s : rem s = take (index x s) s ++ drop (index x s).+1 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.

Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x.

Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y).

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 all_mapT (a : pred T2) s : ( x, a (f x)) all a (map 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.

Lemma inj_in_map (A : {pred T1}) :
  {in A &, injective f} {in [pred s | all [in A] s] &, injective map}.

End Map.

Notation "[ 'seq' E | i <- s ]" := (map (fun iE) s)
  (at level 0, E at level 99, i binder,
   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 binder,
   format "[ '[hv' 'seq' E '/ ' | i <- s '/ ' & C ] ']'") : seq_scope.

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

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

Lemma all_sigP T a (s : seq T) : all a s {s' : seq (sig a) | s = map sval s'}.

Section MiscMask.

Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) count P s.

Variable (T : eqType).
Implicit Types (s : seq T) (m : bitseq).

Lemma mask_filter s m : uniq s mask m s = [seq i <- s | i \in mask m s].

Lemma leq_count_subseq P s1 s2 : subseq s1 s2 count P s1 count P s2.

Lemma count_maskP s1 s2 :
  ( x, count_mem x s1 count_mem x s2)
    exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2).

Lemma count_subseqP s1 s2 :
  ( x, count_mem x s1 count_mem x s2)
    exists2 s, subseq s s2 & perm_eq s1 s.

End MiscMask.

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 [in s1] s2) (subseq s1 s2).

Lemma uniq_subseq_pivot x (s1 s2 s3 s4 : seq T) (s := s3 ++ x :: s4) :
  uniq s subseq (s1 ++ x :: s2) s = (subseq s1 s3 && subseq s2 s4).

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

Lemma subseq_rem x : {homo rem x : s1 s2 / @subseq T s1 s2}.

End FilterSubseq.

Arguments subseq_uniqP [T s1 s2].

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 subset_mapP (s : seq T1) (s' : seq T2) :
    {subset s' map f s} exists2 t, all (mem s) t & s' = map f t.

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 (