- -

Library mathcomp.ssreflect.seq

- -

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

- -

- The seq type is the ssreflect type for sequences; it is an alias for the - standard Coq list type. The ssreflect library equips it with many - operations, as well as eqType and predType (and, later, choiceType) - structures. The operations are geared towards reflection: they generally - expect and provide boolean predicates, e.g., the membership predicate - expects an eqType. To avoid any confusion we do not Import the Coq List - module. - As there is no true subtyping in Coq, we don't use a type for non-empty - sequences; rather, we pass explicitly the head and tail of the sequence. - The empty sequence is especially bothersome for subscripting, since it - forces us to pass a default value. This default value can often be hidden - by a notation. - Here is the list of seq operations: -

Constructors:

- - seq T == the type of sequences of items of type T. - bitseq == seq bool. - [:: ], nil, Nil T == the empty sequence (of type T). - x :: s, cons x s, Cons T x s == the sequence x followed by s (of type T). - [:: x] == the singleton sequence. - [:: x_0; ...; x_n] == the explicit sequence of the x_i. - [:: x_0, ..., x_n & s] == the sequence of the x_i, followed by s. - rcons s x == the sequence s, followed by x. - All of the above, except rcons, can be used in patterns. We define a view - lastP and an induction principle last_ind that can be used to decompose - or traverse a sequence in a right to left order. The view lemma lastP has - a dependent family type, so the ssreflect tactic case/lastP: p => [|p' x] - will generate two subgoals in which p has been replaced by [:: ] and by - rcons p' x, respectively. -

Factories:

- - nseq n x == a sequence of n x's. - ncons n x s == a sequence of n x's, followed by s. - seqn n x_0 ... x_n-1 == the sequence of the x_i; can be partially applied. - iota m n == the sequence m, m + 1, ..., m + n - 1. - mkseq f n == the sequence f 0, f 1, ..., f (n - 1). -

Sequential access:

- - head x0 s == the head (zero'th item) of s if s is non-empty, else x0. - ohead s == None if s is empty, else Some x when the head of s is x. - behead s == s minus its head, i.e., s' if s = x :: s', else [:: ]. - last x s == the last element of x :: s (which is non-empty). - belast x s == x :: s minus its last item. -

Dimensions:

- - size s == the number of items (length) in s. - shape ss == the sequence of sizes of the items of the sequence of - sequences ss. -

Random access:

- - nth x0 s i == the item i of s (numbered from 0), or x0 if s does - not have at least i+1 items (i.e., size x <= i) - s`i == standard notation for nth x0 s i for a default x0, - e.g., 0 for rings. - set_nth x0 s i y == s where item i has been changed to y; if s does not - have an item i, it is first padded with copies of x0 - to size i+1. - incr_nth s i == the nat sequence s with item i incremented (s is - first padded with 0's to size i+1, if needed). -
Predicates:
- - nilp s <=> s is [:: ]. - := (size s == 0). - x \in s == x appears in s (this requires an eqType for T). - index x s == the first index at which x appears in s, or size s if - x \notin s. - has a s <=> a holds for some item in s, where a is an applicative - bool predicate. - all a s <=> a holds for all items in s. - 'has_aP <-> the view reflect (exists2 x, x \in s & A x) (has a s), - where aP x : reflect (A x) (a x). - 'all_aP <=> the view for reflect {in s, forall x, A x} (all a s). - all2 r s t <=> the (bool) relation r holds for all respective items - in s and t, which must also have the same size, i.e., - for s := [:: x1; ...; x_m] and t := [:: y1; ...; y_n], - the condition [&& r x_1 y_1, ..., r x_n y_n & m == n]. - find p s == the index of the first item in s for which p holds, - or size s if no such item is found. - count p s == the number of items of s for which p holds. - count_mem x s == the multiplicity of x in s, i.e., count (pred1 x) s. - tally s == a tally of s, i.e., a sequence of (item, multiplicity) - pairs for all items in sequence s (without duplicates). - incr_tally bs x == increment the multiplicity of x in the tally bs, or add - x with multiplicity 1 at then end if x is not in bs. - bs \is a wf_tally <=> bs is well-formed tally, with no duplicate items or - null multiplicities. - tally_seq bs == the expansion of a tally bs into a sequence where each - (x, n) pair expands into a sequence of n x's. - constant s <=> all items in s are identical (trivial if s = [:: ]). - uniq s <=> all the items in s are pairwise different. - subseq s1 s2 <=> s1 is a subsequence of s2, i.e., s1 = mask m s2 for - some m : bitseq (see below). - perm_eq s1 s2 <=> s2 is a permutation of s1, i.e., s1 and s2 have the - items (with the same repetitions), but possibly in a - different order. - perm_eql s1 s2 <-> s1 and s2 behave identically on the left of perm_eq. - perm_eqr s1 s2 <-> s1 and s2 behave identically on the right of perm_eq. -> These left/right transitive versions of perm_eq make it easier to - chain a sequence of equivalences. - permutations s == a duplicate-free list of all permutations of s. -
Filtering:
- - filter p s == the subsequence of s consisting of all the items - for which the (boolean) predicate p holds. - rem x s == the subsequence of s, where the first occurrence - of x has been removed (compare filter (predC1 x) s - where ALL occurrences of x are removed). - undup s == the subsequence of s containing only the first - occurrence of each item in s, i.e., s with all - duplicates removed. - mask m s == the subsequence of s selected by m : bitseq, with - item i of s selected by bit i in m (extra items or - bits are ignored. -
Surgery:
- - s1 ++ s2, cat s1 s2 == the concatenation of s1 and s2. - take n s == the sequence containing only the first n items of s - (or all of s if size s <= n). - drop n s == s minus its first n items ( [:: ] if size s <= n) - rot n s == s rotated left n times (or s if size s <= n). - := drop n s ++ take n s - rotr n s == s rotated right n times (or s if size s <= n). - rev s == the (linear time) reversal of s. - catrev s1 s2 == the reversal of s1 followed by s2 (this is the - recursive form of rev). -
Dependent iterator: for s : seq S and t : S -> seq T
- - [seq E | x <- s, y <- t] := flatten [seq [seq E | x <- t] | y <- s] - == the sequence of all the f x y, with x and y drawn from - s and t, respectively, in row-major order, - and where t is possibly dependent in elements of s - allpairs_dep f s t := self expanding definition for - [seq f x y | x <- s, y <- t i] -
Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m],
- - allpairs f s t := same as allpairs_dep but where t is non dependent, - i.e. self expanding definition for - [seq f x y | x <- s, y <- t] - := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] - map f s == the sequence [:: f x_1, ..., f x_n]. - pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik, - pf x_i = Some y_i, and pf x_j = None iff j is not in - {i1, ..., ik}. - foldr f a s == the right fold of s by f (i.e., the natural iterator). - := f x_1 (f x_2 ... (f x_n a)) - sumn s == x_1 + (x_2 + ... + (x_n + 0)) (when s : seq nat). - foldl f a s == the left fold of s by f. - := f (f ... (f a x_1) ... x_n-1) x_n - scanl f a s == the sequence of partial accumulators of foldl f a s. - := [:: f a x_1; ...; foldl f a s] - pairmap f a s == the sequence of f applied to consecutive items in a :: s. - := [:: f a x_1; f x_1 x_2; ...; f x_n-1 x_n] - zip s t == itemwise pairing of s and t (dropping any extra items). - := [:: (x_1, y_1); ...; (x_mn, y_mn) ] with mn = minn n m. - unzip1 s == [:: (x_1).1; ...; (x_n).1] when s : seq (S * T). - unzip2 s == [:: (x_1).2; ...; (x_n).2] when s : seq (S * T). - flatten s == x_1 ++ ... ++ x_n ++ [:: ] when s : seq (seq T). - reshape r s == s reshaped into a sequence of sequences whose sizes are - given by r (truncating if s is too long or too short). - := [:: [:: x_1; ...; x_r1]; - [:: x(r1 + 1); ...; x(r0 + r1) ]; - ...; - [:: x(r1 + ... + r(k-1) + 1); ...; x(r0 + ... rk) ]#] - flatten_index sh r c == the index, in flatten ss, of the item of indexes - (r, c) in any sequence of sequences ss of shape sh - := sh_1 + sh_2 + ... + sh_r + c - reshape_index sh i == the index, in reshape sh s, of the sequence - containing the i-th item of s. - reshape_offset sh i == the offset, in the (reshape_index sh i)-th - sequence of reshape sh s of the i-th item of s -
Notation for manifest comprehensions:
- - [seq x <- s | C] := filter (fun x => C) s. - [seq E | x <- s] := map (fun x => E) s. - [seq x <- s | C1 & C2] := [seq x <- s | C1 && C2]. - [seq E | x <- s & C] := [seq E | x <- [seq x | C] ]. -> The above allow optional type casts on the eigenvariables, as in - [seq x : T <- s | C] or [seq E | x : T <- s, y : U <- t]. The cast may be - needed as type inference considers E or C before s. - We are quite systematic in providing lemmas to rewrite any composition - of two operations. "rev", whose simplifications are not natural, is - protected with nosimpl. -
The following are equivalent:
- - [<-> P0; P1; ..; Pn] <-> P0, P1, ..., Pn are all equivalent. - := P0 -> P1 -> ... -> Pn -> P0 - if T : [<-> P0; P1; ..; Pn] is such an equivalence, and i, j are in nat - then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj; - when i (resp. j) is out of bounds, Pi (resp. Pj) defaults to P0. -

-
- -
-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.
- -
-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.
- -
-Variant last_spec : seq T → Type :=
-  | LastNil : last_spec [::]
-  | LastRcons s x : last_spec (rcons s x).
- -
-Lemma lastP s : last_spec s.
- -
-Lemma last_ind P :
-  P [::] → (∀ s x, P s → P (rcons s x)) → ∀ s, P s.
- -
-
- -
- Sequence indexing. -
-
- -
-Fixpoint nth s n {struct n} :=
-  if s is x :: s' then if n is n'.+1 then @nth s' n' else x else x0.
- -
-Fixpoint set_nth s n y {struct n} :=
-  if s is x :: s' then if n is n'.+1 then x :: @set_nth s' n' y else y :: s'
-  else ncons n x0 [:: y ].
- -
-Lemma nth0 s : nth s 0 = head s.
- -
-Lemma nth_default s n : size s ≤ n → nth s n = x0.
- -
-Lemma nth_nil n : nth [::] n = x0.
- -
-Lemma last_nth x s : last x s = nth (x :: s) (size s).
- -
-Lemma nth_last s : nth s (size s ).-1 = last x0 s.
- -
-Lemma nth_behead s n : nth (behead s) n = nth s n .+1.
- -
-Lemma nth_cat s1 s2 n :
-  nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1).
- -
-Lemma nth_rcons s x n :
-  nth (rcons s x) n =
-    if n < size s then nth s n else if n == size s then x else x0.
- -
-Lemma nth_ncons m x s n :
-  nth (ncons m x s) n = if n < m then x else nth s (n - m).
- -
-Lemma nth_nseq m x n : nth (nseq m x) n = (if n < m then x else x0 ).
- -
-Lemma eq_from_nth s1 s2 :
-    size s1 = size s2 → (∀ i, i < size s1 → nth s1 i = nth s2 i ) →
-  s1 = s2.
- -
-Lemma size_set_nth s n y : size (set_nth s n y) = maxn n .+1 (size s).
- -
-Lemma set_nth_nil n y : set_nth [::] n y = ncons n x0 [:: y ].
- -
-Lemma nth_set_nth s n y : nth (set_nth s n y) =1 [eta nth s with n |-> y ].
- -
-Lemma set_set_nth s n1 y1 n2 y2 (s2 := set_nth s n2 y2) :
-  set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1.
- -
-
- -
- find, count, has, all. -
-
- -
-Section SeqFind.
- -
-Variable a : pred T.
- -
-Fixpoint find s := if s is x :: s' then if a x then 0 else (find s').+1 else 0.
- -
-Fixpoint filter s :=
-  if s is x :: s' then if a x then x :: filter s' else filter s' else [::].
- -
-Fixpoint count s := if s is x :: s' then a x + count s' else 0.
- -
-Fixpoint has s := if s is x :: s' then a x || has s' else false.
- -
-Fixpoint all s := if s is x :: s' then a x && all s' else true.
- -
-Lemma size_filter s : size (filter s) = count s.
- -
-Lemma has_count s : has s = (0 < count s ).
- -
-Lemma count_size s : count s ≤ size s.
- -
-Lemma all_count s : all s = (count s == size s ).
- -
-Lemma filter_all s : all (filter s).
- -
-Lemma all_filterP s : reflect (filter s = s) (all s).
- -
-Lemma filter_id s : filter (filter s) = filter s.
- -
-Lemma has_find s : has s = (find s < size s ).
- -
-Lemma find_size s : find s ≤ size s.
- -
-Lemma find_cat s1 s2 :
-  find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2.
- -
-Lemma has_nil : has [::] = false.
- -
-Lemma has_seq1 x : has [:: x ] = a x.
- -
-Lemma has_nseq n x : has (nseq n x) = (0 < n ) && a x.
- -
-Lemma has_seqb (b : bool) x : has (nseq b x) = b && a x.
- -
-Lemma all_nil : all [::] = true.
- -
-Lemma all_seq1 x : all [:: x ] = a x.
- -
-Lemma all_nseq n x : all (nseq n x) = (n == 0) || a x.
- -
-Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x.
- -
-Lemma filter_nseq n x : filter (nseq n x) = nseq (a x × n) x.
- -
-Lemma count_nseq n x : count (nseq n x) = a x × n.
- -
-Lemma find_nseq n x : find (nseq n x) = ~~ a x × n.
- -
-Lemma nth_find s : has s → a (nth s (find s)).
- -
-Lemma before_find s i : i < find s → a (nth s i) = false.
- -
-Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
- -
-Lemma filter_rcons s x :
-  filter (rcons s x) = if a x then rcons (filter s) x else filter s.
- -
-Lemma count_cat s1 s2 : count (s1 ++ s2) = count s1 + count s2.
- -
-Lemma has_cat s1 s2 : has (s1 ++ s2) = has s1 || has s2.
- -
-Lemma has_rcons s x : has (rcons s x) = a x || has s.
- -
-Lemma all_cat s1 s2 : all (s1 ++ s2) = all s1 && all s2.
- -
-Lemma all_rcons s x : all (rcons s x) = a x && all s.
- -
-End SeqFind.
- -
-Lemma eq_find a1 a2 : a1 =1 a2 → find a1 =1 find a2.
- -
-Lemma eq_filter a1 a2 : a1 =1 a2 → filter a1 =1 filter a2.
- -
-Lemma eq_count a1 a2 : a1 =1 a2 → count a1 =1 count a2.
- -
-Lemma eq_has a1 a2 : a1 =1 a2 → has a1 =1 has a2.
- -
-Lemma eq_all a1 a2 : a1 =1 a2 → all a1 =1 all a2.
- -
-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 s2 : n0 ≤ size s1 → take n0 (s1 ++ s2) = take n0 s1.
- -
-Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
- -
-Lemma nth_take i : i < n0 → ∀ s, nth (take n0 s) i = nth s i.
- -
-
- -
- drop_nth and take_nth below do NOT use the default n0, because the "n" - can be inferred from the condition, whereas the nth default value x0 - will have to be given explicitly (and this will provide "d" as well). -
-
- -
-Lemma drop_nth n s : n < size s → drop n s = nth s n :: drop n .+1 s.
- -
-Lemma take_nth n s : n < size s → take n .+1 s = rcons (take n s) (nth s n).
- -
-
- -
- Rotation -
-
- -
-Definition rot n s := drop n s ++ take n s.
- -
-Lemma rot0 s : rot 0 s = s.
- -
-Lemma size_rot s : size (rot n0 s) = size s.
- -
-Lemma rot_oversize n s : size s ≤ n → rot n s = s.
- -
-Lemma rot_size s : rot (size s) s = s.
- -
-Lemma has_rot s a : has a (rot n0 s) = has a s.
- -
-Lemma rot_size_cat s1 s2 : rot (size s1) (s1 ++ s2) = s2 ++ s1.
- -
-Definition rotr n s := rot (size s - n) s.
- -
-Lemma rotK : cancel (rot n0) (rotr n0).
- -
-Lemma rot_inj : injective (rot n0).
- -
-
- -
- (efficient) reversal -
-
- -
-Fixpoint catrev s1 s2 := if s1 is x :: s1' then catrev s1' (x :: s2) else s2.
- -
-Definition rev s := catrev s [::].
- -
-Lemma catrev_catl s t u : catrev (s ++ t) u = catrev t (catrev s u).
- -
-Lemma catrev_catr s t u : catrev s (t ++ u) = catrev s t ++ u.
- -
-Lemma catrevE s t : catrev s t = rev s ++ t.
- -
-Lemma rev_cons x s : rev (x :: s) = rcons (rev s) x.
- -
-Lemma size_rev s : size (rev s) = size s.
- -
-Lemma rev_cat s t : rev (s ++ t) = rev t ++ rev s.
- -
-Lemma rev_rcons s x : rev (rcons s x) = x :: rev s.
- -
-Lemma revK : involutive rev.
- -
-Lemma nth_rev n s : n < size s → nth (rev s) n = nth s (size s - n .+1).
- -
-Lemma filter_rev a s : filter a (rev s) = rev (filter a s).
- -
-Lemma count_rev a s : count a (rev s) = count a s.
- -
-Lemma has_rev a s : has a (rev s) = has a s.
- -
-Lemma all_rev a s : all a (rev s) = all a s.
- -
-End Sequences.
- -
- -
- -
-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 seq_ind2 {S T} (P : seq S → seq T → Type) :
-    P [::] [::] →
-    (∀ x y s t, size s = size t → P s t → P (x :: s) (y :: t)) →
-  ∀ s t, size s = size t → P s t.
- -
-Section RotRcons.
- -
-Variable T : Type.
-Implicit Types (x : T) (s : seq T).
- -
-Lemma rot1_cons x s : rot 1 (x :: s) = rcons s x.
- -
-Lemma rcons_inj s1 s2 x1 x2 :
-  rcons s1 x1 = rcons s2 x2 :> seq T → (s1 , x1 ) = (s2 , x2 ).
- -
-Lemma rcons_injl x : injective (rcons ^~ x).
- -
-Lemma rcons_injr s : injective (rcons s).
- -
-End RotRcons.
- -
- -
-
- -
- Equality and eqType for seq. -
-
- -
-Section EqSeq.
- -
-Variables (n0 : nat) (T : eqType) (x0 : T).
-Implicit Types (x y z : T) (s : seq T).
- -
-Fixpoint eqseq s1 s2 {struct s2} :=
-  match s1, s2 with
-  | [::], [::] ⇒ true
-  | x1 :: s1', x2 :: s2' ⇒ (x1 == x2) && eqseq s1' s2'
-  | _, _ ⇒ false
-  end.
- -
-Lemma eqseqP : Equality.axiom eqseq.
- -
-Canonical seq_eqMixin := EqMixin eqseqP.
-Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.
- -
-Lemma eqseqE : eqseq = eq_op.
- -
-Lemma eqseq_cons x1 x2 s1 s2 :
-  (x1 :: s1 == x2 :: s2 ) = (x1 == x2 ) && (s1 == s2 ).
- -
-Lemma eqseq_cat s1 s2 s3 s4 :
-  size s1 = size s2 → (s1 ++ s3 == s2 ++ s4 ) = (s1 == s2 ) && (s3 == s4 ).
- -
-Lemma eqseq_rcons s1 s2 x1 x2 :
-  (rcons s1 x1 == rcons s2 x2 ) = (s1 == s2 ) && (x1 == x2 ).
- -
-Lemma size_eq0 s : (size s == 0) = (s == [::]).
- -
-Lemma has_filter a s : has a s = (filter a s != [::]).
- -
-
- -
- mem_seq and index. - mem_seq defines a predType for seq. -
-
- -
-Fixpoint mem_seq (s : seq T) :=
-  if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
- -
-Definition seq_eqclass := seq T.
-Identity Coercion seq_of_eqclass : seq_eqclass >-> seq.
-Coercion pred_of_seq (s : seq_eqclass) : {pred T } := mem_seq s.
- -
-Canonical seq_predType := PredType (pred_of_seq : seq T → pred T).
-
- -
- The line below makes mem_seq a canonical instance of topred. -
-
-Canonical mem_seq_predType := PredType mem_seq.
- -
-Lemma in_cons y s x : (x \in y :: s ) = (x == y ) || (x \in s ).
- -
-Lemma in_nil x : (x \in [::]) = false.
- -
-Lemma mem_seq1 x y : (x \in [:: y ]) = (x == y ).
- -
- (* to be repeated after the Section discharge. *)
-Let inE := (mem_seq1 , in_cons , inE ).
- -
-Lemma mem_seq2 x y z : (x \in [:: y ; z ]) = xpred2 y z x.
- -
-Lemma mem_seq3 x y z t : (x \in [:: y ; z ; t ]) = xpred3 y z t x.
- -
-Lemma mem_seq4 x y z t u : (x \in [:: y ; z ; t ; u ]) = xpred4 y z t u x.
- -
-Lemma mem_cat x s1 s2 : (x \in s1 ++ s2 ) = (x \in s1 ) || (x \in s2 ).
- -
-Lemma mem_rcons s y : rcons s y =i y :: s.
- -
-Lemma mem_head x s : x \in x :: s.
- -
-Lemma mem_last x s : last x s \in x :: s.
- -
-Lemma mem_behead s : {subset behead s ≤ s }.
- -
-Lemma mem_belast s y : {subset belast y s ≤ y :: s }.
- -
-Lemma mem_nth s n : n < size s → nth s n \in s.
- -
-Lemma mem_take s x : x \in take n0 s → x \in s.
- -
-Lemma mem_drop s x : x \in drop n0 s → x \in s.
- -
-Lemma last_eq s z x y : x != y → z != y → (last x s == y ) = (last z s == y ).
- -
-Section Filters.
- -
-Implicit Type a : pred T.
- -
-Lemma hasP {a s} : reflect (exists2 x, x \in s & a x) (has a s).
- -
-Lemma allP {a s} : reflect {in s , ∀ x, a x } (all a s).
- -
-Lemma hasPn a s : reflect {in s , ∀ x, ~~ a x } (~~ has a s).
- -
-Lemma allPn a s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).
- -
-Lemma mem_filter a x s : (x \in filter a s ) = a x && (x \in s ).
- -
-Variables (a : pred T) (s : seq T) (A : T → Prop).
-Hypothesis aP : ∀ x, reflect (A x) (a x).
- -
-Lemma hasPP : reflect (exists2 x, x \in s & A x) (has a s).
- -
-Lemma allPP : reflect {in s , ∀ x, A x } (all a s).
- -
-End Filters.
- -
-Notation "'has_ view" := (hasPP _ (fun _ ⇒ view))
-  (at level 4, right associativity, format "''has_' view").
-Notation "'all_ view" := (allPP _ (fun _ ⇒ view))
-  (at level 4, right associativity, format "''all_' view").
- -
-Section EqIn.
- -
-Variables a1 a2 : pred T.
- -
-Lemma eq_in_filter s : {in s , a1 =1 a2 } → filter a1 s = filter a2 s.
- -
-Lemma eq_in_find s : {in s , a1 =1 a2 } → find a1 s = find a2 s.
- -
-Lemma eq_in_count s : {in s , a1 =1 a2 } → count a1 s = count a2 s.
- -
-Lemma eq_in_all s : {in s , a1 =1 a2 } → all a1 s = all a2 s.
- -
-Lemma eq_in_has s : {in s , a1 =1 a2 } → has a1 s = has a2 s.
- -
-End EqIn.
- -
-Lemma eq_has_r s1 s2 : s1 =i s2 → has ^~ s1 =1 has ^~ s2.
- -
-Lemma eq_all_r s1 s2 : s1 =i s2 → all ^~ s1 =1 all ^~ s2.
- -
-Lemma has_sym s1 s2 : has (mem s1) s2 = has (mem s2) s1.
- -
-Lemma has_pred1 x s : has (pred1 x) s = (x \in s ).
- -
-Lemma mem_rev s : rev s =i s.
- -
-
- -
- Constant sequences, i.e., the image of nseq. -
-
- -
-Definition constant s := if s is x :: s' then all (pred1 x) s' else true.
- -
-Lemma all_pred1P x s : reflect (s = nseq (size s) x) (all (pred1 x) s).
- -
-Lemma all_pred1_constant x s : all (pred1 x) s → constant s.
- -
-Lemma all_pred1_nseq x n : all (pred1 x) (nseq n x).
- -
-Lemma mem_nseq n x y : (y \in nseq n x ) = (0 < n ) && (y == x ).
- -
-Lemma nseqP n x y : reflect (y = x ∧ n > 0) (y \in nseq n x).
- -
-Lemma constant_nseq n x : constant (nseq n x).
- -
-
- -
- Uses x0 -
-
-Lemma constantP s : reflect (∃ x, s = nseq (size s) x) (constant s).
- -
-
- -
- Duplicate-freenes. -
-
- -
-Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
- -
-Lemma cons_uniq x s : uniq (x :: s) = (x \notin s ) && uniq s.
- -
-Lemma cat_uniq s1 s2 :
-  uniq (s1 ++ s2) = [&& uniq s1 , ~~ has (mem s1) s2 & uniq s2 ].
- -
-Lemma uniq_catC s1 s2 : uniq (s1 ++ s2) = uniq (s2 ++ s1).
- -
-Lemma uniq_catCA s1 s2 s3 : uniq (s1 ++ s2 ++ s3) = uniq (s2 ++ s1 ++ s3).
- -
-Lemma rcons_uniq s x : uniq (rcons s x) = (x \notin s ) && uniq s.
- -
-Lemma filter_uniq s a : uniq s → uniq (filter a s).
- -
-Lemma rot_uniq s : uniq (rot n0 s) = uniq s.
- -
-Lemma rev_uniq s : uniq (rev s) = uniq s.
- -
-Lemma count_memPn x s : reflect (count_mem x s = 0) (x \notin s).
- -
-Lemma count_uniq_mem s x : uniq s → count_mem x s = (x \in s ).
- -
-Lemma filter_pred1_uniq s x : uniq s → x \in s → filter (pred1 x) s = [:: x ].
- -
-
- -
- Removing duplicates -
-
- -
-Fixpoint undup s :=
-  if s is x :: s' then if x \in s' then undup s' else x :: undup s' else [::].
- -
-Lemma size_undup s : size (undup s) ≤ size s.
- -
-Lemma mem_undup s : undup s =i s.
- -
-Lemma undup_uniq s : uniq (undup s).
- -
-Lemma undup_id s : uniq s → undup s = s.
- -
-Lemma ltn_size_undup s : (size (undup s) < size s ) = ~~ uniq s.
- -
-Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
- -
-Lemma undup_nil s : undup s = [::] → s = [::].
- -
-
- -
- Lookup -
-
- -
-Definition index x := find (pred1 x).
- -
-Lemma index_size x s : index x s ≤ size s.
- -
-Lemma index_mem x s : (index x s < size s ) = (x \in s ).
- -
-Lemma nth_index x s : x \in s → nth s (index x s) = x.
- -
-Lemma index_cat x s1 s2 :
- index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2.
- -
-Lemma nthK s: uniq s → {in gtn (size s), cancel (nth s) (index ^~ s)}.
- -
-Lemma index_uniq i s : i < size s → uniq s → index (nth s i) s = i.
- -
-Lemma index_head x s : index x (x :: s) = 0.
- -
-Lemma index_last x s : uniq (x :: s) → index (last x s) (x :: s) = size s.
- -
-Lemma nth_uniq s i j :
-  i < size s → j < size s → uniq s → (nth s i == nth s j ) = (i == j ).
- -
-Lemma uniqPn s :
-  reflect (∃ i j, [/\ i < j , j < size s & nth s i = nth s j ]) (~~ uniq s).
- -
-Lemma uniqP s : reflect {in gtn (size s) &, injective (nth s)} (uniq s).
- -
-Lemma mem_rot s : rot n0 s =i s.
- -
-Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2 ) = (s1 == s2 ).
- -
-Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
- -
-Lemma rot_to s x : x \in s → rot_to_spec s x.
- -
-End 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 permP s1 s2 : reflect (count ^~ s1 =1 count ^~ s2) (perm_eq s1 s2).
- -
-Lemma perm_refl s : perm_eq s s.
- Hint Resolve perm_refl : core.
- -
-Lemma perm_sym : symmetric perm_eq.
- -
-Lemma perm_trans : transitive perm_eq.
- -
-Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
-Notation perm_eqr s1 s2 := (perm_eq ^~ s1 =1 perm_eq ^~ s2).
- -
-Lemma permEl s1 s2 : perm_eql s1 s2 → perm_eq s1 s2.
- -
-Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
- -
-Lemma permPr s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2).
- -
-Lemma perm_catC s1 s2 : perm_eql (s1 ++ s2) (s2 ++ s1).
- -
-Lemma perm_cat2l s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.
- -
-Lemma perm_catl s t1 t2 : perm_eq t1 t2 → perm_eql (s ++ t1) (s ++ t2).
- -
-Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.
- -
-Lemma perm_cat2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.
- -
-Lemma perm_catr s1 s2 t : perm_eq s1 s2 → perm_eql (s1 ++ t) (s2 ++ t).
- -
-Lemma perm_cat s1 s2 t1 t2 :
-  perm_eq s1 s2 → perm_eq t1 t2 → perm_eq (s1 ++ t1) (s2 ++ t2).
- -
-Lemma perm_catAC s1 s2 s3 : perm_eql ((s1 ++ s2 ) ++ s3) ((s1 ++ s3 ) ++ s2).
- -
-Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).
- -
-Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s).
- -
-Lemma perm_rot n s : perm_eql (rot n s) s.
- -
-Lemma perm_rotr n s : perm_eql (rotr n s) s.
- -
-Lemma perm_rev s : perm_eql (rev s) s.
- -
-Lemma perm_filter s1 s2 a :
-  perm_eq s1 s2 → perm_eq (filter a s1) (filter a s2).
- -
-Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
- -
-Lemma perm_size s1 s2 : perm_eq s1 s2 → size s1 = size s2.
- -
-Lemma perm_mem s1 s2 : perm_eq s1 s2 → s1 =i s2.
- -
-Lemma perm_nilP s : reflect (s = [::]) (perm_eq s [::]).
- -
-Lemma perm_consP x s t :
-  reflect (∃ i u, rot i t = x :: u ∧ perm_eq u s)
-          (perm_eq t (x :: s)).
- -
-Lemma perm_has s1 s2 a : perm_eq s1 s2 → has a s1 = has a s2.
- -
-Lemma perm_all s1 s2 a : perm_eq s1 s2 → all a s1 = all a s2.
- -
-Lemma perm_small_eq s1 s2 : size s2 ≤ 1 → perm_eq s1 s2 → s1 = s2.
- -
-Lemma uniq_leq_size s1 s2 : uniq s1 → {subset s1 ≤ s2 } → size s1 ≤ size s2.
- -
-Lemma leq_size_uniq s1 s2 :
-  uniq s1 → {subset s1 ≤ s2 } → size s2 ≤ size s1 → uniq s2.
- -
-Lemma uniq_size_uniq s1 s2 :
-  uniq s1 → s1 =i s2 → uniq s2 = (size s2 == size s1 ).
- -
-Lemma uniq_min_size s1 s2 :
-    uniq s1 → {subset s1 ≤ s2 } → size s2 ≤ size s1 →
-  (size s1 = size s2 ) × (s1 =i s2 ).
- -
-Lemma eq_uniq s1 s2 : size s1 = size s2 → s1 =i s2 → uniq s1 = uniq s2.
- -
-Lemma perm_uniq s1 s2 : perm_eq s1 s2 → uniq s1 = uniq s2.
- -
-Lemma uniq_perm s1 s2 : uniq s1 → uniq s2 → s1 =i s2 → perm_eq s1 s2.
- -
-Lemma perm_undup s1 s2 : s1 =i s2 → perm_eq (undup s1) (undup s2).
- -
-Lemma count_mem_uniq s : (∀ x, count_mem x s = (x \in s )) → uniq s.
- -
-Lemma catCA_perm_ind P :
-    (∀ s1 s2 s3, P (s1 ++ s2 ++ s3) → P (s2 ++ s1 ++ s3)) →
-  (∀ s1 s2, perm_eq s1 s2 → P s1 → P s2 ).
- -
-Lemma catCA_perm_subst R F :
-    (∀ s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R ) →
-  (∀ s1 s2, perm_eq s1 s2 → F s1 = F s2 ).
- -
-End PermSeq.
- -
-Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
-Notation perm_eqr s1 s2 := (perm_eq ^~ s1 =1 perm_eq ^~ s2).
- -
-Hint Resolve perm_refl : core.
- -
-Section RotrLemmas.
- -
-Variables (n0 : nat) (T : Type) (T' : eqType).
-Implicit Types (x : T) (s : seq T).
- -
-Lemma size_rotr s : size (rotr n0 s) = size s.
- -
-Lemma mem_rotr (s : seq T') : rotr n0 s =i s.
- -
-Lemma rotr_size_cat s1 s2 : rotr (size s2) (s1 ++ s2) = s2 ++ s1.
- -
-Lemma rotr1_rcons x s : rotr 1 (rcons s x) = x :: s.
- -
-Lemma has_rotr a s : has a (rotr n0 s) = has a s.
- -
-Lemma rotr_uniq (s : seq T') : uniq (rotr n0 s) = uniq s.
- -
-Lemma rotrK : cancel (@rotr T n0) (rot n0).
- -
-Lemma rotr_inj : injective (@rotr T n0).
- -
-Lemma take_rev s : take n0 (rev s) = rev (drop (size s - n0) s).
- -
-Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).
- -
-Lemma rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).
- -
-Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).
- -
-End RotrLemmas.
- -
- -
-Section RotCompLemmas.
- -
-Variable T : Type.
-Implicit Type s : seq T.
- -
-Lemma rot_addn m n s : m + n ≤ size s → rot (m + n) s = rot m (rot n s).
- -
-Lemma rotS n s : n < size s → rot n .+1 s = rot 1 (rot n s).
- -
-Lemma rot_add_mod m n s : n ≤ size s → m ≤ size s →
-  rot m (rot n s) = rot (if m + n ≤ size s then m + n else m + n - size s) s.
- -
-Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s).
- -
-Lemma rot_rotr m n s : rot m (rotr n s) = rotr n (rot m s).
- -
-Lemma rotr_rotr m n s : rotr m (rotr n s) = rotr n (rotr m s).
- -
-End RotCompLemmas.
- -
-Section Mask.
- -
-Variables (n0 : nat) (T : Type).
-Implicit Types (m : bitseq) (s : seq T).
- -
-Fixpoint mask m s {struct m} :=
-  match m, s with
-  | b :: m', x :: s' ⇒ if b then x :: mask m' s' else mask m' s'
-  | _, _ ⇒ [::]
-  end.
- -
-Lemma mask_false s n : mask (nseq n false) s = [::].
- -
-Lemma mask_true s n : size s ≤ n → mask (nseq n true) s = s.
- -
-Lemma mask0 m : mask m [::] = [::].
- -
-Lemma mask1 b x : mask [:: b ] [:: x ] = nseq b x.
- -
-Lemma mask_cons b m x s : mask (b :: m) (x :: s) = nseq b x ++ mask m s.
- -
-Lemma size_mask m s : size m = size s → size (mask m s) = count id m.
- -
-Lemma mask_cat m1 m2 s1 s2 :
-  size m1 = size s1 → mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.
- -
-Lemma has_mask_cons a b m x s :
-  has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).
- -
-Lemma has_mask a m s : has a (mask m s) → has a s.
- -
-Lemma mask_rot m s : size m = size s →
-   mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s).
- -
-Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s }.
- -
-End Mask.
- -
-Section EqMask.
- -
-Variables (n0 : nat) (T : eqType).
-Implicit Types (s : seq T) (m : bitseq).
- -
-Lemma mem_mask_cons x b m y s :
-  (x \in mask (b :: m) (y :: s)) = b && (x == y ) || (x \in mask m s ).
- -
-Lemma mem_mask x m s : x \in mask m s → x \in s.
- -
-Lemma mask_uniq s : uniq s → ∀ m, uniq (mask m s).
- -
-Lemma mem_mask_rot m s :
-  size m = size s → mask (rot n0 m) (rot n0 s) =i mask m s.
- -
-End EqMask.
- -
-Section Subseq.
- -
-Variable T : eqType.
-Implicit Type s : seq T.
- -
-Fixpoint subseq s1 s2 :=
-  if s2 is y :: s2' then
-    if s1 is x :: s1' then subseq (if x == y then s1' else s1) s2' else true
-  else s1 == [::].
- -
-Lemma sub0seq s : subseq [::] s.
- -
-Lemma subseq0 s : subseq s [::] = (s == [::]).
- -
-Lemma subseq_refl s : subseq s s.
- Hint Resolve subseq_refl : core.
- -
-Lemma subseqP s1 s2 :
-  reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2).
- -
-Lemma mask_subseq m s : subseq (mask m s) s.
- -
-Lemma subseq_trans : transitive subseq.
- -
-Lemma cat_subseq s1 s2 s3 s4 :
-  subseq s1 s3 → subseq s2 s4 → subseq (s1 ++ s2) (s3 ++ s4).
- -
-Lemma prefix_subseq s1 s2 : subseq s1 (s1 ++ s2).
- -
-Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2).
- -
-Lemma take_subseq s i : subseq (take i s) s.
- -
-Lemma drop_subseq s i : subseq (drop i s) s.
- -
-Lemma mem_subseq s1 s2 : subseq s1 s2 → {subset s1 ≤ s2 }.
- -
-Lemma sub1seq x s : subseq [:: x ] s = (x \in s ).
- -
-Lemma size_subseq s1 s2 : subseq s1 s2 → size s1 ≤ size s2.
- -
-Lemma size_subseq_leqif s1 s2 :
-  subseq s1 s2 → size s1 ≤ size s2 ?= iff (s1 == s2 ).
- -
-Lemma subseq_cons s x : subseq s (x :: s).
- -
-Lemma subseq_rcons s x : subseq s (rcons s x).
- -
-Lemma subseq_uniq s1 s2 : subseq s1 s2 → uniq s2 → uniq s1.
- -
-End Subseq.
- -
- -
-Hint Resolve subseq_refl : core.
- -
-Section Rem.
- -
-Variables (T : eqType) (x : T).
- -
-Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s.
- -
-Lemma rem_id s : x \notin s → rem s = s.
- -
-Lemma perm_to_rem s : x \in s → perm_eq s (x :: rem s).
- -
-Lemma size_rem s : x \in s → size (rem s) = (size s ).-1.
- -
-Lemma rem_subseq s : subseq (rem s) s.
- -
-Lemma rem_uniq s : uniq s → uniq (rem s).
- -
-Lemma mem_rem s : {subset rem s ≤ s }.
- -
-Lemma rem_filter s : uniq s → rem s = filter (predC1 x) s.
- -
-Lemma mem_rem_uniq s : uniq s → rem s =i [predD1 s & x ].
- -
-Lemma mem_rem_uniqF s : uniq s → x \in rem s = false.
- -
-End Rem.
- -
-Section Map.
- -
-Variables (n0 : nat) (T1 : Type) (x1 : T1).
-Variables (T2 : Type) (x2 : T2) (f : T1 → T2).
- -
-Fixpoint map s := if s is x :: s' then f x :: map s' else [::].
- -
-Lemma map_cons x s : map (x :: s) = f x :: map s.
- -
-Lemma map_nseq x : map (nseq n0 x) = nseq n0 (f x).
- -
-Lemma map_cat s1 s2 : map (s1 ++ s2) = map s1 ++ map s2.
- -
-Lemma size_map s : size (map s) = size s.
- -
-Lemma behead_map s : behead (map s) = map (behead s).
- -
-Lemma nth_map n s : n < size s → nth x2 (map s) n = f (nth x1 s n).
- -
-Lemma map_rcons s x : map (rcons s x) = rcons (map s) (f x).
- -
-Lemma last_map s x : last (f x) (map s) = f (last x s).
- -
-Lemma belast_map s x : belast (f x) (map s) = map (belast x s).
- -
-Lemma filter_map a s : filter a (map s) = map (filter (preim f a) s).
- -
-Lemma find_map a s : find a (map s) = find (preim f a) s.
- -
-Lemma has_map a s : has a (map s) = has (preim f a) s.
- -
-Lemma all_map a s : all a (map s) = all (preim f a) s.
- -
-Lemma count_map a s : count a (map s) = count (preim f a) s.
- -
-Lemma map_take s : map (take n0 s) = take n0 (map s).
- -
-Lemma map_drop s : map (drop n0 s) = drop n0 (map s).
- -
-Lemma map_rot s : map (rot n0 s) = rot n0 (map s).
- -
-Lemma map_rotr s : map (rotr n0 s) = rotr n0 (map s).
- -
-Lemma map_rev s : map (rev s) = rev (map s).
- -
-Lemma map_mask m s : map (mask m s) = mask m (map s).
- -
-Lemma inj_map : injective f → injective map.
- -
-End Map.
- -
-Notation "[ 'seq' E | i <- s ]" := (map (fun 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.
- -
-Notation "[ 'seq' E : R | i <- s ]" := (@map _ R (fun i ⇒ E) s)
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
- -
-Notation "[ 'seq' E : R | i <- s & C ]" := [seq E : R | i <- [seq i <- s | C]]
- (at level 0, E at level 99, i ident, only parsing) : seq_scope.
- -
-Notation "[ 'seq' E : R | i : T <- s ]" := (@map T R (fun i : T ⇒ E) s)
-  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
- -
-Notation "[ 'seq' E : R | i : T <- s & C ]" :=
-  [seq E : R | i : T <- [seq i : T <- s | C]]
- (at level 0, E at level 99, i ident, only parsing) : seq_scope.
- -
-Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
- -
-Section FilterSubseq.
- -
-Variable T : eqType.
-Implicit Types (s : seq T) (a : pred T).
- -
-Lemma filter_subseq a s : subseq (filter a s) s.
- -
-Lemma subseq_filter s1 s2 a :
-  subseq s1 (filter a s2) = all a s1 && subseq s1 s2.
- -
-Lemma subseq_uniqP s1 s2 :
-  uniq s2 → reflect (s1 = filter (mem s1) s2) (subseq s1 s2).
- -
-Lemma perm_to_subseq s1 s2 :
-  subseq s1 s2 → {s3 | perm_eq s2 (s1 ++ s3)}.
- -
-End FilterSubseq.
- -
- -
-Section EqMap.
- -
-Variables (n0 : nat) (T1 : eqType) (x1 : T1).
-Variables (T2 : eqType) (x2 : T2) (f : T1 → T2).
-Implicit Type s : seq T1.
- -
-Lemma map_f s x : x \in s → f x \in map f s.
- -
-Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s).
- -
-Lemma map_uniq s : uniq (map f s) → uniq s.
- -
-Lemma map_inj_in_uniq s : {in s &, injective f } → uniq (map f s) = uniq s.
- -
-Lemma map_subseq s1 s2 : subseq s1 s2 → subseq (map f s1) (map f s2).
- -
-Lemma nth_index_map s x0 x :
-  {in s &, injective f } → x \in s → nth x0 s (index (f x) (map f s)) = x.
- -
-Lemma perm_map s t : perm_eq s t → perm_eq (map f s) (map f t).
- -
-Hypothesis Hf : injective f.
- -
-Lemma mem_map s x : (f x \in map f s ) = (x \in s ).
- -
-Lemma index_map s x : index (f x) (map f s) = index x s.
- -
-Lemma map_inj_uniq s : uniq (map f s) = uniq s.
- -
-Lemma perm_map_inj s t : perm_eq (map f s) (map f t) → perm_eq s t.
- -
-End EqMap.
- -
- -
-Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) :
-  {f | uniq s → size fs = size s → map f s = fs }.
- -
-Section MapComp.
- -
-Variable T1 T2 T3 : Type.
- -
-Lemma map_id (s : seq T1) : map id s = s.
- -
-Lemma eq_map (f1 f2 : T1 → T2) : f1 =1 f2 → map f1 =1 map f2.
- -
-Lemma map_comp (f1 : T2 → T3) (f2 : T1 → T2) s :
-  map (f1 \o f2) s = map f1 (map f2 s).
- -
-Lemma mapK (f1 : T1 → T2) (f2 : T2 → T1) :
-  cancel f1 f2 → cancel (map f1) (map f2).
- -
-End MapComp.
- -
-Lemma eq_in_map (T1 : eqType) T2 (f1 f2 : T1 → T2) (s : seq T1) :
-  {in s , f1 =1 f2 } ↔ map f1 s = map f2 s.
- -
-Lemma map_id_in (T : eqType) f (s : seq T) : {in s , f =1 id } → map f s = s.
- -
-
- -
- Map a partial function -
-
- -
-Section Pmap.
- -
-Variables (aT rT : Type) (f : aT → option rT) (g : rT → aT).
- -
-Fixpoint pmap s :=
-  if s is x :: s' then let r := pmap s' in oapp (cons ^~ r) r (f x) else [::].
- -
-Lemma map_pK : pcancel g f → cancel (map g) pmap.
- -
-Lemma size_pmap s : size (pmap s) = count [eta f ] s.
- -
-Lemma pmapS_filter s : map some (pmap s) = map f (filter [eta f ] s).
- -
-Hypothesis fK : ocancel f g.
- -
-Lemma pmap_filter s : map g (pmap s) = filter [eta f ] s.
- -
-Lemma pmap_cat s t : pmap (s ++ t) = pmap s ++ pmap t.
- -
-End Pmap.
- -
-Section EqPmap.
- -
-Variables (aT rT : eqType) (f : aT → option rT) (g : rT → aT).
- -
-Lemma eq_pmap (f1 f2 : aT → option rT) : f1 =1 f2 → pmap f1 =1 pmap f2.
- -
-Lemma mem_pmap s u : (u \in pmap f s ) = (Some u \in map f s ).
- -
-Hypothesis fK : ocancel f g.
- -
-Lemma can2_mem_pmap : pcancel g f → ∀ s u, (u \in pmap f s ) = (g u \in s ).
- -
-Lemma pmap_uniq s : uniq s → uniq (pmap f s).
- -
-Lemma perm_pmap s t : perm_eq s t → perm_eq (pmap f s) (pmap f t).
- -
-End EqPmap.
- -
-Section PmapSub.
- -
-Variables (T : Type) (p : pred T) (sT : subType p).
- -
-Lemma size_pmap_sub s : size (pmap (insub : T → option sT) s) = count p s.
- -
-End PmapSub.
- -
-Section EqPmapSub.
- -
-Variables (T : eqType) (p : pred T) (sT : subType p).
- -
-Let insT : T → option sT := insub.
- -
-Lemma mem_pmap_sub s u : (u \in pmap insT s ) = (val u \in s ).
- -
-Lemma pmap_sub_uniq s : uniq s → uniq (pmap insT s).
- -
-End EqPmapSub.
- -
-
- -
- Index sequence -
-
- -
-Fixpoint iota m n := if n is n'.+1 then m :: iota m .+1 n' else [::].
- -
-Lemma size_iota m n : size (iota m n) = n.
- -
-Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
- -
-Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
- -
-Lemma nth_iota p m n i : i < n → nth p (iota m n) i = m + i.
- -
-Lemma mem_iota m n i : (i \in iota m n ) = (m ≤ i ) && (i < m + n ).
- -
-Lemma iota_uniq m n : uniq (iota m n).
- -
-
- -
- Making a sequence of a specific length, using indexes to compute items. -
-
- -
-Section MakeSeq.
- -
-Variables (T : Type) (x0 : T).
- -
-Definition mkseq f n : seq T := map f (iota 0 n).
- -
-Lemma size_mkseq f n : size (mkseq f n) = n.
- -
-Lemma eq_mkseq f g : f =1 g → mkseq f =1 mkseq g.
- -
-Lemma nth_mkseq f n i : i < n → nth x0 (mkseq f n) i = f i.
- -
-Lemma mkseq_nth s : mkseq (nth x0 s) (size s) = s.
- -
-End MakeSeq.
- -
-Section MakeEqSeq.
- -
-Variable T : eqType.
- -
-Lemma mkseq_uniq (f : nat → T) n : injective f → uniq (mkseq f n).
- -
-Lemma perm_iotaP {s t : seq T} x0 (It := iota 0 (size t)) :
-  reflect (exists2 Is, perm_eq Is It & s = map (nth x0 t) Is) (perm_eq s t).
- -
-End MakeEqSeq.
- -
- -
-Section FoldRight.
- -
-Variables (T : Type) (R : Type) (f : T → R → R) (z0 : R).
- -
-Fixpoint foldr s := if s is x :: s' then f x (foldr s') else z0.
- -
-End FoldRight.
- -
-Section FoldRightComp.
- -
-Variables (T1 T2 : Type) (h : T1 → T2).
-Variables (R : Type) (f : T2 → R → R) (z0 : R).
- -
-Lemma foldr_cat s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.
- -
-Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x 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 (a : pred T) s : sumn [seq a i : nat | i <- s ] = count a s.
- -
-Lemma sumn_rcons s n : sumn (rcons s n) = sumn s + n.
- -
-Lemma perm_sumn s1 s2 : perm_eq s1 s2 → sumn s1 = sumn s2.
- -
-Lemma sumn_rot s n : sumn (rot n s) = sumn s.
- -
-Lemma sumn_rev s : sumn (rev s) = sumn s.
- -
-Lemma natnseq0P s : reflect (s = nseq (size s) 0) (sumn s == 0).
- -
-Section FoldLeft.
- -
-Variables (T R : Type) (f : R → T → R).
- -
-Fixpoint foldl z s := if s is x :: s' then foldl (f z x) s' else z.
- -
-Lemma foldl_rev z s : foldl z (rev s) = foldr (fun x 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).
- -
-Fixpoint all2 (r : S → T → bool) s t :=
-  match s, t with
-  | [::], [::] ⇒ true
-  | x :: s, y :: t ⇒ r x y && all2 r s t
-  | _, _ ⇒ false
-  end.
- -
-Lemma zip_unzip s : zip (unzip1 s) (unzip2 s) = s.
- -
-Lemma unzip1_zip s t : size s ≤ size t → unzip1 (zip s t) = s.
- -
-Lemma unzip2_zip s t : size t ≤ size s → unzip2 (zip s t) = t.
- -
-Lemma size1_zip s t : size s ≤ size t → size (zip s t) = size s.
- -
-Lemma size2_zip s t : size t ≤ size s → size (zip s t) = size t.
- -
-Lemma size_zip s t : size (zip s t) = minn (size s) (size t).
- -
-Lemma zip_cat s1 s2 t1 t2 :
-  size s1 = size t1 → zip (s1 ++ s2) (t1 ++ t2) = zip s1 t1 ++ zip s2 t2.
- -
-Lemma nth_zip x y s t i :
-  size s = size t → nth (x , y ) (zip s t) i = (nth x s i , nth y t i ).
- -
-Lemma nth_zip_cond p s t i :
-   nth p (zip s t) i
-     = (if i < size (zip s t) then (nth p .1 s i , nth p .2 t i ) else p ).
- -
-Lemma zip_rcons s t x y :
-  size s = size t → zip (rcons s x) (rcons t y) = rcons (zip s t) (x , y ).
- -
-Lemma rev_zip s t : size s = size t → rev (zip s t) = zip (rev s) (rev t).
- -
-Lemma all2E r s t :
-  all2 r s t = (size s == size t ) && all [pred xy | r xy .1 xy .2 ] (zip s t).
- -
-End Zip.
- -
- -
-Section Flatten.
- -
-Variable T : Type.
-Implicit Types (s : seq T) (ss : seq (seq T)).
- -
-Definition flatten := foldr cat (Nil T).
-Definition shape := map (@size T).
-Fixpoint reshape sh s :=
-  if sh is n :: sh' then take n s :: reshape sh' (drop n s) else [::].
- -
-Definition flatten_index sh r c := sumn (take r sh) + c.
-Definition reshape_index sh i := find (pred1 0) (scanl subn i .+1 sh).
-Definition reshape_offset sh i := i - sumn (take (reshape_index sh i) sh).
- -
-Lemma size_flatten ss : size (flatten ss) = sumn (shape ss).
- -
-Lemma flatten_cat ss1 ss2 : flatten (ss1 ++ ss2) = flatten ss1 ++ flatten ss2.
- -
-Lemma size_reshape sh s : size (reshape sh s) = size sh.
- -
-Lemma nth_reshape (sh : seq nat) l n :
-  nth [::] (reshape sh l) n = take (nth 0 sh n) (drop (sumn (take n sh)) l).
- -
-Lemma flattenK ss : reshape (shape ss) (flatten ss) = ss.
- -
-Lemma reshapeKr sh s : size s ≤ sumn sh → flatten (reshape sh s) = s.
- -
-Lemma reshapeKl sh s : size s ≥ sumn sh → shape (reshape sh s) = sh.
- -
-Lemma flatten_rcons ss s : flatten (rcons ss s) = flatten ss ++ s.
- -
-Lemma flatten_seq1 s : flatten [seq [:: x ] | x <- s ] = s.
- -
-Lemma count_flatten ss P :
-  count P (flatten ss) = sumn [seq count P x | x <- ss ].
- -
-Lemma filter_flatten ss (P : pred T) :
-  filter P (flatten ss) = flatten [seq filter P i | i <- ss ].
- -
-Lemma rev_flatten ss :
-  rev (flatten ss) = flatten (rev (map rev ss)).
- -
-Lemma nth_shape ss i : nth 0 (shape ss) i = size (nth [::] ss i).
- -
-Lemma shape_rev ss : shape (rev ss) = rev (shape ss).
- -
-Lemma eq_from_flatten_shape ss1 ss2 :
-  flatten ss1 = flatten ss2 → shape ss1 = shape ss2 → ss1 = ss2.
- -
-Lemma rev_reshape sh s :
-  size s = sumn sh → rev (reshape sh s) = map rev (reshape (rev sh) (rev s)).
- -
-Lemma reshape_rcons s sh n (m := sumn sh) :
-  m + n = size s →
-  reshape (rcons sh n) s = rcons (reshape sh (take m s)) (drop m s).
- -
-Lemma flatten_indexP sh r c :
-  c < nth 0 sh r → flatten_index sh r c < sumn sh.
- -
-Lemma reshape_indexP sh i : i < sumn sh → reshape_index sh i < size sh.
- -
-Lemma reshape_offsetP sh i :
-  i < sumn sh → reshape_offset sh i < nth 0 sh (reshape_index sh i).
- -
-Lemma reshape_indexK sh i :
-  flatten_index sh (reshape_index sh i) (reshape_offset sh i) = i.
- -
-Lemma flatten_indexKl sh r c :
-  c < nth 0 sh r → reshape_index sh (flatten_index sh r c) = r.
- -
-Lemma flatten_indexKr sh r c :
-  c < nth 0 sh r → reshape_offset sh (flatten_index sh r c) = c.
- -
-Lemma nth_flatten x0 ss i (r := reshape_index (shape ss) i) :
-  nth x0 (flatten ss) i = nth x0 (nth [::] ss r) (reshape_offset (shape ss) i).
- -
-Lemma reshape_leq sh i1 i2
-  (r1 := reshape_index sh i1) (c1 := reshape_offset sh i1)
-  (r2 := reshape_index sh i2) (c2 := reshape_offset sh i2) :
-  (i1 ≤ i2 ) = ((r1 < r2 ) || ((r1 == r2 ) && (c1 ≤ c2 ))).
- -
-End Flatten.
- -
- -
-Lemma map_flatten S T (f : T → S) ss :
-  map f (flatten ss) = flatten (map (map f) ss).
- -
-Lemma sumn_flatten (ss : seq (seq nat)) :
-  sumn (flatten ss) = sumn (map sumn ss).
- -
-Lemma map_reshape T S (f : T → S) sh s :
-  map (map f) (reshape sh s) = reshape sh (map f s).
- -
-Section EqFlatten.
- -
-Variables S T : eqType.
- -
-Lemma flattenP (A : seq (seq T)) x :
-  reflect (exists2 s, s \in A & x \in s) (x \in flatten A).
- -
-Lemma flatten_mapP (A : S → seq T) s y :
-  reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)).
- -
-Lemma perm_flatten (ss1 ss2 : seq (seq T)) :
-  perm_eq ss1 ss2 → perm_eq (flatten ss1) (flatten ss2).
- -
-End EqFlatten.
- -
- -
-Notation "[ 'seq' E | x <- s , y <- t ]" :=
-  (flatten [seq [seq E | y <- t] | x <- s])
-  (at level 0, E at level 99, x ident, y ident,
-   format "[ '[hv' 'seq' E '/ ' | x <- s , '/ ' y <- t ] ']'")
-   : seq_scope.
-Notation "[ 'seq' E | x : S <- s , y : T <- t ]" :=
-  (flatten [seq [seq E | y : T <- t] | x : S <- s])
-  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
-Notation "[ 'seq' E : R | x : S <- s , y : T <- t ]" :=
-  (flatten [seq [seq E : R | y : T <- t] | x : S <- s])
-  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
-Notation "[ 'seq' E : R | x <- s , y <- t ]" :=
-  (flatten [seq [seq E : R | y <- t] | x <- s])
-  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
- -
-Section AllPairsDep.
- -
-Variables (S S' : Type) (T T' : S → Type) (R : Type).
-Implicit Type f : ∀ x, T x → R.
- -
-Definition allpairs_dep f s t := [seq f x y | x <- s , y <- t x ].
- -
-Lemma size_allpairs_dep f s t :
-  size [seq f x y | x <- s , y <- t x ] = sumn [seq size (t x) | x <- s ].
- -
-Lemma eq_allpairs (f1 f2 : ∀ x, T x → R) s t :
-    (∀ x, f1 x =1 f2 x ) →
-  [seq f1 x y | x <- s , y <- t x ] = [seq f2 x y | x <- s , y <- t x ].
- -
-Lemma allpairs_cat f s1 s2 t :
-  [seq f x y | x <- s1 ++ s2 , y <- t x ] =
-    [seq f x y | x <- s1 , y <- t x ] ++ [seq f x y | x <- s2 , y <- t x ].
- -
-Lemma allpairs_mapl f (g : S' → S) s t :
-  [seq f x y | x <- map g s , y <- t x ] = [seq f (g x) y | x <- s , y <- t (g x)].
- -
-Lemma allpairs_mapr f (g : ∀ x, T' x → T x) s t :
-  [seq f x y | x <- s , y <- map (g x) (t x)] =
-    [seq f x (g x y) | x <- s , y <- t x ].
- -
-End AllPairsDep.
- -
- -
-Lemma map_allpairs S T R R' (g : R' → R) f s t :
-  map g [seq f x y | x : S <- s , y : T x <- t x ] =
-    [seq g (f x y) | x <- s , y <- t x ].
- -
-Section AllPairsNonDep.
- -
-Variables (S T R : Type) (f : S → T → R).
-Implicit Types (s : seq S) (t : seq T).
- -
-Definition allpairs s t := [seq f x y | x <- s , y <- t ].
- -
-Lemma size_allpairs s t : size [seq f x y | x <- s , y <- t ] = size s × size t.
- -
-End AllPairsNonDep.
- -
- -
-Section EqAllPairsDep.
- -
-Variables (S : eqType) (T : S → eqType).
-Implicit Types (R : eqType) (s : seq S) (t : ∀ x, seq (T x)).
- -
-Lemma allpairsPdep R (f : ∀ x, T x → R) s t (z : R) :
-  reflect (∃ x y, [/\ x \in s , y \in t x & z = f x y ])
-          (z \in [seq f x y | x <- s , y <- t x ]).
- -
-Variable R : eqType.
-Implicit Type f : ∀ x, T x → R.
- -
-Lemma allpairs_f_dep f s t x y :
-  x \in s → y \in t x → f x y \in [seq f x y | x <- s , y <- t x ].
- -
-Lemma eq_in_allpairs_dep f1 f2 s t :
-    {in s , ∀ x, {in t x , f1 x =1 f2 x }} ↔
-  [seq f1 x y : R | x <- s , y <- t x ] = [seq f2 x y | x <- s , y <- t x ].
- -
-Lemma mem_allpairs_dep f s1 t1 s2 t2 :
-    s1 =i s2 → {in s1 , ∀ x, t1 x =i t2 x } →
-  [seq f x y | x <- s1 , y <- t1 x ] =i [seq f x y | x <- s2 , y <- t2 x ].
- -
-Lemma allpairs_catr f s t1 t2 :
-  [seq f x y | x <- s , y <- t1 x ++ t2 x ] =i
-    [seq f x y | x <- s , y <- t1 x ] ++ [seq f x y | x <- s , y <- t2 x ].
- -
-Lemma allpairs_uniq_dep f s t (st := [seq Tagged T y | x <- s , y <- t x ]) :
-  let g (p : {x : S & T x }) : R := f (tag p) (tagged p) in
-    uniq s → {in s , ∀ x, uniq (t x)} → {in st &, injective g } →
-  uniq [seq f x y | x <- s , y <- t x ].
- -
-End EqAllPairsDep.
- -
- -
-Section EqAllPairs.
- -
-Variables S T R : eqType.
-Implicit Types (f : S → T → R) (s : seq S) (t : seq T).
- -
-Lemma allpairsP f s t (z : R) :
-  reflect (∃ p, [/\ p .1 \in s , p .2 \in t & z = f p .1 p .2 ])
-          (z \in [seq f x y | x <- s , y <- t ]).
- -
-Lemma allpairs_f f s t x y :
-  x \in s → y \in t → f x y \in [seq f x y | x <- s , y <- t ].
- -
-Lemma eq_in_allpairs f1 f2 s t :
-    {in s & t , f1 =2 f2 } ↔
-  [seq f1 x y : R | x <- s , y <- t ] = [seq f2 x y | x <- s , y <- t ].
- -
-Lemma mem_allpairs f s1 t1 s2 t2 :
-    s1 =i s2 → t1 =i t2 →
-  [seq f x y | x <- s1 , y <- t1 ] =i [seq f x y | x <- s2 , y <- t2 ].
- -
-Lemma allpairs_uniq f s t (st := [seq (x , y ) | x <- s , y <- t ]) :
-    uniq s → uniq t → {in st &, injective (prod_curry f)} →
-  uniq [seq f x y | x <- s , y <- t ].
- -
-End EqAllPairs.
- -
- -
-Section Permutations.
- -
-Variable T : eqType.
-Implicit Types (x : T) (s t : seq T) (bs : seq (T × nat)) (acc : seq (seq T)).
- -
-Fixpoint incr_tally bs x :=
-  if bs isn't b :: bs then [:: (x , 1)] else
-  if x == b.1 then (x , b.2 .+1 ) :: bs else b :: incr_tally bs x.
- -
-Definition tally s := foldl incr_tally [::] s.
- -
-Definition wf_tally :=
-  [qualify a bs : seq (T × nat) | uniq (unzip1 bs) && (0 \notin unzip2 bs )].
- -
-Definition tally_seq bs := flatten [seq nseq b .2 b .1 | b <- bs ].
- -
-Lemma size_tally_seq bs : size (tally_seq bs) = sumn (unzip2 bs).
- -
-Lemma tally_seqK : {in wf_tally , cancel tally_seq tally }.
- -
-Lemma incr_tallyP x : {homo incr_tally ^~ x : bs / bs \in wf_tally }.
- -
-Lemma tallyP s : tally s \is a wf_tally.
- -
-Lemma tallyK s : perm_eq (tally_seq (tally s)) s.
- -
-Lemma tallyEl s : perm_eq (unzip1 (tally s)) (undup s).
- -
-Lemma tallyE s : perm_eq (tally s) [seq (x , count_mem x s ) | x <- undup s ].
- -
-Lemma perm_tally s1 s2 : perm_eq s1 s2 → perm_eq (tally s1) (tally s2).
- -
-Lemma perm_tally_seq bs1 bs2 :
-  perm_eq bs1 bs2 → perm_eq (tally_seq bs1) (tally_seq bs2).
- -
-Lemma perm_count_undup s :
-  perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s ]) s.
- -
- -
- -
-Definition permutations s := perms_rec (size s) [::] (tally s) [::].
- -
-Let permsP s : ∃ n bs,
-   [/\ permutations s = perms_rec n [::] bs [::],
-       size (tseq bs) == n , perm_eq (tseq bs) s & uniq (unzip1 bs)].
- -
-Let cons_permsE : ∀ n x bs bs1 bs2,
-  let cp := cons_perms n bs bs2 in let perms s := perms_rec n s bs1 [::] in
-  cp (perms [:: x ]) = cp [::] ++ [seq rcons t x | t <- perms [::]].
- -
-Lemma mem_permutations s t : (t \in permutations s ) = perm_eq t s.
- -
-Lemma permutations_uniq s : uniq (permutations s).
- -
-Notation perms := permutations.
-Lemma permutationsE s :
-    0 < size s →
-  perm_eq (perms s) [seq x :: t | x <- undup s , t <- perms (rem x s)].
- -
-Lemma permutationsErot x s (le_x := fun t ⇒ iota 0 (index x t + 1)) :
-  perm_eq (perms (x :: s)) [seq rot i (x :: t) | t <- perms s , i <- le_x t ].
- -
-Lemma size_permutations s : uniq s → size (permutations s) = (size s )`!.
- -
-Lemma permutations_all_uniq s : uniq s → all uniq (permutations s).
- -
-Lemma perm_permutations s t :
-  perm_eq s t → perm_eq (permutations s) (permutations t).
- -
-End Permutations.
- -
-Section AllIff.
-
- -
- The Following Are Equivalent -

- - We introduce a specific conjunction, used to chain the consecutive - items in a circular list of implications -
-
-Inductive all_iff_and (P Q : Prop) : Prop := AllIffConj of P & Q.
- -
-Definition all_iff (P0 : Prop) (Ps : seq Prop) : Prop :=
-  let fix loop (P : Prop) (Qs : seq Prop) : Prop :=
-    if Qs is Q :: Qs then all_iff_and (P → Q) (loop Q Qs) else P → P0 in
-  loop P0 Ps.
- -
-Lemma all_iffLR P0 Ps :
-   all_iff P0 Ps → ∀ m n, nth P0 (P0 :: Ps) m → nth P0 (P0 :: Ps) n.
- -
-Lemma all_iffP P0 Ps :
-   all_iff P0 Ps → ∀ m n, nth P0 (P0 :: Ps) m ↔ nth P0 (P0 :: Ps) n.
- -
-End AllIff.
-Coercion all_iffP : all_iff >-> Funclass.
- -
-
- -
- This means "the following are all equivalent: P0, ... Pn" -
-
-Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
-  (at level 0, format "[ '<->' '[' P0 ; '/' P1 ; '/' .. ; '/' Pn ']' ]")
-  : form_scope.
- -
-
- -
- Temporary backward compatibility. -
-
-Notation perm_eqP := (deprecate perm_eqP permP) (only parsing).
-Notation perm_eqlP := (deprecate perm_eqlP permPl) (only parsing).
-Notation perm_eqrP := (deprecate perm_eqrP permPr) (only parsing).
-Notation perm_eqlE := (deprecate perm_eqlE permEl _ _ _) (only parsing).
-Notation perm_eq_refl := (deprecate perm_eq_refl perm_refl _) (only parsing).
-Notation perm_eq_sym := (deprecate perm_eq_sym perm_sym _) (only parsing).
-Notation "@ 'perm_eq_trans'" := (deprecate perm_eq_trans perm_trans)
-  (at level 10, only parsing).
-Notation perm_eq_trans := (@perm_eq_trans _ _ _ _) (only parsing).
-Notation perm_eq_size := (deprecate perm_eq_size perm_size _ _ _)
-  (only parsing).
-Notation perm_eq_mem := (deprecate perm_eq_mem perm_mem _ _ _)
-  (only parsing).
-Notation perm_eq_uniq := (deprecate perm_eq_uniq perm_uniq _ _ _)
-  (only parsing).
-Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _)
-  (only parsing).
-Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _)
-  (only parsing).
-Notation perm_eq_all := (deprecate perm_eq_all perm_all _ _ _)
-  (only parsing).
-Notation perm_eq_small := (deprecate perm_eq_small perm_small_eq _ _ _)
-  (only parsing).
-Notation perm_eq_nilP := (deprecate perm_eq_nilP perm_nilP) (only parsing).
-Notation perm_eq_consP := (deprecate perm_eq_consP perm_consP) (only parsing).
-Notation leq_size_perm :=
-  ((fun T s1 s2 Us1 ss12 les21 ⇒
-   let: (Esz12, Es12) :=
-     deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21
-   in conj Es12 Esz12) _ _ _)
-  (only parsing).
-Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _)
-  (only parsing).
-Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing).
-Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _)
-  (only parsing).
-
-