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 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 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 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 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 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_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 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 : 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 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 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 (mem 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 (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.
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 (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` failing 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.
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.

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

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}.
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_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}.

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

Lemma sub_map s1 s2 : {subset s1 s2} {subset map f s1 map f s2}.

Lemma eq_mem_map s1 s2 : s1 =i s2 map f s1 =i map f s2.

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 undup_map_inj s : undup (map f s) = map f (undup s).

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

End EqMap.

Arguments mapP {T1 T2 f s y}.

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.

Lemma eq_in_pmap (aT : eqType) rT (f1 f2 : aT option rT) s :
  {in s, f1 =1 f2} pmap f1 s = pmap f2 s.

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

Section EqPmap.

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

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 iotaD m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.

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

Lemma filter_iota_ltn m n j : j n
  [seq i <- iota m n | i < m + j] = iota m j.

Lemma filter_iota_leq n m j : j < n
  [seq i <- iota m n | i m + j] = iota m j.+1.

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.

Variant mkseq_spec s : seq T Type :=
| MapIota n f : s = mkseq f n mkseq_spec s (mkseq f n).

Lemma mkseqP s : mkseq_spec s s.

Lemma map_nth_iota0 s i :
  i size s [seq nth x0 s j | j <- iota 0 i] = take i s.

Lemma map_nth_iota s i j : j size s - i
  [seq nth x0 s k | k <- iota i j] = take j (drop i 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.

Arguments perm_iotaP {T s t}.

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_rcons s x : foldr f z0 (rcons s x) = foldr f (f x z0) s.

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.

Lemma foldl_rcons z s x : foldl z (rcons s x) = f (foldl z s) x.

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 scanl_rcons x s1 y :
  scanl x (rcons s1 y) = rcons (scanl x s1) (foldl g x (rcons s1 y)).

Lemma nth_cons_scanl s n : n size s
   x, nth x1 (x :: scanl x s) n = foldl g x (take n s).

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) (r : S T bool).

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 s t :=
  match s, t with
  | [::], [::]true
  | x :: s, y :: tr x y && all2 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 s t :
  all2 s t = (size s == size t) && all [pred xy | r xy.1 xy.2] (zip s t).

Lemma zip_map I f g (s : seq I) :
  zip (map f s) (map g s) = [seq (f i, g i) | i <- s].

End Zip.


Lemma eqseq_all (T : eqType) (s t : seq T) : (s == t) = all2 eq_op s t.

Lemma eq_map_all I (T : eqType) (f g : I T) (s : seq I) :
  (map f s == map g s) = all [pred xy | xy.1 == xy.2] [seq (f i, g i) | i <- s].

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).
Arguments flattenP {A x}.

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.

Arguments flattenP {T A x}.
Arguments flatten_mapP {S T A s y}.

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 allpairs0l f t : [seq f x y | x <- [::], y <- t x] = [::].

Lemma allpairs0r f s : [seq f x y | x <- s, y <- [::]] = [::].

Lemma allpairs1l f x t :
   [seq f x y | x <- [:: x], y <- t x] = [seq f x y | y <- t x].

Lemma allpairs1r f s y :
  [seq f x y | x <- s, y <- [:: y x]] = [seq f x (y x) | x <- s].

Lemma allpairs_cons f x s t :
  [seq f x y | x <- x :: s, y <- t x] =
    [seq f x y | y <- t x] ++ [seq f x y | x <- s, y <- t x].

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 eq_allpairsr (f : x, T x R) s t1 t2 : ( x, t1 x = t2 x)
  [seq f x y | x <- s, y <- t1 x] = [seq f x y | x <- s, y <- t2 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_rcons f x s t :
  [seq f x y | x <- rcons s x, y <- t x] =
    [seq f x y | x <- s, y <- t x] ++ [seq f x y | 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.

Arguments allpairs_dep {S T R} f s t /.

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.

Arguments allpairs {S T R} f s t /.

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 x R.

Lemma allpairs_f_dep f s t x y :
  x \in s y \in t x f x y \in [seq f x y | x <- s, y <- t x].

Lemma eq_in_allpairs_dep f1 f2 s t :
    {in s, x, {in t x, f1 x =1 f2 x}}
  [seq f1 x y : R | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].

Lemma mem_allpairs_dep f s1 t1 s2 t2 :
    s1 =i s2 {in s1, x, t1 x =i t2 x}
  [seq f x y | x <- s1, y <- t1 x] =i [seq f x y | x <- s2, y <- t2 x].

Lemma allpairs_uniq_dep f s t (st := [seq Tagged T y | x <- s, y <- t x]) :
  let g (p : {x : S & T x}) : R := f (tag p) (tagged p) in
    uniq s {in s, x, uniq (t x)} {in st &, injective g}
  uniq [seq f x y | x <- s, y <- t x].

End EqAllPairsDep.

Arguments allpairsPdep {S T R f s t z}.

Section MemAllPairs.

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

Lemma perm_allpairs_catr f s t1 t2 :
  perm_eql [seq f x y | x <- s, y <- t1 x ++ t2 x]
           ([seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]).

Lemma mem_allpairs_catr f s y0 t :
  [seq f x y | x <- s, y <- y0 x ++ t x] =i
    [seq f x y | x <- s, y <- y0 x] ++ [seq f x y | x <- s, y <- t x].

Lemma perm_allpairs_consr f s y0 t :
  perm_eql [seq f x y | x <- s, y <- y0 x :: t x]
           ([seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]).

Lemma mem_allpairs_consr f s t y0 :
  [seq f x y | x <- s, y <- y0 x :: t x] =i
  [seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x].

Lemma allpairs_rconsr f s y0 t :
  perm_eql [seq f x y | x <- s, y <- rcons (t x) (y0 x)]
           ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]).

Lemma mem_allpairs_rconsr f s t y0 :
  [seq f x y | x <- s, y <- rcons (t x) (y0 x)] =i
    ([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]).

End MemAllPairs.

Lemma all_allpairsP
      (S : eqType) (T : S eqType) (R : Type)
      (p : pred R) (f : x : S, T x R)
      (s : seq S) (t : x : S, seq (T x)) :
  reflect ( (x : S) (y : T x), x \in s y \in t x p (f x y))
          (all p [seq f x y | x <- s, y <- t x]).

Arguments all_allpairsP {S T R p f s t}.

Section EqAllPairs.

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

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

Lemma allpairs_f f s t x y :
  x \in s y \in t f x y \in [seq f x y | x <- s, y <- t].

Lemma eq_in_allpairs f1 f2 s t :
    {in s & t, f1 =2 f2}
  [seq f1 x y : R | x <- s, y <- t] = [seq f2 x y | x <- s, y <- t].

Lemma mem_allpairs f s1 t1 s2 t2 :
    s1 =i s2 t1 =i t2
  [seq f x y | x <- s1, y <- t1] =i [seq f x y | x <- s2, y <- t2].

Lemma allpairs_uniq f s t (st := [seq (x, y) | x <- s, y <- t]) :
    uniq s uniq t {in st &, injective (prod_curry f)}
  uniq [seq f x y | x <- s, y <- t].

End EqAllPairs.

Arguments allpairsP {S T R f s t z}.
Arguments perm_nilP {T s}.
Arguments perm_consP {T x s t}.

Section AllRel.

Variables (T S : Type) (r : T S bool).
Implicit Types (x : T) (y : S) (xs : seq T) (ys : seq S).

Definition allrel xs ys := all [pred x | all (r x) ys] xs.

Lemma allrel0l ys : allrel [::] ys.

Lemma allrel0r xs : allrel xs [::].

Lemma allrel_consl x xs ys : allrel (x :: xs) ys = all (r x) ys && allrel xs ys.

Lemma allrel_consr xs y ys :
  allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys.

Lemma allrel_cons2 x y xs ys :
  allrel (x :: xs) (y :: ys) =
  [&& r x y, all (r x) ys, all (r^~ y) xs & allrel xs ys].

Lemma allrel1l x ys : allrel [:: x] ys = all (r x) ys.

Lemma allrel1r xs y : allrel xs [:: y] = all (r^~ y) xs.

Lemma allrel_catl xs xs' ys :
  allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys.

Lemma allrel_catr xs ys ys' :
  allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'.

Lemma allrel_maskl m xs ys : allrel xs ys allrel (mask m xs) ys.

Lemma allrel_maskr m xs ys : allrel xs ys allrel xs (mask m ys).

Lemma allrel_filterl a xs ys : allrel xs ys allrel (filter a xs) ys.

Lemma allrel_filterr a xs ys : allrel xs ys allrel xs (filter a ys).

Lemma allrel_allpairsE xs ys :
  allrel xs ys = all id [seq r x y | x <- xs, y <- ys].

End AllRel.

Arguments allrel {T S} r xs ys : simpl never.
Arguments allrel0l {T S} r ys.
Arguments allrel0r {T S} r xs.
Arguments allrel_consl {T S} r x xs ys.
Arguments allrel_consr {T S} r xs y ys.
Arguments allrel1l {T S} r x ys.
Arguments allrel1r {T S} r xs y.
Arguments allrel_catl {T S} r xs xs' ys.
Arguments allrel_catr {T S} r xs ys ys'.
Arguments allrel_maskl {T S} r m xs ys.
Arguments allrel_maskr {T S} r m xs ys.
Arguments allrel_filterl {T S} r a xs ys.
Arguments allrel_filterr {T S} r a xs ys.
Arguments allrel_allpairsE {T S} r xs ys.

Notation all2rel r xs := (allrel r xs xs).

Lemma sub_in_allrel
      {T S : Type} (P : {pred T}) (Q : {pred S}) (r r' : T S bool) :
  {in P & Q, x y, r x y r' x y}
   xs ys, all P xs all Q ys allrel r xs ys allrel r' xs ys.

Lemma sub_allrel {T S : Type} (r r' : T S bool) :
  ( x y, r x y r' x y)
   xs ys, allrel r xs ys allrel r' xs ys.

Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' :
  {in P & Q, r =2 r'}
   xs ys, all P xs all Q ys allrel r xs ys = allrel r' xs ys.

Lemma eq_allrel {T S : Type} (r r' : T S bool) :
  r =2 r' allrel r =2 allrel r'.

Lemma allrelC {T S : Type} (r : T S bool) xs ys :
  allrel r xs ys = allrel (fun yr^~ y) ys xs.

Lemma allrel_mapl {T T' S : Type} (f : T' T) (r : T S bool) xs ys :
  allrel r (map f xs) ys = allrel (fun xr (f x)) xs ys.

Lemma allrel_mapr {T S S' : Type} (f : S' S) (r : T S bool) xs ys :
  allrel r xs (map f ys) = allrel (fun x yr x (f y)) xs ys.

Lemma allrelP {T S : eqType} {r : T S bool} {xs ys} :
  reflect {in xs & ys, x y, r x y} (allrel r xs ys).

Lemma allrelT {T S : Type} (xs : seq T) (ys : seq S) :
  allrel (fun _ _true) xs ys = true.

Lemma allrel_relI {T S : Type} (r r' : T S bool) xs ys :
  allrel (fun x yr x y && r' x y) xs ys = allrel r xs ys && allrel r' xs ys.

Section All2Rel.

Variable (T : nonPropType) (r : rel T).
Implicit Types (x y z : T) (xs : seq T).
Hypothesis (rsym : symmetric r).

Lemma all2rel1 x : all2rel r [:: x] = r x x.

Lemma all2rel2 x y : all2rel r [:: x; y] = r x x && r y y && r x y.

Lemma all2rel_cons x xs :
  all2rel r (x :: xs) = [&& r x x, all (r x) xs & all2rel r xs].

End All2Rel.

Section Pairwise.

Variables (T : Type) (r : T T bool).
Implicit Types (x y : T) (xs ys : seq T).

Fixpoint pairwise xs : bool :=
  if xs is x :: xs then all (r x) xs && pairwise xs else true.

Lemma pairwise_cons x xs : pairwise (x :: xs) = all (r x) xs && pairwise xs.

Lemma pairwise_cat xs ys :
  pairwise (xs ++ ys) = [&& allrel r xs ys, pairwise xs & pairwise ys].

Lemma pairwise_rcons xs x :
  pairwise (rcons xs x) = all (r^~ x) xs && pairwise xs.

Lemma pairwise2 x y : pairwise [:: x; y] = r x y.

Lemma pairwise_mask m xs : pairwise xs pairwise (mask m xs).

Lemma pairwise_filter a xs : pairwise xs pairwise (filter a xs).

Lemma pairwiseP x0 xs :
  reflect {in gtn (size xs) &, {homo nth x0 xs : i j / i < j >-> r i j}}
          (pairwise xs).

Lemma pairwise_all2rel :
  reflexive r symmetric r xs, pairwise xs = all2rel r xs.

End Pairwise.

Arguments pairwise {T} r xs.
Arguments pairwise_cons {T} r x xs.
Arguments pairwise_cat {T} r xs ys.
Arguments pairwise_rcons {T} r xs x.
Arguments pairwise2 {T} r x y.
Arguments pairwise_mask {T r} m {xs}.
Arguments pairwise_filter {T r} a {xs}.
Arguments pairwiseP {T r} x0 {xs}.
Arguments pairwise_all2rel {T r} r_refl r_sym xs.

Lemma sub_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) :
  {in P &, subrel r r'}
   xs, all P xs pairwise r xs pairwise r' xs.

Lemma sub_pairwise {T : Type} (r r' : rel T) xs :
  subrel r r' pairwise r xs pairwise r' xs.

Lemma eq_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) :
  {in P &, r =2 r'} xs, all P xs pairwise r xs = pairwise r' xs.

Lemma eq_pairwise {T : Type} (r r' : rel T) :
  r =2 r' pairwise r =i pairwise r'.

Lemma pairwise_map {T T' : Type} (f : T' T) (r : rel T) xs :
  pairwise r (map f xs) = pairwise (relpre f r) xs.

Lemma pairwise_relI {T : Type} (r r' : rel T) (s : seq T) :
  pairwise [rel x y | r x y && r' x y] s = pairwise r s && pairwise r' s.

Section EqPairwise.

Variables (T : eqType) (r : T T bool).
Implicit Types (xs ys : seq T).

Lemma subseq_pairwise xs ys : subseq xs ys pairwise r ys pairwise r xs.

Lemma uniq_pairwise xs : uniq xs = pairwise [rel x y | x != y] xs.

Lemma pairwise_uniq xs : irreflexive r pairwise r xs uniq xs.

Lemma pairwise_eq : antisymmetric r
   xs ys, pairwise r xs pairwise r ys perm_eq xs ys xs = ys.

End EqPairwise.

Arguments subseq_pairwise {T r xs ys}.
Arguments uniq_pairwise {T} xs.
Arguments pairwise_uniq {T r xs}.
Arguments pairwise_eq {T r} r_asym {xs ys}.

Section Permutations.

Variable T : eqType.
Implicit Types (x : T) (s t : seq T) (bs : seq (T × nat)) (acc : seq (seq T)).

Fixpoint incr_tally bs x :=
  if bs isn't b :: bs then [:: (x, 1)] else
  if x == b.1 then (x, b.2.+1) :: bs else b :: incr_tally bs x.

Definition tally s := foldl incr_tally [::] s.

Definition wf_tally :=
  [qualify a bs : seq (T × nat) | uniq (unzip1 bs) && (0 \notin unzip2 bs)].

Definition tally_seq bs := flatten [seq nseq b.2 b.1 | b <- bs].

Lemma size_tally_seq bs : size (tally_seq bs) = sumn (unzip2 bs).

Lemma tally_seqK : {in wf_tally, cancel tally_seq tally}.

Lemma incr_tallyP x : {homo incr_tally^~ x : bs / bs \in wf_tally}.

Lemma tallyP s : tally s \is a wf_tally.

Lemma tallyK s : perm_eq (tally_seq (tally s)) s.

Lemma tallyEl s : perm_eq (unzip1 (tally s)) (undup s).

Lemma tallyE s : perm_eq (tally s) [seq (x, count_mem x s) | x <- undup s].

Lemma perm_tally s1 s2 : perm_eq s1 s2 perm_eq (tally s1) (tally s2).

Lemma perm_tally_seq bs1 bs2 :
  perm_eq bs1 bs2 perm_eq (tally_seq bs1) (tally_seq bs2).

Lemma perm_count_undup s :
  perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s.



Definition permutations s := perms_rec (size s) [::] (tally s) [::].

Let permsP s : n bs,
   [/\ permutations s = perms_rec n [::] bs [::],
       size (tseq bs) == n, perm_eq (tseq bs) s & uniq (unzip1 bs)].

Let cons_permsE : n x bs bs1 bs2,
  let cp := cons_perms n bs bs2 in let perms s := perms_rec n s bs1 [::] in
  cp (perms [:: x]) = cp [::] ++ [seq rcons t x | t <- perms [::]].

Lemma mem_permutations s t : (t \in permutations s) = perm_eq t s.

Lemma permutations_uniq s : uniq (permutations s).

Notation perms := permutations.
Lemma permutationsE s :
    0 < size s
  perm_eq (perms s) [seq x :: t | x <- undup s, t <- perms (rem x s)].

Lemma permutationsErot x s (le_x := fun tiota 0 (index x t + 1)) :
  perm_eq (perms (x :: s)) [seq rot i (x :: t) | t <- perms s, i <- le_x t].

Lemma size_permutations s : uniq s size (permutations s) = (size s)`!.

Lemma permutations_all_uniq s : uniq s all uniq (permutations s).

Lemma perm_permutations s t :
  perm_eq s t perm_eq (permutations s) (permutations t).

End Permutations.

Section AllIff.
The Following Are Equivalent
We introduce a specific conjunction, used to chain the consecutive items in a circular list of implications
Inductive all_iff_and (P Q : Prop) : Prop := AllIffConj of P & Q.

Definition all_iff (P0 : Prop) (Ps : seq Prop) : Prop :=
  let fix loop (P : Prop) (Qs : seq Prop) : Prop :=
    if Qs is Q :: Qs then all_iff_and (P Q) (loop Q Qs) else P P0 in
  loop P0 Ps.

Lemma all_iffLR P0 Ps : all_iff P0 Ps
   m n, nth P0 (P0 :: Ps) m nth P0 (P0 :: Ps) n.

Lemma all_iffP P0 Ps :
   all_iff P0 Ps m n, nth P0 (P0 :: Ps) m nth P0 (P0 :: Ps) n.

End AllIff.
Arguments all_iffLR {P0 Ps}.
Arguments all_iffP {P0 Ps}.
Coercion all_iffP : all_iff >-> Funclass.

This means "the following are all equivalent: P0, ... Pn"
Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
  (all_iff P0 (@cons Prop P1 (.. (@cons Prop Pn nil) ..))) : form_scope.

Ltac tfae := do !apply: AllIffConj.

Temporary backward compatibility.
#[deprecated(since="mathcomp 1.11.0", note="Use takeD instead.")]
Notation take_addn := takeD (only parsing).
#[deprecated(since="mathcomp 1.11.0", note="Use rotD instead.")]
Notation rot_addn := rotD (only parsing).
#[deprecated(since="mathcomp 1.11.0", note="Use nseqD instead.")]
Notation nseq_addn := nseqD (only parsing).
#[deprecated(since="mathcomp 1.12.0", note="Use mem_allpairs_catr instead.")]
Notation allpairs_catr := mem_allpairs_catr (only parsing).
#[deprecated(since="mathcomp 1.12.0", note="Use mem_allpairs_consr instead.")]
Notation allpairs_consr := mem_allpairs_consr (only parsing).
#[deprecated(since="mathcomp 1.12.0", note="Use allpairs_rconsr instead.")]
Notation perm_allpairs_rconsr := allpairs_rconsr (only parsing).
#[deprecated(since="mathcomp 1.12.0", note="Use iotaDl instead.")]
Notation iota_addl := iotaDl (only parsing).
#[deprecated(since="mathcomp 1.13.0", note="Use iotaD instead.")]
Notation iota_add := iotaD (only parsing).