Library mathcomp.ssreflect.seq

(* (c) Copyright 2006-2015 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. subfilter s : seq sT == when sT has a subType p structure, the sequence of items of type sT corresponding to items of s for which 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) ]#]

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

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

Implicit Arguments nilP [T s].
Implicit Arguments all_filterP [T a 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.

End Rev.

Implicit Arguments revK [[T]].

Equality and eqType for seq.

Section EqSeq.

Variables (n0 : nat) (T : eqType) (x0 : T).
Notation Local nth := (nth x0).
Implicit Type s : seq T.
Implicit Types x y z : T.

Fixpoint eqseq s1 s2 {struct s2} :=
  match s1, s2 with
  | [::], [::] ⇒ true
  | x1 :: s1', x2 :: s2' ⇒ (x1 == x2) && eqseq s1' s2'
  | _, _ ⇒ false
  end.

Lemma eqseqP : Equality.axiom eqseq.

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


Implicit Arguments eqseqP [T x y].
Implicit Arguments hasP [T a s].
Implicit Arguments hasPn [T a s].
Implicit Arguments allP [T a s].
Implicit Arguments allPn [T a s].
Implicit Arguments nseqP [T n x y].
Implicit Arguments count_memPn [T x s].

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

Implicit Arguments nthP [T s x].
Implicit Arguments has_nthP [T a s].
Implicit Arguments all_nthP [T a s].

Definition bitseq := seq bool.
Canonical 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.

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

Implicit Arguments perm_eqP [T s1 s2].
Implicit Arguments perm_eqlP [T s1 s2].
Implicit Arguments perm_eqrP [T s1 s2].
Hint Resolve perm_eq_refl.

Section RotrLemmas.

Variables (n0 : nat) (T : Type) (T' : eqType).
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_rot s : rev (rot n0 s) = rotr n0 (rev s).

Lemma rev_rotr s : rev (rotr n0 s) = rot 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.

Implicit Arguments subseqP [T s1 s2].

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.

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

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.

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

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 m n i : i < n → nth 0 (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.

Implicit Arguments perm_eq_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_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 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 [::].

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

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

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.

End Flatten.


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

End EqFlatten.

Implicit Arguments flattenP [T A x].
Implicit Arguments flatten_mapP [S T A s y].

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.