+ +

Library mathcomp.ssreflect.seq

+ +

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

+ +

+ 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 p s == the (applicative, boolean) predicate p holds for some + item in s. + all p s == p holds for all items in s. + find p s == the 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 number of times x occurs in s := count (pred1 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. +
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). +
Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m],
+ + map f s == the sequence [:: f x_1, ..., f x_n]. + allpairs f s t == the sequence of all the f x y, with x and y drawn from + s and t, respectively, in row-major order. + := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] + 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 E | x <- s, y <- t] := allpairs (fun x y => E) s t. + [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. +

+ +
+Set Implicit Arguments.
+ +
+Delimit Scope seq_scope with SEQ.
+Open Scope seq_scope.
+ +
+

+ +

+ Inductive seq (T : Type) : Type := Nil | Cons of T & seq T. +

+Notation seq := list.
+Notation Cons T := (@cons T) (only parsing).
+Notation Nil T := (@nil T) (only parsing).
+ +
+ +
+

+ +

+ As :: and ++ are (improperly) declared in Init.datatypes, we only rebind + them here. +

+Infix "::" := cons : seq_scope.
+ +
+

+ +

+ GG - this triggers a camlp4 warning, as if this Notation had been Reserved +

+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 x ⇒ seqn_rec (fun s ⇒ f (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 cats0 s : s ++ [::] = s.
+ +
+Lemma catA s1 s2 s3 : s1 ++ s2 ++ s3 = (s1 ++ s2 ) ++ s3.
+ +
+Lemma size_cat s1 s2 : size (s1 ++ s2) = size s1 + size s2.
+ +
+

+ +

+ last, belast, rcons, and last induction. +

+ +
+Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z ].
+ +
+Lemma rcons_cons x s z : rcons (x :: s) z = x :: rcons s z.
+ +
+Lemma cats1 s z : s ++ [:: z ] = rcons s z.
+ +
+Fixpoint last x s := if s is x' :: s' then last x' s' else x.
+Fixpoint belast x s := if s is x' :: s' then x :: (belast x' s') else [::].
+ +
+Lemma lastI x s : x :: s = rcons (belast x s) (last x s).
+ +
+Lemma last_cons x y s : last x (y :: s) = last y s.
+ +
+Lemma size_rcons s x : size (rcons s x) = (size s ).+1.
+ +
+Lemma size_belast x s : size (belast x s) = size s.
+ +
+Lemma last_cat x s1 s2 : last x (s1 ++ s2) = last (last x s1) s2.
+ +
+Lemma last_rcons x s z : last x (rcons s z) = z.
+ +
+Lemma belast_cat x s1 s2 :
+  belast x (s1 ++ s2) = belast x s1 ++ belast (last x s1) s2.
+ +
+Lemma belast_rcons x s z : belast x (rcons s z) = x :: s.
+ +
+Lemma cat_rcons x s1 s2 : rcons s1 x ++ s2 = s1 ++ x :: s2.
+ +
+Lemma rcons_cat x s1 s2 : rcons (s1 ++ s2) x = s1 ++ rcons s2 x.
+ +
+CoInductive 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_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 find_nseq n x : find (nseq n x) = ~~ a x × n.
+ +
+Lemma nth_find s : has s → a (nth s (find s)).
+ +
+Lemma before_find s i : i < find s → a (nth s i) = false.
+ +
+Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
+ +
+Lemma filter_rcons s x :
+  filter (rcons s x) = if a x then rcons (filter s) x else filter s.
+ +
+Lemma count_cat s1 s2 : count (s1 ++ s2) = count s1 + count s2.
+ +
+Lemma has_cat s1 s2 : has (s1 ++ s2) = has s1 || has s2.
+ +
+Lemma has_rcons s x : has (rcons s x) = a x || has s.
+ +
+Lemma all_cat s1 s2 : all (s1 ++ s2) = all s1 && all s2.
+ +
+Lemma all_rcons s x : all (rcons s x) = a x && all s.
+ +
+End SeqFind.
+ +
+Lemma eq_find a1 a2 : a1 =1 a2 → find a1 =1 find a2.
+ +
+Lemma eq_filter a1 a2 : a1 =1 a2 → filter a1 =1 filter a2.
+ +
+Lemma eq_count a1 a2 : a1 =1 a2 → count a1 =1 count a2.
+ +
+Lemma eq_has a1 a2 : a1 =1 a2 → has a1 =1 has a2.
+ +
+Lemma eq_all a1 a2 : a1 =1 a2 → all a1 =1 all a2.
+ +
+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'.+1 ⇒ drop 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'.+1 ⇒ x :: 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 :
+    n0 ≤ size s1 →
+  ∀ s2, take n0 (s1 ++ s2) = take n0 s1.
+ +
+Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
+ +
+Lemma nth_take i : i < n0 → ∀ s, nth (take n0 s) i = nth s i.
+ +
+

+ +

+ 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).
+ +
+Lemma rot1_cons x s : rot 1 (x :: s) = rcons s x.
+ +
+

+ +

+ (efficient) reversal +

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

+ +

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

+ +
+Definition rev T (s : seq T) := nosimpl (catrev s [::]).
+ +
+ +
+ +
+Notation count_mem x := (count (pred_of_simpl (pred1 x))).
+ +
+Infix "++" := cat : seq_scope.
+ +
+Notation "[ 'seq' x <- s | C ]" := (filter (fun x ⇒ C%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 : T ⇒ C%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 seq2_ind T1 T2 (P : seq T1 → seq T2 → Type) :
+    P [::] [::] → (∀ x1 x2 s1 s2, P s1 s2 → P (x1 :: s1) (x2 :: s2)) →
+  ∀ s1 s2, size s1 = size s2 → P s1 s2.
+ +
+Section Rev.
+ +
+Variable T : Type.
+Implicit Types s t : seq T.
+ +
+Lemma catrev_catl s t u : catrev (s ++ t) u = catrev t (catrev s u).
+ +
+Lemma catrev_catr s t u : catrev s (t ++ u) = catrev s t ++ u.
+ +
+Lemma catrevE s t : catrev s t = rev s ++ t.
+ +
+Lemma rev_cons x s : rev (x :: s) = rcons (rev s) x.
+ +
+Lemma size_rev s : size (rev s) = size s.
+ +
+Lemma rev_cat s t : rev (s ++ t) = rev t ++ rev s.
+ +
+Lemma rev_rcons s x : rev (rcons s x) = x :: rev s.
+ +
+Lemma revK : involutive (@rev T).
+ +
+Lemma nth_rev x0 n s :
+  n < size s → nth x0 (rev s) n = nth x0 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 take_rev s n : take n (rev s) = rev (drop (size s - n) s).
+ +
+Lemma drop_rev s n : drop n (rev s) = rev (take (size s - n) s).
+ +
+End Rev.
+ +
+ +
+

+ +

+ Equality and eqType for seq. +

+ +
+Section EqSeq.
+ +
+Variables (n0 : nat) (T : eqType) (x0 : T).
+Implicit Type s : seq T.
+Implicit Types x y z : T.
+ +
+Fixpoint eqseq s1 s2 {struct s2} :=
+  match s1, s2 with
+  | [::], [::] ⇒ true
+  | x1 :: s1', x2 :: s2' ⇒ (x1 == x2) && eqseq s1' s2'
+  | _, _ ⇒ false
+  end.
+ +
+Lemma eqseqP : Equality.axiom eqseq.
+ +
+Canonical 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 eqseq_class := seq T.
+Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
+ +
+Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s ].
+ +
+Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
+

+ +

+ The line below makes mem_seq a canonical instance of topred. +

+Canonical mem_seq_predType := mkPredType mem_seq.
+ +
+Lemma in_cons y s x : (x \in y :: s ) = (x == y ) || (x \in s ).
+ +
+Lemma in_nil x : (x \in [::]) = false.
+ +
+Lemma mem_seq1 x y : (x \in [:: y ]) = (x == y ).
+ +
+ (* to be repeated after the Section discharge. *)
+Let inE := (mem_seq1 , in_cons , inE ).
+ +
+Lemma mem_seq2 x y1 y2 : (x \in [:: y1 ; y2 ]) = xpred2 y1 y2 x.
+ +
+Lemma mem_seq3 x y1 y2 y3 : (x \in [:: y1 ; y2 ; y3 ]) = xpred3 y1 y2 y3 x.
+ +
+Lemma mem_seq4 x y1 y2 y3 y4 :
+ (x \in [:: y1 ; y2 ; y3 ; y4 ]) = xpred4 y1 y2 y3 y4 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.
+ +
+Section Filters.
+ +
+Variable a : pred T.
+ +
+Lemma hasP s : reflect (exists2 x, x \in s & a x) (has a s).
+ +
+Lemma hasPn s : reflect (∀ x, x \in s → ~~ a x) (~~ has a s).
+ +
+Lemma allP s : reflect (∀ x, x \in s → a x) (all a s).
+ +
+Lemma allPn s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).
+ +
+Lemma mem_filter x s : (x \in filter a s ) = a x && (x \in s ).
+ +
+End Filters.
+ +
+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 nseqP n x y : reflect (y = x ∧ n > 0) (y \in nseq n x).
+ +
+Lemma constant_nseq n x : constant (nseq n x).
+ +
+

+ +

+ Uses x0 +

+Lemma constantP s : reflect (∃ x, s = nseq (size s) x) (constant s).
+ +
+

+ +

+ Duplicate-freenes. +

+ +
+Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
+ +
+Lemma cons_uniq x s : uniq (x :: s) = (x \notin s ) && uniq s.
+ +
+Lemma cat_uniq s1 s2 :
+ uniq (s1 ++ s2) = [&& uniq s1 , ~~ has (mem s1) s2 & uniq s2 ].
+ +
+Lemma uniq_catC s1 s2 : uniq (s1 ++ s2) = uniq (s2 ++ s1).
+ +
+Lemma uniq_catCA s1 s2 s3 : uniq (s1 ++ s2 ++ s3) = uniq (s2 ++ s1 ++ s3).
+ +
+Lemma rcons_uniq s x : uniq (rcons s x) = (x \notin s ) && uniq s.
+ +
+Lemma filter_uniq s a : uniq s → uniq (filter a s).
+ +
+Lemma rot_uniq s : uniq (rot n0 s) = uniq s.
+ +
+Lemma rev_uniq s : uniq (rev s) = uniq s.
+ +
+Lemma count_memPn x s : reflect (count_mem x s = 0) (x \notin s).
+ +
+Lemma count_uniq_mem s x : uniq s → count_mem x s = (x \in s ).
+ +
+Lemma filter_pred1_uniq s x : uniq s → x \in s → filter (pred1 x) s = [:: x ].
+ +
+

+ +

+ Removing duplicates +

+ +
+Fixpoint undup s :=
+ if s is x :: s' then if x \in s' then undup s' else x :: undup s' else [::].
+ +
+Lemma size_undup s : size (undup s) ≤ size s.
+ +
+Lemma mem_undup s : undup s =i s.
+ +
+Lemma undup_uniq s : uniq (undup s).
+ +
+Lemma undup_id s : uniq s → undup s = s.
+ +
+Lemma ltn_size_undup s : (size (undup s) < size s ) = ~~ uniq s.
+ +
+Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
+ +
+Lemma undup_nil s : undup s = [::] → s = [::].
+ +
+

+ +

+ Lookup +

+ +
+Definition index x := find (pred1 x).
+ +
+Lemma index_size x s : index x s ≤ size s.
+ +
+Lemma index_mem x s : (index x s < size s ) = (x \in s ).
+ +
+Lemma nth_index x s : x \in s → nth s (index x s) = x.
+ +
+Lemma index_cat x s1 s2 :
+ index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2.
+ +
+Lemma 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 [pred i | i < 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 ).
+ +
+CoInductive 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 EqSeq.
+ +
+Definition inE := (mem_seq1 , in_cons , inE ).
+ +
+ +
+ +
+Section NthTheory.
+ +
+Lemma nthP (T : eqType) (s : seq T) x x0 :
+  reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s).
+ +
+Variable T : Type.
+ +
+Lemma has_nthP (a : pred T) s x0 :
+  reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).
+ +
+Lemma all_nthP (a : pred T) s x0 :
+  reflect (∀ i, i < size s → a (nth x0 s i)) (all a s).
+ +
+End NthTheory.
+ +
+Lemma set_nth_default T s (y0 x0 : T) n : n < size s → nth x0 s n = nth y0 s n.
+ +
+Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x).
+ +
+ +
+Definition bitseq := seq bool.
+Canonical bitseq_eqType := Eval hnf in [eqType of bitseq ].
+Canonical bitseq_predType := Eval hnf in [predType of bitseq ].
+ +
+

+ +

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

+ +
+Fixpoint incr_nth v i {struct i} :=
+  if v is n :: v' then if i is i'.+1 then n :: incr_nth v' i' else n.+1 :: v'
+  else ncons i 0 [:: 1].
+ +
+Lemma nth_incr_nth v i j : nth 0 (incr_nth v i) j = (i == j ) + nth 0 v j.
+ +
+Lemma size_incr_nth v i :
+  size (incr_nth v i) = if i < size v then size v else i .+1.
+ +
+Lemma incr_nth_inj v : injective (incr_nth v).
+ +
+Lemma incr_nthC v i j :
+  incr_nth (incr_nth v i) j = incr_nth (incr_nth v j) i.
+ +
+

+ +

+ Equality up to permutation +

+ +
+Section PermSeq.
+ +
+Variable T : eqType.
+Implicit Type s : seq T.
+ +
+Definition perm_eq s1 s2 :=
+  all [pred x | count_mem x s1 == count_mem x s2 ] (s1 ++ s2).
+ +
+Lemma perm_eqP s1 s2 : reflect (count ^~ s1 =1 count ^~ s2) (perm_eq s1 s2).
+ +
+Lemma perm_eq_refl s : perm_eq s s.
+ Hint Resolve perm_eq_refl.
+ +
+Lemma perm_eq_sym : symmetric perm_eq.
+ +
+Lemma perm_eq_trans : transitive perm_eq.
+ +
+Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
+Notation perm_eqr s1 s2 := (perm_eq ^~ s1 =1 perm_eq ^~ s2).
+ +
+Lemma perm_eqlE s1 s2 : perm_eql s1 s2 → perm_eq s1 s2.
+ +
+Lemma perm_eqlP s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
+ +
+Lemma perm_eqrP 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_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_catAC s1 s2 s3 : perm_eql ((s1 ++ s2 ) ++ s3) ((s1 ++ s3 ) ++ s2).
+ +
+Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).
+ +
+Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s).
+ +
+Lemma perm_rot n s : perm_eql (rot n s) s.
+ +
+Lemma perm_rotr n s : perm_eql (rotr n s) s.
+ +
+Lemma perm_eq_rev s : perm_eq s (rev s).
+ +
+Lemma perm_filter s1 s2 P :
+  perm_eq s1 s2 → perm_eq (filter P s1) (filter P s2).
+ +
+Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
+ +
+Lemma perm_eq_mem s1 s2 : perm_eq s1 s2 → s1 =i s2.
+ +
+Lemma perm_eq_all s1 s2 P : perm_eq s1 s2 → all P s1 = all P s2.
+ +
+Lemma perm_eq_size s1 s2 : perm_eq s1 s2 → size s1 = size s2.
+ +
+Lemma perm_eq_small 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 leq_size_perm s1 s2 :
+    uniq s1 → {subset s1 ≤ s2 } → size s2 ≤ size s1 →
+  s1 =i s2 ∧ size s1 = size s2.
+ +
+Lemma perm_uniq s1 s2 : s1 =i s2 → size s1 = size s2 → uniq s1 = uniq s2.
+ +
+Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 → uniq s1 = uniq s2.
+ +
+Lemma uniq_perm_eq s1 s2 : uniq s1 → uniq s2 → s1 =i s2 → perm_eq s1 s2.
+ +
+Lemma count_mem_uniq s : (∀ x, count_mem x s = (x \in s )) → uniq s.
+ +
+Lemma catCA_perm_ind P :
+    (∀ s1 s2 s3, P (s1 ++ s2 ++ s3) → P (s2 ++ s1 ++ s3)) →
+  (∀ s1 s2, perm_eq s1 s2 → P s1 → P s2 ).
+ +
+Lemma catCA_perm_subst R F :
+    (∀ s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R ) →
+  (∀ s1 s2, perm_eq s1 s2 → F s1 = F s2 ).
+ +
+End PermSeq.
+ +
+Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
+Notation perm_eqr s1 s2 := (perm_eq ^~ s1 =1 perm_eq ^~ s2).
+ +
+Hint Resolve perm_eq_refl.
+ +
+Section RotrLemmas.
+ +
+Variables (n0 : nat) (T : Type) (T' : eqType).
+Implicit Type 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 rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).
+ +
+Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).
+ +
+End RotrLemmas.
+ +
+Section RotCompLemmas.
+ +
+Variable T : Type.
+Implicit Type s : seq T.
+ +
+Lemma rot_addn m n s : m + n ≤ size s → rot (m + n) s = rot m (rot n s).
+ +
+Lemma rotS n s : n < size s → rot n .+1 s = rot 1 (rot n s).
+ +
+Lemma rot_add_mod m n s : n ≤ size s → m ≤ size s →
+  rot m (rot n s) = rot (if m + n ≤ size s then m + n else m + n - size s) s.
+ +
+Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s).
+ +
+Lemma rot_rotr m n s : rot m (rotr n s) = rotr n (rot m s).
+ +
+Lemma rotr_rotr m n s : rotr m (rotr n s) = rotr n (rotr m s).
+ +
+End RotCompLemmas.
+ +
+Section Mask.
+ +
+Variables (n0 : nat) (T : Type).
+Implicit Types (m : bitseq) (s : seq T).
+ +
+Fixpoint mask m s {struct m} :=
+  match m, s with
+  | b :: m', x :: s' ⇒ if b then x :: mask m' s' else mask m' s'
+  | _, _ ⇒ [::]
+  end.
+ +
+Lemma mask_false s n : mask (nseq n false) s = [::].
+ +
+Lemma mask_true s n : size s ≤ n → mask (nseq n true) s = s.
+ +
+Lemma mask0 m : mask m [::] = [::].
+ +
+Lemma mask1 b x : mask [:: b ] [:: x ] = nseq b x.
+ +
+Lemma mask_cons b m x s : mask (b :: m) (x :: s) = nseq b x ++ mask m s.
+ +
+Lemma size_mask m s : size m = size s → size (mask m s) = count id m.
+ +
+Lemma mask_cat m1 m2 s1 s2 :
+  size m1 = size s1 → mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.
+ +
+Lemma has_mask_cons a b m x s :
+  has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).
+ +
+Lemma has_mask a m s : has a (mask m s) → has a s.
+ +
+Lemma mask_rot m s : size m = size s →
+   mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s).
+ +
+Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s }.
+ +
+End Mask.
+ +
+Section EqMask.
+ +
+Variables (n0 : nat) (T : eqType).
+Implicit Types (s : seq T) (m : bitseq).
+ +
+Lemma mem_mask_cons x b m y s :
+  (x \in mask (b :: m) (y :: s)) = b && (x == y ) || (x \in mask m s ).
+ +
+Lemma mem_mask x m s : x \in mask m s → x \in s.
+ +
+Lemma mask_uniq s : uniq s → ∀ m, uniq (mask m s).
+ +
+Lemma mem_mask_rot m s :
+  size m = size s → mask (rot n0 m) (rot n0 s) =i mask m s.
+ +
+End EqMask.
+ +
+Section Subseq.
+ +
+Variable T : eqType.
+Implicit Type s : seq T.
+ +
+Fixpoint subseq s1 s2 :=
+  if s2 is y :: s2' then
+    if s1 is x :: s1' then subseq (if x == y then s1' else s1) s2' else true
+  else s1 == [::].
+ +
+Lemma sub0seq s : subseq [::] s.
+ +
+Lemma subseq0 s : subseq s [::] = (s == [::]).
+ +
+Lemma 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 subseq_refl s : subseq s s.
+ Hint Resolve subseq_refl.
+ +
+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 mem_subseq s1 s2 : subseq s1 s2 → {subset s1 ≤ s2 }.
+ +
+Lemma sub1seq x s : subseq [:: x ] s = (x \in s ).
+ +
+Lemma size_subseq s1 s2 : subseq s1 s2 → size s1 ≤ size s2.
+ +
+Lemma size_subseq_leqif s1 s2 :
+  subseq s1 s2 → size s1 ≤ size s2 ?= iff (s1 == s2 ).
+ +
+Lemma subseq_cons s x : subseq s (x :: s).
+ +
+Lemma subseq_rcons s x : subseq s (rcons s x).
+ +
+Lemma subseq_uniq s1 s2 : subseq s1 s2 → uniq s2 → uniq s1.
+ +
+End Subseq.
+ +
+ +
+Hint Resolve subseq_refl.
+ +
+Section Rem.
+ +
+Variables (T : eqType) (x : T).
+ +
+Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s.
+ +
+Lemma rem_id s : x \notin s → rem s = s.
+ +
+Lemma perm_to_rem s : x \in s → perm_eq s (x :: rem s).
+ +
+Lemma size_rem s : x \in s → size (rem s) = (size s ).-1.
+ +
+Lemma rem_subseq s : subseq (rem s) s.
+ +
+Lemma rem_uniq s : uniq s → uniq (rem s).
+ +
+Lemma mem_rem s : {subset rem s ≤ s }.
+ +
+Lemma rem_filter s : uniq s → rem s = filter (predC1 x) s.
+ +
+Lemma mem_rem_uniq s : uniq s → rem s =i [predD1 s & x ].
+ +
+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 i ⇒ E) 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 : T ⇒ E) 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.
+ +
+Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
+ +
+Section FilterSubseq.
+ +
+Variable T : eqType.
+Implicit Types (s : seq T) (a : pred T).
+ +
+Lemma filter_subseq a s : subseq (filter a s) s.
+ +
+Lemma subseq_filter s1 s2 a :
+  subseq s1 (filter a s2) = all a s1 && subseq s1 s2.
+ +
+Lemma subseq_uniqP s1 s2 :
+  uniq s2 → reflect (s1 = filter (mem s1) s2) (subseq s1 s2).
+ +
+Lemma perm_to_subseq s1 s2 :
+  subseq s1 s2 → {s3 | perm_eq s2 (s1 ++ s3)}.
+ +
+End FilterSubseq.
+ +
+ +
+Section EqMap.
+ +
+Variables (n0 : nat) (T1 : eqType) (x1 : T1).
+Variables (T2 : eqType) (x2 : T2) (f : T1 → T2).
+Implicit Type s : seq T1.
+ +
+Lemma map_f s x : x \in s → f x \in map f s.
+ +
+Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s).
+ +
+Lemma map_uniq s : uniq (map f s) → uniq s.
+ +
+Lemma map_inj_in_uniq s : {in s &, injective f } → uniq (map f s) = uniq s.
+ +
+Lemma map_subseq s1 s2 : subseq s1 s2 → subseq (map f s1) (map f s2).
+ +
+Lemma nth_index_map s x0 x :
+  {in s &, injective f } → x \in s → nth x0 s (index (f x) (map f s)) = x.
+ +
+Lemma perm_map s t : perm_eq s t → perm_eq (map f s) (map f t).
+ +
+Hypothesis Hf : injective f.
+ +
+Lemma mem_map s x : (f x \in map f s ) = (x \in s ).
+ +
+Lemma index_map s x : index (f x) (map f s) = index x s.
+ +
+Lemma map_inj_uniq s : uniq (map f s) = uniq s.
+ +
+End EqMap.
+ +
+ +
+Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) :
+  {f | uniq s → size fs = size s → map f s = fs }.
+ +
+Section MapComp.
+ +
+Variable T1 T2 T3 : Type.
+ +
+Lemma map_id (s : seq T1) : map id s = s.
+ +
+Lemma eq_map (f1 f2 : T1 → T2) : f1 =1 f2 → map f1 =1 map f2.
+ +
+Lemma map_comp (f1 : T2 → T3) (f2 : T1 → T2) s :
+  map (f1 \o f2) s = map f1 (map f2 s).
+ +
+Lemma mapK (f1 : T1 → T2) (f2 : T2 → T1) :
+  cancel f1 f2 → cancel (map f1) (map f2).
+ +
+End MapComp.
+ +
+Lemma eq_in_map (T1 : eqType) T2 (f1 f2 : T1 → T2) (s : seq T1) :
+  {in s , f1 =1 f2 } ↔ map f1 s = map f2 s.
+ +
+Lemma map_id_in (T : eqType) f (s : seq T) : {in s , f =1 id } → map f s = s.
+ +
+

+ +

+ Map a partial function +

+ +
+Section Pmap.
+ +
+Variables (aT rT : Type) (f : aT → option rT) (g : rT → aT).
+ +
+Fixpoint pmap s :=
+ if s is x :: s' then let r := pmap s' in oapp (cons ^~ r) r (f x) else [::].
+ +
+Lemma map_pK : pcancel g f → cancel (map g) pmap.
+ +
+Lemma size_pmap s : size (pmap s) = count [eta f ] s.
+ +
+Lemma pmapS_filter s : map some (pmap s) = map f (filter [eta f ] s).
+ +
+Hypothesis fK : ocancel f g.
+ +
+Lemma pmap_filter s : map g (pmap s) = filter [eta f ] s.
+ +
+End Pmap.
+ +
+Section EqPmap.
+ +
+Variables (aT rT : eqType) (f : aT → option rT) (g : rT → aT).
+ +
+Lemma eq_pmap (f1 f2 : aT → option rT) : f1 =1 f2 → pmap f1 =1 pmap f2.
+ +
+Lemma mem_pmap s u : (u \in pmap f s ) = (Some u \in map f s ).
+ +
+Hypothesis fK : ocancel f g.
+ +
+Lemma can2_mem_pmap : pcancel g f → ∀ s u, (u \in pmap f s ) = (g u \in s ).
+ +
+Lemma pmap_uniq s : uniq s → uniq (pmap f s).
+ +
+End EqPmap.
+ +
+Section PmapSub.
+ +
+Variables (T : Type) (p : pred T) (sT : subType p).
+ +
+Lemma size_pmap_sub s : size (pmap (insub : T → option sT) s) = count p s.
+ +
+End PmapSub.
+ +
+Section EqPmapSub.
+ +
+Variables (T : eqType) (p : pred T) (sT : subType p).
+ +
+Let insT : T → option sT := insub.
+ +
+Lemma mem_pmap_sub s u : (u \in pmap insT s ) = (val u \in s ).
+ +
+Lemma pmap_sub_uniq s : uniq s → uniq (pmap insT s).
+ +
+End EqPmapSub.
+ +
+

+ +

+ Index sequence +

+ +
+Fixpoint iota m n := if n is n'.+1 then m :: iota m .+1 n' else [::].
+ +
+Lemma size_iota m n : size (iota m n) = n.
+ +
+Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
+ +
+Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
+ +
+Lemma nth_iota p m n i : i < n → nth p (iota m n) i = m + i.
+ +
+Lemma mem_iota m n i : (i \in iota m n ) = (m ≤ i ) && (i < m + n ).
+ +
+Lemma iota_uniq m n : uniq (iota m n).
+ +
+

+ +

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

+ +
+Section MakeSeq.
+ +
+Variables (T : Type) (x0 : T).
+ +
+Definition mkseq f n : seq T := map f (iota 0 n).
+ +
+Lemma size_mkseq f n : size (mkseq f n) = n.
+ +
+Lemma eq_mkseq f g : f =1 g → mkseq f =1 mkseq g.
+ +
+Lemma nth_mkseq f n i : i < n → nth x0 (mkseq f n) i = f i.
+ +
+Lemma mkseq_nth s : mkseq (nth x0 s) (size s) = s.
+ +
+End MakeSeq.
+ +
+Section MakeEqSeq.
+ +
+Variable T : eqType.
+ +
+Lemma mkseq_uniq (f : nat → T) n : injective f → uniq (mkseq f n).
+ +
+Lemma perm_eq_iotaP {s t : seq T} x0 (It := iota 0 (size t)) :
+ reflect (exists2 Is, perm_eq Is It & s = map (nth x0 t) Is) (perm_eq s t).
+ +
+End MakeEqSeq.
+ +
+ +
+Section FoldRight.
+ +
+Variables (T : Type) (R : Type) (f : T → R → R) (z0 : R).
+ +
+Fixpoint foldr s := if s is x :: s' then f x (foldr s') else z0.
+ +
+End FoldRight.
+ +
+Section FoldRightComp.
+ +
+Variables (T1 T2 : Type) (h : T1 → T2).
+Variables (R : Type) (f : T2 → R → R) (z0 : R).
+ +
+Lemma foldr_cat s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.
+ +
+Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x z ⇒ f (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 (P : pred T) s :
+  sumn [seq (P i : nat ) | i <- s ] = count P s.
+ +
+Lemma sumn_rcons s n : sumn (rcons s n) = sumn s + n.
+ +
+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 z ⇒ f z x) z s.
+ +
+Lemma foldl_cat z s1 s2 : foldl z (s1 ++ s2) = foldl (foldl z s1) s2.
+ +
+End FoldLeft.
+ +
+Section Scan.
+ +
+Variables (T1 : Type) (x1 : T1) (T2 : Type) (x2 : T2).
+Variables (f : T1 → T1 → T2) (g : T1 → T2 → T1).
+ +
+Fixpoint pairmap x s := if s is y :: s' then f x y :: pairmap y s' else [::].
+ +
+Lemma size_pairmap x s : size (pairmap x s) = size s.
+ +
+Lemma pairmap_cat x s1 s2 :
+  pairmap x (s1 ++ s2) = pairmap x s1 ++ pairmap (last x s1) s2.
+ +
+Lemma nth_pairmap s n : n < size s →
+  ∀ x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n).
+ +
+Fixpoint scanl x s :=
+  if s is y :: s' then let x' := g x y in x' :: scanl x' s' else [::].
+ +
+Lemma size_scanl x s : size (scanl x s) = size s.
+ +
+Lemma scanl_cat x s1 s2 :
+  scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2.
+ +
+Lemma nth_scanl s n : n < size s →
+  ∀ x, nth x1 (scanl x s) n = foldl g x (take n .+1 s).
+ +
+Lemma scanlK :
+  (∀ x, cancel (g x) (f x)) → ∀ x, cancel (scanl x) (pairmap x).
+ +
+Lemma pairmapK :
+  (∀ x, cancel (f x) (g x)) → ∀ x, cancel (pairmap x) (scanl x).
+ +
+End Scan.
+ +
+ +
+Section Zip.
+ +
+Variables S T : Type.
+ +
+Fixpoint zip (s : seq S) (t : seq T) {struct t} :=
+  match s, t with
+  | x :: s', y :: t' ⇒ (x, y) :: zip s' t'
+  | _, _ ⇒ [::]
+  end.
+ +
+Definition unzip1 := map (@fst S T).
+Definition unzip2 := map (@snd S T).
+ +
+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 s1 s2 z1 z2 :
+    size s1 = size s2 →
+  zip (rcons s1 z1) (rcons s2 z2) = rcons (zip s1 s2) (z1 , z2 ).
+ +
+Lemma rev_zip s1 s2 :
+  size s1 = size s2 → rev (zip s1 s2) = zip (rev s1) (rev s2).
+ +
+End Zip.
+ +
+ +
+Section Flatten.
+ +
+Variable T : Type.
+Implicit Types (s : seq T) (ss : seq (seq T)).
+ +
+Definition flatten := foldr cat (Nil T).
+Definition shape := map (@size T).
+Fixpoint reshape sh s :=
+  if sh is n :: sh' then take n s :: reshape sh' (drop n s) else [::].
+ +
+Definition flatten_index sh r c := sumn (take r sh) + c.
+Definition reshape_index sh i := find (pred1 0) (scanl subn i .+1 sh).
+Definition reshape_offset sh i := i - sumn (take (reshape_index sh i) sh).
+ +
+Lemma size_flatten ss : size (flatten ss) = sumn (shape ss).
+ +
+Lemma flatten_cat ss1 ss2 : flatten (ss1 ++ ss2) = flatten ss1 ++ flatten ss2.
+ +
+Lemma size_reshape sh s : size (reshape sh s) = size sh.
+ +
+Lemma nth_reshape (sh : seq nat) l n :
+  nth [::] (reshape sh l) n = take (nth 0 sh n) (drop (sumn (take n sh)) l).
+ +
+Lemma flattenK ss : reshape (shape ss) (flatten ss) = ss.
+ +
+Lemma reshapeKr sh s : size s ≤ sumn sh → flatten (reshape sh s) = s.
+ +
+Lemma reshapeKl sh s : size s ≥ sumn sh → shape (reshape sh s) = sh.
+ +
+Lemma flatten_rcons ss s : flatten (rcons ss s) = flatten ss ++ s.
+ +
+Lemma flatten_seq1 s : flatten [seq [:: x ] | x <- s ] = s.
+ +
+Lemma count_flatten ss P :
+  count P (flatten ss) = sumn [seq count P x | x <- ss ].
+ +
+Lemma filter_flatten ss (P : pred T) :
+  filter P (flatten ss) = flatten [seq filter P i | i <- ss ].
+ +
+Lemma rev_flatten ss :
+  rev (flatten ss) = flatten (rev (map rev ss)).
+ +
+Lemma nth_shape ss i : nth 0 (shape ss) i = size (nth [::] ss i).
+ +
+Lemma shape_rev ss : shape (rev ss) = rev (shape ss).
+ +
+Lemma eq_from_flatten_shape ss1 ss2 :
+  flatten ss1 = flatten ss2 → shape ss1 = shape ss2 → ss1 = ss2.
+ +
+Lemma rev_reshape sh s :
+  size s = sumn sh → rev (reshape sh s) = map rev (reshape (rev sh) (rev s)).
+ +
+Lemma reshape_rcons s sh n (m := sumn sh) :
+  m + n = size s →
+  reshape (rcons sh n) s = rcons (reshape sh (take m s)) (drop m s).
+ +
+Lemma flatten_indexP sh r c :
+  c < nth 0 sh r → flatten_index sh r c < sumn sh.
+ +
+Lemma reshape_indexP sh i : i < sumn sh → reshape_index sh i < size sh.
+ +
+Lemma reshape_offsetP sh i :
+  i < sumn sh → reshape_offset sh i < nth 0 sh (reshape_index sh i).
+ +
+Lemma reshape_indexK sh i :
+  flatten_index sh (reshape_index sh i) (reshape_offset sh i) = i.
+ +
+Lemma flatten_indexKl sh r c :
+  c < nth 0 sh r → reshape_index sh (flatten_index sh r c) = r.
+ +
+Lemma flatten_indexKr sh r c :
+  c < nth 0 sh r → reshape_offset sh (flatten_index sh r c) = c.
+ +
+Lemma nth_flatten x0 ss i (r := reshape_index (shape ss) i) :
+  nth x0 (flatten ss) i = nth x0 (nth [::] ss r) (reshape_offset (shape ss) i).
+ +
+Lemma reshape_leq sh i1 i2
+  (r1 := reshape_index sh i1) (c1 := reshape_offset sh i1)
+  (r2 := reshape_index sh i2) (c2 := reshape_offset sh i2) :
+  (i1 ≤ i2 ) = ((r1 < r2 ) || ((r1 == r2 ) && (c1 ≤ c2 ))).
+ +
+End Flatten.
+ +
+ +
+Lemma map_flatten S T (f : T → S) ss :
+  map f (flatten ss) = flatten (map (map f) ss).
+ +
+Lemma sumn_flatten (ss : seq (seq nat)) :
+  sumn (flatten ss) = sumn (map sumn ss).
+ +
+Lemma map_reshape T S (f : T → S) sh s :
+  map (map f) (reshape sh s) = reshape sh (map f s).
+ +
+Section EqFlatten.
+ +
+Variables S T : eqType.
+ +
+Lemma flattenP (A : seq (seq T)) x :
+  reflect (exists2 s, s \in A & x \in s) (x \in flatten A).
+ +
+Lemma flatten_mapP (A : S → seq T) s y :
+  reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)).
+ +
+End EqFlatten.
+ +
+ +
+Lemma perm_undup_count (T : eqType) (s : seq T) :
+  perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s ]) s.
+ +
+Section AllPairs.
+ +
+Variables (S T R : Type) (f : S → T → R).
+Implicit Types (s : seq S) (t : seq T).
+ +
+Definition allpairs s t := foldr (fun x ⇒ cat (map (f x) t)) [::] s.
+ +
+Lemma size_allpairs s t : size (allpairs s t) = size s × size t.
+ +
+Lemma allpairs_cat s1 s2 t :
+  allpairs (s1 ++ s2) t = allpairs s1 t ++ allpairs s2 t.
+ +
+End AllPairs.
+ +
+ +
+Notation "[ 'seq' E | i <- s , j <- t ]" := (allpairs (fun i j ⇒ E) s t)
+  (at level 0, E at level 99, i ident, j ident,
+   format "[ '[hv' 'seq' E '/ ' | i <- s , '/ ' j <- t ] ']'")
+   : seq_scope.
+Notation "[ 'seq' E | i : T <- s , j : U <- t ]" :=
+  (allpairs (fun (i : T) (j : U) ⇒ E) s t)
+  (at level 0, E at level 99, i ident, j ident, only parsing) : seq_scope.
+ +
+Section EqAllPairs.
+ +
+Variables S T : eqType.
+Implicit Types (R : eqType) (s : seq S) (t : seq T).
+ +
+Lemma allpairsP R (f : S → T → R) s t z :
+  reflect (∃ p, [/\ p .1 \in s , p .2 \in t & z = f p .1 p .2 ])
+          (z \in allpairs f s t).
+ +
+Lemma mem_allpairs R (f : S → T → R) s1 t1 s2 t2 :
+  s1 =i s2 → t1 =i t2 → allpairs f s1 t1 =i allpairs f s2 t2.
+ +
+Lemma allpairs_catr R (f : S → T → R) s t1 t2 :
+  allpairs f s (t1 ++ t2) =i allpairs f s t1 ++ allpairs f s t2.
+ +
+Lemma allpairs_uniq R (f : S → T → R) s t :
+    uniq s → uniq t →
+    {in [seq (x , y ) | x <- s , y <- t ] &, injective (prod_curry f)} →
+  uniq (allpairs f s t).
+ +
+End EqAllPairs.
+