Module mathcomp.boot.seq
From HB Require Import structures.From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
The seq type is the ssreflect type for sequences; it is an alias for the
standard Coq list type. The ssreflect library equips it with many
operations, as well as eqType and predType (and, later, choiceType)
structures. The operations are geared towards reflection: they generally
expect and provide boolean predicates, e.g., the membership predicate
expects an eqType. To avoid any confusion we do not Import the Coq List
module.
As there is no true subtyping in Coq, we don't use a type for non-empty
sequences; rather, we pass explicitly the head and tail of the sequence.
The empty sequence is especially bothersome for subscripting, since it
forces us to pass a default value. This default value can often be hidden
by a notation.
Here is the list of seq operations:
** Constructors:
seq T == the type of sequences of items of type T.
bitseq == seq bool.
[::], nil, Nil T == the empty sequence (of type T).
x :: s, cons x s, Cons T x s == the sequence x followed by s (of type T).
[:: x] == the singleton sequence.
[:: x_0; ...; x_n] == the explicit sequence of the x_i.
[:: x_0, ..., x_n & s] == the sequence of the x_i, followed by s.
rcons s x == the sequence s, followed by x.
All of the above, except rcons, can be used in patterns. We define a view
lastP and an induction principle last_ind that can be used to decompose
or traverse a sequence in a right to left order. The view lemma lastP has
a dependent family type, so the ssreflect tactic case/lastP: p => [|p' x]
will generate two subgoals in which p has been replaced by [::] and by
rcons p' x, respectively.
** Factories:
nseq n x == a sequence of n x's.
ncons n x s == a sequence of n x's, followed by s.
seqn n x_0 ... x_n-1 == the sequence of the x_i; can be partially applied.
iota m n == the sequence m, m + 1, ..., m + n - 1.
mkseq f n == the sequence f 0, f 1, ..., f (n - 1).
** Sequential access:
head x0 s == the head (zero'th item) of s if s is non-empty, else x0.
ohead s == None if s is empty, else Some x when the head of s is x.
behead s == s minus its head, i.e., s' if s = x :: s', else [::].
last x s == the last element of x :: s (which is non-empty).
belast x s == x :: s minus its last item.
** Dimensions:
size s == the number of items (length) in s.
shape ss == the sequence of sizes of the items of the sequence of
sequences ss.
** Random access:
nth x0 s i == the item i of s (numbered from 0), or x0 if s does
not have at least i+1 items (i.e., size x <= i)
s`_i == standard notation for nth x0 s i for a default x0,
e.g., 0 for rings.
onth s i == Some x if x is the i^th idem of s (numbered from 0),
or None if size s <= i)
set_nth x0 s i y == s where item i has been changed to y; if s does not
have an item i, it is first padded with copies of x0
to size i+1.
incr_nth s i == the nat sequence s with item i incremented (s is
first padded with 0's to size i+1, if needed).
** Predicates:
nilp s <=> s is [::].
:= (size s == 0).
x \in s == x appears in s (this requires an eqType for T).
index x s == the first index at which x appears in s, or size s if
x \notin s.
has a s <=> a holds for some item in s, where a is an applicative
bool predicate.
all a s <=> a holds for all items in s.
'has_aP <-> the view reflect (exists2 x, x \in s & A x) (has a s),
where aP x : reflect (A x) (a x).
'all_aP <=> the view for reflect {in s, forall x, A x} (all a s).
all2 r s t <=> the (bool) relation r holds for all _respective_ items
in s and t, which must also have the same size, i.e.,
for s := [:: x1; ...; x_m] and t := [:: y1; ...; y_n],
the condition [&& r x_1 y_1, ..., r x_n y_n & m == n].
find p s == the index of the first item in s for which p holds,
or size s if no such item is found.
count p s == the number of items of s for which p holds.
count_mem x s == the multiplicity of x in s, i.e., count (pred1 x) s.
tally s == a tally of s, i.e., a sequence of (item, multiplicity)
pairs for all items in sequence s (without duplicates).
incr_tally bs x == increment the multiplicity of x in the tally bs, or add
x with multiplicity 1 at then end if x is not in bs.
bs \is a wf_tally <=> bs is well-formed tally, with no duplicate items or
null multiplicities.
tally_seq bs == the expansion of a tally bs into a sequence where each
(x, n) pair expands into a sequence of n x's.
constant s <=> all items in s are identical (trivial if s = [::]).
uniq s <=> all the items in s are pairwise different.
subseq s1 s2 <=> s1 is a subsequence of s2, i.e., s1 = mask m s2 for
some m : bitseq (see below).
infix s1 s2 <=> s1 is a contiguous subsequence of s2, i.e.,
s ++ s1 ++ s' = s2 for some sequences s, s'.
prefix s1 s2 <=> s1 is a subchain of s2 appearing at the beginning
of s2.
suffix s1 s2 <=> s1 is a subchain of s2 appearing at the end of s2.
infix_index s1 s2 <=> the first index at which s1 appears in s2,
or (size s2).+1 if infix s1 s2 is false.
perm_eq s1 s2 <=> s2 is a permutation of s1, i.e., s1 and s2 have the
items (with the same repetitions), but possibly in a
different order.
perm_eql s1 s2 <-> s1 and s2 behave identically on the left of perm_eq.
perm_eqr s1 s2 <-> s1 and s2 behave identically on the right of perm_eq.
--> These left/right transitive versions of perm_eq make it easier to
chain a sequence of equivalences.
permutations s == a duplicate-free list of all permutations of s.
** Filtering:
filter p s == the subsequence of s consisting of all the items
for which the (boolean) predicate p holds.
rem x s == the subsequence of s, where the first occurrence
of x has been removed (compare filter (predC1 x) s
where ALL occurrences of x are removed).
undup s == the subsequence of s containing only the first
occurrence of each item in s, i.e., s with all
duplicates removed.
mask m s == the subsequence of s selected by m : bitseq, with
item i of s selected by bit i in m (extra items or
bits are ignored.
mindex m i == the natural number such that
nth x0 (mask m s) i = nth x0 s (mindex m i)
** 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 x]
** Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m],
allpairs f s t := same as allpairs_dep but where t is non dependent,
i.e. self expanding definition for
[seq f x y | x <- s, y <- t]
:= [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m]
allrel r xs ys := all [pred x | all (r x) ys] xs
<=> r x y holds whenever x is in xs and y is in ys
all2rel r xs := allrel r xs xs
<=> the proposition r x y holds for all possible x, y in xs.
pairwise r xs <=> the relation r holds for any i-th and j-th element of
xs such that i < j.
map f s == the sequence [:: f x_1, ..., f x_n].
pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik,
pf x_i = Some y_i, and pf x_j = None iff j is not in
{i1, ..., ik}.
foldr f a s == the right fold of s by f (i.e., the natural iterator).
:= f x_1 (f x_2 ... (f x_n a))
sumn s == x_1 + (x_2 + ... + (x_n + 0)) (when s : seq nat).
foldl f a s == the left fold of s by f.
:= f (f ... (f a x_1) ... x_n-1) x_n
scanl f a s == the sequence of partial accumulators of foldl f a s.
:= [:: f a x_1; ...; foldl f a s]
pairmap f a s == the sequence of f applied to consecutive items in a :: s.
:= [:: f a x_1; f x_1 x_2; ...; f x_n-1 x_n]
zip s t == itemwise pairing of s and t (dropping any extra items).
:= [:: (x_1, y_1); ...; (x_mn, y_mn)] with mn = minn n m.
unzip1 s == [:: (x_1).1; ...; (x_n).1] when s : seq (S * T).
unzip2 s == [:: (x_1).2; ...; (x_n).2] when s : seq (S * T).
flatten s == x_1 ++ ... ++ x_n ++ [::] when s : seq (seq T).
reshape r s == s reshaped into a sequence of sequences whose sizes are
given by r (truncating if s is too long or too short).
:= [:: [:: x_1; ...; x_r1];
[:: x_(r1 + 1); ...; x_(r1 + r2)];
...;
[:: x_(r1 + ... + r(k-1) + 1); ...; x_(r1 + ... 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 <- s | 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 simpl never.
** The following are equivalent:
[<-> P0; P1; ..; Pn] <-> P0, P1, ..., Pn are all equivalent.
:= P0 -> P1 -> ... -> Pn -> P0
if T : [<-> P0; P1; ..; Pn] is such an equivalence, and i, j are in nat
then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj;
when i (resp. j) is out of bounds, Pi (resp. Pj) defaults to P0.
The tactic tfae splits the goal into n+1 implications to prove.
An example of use can be found in fingraph theorem orbitPcycle.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope seq_scope.
Reserved Notation "[ '<->' P0 ; P1 ; .. ; Pn ]"
(format "[ '<->' '[' P0 ; '/' P1 ; '/' .. ; '/' Pn ']' ]").
Delimit Scope seq_scope with SEQ.
Open Scope seq_scope.
Notation seq := list.
Bind Scope seq_scope with list.
Arguments cons {T%_type} x s%_SEQ : rename.
Arguments nil {T%_type} : rename.
Notation Cons T := (@cons T) (only parsing).
Notation Nil T := (@nil T) (only parsing).
Infix "::" := cons : seq_scope.
Notation "[ :: ]" := nil (format "[ :: ]") : seq_scope.
Notation "[ :: x1 ]" := (x1 :: [::]) (format "[ :: x1 ]") : seq_scope.
Notation "[ :: x & s ]" := (x :: s) (only parsing) : seq_scope.
Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
(format
"'[hv' [ :: '[' x1 , '/' x2 , '/' .. , '/' xn ']' '/ ' & s ] ']'"
) : seq_scope.
Notation "[ :: x1 ; x2 ; .. ; xn ]" := (x1 :: x2 :: .. [:: xn] ..)
(format "[ :: '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]"
) : seq_scope.
Section Sequences.
Variable n0 : nat.
Variable T : Type.
Variable x0 : T.
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 = [::]
Proof.
by case: s. Qed.
Definition nilp s := size s == 0.
Lemma nilP s : reflect (s = [::]) (nilp s).
Proof.
by case: s => [|x s]; constructor. Qed.
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.
Proof.
by case: s. Qed.
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.
Proof.
by elim: n => //= n ->. Qed.
Lemma size_nseq n x : size (nseq n x) = n.
Proof.
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.
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
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma cat_nseq n x s : nseq n x ++ s = ncons n x s.
Proof.
by elim: n => //= n ->. Qed.
Lemma nseqD n1 n2 x : nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x.
Lemma cats0 s : s ++ [::] = s.
Proof.
by elim: s => //= x s ->. Qed.
Lemma catA s1 s2 s3 : s1 ++ s2 ++ s3 = (s1 ++ s2) ++ s3.
Proof.
by elim: s1 => //= x s1 ->. Qed.
Lemma size_cat s1 s2 : size (s1 ++ s2) = size s1 + size s2.
Proof.
by elim: s1 => //= x s1 ->. Qed.
Lemma cat_nilp s1 s2 : nilp (s1 ++ s2) = nilp s1 && nilp s2.
Proof.
by case: s1. Qed.
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.
Proof.
by []. Qed.
Lemma cats1 s z : s ++ [:: z] = rcons s z.
Proof.
by elim: s => //= x s ->. Qed.
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).
Proof.
by elim: s x => [|y s IHs] x //=; rewrite IHs. Qed.
Lemma last_cons x y s : last x (y :: s) = last y s.
Proof.
by []. Qed.
Lemma size_rcons s x : size (rcons s x) = (size s).+1.
Lemma size_belast x s : size (belast x s) = size s.
Proof.
by elim: s x => [|y s IHs] x //=; rewrite IHs. Qed.
Lemma last_cat x s1 s2 : last x (s1 ++ s2) = last (last x s1) s2.
Proof.
by elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.
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.
Proof.
by elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.
Lemma belast_rcons x s z : belast x (rcons s z) = x :: s.
Proof.
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.
Proof.
Lemma last_ind P :
P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s.
Proof.
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
Proof.
by []. Qed.
Lemma nth_default s n : size s <= n -> nth s n = x0.
Proof.
by elim: s n => [|x s IHs] []. Qed.
Lemma if_nth s b n : b || (size s <= n) ->
(if b then nth s n else x0) = nth s n.
Proof.
Lemma nth_nil n : nth [::] n = x0.
Proof.
by case: n. Qed.
Lemma nth_seq1 n x : nth [:: x] n = if n == 0 then x else x0.
Proof.
by case: n => [|[]]. Qed.
Lemma last_nth x s : last x s = nth (x :: s) (size s).
Proof.
by elim: s x => [|y s IHs] x /=. Qed.
Lemma nth_last s : nth s (size s).-1 = last x0 s.
Proof.
Lemma nth_behead s n : nth (behead s) n = nth s n.+1.
Proof.
by case: s n => [|x s] [|n]. Qed.
Lemma nth_cat s1 s2 n :
nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1).
Proof.
by elim: s1 n => [|x s1 IHs] []. Qed.
Lemma nth_cons x s n : nth (x :: s) n = if n > 0 then nth s n.-1 else x.
Proof.
by case: n. Qed.
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.
Proof.
Lemma nth_rcons_default s i : nth (rcons s x0) i = nth s i.
Proof.
Lemma nth_ncons m x s n :
nth (ncons m x s) n = if n < m then x else nth s (n - m).
Proof.
by elim: m n => [|m IHm] []. Qed.
Lemma nth_nseq m x n : nth (nseq m x) n = (if n < m then x else x0).
Proof.
by elim: m n => [|m IHm] []. Qed.
Lemma eq_from_nth s1 s2 :
size s1 = size s2 -> (forall i, i < size s1 -> nth s1 i = nth s2 i) ->
s1 = s2.
Proof.
elim: s1 s2 => [|x1 s1 IHs1] [|x2 s2] //= [eq_sz] eq_s12.
by rewrite [x1](eq_s12 0) // (IHs1 s2) // => i; apply: (eq_s12 i.+1).
Qed.
by rewrite [x1](eq_s12 0) // (IHs1 s2) // => i; apply: (eq_s12 i.+1).
Qed.
Lemma size_set_nth s n y : size (set_nth s n y) = maxn n.+1 (size s).
Proof.
rewrite maxnC; elim: s n => [|x s IHs] [|n] //=.
- by rewrite size_ncons addn1.
- by rewrite IHs maxnSS.
Qed.
- by rewrite size_ncons addn1.
- by rewrite IHs maxnSS.
Qed.
Lemma set_nth_nil n y : set_nth [::] n y = ncons n x0 [:: y].
Proof.
by case: n. Qed.
Lemma nth_set_nth s n y : nth (set_nth s n y) =1 [eta nth s with n |-> y].
Proof.
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.
Proof.
have [-> | ne_n12] := eqVneq.
apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn.
by do 2!rewrite !nth_set_nth /=; case: eqP.
apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA.
by do 2!rewrite !nth_set_nth /=; case: eqP => // ->; case: eqVneq ne_n12.
Qed.
apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn.
by do 2!rewrite !nth_set_nth /=; case: eqP.
apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA.
by do 2!rewrite !nth_set_nth /=; case: eqP => // ->; case: eqVneq ne_n12.
Qed.
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.
Proof.
Lemma has_count s : has s = (0 < count s).
Proof.
Lemma size_filter_gt0 s : (size (filter s) > 0) = (has s).
Proof.
Lemma count_size s : count s <= size s.
Lemma all_count s : all s = (count s == size s).
Proof.
Lemma filter_all s : all (filter s).
Proof.
Lemma all_filterP s : reflect (filter s = s) (all s).
Proof.
apply: (iffP idP) => [| <-]; last exact: filter_all.
by elim: s => //= x s IHs /andP[-> Hs]; rewrite IHs.
Qed.
by elim: s => //= x s IHs /andP[-> Hs]; rewrite IHs.
Qed.
Lemma filter_id s : filter (filter s) = filter s.
Proof.
Lemma has_find s : has s = (find s < size s).
Lemma find_size s : find s <= size s.
Proof.
Lemma find_cat s1 s2 :
find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2.
Lemma has_nil : has [::] = false
Proof.
by []. Qed.
Lemma has_seq1 x : has [:: x] = a x.
Proof.
Lemma has_nseq n x : has (nseq n x) = (0 < n) && a x.
Proof.
Lemma has_seqb (b : bool) x : has (nseq b x) = b && a x.
Lemma all_nil : all [::] = true
Proof.
by []. Qed.
Lemma all_seq1 x : all [:: x] = a x.
Proof.
Lemma all_nseq n x : all (nseq n x) = (n == 0) || a x.
Proof.
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.
Proof.
Lemma count_nseq n x : count (nseq n x) = a x * n.
Proof.
Lemma find_nseq n x : find (nseq n x) = ~~ a x * n.
Proof.
Lemma nth_find s : has s -> a (nth s (find s)).
Proof.
Lemma before_find s i : i < find s -> a (nth s i) = false.
Proof.
Lemma hasNfind s : ~~ has s -> find s = size s.
Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
Proof.
Lemma filter_rcons s x :
filter (rcons s x) = if a x then rcons (filter s) x else filter s.
Proof.
Lemma count_cat s1 s2 : count (s1 ++ s2) = count s1 + count s2.
Proof.
Lemma has_cat s1 s2 : has (s1 ++ s2) = has s1 || has s2.
Proof.
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.
Proof.
Lemma all_rcons s x : all (rcons s x) = a x && all s.
End SeqFind.
Lemma find_pred0 s : find pred0 s = size s
Proof.
by []. Qed.
Lemma find_predT s : find predT s = 0.
Proof.
by case: s. Qed.
Lemma eq_find a1 a2 : a1 =1 a2 -> find a1 =1 find a2.
Proof.
by move=> Ea; elim=> //= x s IHs; rewrite Ea IHs. Qed.
Lemma eq_filter a1 a2 : a1 =1 a2 -> filter a1 =1 filter a2.
Proof.
by move=> Ea; elim=> //= x s IHs; rewrite Ea IHs. Qed.
Lemma eq_count a1 a2 : a1 =1 a2 -> count a1 =1 count a2.
Proof.
Lemma eq_has a1 a2 : a1 =1 a2 -> has a1 =1 has a2.
Lemma eq_all a1 a2 : a1 =1 a2 -> all a1 =1 all a2.
Lemma all_filter (p q : pred T) xs :
all p (filter q xs) = all [pred i | q i ==> p i] xs.
Proof.
by elim: xs => //= x xs <-; case: (q x). Qed.
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.
Proof.
Lemma sub_count s : count a1 s <= count a2 s.
Lemma sub_all s : all a1 s -> all a2 s.
Proof.
End SubPred.
Lemma filter_pred0 s : filter pred0 s = [::]
Proof.
by elim: s. Qed.
Lemma filter_predT s : filter predT s = s.
Proof.
by elim: s => //= x s ->. Qed.
Lemma filter_predI a1 a2 s : filter (predI a1 a2) s = filter a1 (filter a2 s).
Proof.
Lemma count_pred0 s : count pred0 s = 0.
Proof.
Lemma count_predT s : count predT s = size s.
Proof.
Lemma count_predUI a1 a2 s :
count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
Proof.
Lemma count_predC a s : count a s + count (predC a) s = size s.
Proof.
Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s.
Proof.
Lemma has_pred0 s : has pred0 s = false.
Proof.
Lemma has_predT s : has predT s = (0 < size s).
Proof.
Lemma has_predC a s : has (predC a) s = ~~ all a s.
Proof.
by elim: s => //= x s ->; case (a x). Qed.
Lemma has_predU a1 a2 s : has (predU a1 a2) s = has a1 s || has a2 s.
Proof.
Lemma all_pred0 s : all pred0 s = (size s == 0).
Proof.
Lemma all_predT s : all predT s.
Proof.
Lemma allT (a : pred T) s : (forall x, a x) -> all a s.
Lemma all_predC a s : all (predC a) s = ~~ has a s.
Proof.
by elim: s => //= x s ->; case (a x). Qed.
Lemma all_predI a1 a2 s : all (predI a1 a2) s = all a1 s && all a2 s.
Proof.
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
Proof.
by case: s. Qed.
Lemma drop1 : drop 1 =1 behead
Proof.
by case=> [|x [|y s]]. Qed.
Lemma drop_oversize n s : size s <= n -> drop n s = [::].
Proof.
by elim: s n => [|x s IHs] []. Qed.
Lemma drop_size s : drop (size s) s = [::].
Proof.
Lemma drop_cons x s :
drop n0 (x :: s) = if n0 is n.+1 then drop n s else x :: s.
Proof.
by []. Qed.
Lemma size_drop s : size (drop n0 s) = size s - n0.
Proof.
Lemma drop_cat s1 s2 :
drop n0 (s1 ++ s2) =
if n0 < size s1 then drop n0 s1 ++ s2 else drop (n0 - size s1) s2.
Proof.
Lemma drop_size_cat n s1 s2 : size s1 = n -> drop n (s1 ++ s2) = s2.
Proof.
Lemma nconsK n x : cancel (ncons n x) (drop n).
Proof.
by elim: n => // -[]. Qed.
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 = [::]
Proof.
by case: s. Qed.
Lemma take_oversize n s : size s <= n -> take n s = s.
Proof.
by elim: s n => [|x s IHs] [|n] //= /IHs->. Qed.
Lemma take_size s : take (size s) s = s.
Proof.
Lemma take_cons x s :
take n0 (x :: s) = if n0 is n.+1 then x :: (take n s) else [::].
Proof.
by []. Qed.
Lemma drop_rcons s : n0 <= size s ->
forall x, drop n0 (rcons s x) = rcons (drop n0 s) x.
Proof.
Lemma cat_take_drop s : take n0 s ++ drop n0 s = s.
Proof.
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.
Proof.
have [le_sn | lt_ns] := leqP (size s) n0; first by rewrite take_oversize.
by rewrite size_takel // ltnW.
Qed.
by rewrite size_takel // ltnW.
Qed.
Lemma size_take_min s : size (take n0 s) = minn n0 (size s).
Proof.
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.
Proof.
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).
Proof.
rewrite -[s in RHS]cat_take_drop nth_cat size_take ltnNge.
case: ltnP => [?|le_s_n0]; rewrite ?(leq_trans le_s_n0) ?leq_addr ?addKn //=.
by rewrite drop_oversize // !nth_default.
Qed.
case: ltnP => [?|le_s_n0]; rewrite ?(leq_trans le_s_n0) ?leq_addr ?addKn //=.
by rewrite drop_oversize // !nth_default.
Qed.
Lemma find_ltn p s i : has p (take i s) -> find p s < i.
Proof.
by elim: s i => [|y s ihs] [|i]//=; case: (p _) => //= /ihs. Qed.
Lemma has_take p s i : has p s -> has p (take i s) = (find p s < i).
Proof.
by elim: s i => [|y s ihs] [|i]//=; case: (p _) => //= /ihs ->. Qed.
Lemma has_take_leq (p : pred T) (s : seq T) i : i <= size s ->
has p (take i s) = (find p s < i).
Proof.
by elim: s i => [|y s ihs] [|i]//=; case: (p _) => //= /ihs ->. Qed.
Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i.
Proof.
Lemma take_min i j s : take (minn i j) s = take i (take j s).
Proof.
Lemma take_takel i j s : i <= j -> take i (take j s) = take i s.
Lemma take_taker i j s : j <= i -> take i (take j s) = take j s.
Lemma take_drop i j s : take i (drop j s) = drop j (take (i + j) s).
Proof.
Lemma takeD i j s : take (i + j) s = take i s ++ take j (drop i s).
Proof.
Lemma takeC i j s : take i (take j s) = take j (take i s).
Lemma take_nseq i j x : i <= j -> take i (nseq j x) = nseq i x.
Proof.
Lemma drop_nseq i j x : drop i (nseq j x) = nseq (j - i) x.
Proof.
case: (leqP i j) => [/subnKC {1}<-|/ltnW j_le_i].
by rewrite nseqD drop_size_cat // size_nseq.
by rewrite drop_oversize ?size_nseq // (eqP j_le_i).
Qed.
by rewrite nseqD drop_size_cat // size_nseq.
by rewrite drop_oversize ?size_nseq // (eqP j_le_i).
Qed.
Lemma drop_nth n s : n < size s -> drop n s = nth s n :: drop n.+1 s.
Proof.
Lemma take_nth n s : n < size s -> take n.+1 s = rcons (take n s) (nth s n).
Proof.
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.
Proof.
Lemma rot_oversize n s : size s <= n -> rot n s = s.
Proof.
Lemma rot_size s : rot (size s) s = s.
Proof.
Lemma has_rot s a : has a (rot n0 s) = has a s.
Proof.
Lemma rot_size_cat s1 s2 : rot (size s1) (s1 ++ s2) = s2 ++ s1.
Proof.
Definition rotr n s := rot (size s - n) s.
Lemma rotK : cancel (rot n0) (rotr n0).
Proof.
Lemma rot_inj : injective (rot n0)
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).
Proof.
by elim: s u => /=. Qed.
Lemma catrev_catr s t u : catrev s (t ++ u) = catrev s t ++ u.
Proof.
by elim: s t => //= x s IHs t; rewrite -IHs. Qed.
Lemma catrevE s t : catrev s t = rev s ++ t.
Proof.
Lemma rev_cons x s : rev (x :: s) = rcons (rev s) x.
Lemma size_rev s : size (rev s) = size s.
Proof.
Lemma rev_nilp s : nilp (rev s) = nilp s.
Lemma rev_cat s t : rev (s ++ t) = rev t ++ rev s.
Proof.
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).
Proof.
Lemma filter_rev a s : filter a (rev s) = rev (filter a s).
Proof.
Lemma count_rev a s : count a (rev s) = count a s.
Proof.
Lemma has_rev a s : has a (rev s) = has a s.
Lemma all_rev a s : all a (rev s) = all a s.
Lemma rev_nseq n x : rev (nseq n x) = nseq n x.
End Sequences.
Prenex Implicits size ncons nseq head ohead behead last rcons belast.
Arguments seqn {T} n.
Prenex Implicits cat take drop rot rotr catrev.
Prenex Implicits find count nth all has filter.
Arguments rev {T} s : simpl never.
Arguments nth : simpl nomatch.
Arguments set_nth : simpl nomatch.
Arguments take : simpl nomatch.
Arguments drop : simpl nomatch.
Arguments nilP {T s}.
Arguments all_filterP {T a s}.
Arguments rotK n0 {T} s : rename.
Arguments rot_inj {n0 T} [s1 s2] eq_rot_s12 : rename.
Arguments revK {T} s : rename.
Notation count_mem x := (count (pred_of_simpl (pred1 x))).
Infix "++" := cat : seq_scope.
Notation "[ 'seq' x <- s | C ]" := (filter (fun x => C%B) s)
(x at level 99,
format "[ '[hv' 'seq' x <- s '/ ' | C ] ']'") : seq_scope.
Notation "[ 'seq' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
(format "[ '[hv' 'seq' x <- s '/ ' | C1 '/ ' & C2 ] ']'") : seq_scope.
Notation "[ 'seq' ' x <- s | C ]" := (filter (fun x => C%B) s)
(x strict pattern,
format "[ '[hv' 'seq' ' x <- s '/ ' | C ] ']'") : seq_scope.
Notation "[ 'seq' ' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
(x strict pattern,
format "[ '[hv' 'seq' ' x <- s '/ ' | C1 '/ ' & C2 ] ']'") : seq_scope.
Notation "[ 'seq' x : T <- s | C ]" := (filter (fun x : T => C%B) s)
(only parsing).
Notation "[ 'seq' x : T <- s | C1 & C2 ]" := [seq x : T <- s | C1 && C2]
(only parsing).
Lemma seq_ind2 {S T} (P : seq S -> seq T -> Type) :
P [::] [::] ->
(forall x y s t, size s = size t -> P s t -> P (x :: s) (y :: t)) ->
forall s t, size s = size t -> P s t.
Proof.
by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs.
Qed.
Qed.
Section AllIff.
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 ->
forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
Proof.
move=> iffPs; have PsS n: nth P0 Ps n -> nth P0 Ps n.+1.
elim: n P0 Ps iffPs => [|n IHn] P0 [|P [|Q Ps]] //= [iP0P] //; first by case.
by rewrite nth_nil.
by case=> iPQ iffPs; apply: IHn; split=> // /iP0P.
have{PsS} lePs: {homo nth P0 Ps : m n / m <= n >-> (m -> n)}.
by move=> m n /subnK<-; elim: {n}(n - m) => // n IHn /IHn; apply: PsS.
move=> m n P_m; have{m P_m} hP0: P0.
case: m P_m => //= m /(lePs m _ (leq_maxl m (size Ps))).
by rewrite nth_default ?leq_maxr.
case: n =>// n; apply: lePs 0 n (leq0n n) _.
by case: Ps iffPs hP0 => // P Ps [].
Qed.
elim: n P0 Ps iffPs => [|n IHn] P0 [|P [|Q Ps]] //= [iP0P] //; first by case.
by rewrite nth_nil.
by case=> iPQ iffPs; apply: IHn; split=> // /iP0P.
have{PsS} lePs: {homo nth P0 Ps : m n / m <= n >-> (m -> n)}.
by move=> m n /subnK<-; elim: {n}(n - m) => // n IHn /IHn; apply: PsS.
move=> m n P_m; have{m P_m} hP0: P0.
case: m P_m => //= m /(lePs m _ (leq_maxl m (size Ps))).
by rewrite nth_default ?leq_maxr.
case: n =>// n; apply: lePs 0 n (leq0n n) _.
by case: Ps iffPs hP0 => // P Ps [].
Qed.
Lemma all_iffP P0 Ps :
all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m <-> nth P0 (P0 :: Ps) n.
Proof.
End AllIff.
Arguments all_iffLR {P0 Ps}.
Arguments all_iffP {P0 Ps}.
Coercion all_iffP : all_iff >-> Funclass.
Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" :=
(all_iff P0 (@cons Prop P1 (.. (@cons Prop Pn nil) ..))) : form_scope.
Ltac tfae := do !apply: AllIffConj.
Section FindSpec.
Variable (T : Type) (a : {pred T}) (s : seq T).
Variant find_spec : bool -> nat -> Type :=
| NotFound of ~~ has a s : find_spec false (size s)
| Found (i : nat) of i < size s & (forall x0, a (nth x0 s i)) &
(forall x0 j, j < i -> a (nth x0 s j) = false) : find_spec true i.
Lemma findP : find_spec (has a s) (find a s).
Proof.
End FindSpec.
Arguments findP {T}.
Section RotRcons.
Variable T : Type.
Implicit Types (x : T) (s : seq T).
Lemma rot1_cons x s : rot 1 (x :: s) = rcons s x.
Lemma rcons_inj s1 s2 x1 x2 :
rcons s1 x1 = rcons s2 x2 :> seq T -> (s1, x1) = (s2, x2).
Lemma rcons_injl x : injective (rcons^~ x).
Proof.
Lemma rcons_injr s : injective (rcons s).
Proof.
End RotRcons.
Arguments rcons_inj {T s1 x1 s2 x2} eq_rcons : rename.
Arguments rcons_injl {T} x [s1 s2] eq_rcons : rename.
Arguments rcons_injr {T} s [x1 x2] eq_rcons : rename.
Section EqSeq.
Variables (n0 : nat) (T : eqType) (x0 : T).
Local Notation nth := (nth x0).
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.
Proof.
HB.instance Definition _ := hasDecEq.Build (seq T) eqseqP.
Lemma eqseqE : eqseq = eq_op
Proof.
by []. Qed.
Lemma eqseq_cons x1 x2 s1 s2 :
(x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).
Proof.
by []. Qed.
Lemma eqseq_cat s1 s2 s3 s4 :
size s1 = size s2 -> (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).
Proof.
Lemma eqseq_rcons s1 s2 x1 x2 :
(rcons s1 x1 == rcons s2 x2) = (s1 == s2) && (x1 == x2).
Lemma size_eq0 s : (size s == 0) = (s == [::]).
Lemma nilpE s : nilp s = (s == [::])
Proof.
by case: s. Qed.
Lemma has_filter a s : has a s = (filter a s != [::]).
Proof.
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).
Canonical mem_seq_predType := PredType mem_seq.
Lemma in_cons y s x : (x \in y :: s) = (x == y) || (x \in s).
Proof.
by []. Qed.
Lemma in_nil x : (x \in [::]) = false.
Proof.
by []. Qed.
Lemma mem_seq1 x y : (x \in [:: y]) = (x == y).
Let inE := (mem_seq1, in_cons, inE).
Lemma forall_cons {P : T -> Prop} {a s} :
{in a::s, forall x, P x} <-> P a /\ {in s, forall x, P x}.
Proof.
Lemma exists_cons {P : T -> Prop} {a s} :
(exists2 x, x \in a::s & P x) <-> P a \/ exists2 x, x \in s & P x.
Proof.
Lemma mem_seq2 x y z : (x \in [:: y; z]) = xpred2 y z x.
Proof.
Lemma mem_seq3 x y z t : (x \in [:: y; z; t]) = xpred3 y z t x.
Proof.
Lemma mem_seq4 x y z t u : (x \in [:: y; z; t; u]) = xpred4 y z t u x.
Proof.
Lemma mem_cat x s1 s2 : (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
Lemma mem_catC x s1 s2 : (x \in s1 ++ s2) = (x \in s2 ++ s1).
Lemma mem_rcons s y : rcons s y =i y :: s.
Lemma mem_head x s : x \in x :: s.
Proof.
Lemma mem_last x s : last x s \in x :: s.
Lemma mem_behead s : {subset behead s <= s}.
Proof.
Lemma mem_belast s y : {subset belast y s <= y :: s}.
Proof.
Lemma mem_nth s n : n < size s -> nth s n \in s.
Proof.
Lemma mem_nthE s n : (nth s n \in s) = ((n >= size s) ==> (x0 \in s)).
Proof.
apply/idP/idP; first by case: ltnP => // ?; rewrite nth_default.
by case: ltnP => //= ns x0s; [rewrite mem_nth|rewrite nth_default].
Qed.
by case: ltnP => //= ns x0s; [rewrite mem_nth|rewrite nth_default].
Qed.
Lemma mem_take s x : x \in take n0 s -> x \in s.
Proof.
Lemma mem_drop s x : x \in drop n0 s -> x \in s.
Proof.
Lemma last_eq s z x y : x != y -> z != y -> (last x s == y) = (last z s == y).
Section Filters.
Lemma subset_cons2 x s s' : {subset s <= s'} -> {subset x :: s <= x :: s'}.
Lemma subset_cons x s s' : {subset s <= s'} -> {subset s <= x :: s'}.
Implicit Type a : pred T.
Lemma hasP {a s} : reflect (exists2 x, x \in s & a x) (has a s).
Proof.
elim: s => [|y s IHs] /=; first by right; case.
exact: equivP (orPP idP IHs) (iff_sym exists_cons).
Qed.
exact: equivP (orPP idP IHs) (iff_sym exists_cons).
Qed.
Lemma allP {a s} : reflect {in s, forall x, a x} (all a s).
Proof.
Lemma hasPn a s : reflect {in s, forall x, ~~ a x} (~~ has a s).
Lemma allPn a s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).
Lemma allss s : all [in s] s
Proof.
exact/allP. Qed.
Lemma mem_filter a x s : (x \in filter a s) = a x && (x \in s).
Proof.
Variables (a : pred T) (s : seq T) (A : T -> Prop).
Hypothesis aP : forall x, reflect (A x) (a x).
Lemma hasPP : reflect (exists2 x, x \in s & A x) (has a s).
Lemma allPP : reflect {in s, forall x, A x} (all a 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.
Proof.
Lemma eq_in_find s : {in s, a1 =1 a2} -> find a1 s = find a2 s.
Proof.
Lemma eq_in_count s : {in s, a1 =1 a2} -> count a1 s = count a2 s.
Proof.
Lemma eq_in_all s : {in s, a1 =1 a2} -> all a1 s = all a2 s.
Proof.
Lemma eq_in_has s : {in s, a1 =1 a2} -> has a1 s = has a2 s.
Proof.
End EqIn.
Lemma eq_has_r s1 s2 : s1 =i s2 -> has^~ s1 =1 has^~ s2.
Lemma eq_all_r s1 s2 : s1 =i s2 -> all^~ s1 =1 all^~ s2.
Lemma has_sym s1 s2 : has [in s1] s2 = has [in s2] s1.
Lemma has_pred1 x s : has (pred1 x) s = (x \in s).
Lemma mem_rev s : rev s =i s.
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).
Proof.
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).
Proof.
Lemma constantP s : reflect (exists x, s = nseq (size s) x) (constant s).
Proof.
apply: (iffP idP) => [| [x ->]]; last exact: constant_nseq.
case: s => [|x s] /=; first by exists x0.
by move/all_pred1P=> def_s; exists x; rewrite -def_s.
Qed.
case: s => [|x s] /=; first by exists x0.
by move/all_pred1P=> def_s; exists x; rewrite -def_s.
Qed.
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.
Proof.
by []. Qed.
Lemma cat_uniq s1 s2 :
uniq (s1 ++ s2) = [&& uniq s1, ~~ has [in s1] s2 & uniq s2].
Proof.
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 uniq_cat_inLR x s1 s2 : uniq (s1 ++ s2) ->
x \in s1 ++ s2 -> (x \in s1) = (x \notin s2).
Proof.
Lemma uniq_cat_inRL x s1 s2 : uniq (s1 ++ s2) ->
x \in s1 ++ s2 -> (x \in s2) = (x \notin s1).
Proof.
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).
Proof.
Lemma rot_uniq s : uniq (rot n0 s) = uniq s.
Proof.
Lemma rev_uniq s : uniq (rev s) = uniq s.
Proof.
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).
Proof.
Lemma leq_uniq_countP x s1 s2 : uniq s1 ->
reflect (x \in s1 -> x \in s2) (count_mem x s1 <= count_mem x s2).
Proof.
Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} ->
(forall x, count_mem x s1 <= count_mem x s2).
Proof.
Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x].
Proof.
move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)).
by rewrite size_filter count_uniq_mem ?s_x.
Qed.
by rewrite size_filter count_uniq_mem ?s_x.
Qed.
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.
Proof.
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.
Proof.
Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
Proof.
Lemma undup_nil s : undup s = [::] -> s = [::].
Lemma undup_cat s t :
undup (s ++ t) = [seq x <- undup s | x \notin t] ++ undup t.
Lemma undup_rcons s x : undup (rcons s x) = rcons [seq y <- undup s | y != x] x.
Lemma count_undup s p : count p (undup s) <= count p s.
Proof.
Lemma has_undup p s : has p (undup s) = has p s.
Lemma all_undup p s : all p (undup s) = all p s.
Definition index x := find (pred1 x).
Lemma index_size x s : index x s <= size s.
Lemma index_mem x s : (index x s < size s) = (x \in s).
Lemma memNindex x s : x \notin s -> index x s = size s.
Lemma nth_index x s : x \in s -> nth s (index x s) = x.
Lemma index_inj s : {in s &, injective (index ^~ s)}.
Lemma index_cat x s1 s2 :
index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2.
Lemma index_ltn x s i : x \in take i s -> index x s < i.
Lemma in_take x s i : x \in s -> (x \in take i s) = (index x s < i).
Lemma in_take_leq x s i : i <= size s -> (x \in take i s) = (index x s < i).
Proof.
Lemma index_nth i s : i < size s -> index (nth s i) s <= i.
Proof.
Lemma nthK s: uniq s -> {in gtn (size s), cancel (nth s) (index^~ s)}.
Proof.
Lemma index_uniq i s : i < size s -> uniq s -> index (nth s i) s = i.
Proof.
Lemma index_head x s : index x (x :: s) = 0.
Proof.
Lemma index_last x s : uniq (x :: s) -> index (last x s) (x :: s) = size s.
Proof.
rewrite lastI rcons_uniq -cats1 index_cat size_belast.
by case: ifP => //=; rewrite eqxx addn0.
Qed.
by case: ifP => //=; rewrite eqxx addn0.
Qed.
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 (exists i j, [/\ i < j, j < size s & nth s i = nth s j]) (~~ uniq s).
Proof.
Lemma uniqP s : reflect {in gtn (size s) &, injective (nth s)} (uniq s).
Proof.
Lemma mem_rot s : rot n0 s =i s.
Proof.
Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
Lemma drop_index s (n := index x0 s) : x0 \in s -> drop n s = x0 :: drop n.+1 s.
Lemma index_pivot x s1 s2 (s := s1 ++ x :: s2) : x \notin s1 ->
index x s = size s1.
Lemma take_pivot x s2 s1 (s := s1 ++ x :: s2) : x \notin s1 ->
take (index x s) s = s1.
Proof.
Lemma rev_pivot x s1 s2 : rev (s1 ++ x :: s2) = rev s2 ++ x :: rev s1.
Lemma eqseq_pivot2l x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 ->
(s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Proof.
move=> xNs1 xNs3; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//].
suff S : size s1 = size s3 by rewrite eqseq_cat// eqseq_cons eqxx in E.
by rewrite -(index_pivot s2 xNs1) (eqP E) index_pivot.
Qed.
suff S : size s1 = size s3 by rewrite eqseq_cat// eqseq_cons eqxx in E.
by rewrite -(index_pivot s2 xNs1) (eqP E) index_pivot.
Qed.
Lemma eqseq_pivot2r x s1 s2 s3 s4 : x \notin s2 -> x \notin s4 ->
(s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Proof.
Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 ->
(s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Proof.
move=> xNs1 xNs2; apply/idP/idP => [E|/andP[/eqP-> /eqP->]//].
rewrite -(@eqseq_pivot2l x)//; have /eqP/(congr1 (count_mem x)) := E.
rewrite !count_cat/= eqxx !addnS (count_memPn _ _ xNs1) (count_memPn _ _ xNs2).
by move=> -[/esym/eqP]; rewrite addn_eq0 => /andP[/eqP/count_memPn].
Qed.
rewrite -(@eqseq_pivot2l x)//; have /eqP/(congr1 (count_mem x)) := E.
rewrite !count_cat/= eqxx !addnS (count_memPn _ _ xNs1) (count_memPn _ _ xNs2).
by move=> -[/esym/eqP]; rewrite addn_eq0 => /andP[/eqP/count_memPn].
Qed.
Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 -> x \notin s4 ->
(s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Proof.
Lemma uniq_eqseq_pivotl x s1 s2 s3 s4 : uniq (s1 ++ x :: s2) ->
(s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Proof.
Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4) ->
(s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Proof.
End EqSeq.
Arguments eqseq : simpl nomatch.
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 RotIndex.
Variables (T : eqType).
Implicit Types x y z : T.
Lemma rot_index s x (i := index x s) : x \in s ->
rot i s = x :: (drop i.+1 s ++ take i s).
Proof.
Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
Lemma rot_to s x : x \in s -> rot_to_spec s x.
End RotIndex.
Definition inE := (mem_seq1, in_cons, inE).
Prenex Implicits mem_seq1 constant uniq undup index.
Arguments eqseq {T} !_ !_.
Arguments pred_of_seq {T} s x /.
Arguments eqseqP {T x y}.
Arguments hasP {T a s}.
Arguments hasPn {T a s}.
Arguments allP {T a s}.
Arguments allPn {T a s}.
Arguments nseqP {T n x y}.
Arguments count_memPn {T x s}.
Arguments uniqPn {T} x0 {s}.
Arguments uniqP {T} x0 {s}.
Arguments forall_cons {T P a s}.
Arguments exists_cons {T P a s}.
#[export] Hint Extern 0 (is_true (all _ _)) =>
apply: (allss : forall T s, all (mem_seq s) s) : core.
Section NthTheory.
Lemma nthP (T : eqType) (s : seq T) x x0 :
reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s).
Proof.
Variable T : Type.
Implicit Types (a : pred T) (x : T).
Lemma has_nthP a s x0 :
reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).
Proof.
Lemma all_nthP a s x0 :
reflect (forall i, i < size s -> a (nth x0 s i)) (all a s).
Proof.
Lemma set_nthE s x0 n x :
set_nth x0 s n x = if n < size s
then take n s ++ x :: drop n.+1 s
else s ++ ncons (n - size s) x0 [:: x].
Proof.
elim: s n => [|a s IH] n /=; first by rewrite subn0 set_nth_nil.
case: n => [|n]; first by rewrite drop0.
by rewrite ltnS /=; case: ltnP (IH n) => _ ->.
Qed.
case: n => [|n]; first by rewrite drop0.
by rewrite ltnS /=; case: ltnP (IH n) => _ ->.
Qed.
Lemma count_set_nth a s x0 n x :
count a (set_nth x0 s n x) =
count a s + a x - a (nth x0 s n) * (n < size s) + (a x0) * (n - size s).
Proof.
rewrite set_nthE; case: ltnP => [nlts|nges]; last first.
rewrite -cat_nseq !count_cat count_nseq /=.
by rewrite muln0 addn0 subn0 addnAC addnA.
have -> : n - size s = 0 by apply/eqP; rewrite subn_eq0 ltnW.
rewrite -[in count a s](cat_take_drop n s) [drop n s](drop_nth x0)//.
by rewrite !count_cat/= muln1 muln0 addn0 addnAC !addnA [in RHS]addnAC addnK.
Qed.
rewrite -cat_nseq !count_cat count_nseq /=.
by rewrite muln0 addn0 subn0 addnAC addnA.
have -> : n - size s = 0 by apply/eqP; rewrite subn_eq0 ltnW.
rewrite -[in count a s](cat_take_drop n s) [drop n s](drop_nth x0)//.
by rewrite !count_cat/= muln1 muln0 addn0 addnAC !addnA [in RHS]addnAC addnK.
Qed.
Lemma count_set_nth_ltn a s x0 n x : n < size s ->
count a (set_nth x0 s n x) = count a s + a x - a (nth x0 s n).
Proof.
Lemma count_set_nthF a s x0 n x : ~~ a x0 ->
count a (set_nth x0 s n x) = count a s + a x - a (nth x0 s n).
Proof.
move=> /negbTE ax0; rewrite count_set_nth ax0 mul0n addn0.
case: ltnP => [_|nges]; first by rewrite muln1.
by rewrite nth_default// ax0 subn0.
Qed.
case: ltnP => [_|nges]; first by rewrite muln1.
by rewrite nth_default// ax0 subn0.
Qed.
End NthTheory.
Section SetNthLast.
Variables (T : Type) (s : seq T) (y0 x0 : T).
Lemma set_nth_default n : n < size s -> nth x0 s n = nth y0 s n.
Proof.
Lemma set_last_default : size s > 0 -> last x0 s = last y0 s.
Proof.
End SetNthLast.
Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x).
Proof.
by case: s. Qed.
Section LastTakeDrop.
Variable (T : eqType).
Implicit Types (x : T) (n : nat) (s : seq T).
Lemma last_take x n s : last x (take n s) =
if n > 0 then if n <= size s then nth x s n.-1 else last x s else x.
Proof.
elim: n s => [|n ihn] [|y s] //= in x *; rewrite {}ihn ltnS; case: n => //=.
by move=> n; case: ltnP => // n_lt; apply/set_nth_default.
Qed.
by move=> n; case: ltnP => // n_lt; apply/set_nth_default.
Qed.
Lemma last_drop x n s : last x (drop n s) = if n < size s then last x s else x.
Proof.
case: ltnP => sn; last by rewrite drop_oversize.
rewrite -[s in RHS](cat_take_drop n) last_cat.
by rewrite (@set_last_default _ _ x) ?size_drop ?subn_gt0.
Qed.
rewrite -[s in RHS](cat_take_drop n) last_cat.
by rewrite (@set_last_default _ _ x) ?size_drop ?subn_gt0.
Qed.
End LastTakeDrop.
Arguments nthP {T s x}.
Arguments has_nthP {T a s}.
Arguments all_nthP {T a s}.
Definition bitseq := seq bool.
#[hnf] HB.instance Definition _ := Equality.on bitseq.
Canonical bitseq_predType := Eval hnf in [predType of bitseq].
Section FindNth.
Variables (T : Type).
Implicit Types (x : T) (p : pred T) (s : seq T).
Variant split_find_nth_spec p : seq T -> seq T -> seq T -> T -> Type :=
FindNth x s1 s2 of p x & ~~ has p s1 :
split_find_nth_spec p (rcons s1 x ++ s2) s1 s2 x.
Lemma split_find_nth x0 p s (i := find p s) :
has p s -> split_find_nth_spec p s (take i s) (drop i.+1 s) (nth x0 s i).
Proof.
move=> p_s; rewrite -[X in split_find_nth_spec _ X](cat_take_drop i s).
rewrite (drop_nth x0 _) -?has_find// -cat_rcons.
by constructor; [apply: nth_find | rewrite has_take -?leqNgt].
Qed.
rewrite (drop_nth x0 _) -?has_find// -cat_rcons.
by constructor; [apply: nth_find | rewrite has_take -?leqNgt].
Qed.
Variant split_find_spec p : seq T -> seq T -> seq T -> Type :=
FindSplit x s1 s2 of p x & ~~ has p s1 :
split_find_spec p (rcons s1 x ++ s2) s1 s2.
Lemma split_find p s (i := find p s) :
has p s -> split_find_spec p s (take i s) (drop i.+1 s).
Proof.
Lemma nth_rcons_cat_find x0 p s1 s2 x (s := rcons s1 x ++ s2) :
p x -> ~~ has p s1 -> nth x0 s (find p s) = x.
Proof.
End FindNth.
Fixpoint incr_nth v i {struct i} :=
if v is n :: v' then if i is i'.+1 then n :: incr_nth v' i' else n.+1 :: v'
else ncons i 0 [:: 1].
Arguments incr_nth : simpl nomatch.
Lemma nth_incr_nth v i j : nth 0 (incr_nth v i) j = (i == j) + nth 0 v j.
Proof.
Lemma size_incr_nth v i :
size (incr_nth v i) = if i < size v then size v else i.+1.
Proof.
elim: v i => [|n v IHv] [|i] //=; first by rewrite size_ncons /= addn1.
by rewrite IHv; apply: fun_if.
Qed.
by rewrite IHv; apply: fun_if.
Qed.
Lemma incr_nth_inj v : injective (incr_nth v).
Proof.
move=> i j /(congr1 (nth 0 ^~ i)); apply: contra_eq => neq_ij.
by rewrite !nth_incr_nth eqn_add2r eqxx /nat_of_bool ifN_eqC.
Qed.
by rewrite !nth_incr_nth eqn_add2r eqxx /nat_of_bool ifN_eqC.
Qed.
Lemma incr_nthC v i j :
incr_nth (incr_nth v i) j = incr_nth (incr_nth v j) i.
Proof.
apply: (@eq_from_nth _ 0) => [|k _]; last by rewrite !nth_incr_nth addnCA.
by do !rewrite size_incr_nth leqNgt if_neg -/(maxn _ _); apply: maxnAC.
Qed.
by do !rewrite size_incr_nth leqNgt if_neg -/(maxn _ _); apply: maxnAC.
Qed.
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).
Proof.
apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP.
have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *.
have [/eqP|] := posnP (count a (s1 ++ s2)).
by rewrite count_cat addn_eq0; do 2!case: eqP => // ->.
rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x.
have cnt_a' s: count a s = count_mem x s + count a' s.
rewrite -count_predUI -[LHS]addn0 -(count_pred0 s).
by congr (_ + _); apply: eq_count => y /=; case: eqP => // ->.
rewrite !cnt_a' (eqnP (eq_cnt1 _ s12x)) (IHn a') // -ltnS.
apply: leq_trans le_an.
by rewrite ltnS cnt_a' -add1n leq_add2r -has_count has_pred1.
Qed.
have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *.
have [/eqP|] := posnP (count a (s1 ++ s2)).
by rewrite count_cat addn_eq0; do 2!case: eqP => // ->.
rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x.
have cnt_a' s: count a s = count_mem x s + count a' s.
rewrite -count_predUI -[LHS]addn0 -(count_pred0 s).
by congr (_ + _); apply: eq_count => y /=; case: eqP => // ->.
rewrite !cnt_a' (eqnP (eq_cnt1 _ s12x)) (IHn a') // -ltnS.
apply: leq_trans le_an.
by rewrite ltnS cnt_a' -add1n leq_add2r -has_count has_pred1.
Qed.
Lemma perm_refl s : perm_eq s s.
Proof.
exact/permP. Qed.
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
Proof.
by move->. Qed.
Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
Proof.
apply: (iffP idP) => [eq12 s3 | -> //]; apply/idP/idP; last exact: perm_trans.
by rewrite -!(perm_sym s3) => /perm_trans; apply.
Qed.
by rewrite -!(perm_sym s3) => /perm_trans; apply.
Qed.
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.
Proof.
Lemma perm_catl s t1 t2 : perm_eq t1 t2 -> perm_eql (s ++ t1) (s ++ t2).
Proof.
Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.
Proof.
Lemma perm_cat2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.
Proof.
Lemma perm_catr s1 s2 t : perm_eq s1 s2 -> perm_eql (s1 ++ t) (s2 ++ t).
Proof.
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).
Proof.
Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).
Proof.
Lemma perm_catACA s1 s2 s3 s4 :
perm_eql ((s1 ++ s2) ++ (s3 ++ s4)) ((s1 ++ s3) ++ (s2 ++ s4)).
Proof.
Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s).
Lemma perm_rot n s : perm_eql (rot n s) s.
Proof.
Lemma perm_rotr n s : perm_eql (rotr n s) s.
Proof.
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).
Proof.
Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
Proof.
apply/permPl; elim: s => //= x s IHs.
by case: (a x); last rewrite /= -cat1s perm_catCA; rewrite perm_cons.
Qed.
by case: (a x); last rewrite /= -cat1s perm_catCA; rewrite perm_cons.
Qed.
Lemma perm_size s1 s2 : perm_eq s1 s2 -> size s1 = size s2.
Proof.
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 (exists i u, rot i t = x :: u /\ perm_eq u s)
(perm_eq t (x :: s)).
Proof.
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.
Proof.
Lemma uniq_leq_size s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s1 <= size s2.
Proof.
Lemma leq_size_uniq s1 s2 :
uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> uniq s2.
Proof.
elim: s1 s2 => [[] | x s1 IHs s2] // Us1x; have /andP[not_s1x Us1] := Us1x.
case/forall_cons => /rot_to[i s3 def_s2] ss12 le_s21.
rewrite -(rot_uniq i) -(size_rot i) def_s2 /= in le_s21 *.
have ss13 y (s1y : y \in s1): y \in s3.
by have:= ss12 y s1y; rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)).
rewrite IHs // andbT; apply: contraL _ le_s21 => s3x; rewrite -leqNgt.
by apply/(uniq_leq_size Us1x)/allP; rewrite /= s3x; apply/allP.
Qed.
case/forall_cons => /rot_to[i s3 def_s2] ss12 le_s21.
rewrite -(rot_uniq i) -(size_rot i) def_s2 /= in le_s21 *.
have ss13 y (s1y : y \in s1): y \in s3.
by have:= ss12 y s1y; rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)).
rewrite IHs // andbT; apply: contraL _ le_s21 => s3x; rewrite -leqNgt.
by apply/(uniq_leq_size Us1x)/allP; rewrite /= s3x; apply/allP.
Qed.
Lemma uniq_size_uniq s1 s2 :
uniq s1 -> s1 =i s2 -> uniq s2 = (size s2 == size s1).
Proof.
move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12].
by rewrite eqn_leq !uniq_leq_size // => y; rewrite eqs12.
by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12).
Qed.
by rewrite eqn_leq !uniq_leq_size // => y; rewrite eqs12.
by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12).
Qed.
Lemma uniq_min_size s1 s2 :
uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 ->
(size s1 = size s2) * (s1 =i s2).
Proof.
move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21.
suffices: s1 =i s2 by split; first by apply/eqP; rewrite -uniq_size_uniq.
move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x.
rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //.
by apply/allP; rewrite /= s2x; apply/allP.
Qed.
suffices: s1 =i s2 by split; first by apply/eqP; rewrite -uniq_size_uniq.
move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x.
rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //.
by apply/allP; rewrite /= s2x; apply/allP.
Qed.
Lemma eq_uniq s1 s2 : size s1 = size s2 -> s1 =i s2 -> uniq s1 = uniq s2.
Proof.
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.
Proof.
Lemma perm_undup s1 s2 : s1 =i s2 -> perm_eq (undup s1) (undup s2).
Proof.
Lemma count_mem_uniq s : (forall x, count_mem x s = (x \in s)) -> uniq s.
Proof.
move=> count1_s; have Uus := undup_uniq s.
suffices: perm_eq s (undup s) by move/perm_uniq->.
by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup.
Qed.
suffices: perm_eq s (undup s) by move/perm_uniq->.
by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup.
Qed.
Lemma eq_count_undup a s1 s2 :
{in a, s1 =i s2} -> count a (undup s1) = count a (undup s2).
Proof.
move=> s1_eq_s2; rewrite -!size_filter !filter_undup.
apply/perm_size/perm_undup => x.
by rewrite !mem_filter; case: (boolP (a x)) => //= /s1_eq_s2.
Qed.
apply/perm_size/perm_undup => x.
by rewrite !mem_filter; case: (boolP (a x)) => //= /s1_eq_s2.
Qed.
Lemma catCA_perm_ind P :
(forall s1 s2 s3, P (s1 ++ s2 ++ s3) -> P (s2 ++ s1 ++ s3)) ->
(forall s1 s2, perm_eq s1 s2 -> P s1 -> P s2).
Proof.
move=> PcatCA s1 s2 eq_s12; rewrite -[s1]cats0 -[s2]cats0.
elim: s2 nil => [|x s2 IHs] s3 in s1 eq_s12 *.
by case: s1 {eq_s12}(perm_size eq_s12).
have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_mem eq_s12) mem_head.
rewrite -(cat_take_drop i s1) -catA => /PcatCA.
rewrite catA -/(rot i s1) def_s1 /= -cat1s => /PcatCA/IHs/PcatCA; apply.
by rewrite -(perm_cons x) -def_s1 perm_rot.
Qed.
elim: s2 nil => [|x s2 IHs] s3 in s1 eq_s12 *.
by case: s1 {eq_s12}(perm_size eq_s12).
have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_mem eq_s12) mem_head.
rewrite -(cat_take_drop i s1) -catA => /PcatCA.
rewrite catA -/(rot i s1) def_s1 /= -cat1s => /PcatCA/IHs/PcatCA; apply.
by rewrite -(perm_cons x) -def_s1 perm_rot.
Qed.
Lemma catCA_perm_subst R F :
(forall s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R) ->
(forall s1 s2, perm_eq s1 s2 -> F s1 = F s2).
Proof.
move=> FcatCA s1 s2 /catCA_perm_ind => ind_s12.
by apply: (ind_s12 (eq _ \o F)) => //= *; rewrite FcatCA.
Qed.
by apply: (ind_s12 (eq _ \o F)) => //= *; rewrite FcatCA.
Qed.
End PermSeq.
Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2).
Arguments permP {T s1 s2}.
Arguments permPl {T s1 s2}.
Arguments permPr {T s1 s2}.
Prenex Implicits perm_eq.
#[global] Hint Resolve perm_refl : core.
Section RotrLemmas.
Variables (n0 : nat) (T : Type) (T' : eqType).
Implicit Types (x : T) (s : seq T).
Lemma size_rotr s : size (rotr n0 s) = size s.
Proof.
Lemma mem_rotr (s : seq T') : rotr n0 s =i s.
Proof.
Lemma rotr_size_cat s1 s2 : rotr (size s2) (s1 ++ s2) = s2 ++ s1.
Proof.
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.
Proof.
Lemma rotr_uniq (s : seq T') : uniq (rotr n0 s) = uniq s.
Proof.
Lemma rotrK : cancel (@rotr T n0) (rot n0).
Proof.
Lemma rotr_inj : injective (@rotr T n0).
Lemma take_rev s : take n0 (rev s) = rev (drop (size s - n0) s).
Proof.
Lemma rev_take s : rev (take n0 s) = drop (size s - n0) (rev s).
Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).
Proof.
Lemma rev_drop s : rev (drop n0 s) = take (size s - n0) (rev s).
Lemma rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).
Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).
End RotrLemmas.
Arguments rotrK n0 {T} s : rename.
Arguments rotr_inj {n0 T} [s1 s2] eq_rotr_s12 : rename.
Section RotCompLemmas.
Variable T : Type.
Implicit Type s : seq T.
Lemma rotD m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s).
Proof.
move=> sz_s; rewrite [LHS]/rot -[take _ s](cat_take_drop n).
rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop.
by rewrite size_drop !size_takel ?leq_addl ?addnK.
Qed.
rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop.
by rewrite size_drop !size_takel ?leq_addl ?addnK.
Qed.
Lemma rotS n s : n < size s -> rot n.+1 s = rot 1 (rot n s).
Proof.
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.
Proof.
Lemma rot_minn n s : rot n s = rot (minn n (size s)) s.
Proof.
Definition rot_add s n m (k := size s) (p := minn m k + minn n k) :=
locked (if p <= k then p else p - k).
Lemma leq_rot_add n m s : rot_add s n m <= size s.
Lemma rot_addC n m s : rot_add s n m = rot_add s m n.
Lemma rot_rot_add n m s : rot m (rot n s) = rot (rot_add s n m) s.
Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s).
Proof.
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 = [::].
Proof.
by elim: s n => [|x s IHs] [|n] /=. Qed.
Lemma mask_true s n : size s <= n -> mask (nseq n true) s = s.
Proof.
Lemma mask0 m : mask m [::] = [::].
Proof.
by case: m. Qed.
Lemma mask0s s : mask [::] s = [::]
Proof.
by []. Qed.
Lemma mask1 b x : mask [:: b] [:: x] = nseq b x.
Proof.
by case: b. Qed.
Lemma mask_cons b m x s : mask (b :: m) (x :: s) = nseq b x ++ mask m s.
Proof.
by case: b. Qed.
Lemma size_mask m s : size m = size s -> size (mask m s) = count id m.
Proof.
Lemma mask_cat m1 m2 s1 s2 :
size m1 = size s1 -> mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.
Proof.
Lemma mask_rcons b m x s : size m = size s ->
mask (rcons m b) (rcons s x) = mask m s ++ nseq b x.
Lemma all_mask a m s : all a s -> all a (mask m s).
Proof.
Lemma has_mask_cons a b m x s :
has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).
Proof.
by case: b. Qed.
Lemma has_mask a m s : has a (mask m s) -> has a s.
Lemma rev_mask m s : size m = size s -> rev (mask m s) = mask (rev m) (rev s).
Proof.
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).
Proof.
move=> Ems; rewrite mask_cat ?size_drop ?Ems // -rot_size_cat.
by rewrite size_mask -?mask_cat ?size_take ?Ems // !cat_take_drop.
Qed.
by rewrite size_mask -?mask_cat ?size_take ?Ems // !cat_take_drop.
Qed.
Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s}.
Proof.
Lemma takeEmask i s : take i s = mask (nseq i true) s.
Proof.
Lemma dropEmask i s :
drop i s = mask (nseq i false ++ nseq (size s - i) true) s.
End Mask.
Arguments mask _ !_ !_.
Section EqMask.
Variables (n0 : nat) (T : eqType).
Implicit Types (s : seq T) (m : bitseq).
Lemma mem_mask_cons x b m y s :
(x \in mask (b :: m) (y :: s)) = b && (x == y) || (x \in mask m s).
Proof.
by case: b. Qed.
Lemma mem_mask x m s : x \in mask m s -> x \in s.
Lemma in_mask x m s :
uniq s -> (x \in mask m s) = (x \in s) && nth false m (index x s).
Proof.
Lemma mask_uniq s : uniq s -> forall m, uniq (mask m s).
Proof.
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
Proof.
by case: s. Qed.
Lemma subseq0 s : subseq s [::] = (s == [::])
Proof.
by []. Qed.
Lemma subseq_refl s : subseq s s.
Proof.
Lemma subseqP s1 s2 :
reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2).
Proof.
elim: s2 s1 => [|y s2 IHs2] [|x s1].
- by left; exists [::].
- by right=> -[m /eqP/nilP->].
- by left; exists (nseq (size s2).+1 false); rewrite ?size_nseq //= mask_false.
apply: {IHs2}(iffP (IHs2 _)) => [] [m sz_m def_s1].
by exists ((x == y) :: m); rewrite /= ?sz_m // -def_s1; case: eqP => // ->.
case: eqP => [_ | ne_xy]; last first.
by case: m def_s1 sz_m => [|[] m] //; [case | move=> -> [<-]; exists m].
pose i := index true m; have def_m_i: take i m = nseq (size (take i m)) false.
apply/all_pred1P; apply/(all_nthP true) => j.
rewrite size_take ltnNge geq_min negb_or -ltnNge => /andP[lt_j_i _].
rewrite nth_take //= -negb_add addbF -addbT -negb_eqb.
by rewrite [_ == _](before_find _ lt_j_i).
have lt_i_m: i < size m.
rewrite ltnNge; apply/negP=> le_m_i; rewrite take_oversize // in def_m_i.
by rewrite def_m_i mask_false in def_s1.
rewrite size_take lt_i_m in def_m_i.
exists (take i m ++ drop i.+1 m).
rewrite size_cat size_take size_drop lt_i_m.
by rewrite sz_m in lt_i_m *; rewrite subnKC.
rewrite {s1 def_s1}[s1](congr1 behead def_s1).
rewrite -[s2](cat_take_drop i) -[m in LHS](cat_take_drop i) {}def_m_i -cat_cons.
have sz_i_s2: size (take i s2) = i by apply: size_takel; rewrite sz_m in lt_i_m.
rewrite lastI cat_rcons !mask_cat ?size_nseq ?size_belast ?mask_false //=.
by rewrite (drop_nth true) // nth_index -?index_mem.
Qed.
- by left; exists [::].
- by right=> -[m /eqP/nilP->].
- by left; exists (nseq (size s2).+1 false); rewrite ?size_nseq //= mask_false.
apply: {IHs2}(iffP (IHs2 _)) => [] [m sz_m def_s1].
by exists ((x == y) :: m); rewrite /= ?sz_m // -def_s1; case: eqP => // ->.
case: eqP => [_ | ne_xy]; last first.
by case: m def_s1 sz_m => [|[] m] //; [case | move=> -> [<-]; exists m].
pose i := index true m; have def_m_i: take i m = nseq (size (take i m)) false.
apply/all_pred1P; apply/(all_nthP true) => j.
rewrite size_take ltnNge geq_min negb_or -ltnNge => /andP[lt_j_i _].
rewrite nth_take //= -negb_add addbF -addbT -negb_eqb.
by rewrite [_ == _](before_find _ lt_j_i).
have lt_i_m: i < size m.
rewrite ltnNge; apply/negP=> le_m_i; rewrite take_oversize // in def_m_i.
by rewrite def_m_i mask_false in def_s1.
rewrite size_take lt_i_m in def_m_i.
exists (take i m ++ drop i.+1 m).
rewrite size_cat size_take size_drop lt_i_m.
by rewrite sz_m in lt_i_m *; rewrite subnKC.
rewrite {s1 def_s1}[s1](congr1 behead def_s1).
rewrite -[s2](cat_take_drop i) -[m in LHS](cat_take_drop i) {}def_m_i -cat_cons.
have sz_i_s2: size (take i s2) = i by apply: size_takel; rewrite sz_m in lt_i_m.
rewrite lastI cat_rcons !mask_cat ?size_nseq ?size_belast ?mask_false //=.
by rewrite (drop_nth true) // nth_index -?index_mem.
Qed.
Lemma mask_subseq m s : subseq (mask m s) s.
Proof.
Lemma subseq_trans : transitive subseq.
Proof.
move=> _ _ s /subseqP[m2 _ ->] /subseqP[m1 _ ->].
elim: s => [|x s IHs] in m2 m1 *; first by rewrite !mask0.
case: m1 => [|[] m1]; first by rewrite mask0.
case: m2 => [|[] m2] //; first by rewrite /= eqxx IHs.
case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP.
by exists (false :: m); rewrite //= sz_m.
case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP.
by exists (false :: m); rewrite //= sz_m.
Qed.
elim: s => [|x s IHs] in m2 m1 *; first by rewrite !mask0.
case: m1 => [|[] m1]; first by rewrite mask0.
case: m2 => [|[] m2] //; first by rewrite /= eqxx IHs.
case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP.
by exists (false :: m); rewrite //= sz_m.
case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP.
by exists (false :: m); rewrite //= sz_m.
Qed.
Lemma cat_subseq s1 s2 s3 s4 :
subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
Proof.
Lemma prefix_subseq s1 s2 : subseq s1 (s1 ++ s2).
Proof.
Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2).
Proof.
Lemma take_subseq s i : subseq (take i s) s.
Proof.
Lemma drop_subseq s i : subseq (drop i s) s.
Proof.
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.
Proof.
Lemma size_subseq_leqif s1 s2 :
subseq s1 s2 -> size s1 <= size s2 ?= iff (s1 == s2).
Proof.
Lemma subseq_anti : antisymmetric subseq.
Proof.
move=> s1 s2 /andP[] /size_subseq_leqif /leqifP.
by case: eqP => [//|_] + /size_subseq; rewrite ltnNge => /negP.
Qed.
by case: eqP => [//|_] + /size_subseq; rewrite ltnNge => /negP.
Qed.
Lemma subseq_cons s x : subseq s (x :: s).
Proof.
Lemma cons_subseq s1 s2 x : subseq (x :: s1) s2 -> subseq s1 s2.
Proof.
Lemma subseq_rcons s x : subseq s (rcons s x).
Proof.
Lemma subseq_uniq s1 s2 : subseq s1 s2 -> uniq s2 -> uniq s1.
Lemma take_uniq s n : uniq s -> uniq (take n s).
Proof.
Lemma drop_uniq s n : uniq s -> uniq (drop n s).
Proof.
Lemma undup_subseq s : subseq (undup s) s.
Proof.
elim: s => //= x s; case: (_ \in _); last by rewrite eqxx.
by case: (undup s) => //= y u; case: (_ == _) => //=; apply: cons_subseq.
Qed.
by case: (undup s) => //= y u; case: (_ == _) => //=; apply: cons_subseq.
Qed.
Lemma subseq_rev s1 s2 : subseq (rev s1) (rev s2) = subseq s1 s2.
Proof.
Lemma subseq_cat2l s s1 s2 : subseq (s ++ s1) (s ++ s2) = subseq s1 s2.
Lemma subseq_cat2r s s1 s2 : subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2.
Proof.
Lemma subseq_rot p s n :
subseq p s -> exists2 k, k <= n & subseq (rot k p) (rot n s).
Proof.
move=> /subseqP[m size_m ->].
exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq.
by rewrite (leq_trans (count_size _ _))// size_take_min geq_minl.
Qed.
exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq.
by rewrite (leq_trans (count_size _ _))// size_take_min geq_minl.
Qed.
End Subseq.
Prenex Implicits subseq.
Arguments subseqP {T s1 s2}.
#[global] Hint Resolve subseq_refl : core.
Section Rem.
Variables (T : eqType) (x : T).
Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s.
Lemma rem_cons y s : rem (y :: s) = if y == x then s else y :: rem s.
Proof.
by []. Qed.
Lemma remE s : rem s = take (index x s) s ++ drop (index x s).+1 s.
Lemma rem_id s : x \notin s -> rem s = s.
Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s).
Proof.
move=> xs; rewrite remE -[X in perm_eq X](cat_take_drop (index x s)).
by rewrite drop_index// -cat1s perm_catCA cat1s.
Qed.
by rewrite drop_index// -cat1s perm_catCA cat1s.
Qed.
Lemma size_rem s : x \in s -> size (rem s) = (size s).-1.
Proof.
Lemma rem_subseq s : subseq (rem s) s.
Proof.
elim: s => //= y s IHs; rewrite eq_sym.
by case: ifP => _; [apply: subseq_cons | rewrite eqxx].
Qed.
by case: ifP => _; [apply: subseq_cons | rewrite eqxx].
Qed.
Lemma rem_uniq s : uniq s -> uniq (rem s).
Proof.
Lemma mem_rem s : {subset rem s <= s}.
Proof.
Lemma rem_mem y s : y != x -> y \in s -> y \in rem s.
Proof.
Lemma rem_filter s : uniq s -> rem s = filter (predC1 x) s.
Proof.
Lemma mem_rem_uniq s : uniq s -> rem s =i [predD1 s & x].
Proof.
Lemma mem_rem_uniqF s : uniq s -> (x \in rem s) = false.
Proof.
Lemma count_rem P s : count P (rem s) = count P s - (x \in s) && P x.
Proof.
Lemma count_mem_rem y s : count_mem y (rem s) = count_mem y s - (x == y).
End Rem.
Section Map.
Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2) (f : T1 -> T2).
Fixpoint map s := if s is x :: s' then f x :: map s' else [::].
Lemma map_cons x s : map (x :: s) = f x :: map s.
Proof.
by []. Qed.
Lemma map_nseq x : map (nseq n0 x) = nseq n0 (f x).
Lemma map_cat s1 s2 : map (s1 ++ s2) = map s1 ++ map s2.
Proof.
by elim: s1 => [|x s1 IHs] //=; rewrite IHs. Qed.
Lemma size_map s : size (map s) = size s.
Proof.
by elim: s => //= x s ->. Qed.
Lemma behead_map s : behead (map s) = map (behead s).
Proof.
by case: s. Qed.
Lemma nth_map n s : n < size s -> nth x2 (map s) n = f (nth x1 s n).
Proof.
by elim: s n => [|x s IHs] []. Qed.
Lemma map_nth x n s : f (nth x s n) = nth (f x) (map s) n.
Proof.
by elim: n s => [|n IHn] [|y s] /=. Qed.
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).
Proof.
by elim: s x => /=. Qed.
Lemma belast_map s x : belast (f x) (map s) = map (belast x s).
Proof.
by elim: s x => //= y s IHs x; rewrite IHs. Qed.
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.
Proof.
by elim: s => //= x s ->. Qed.
Lemma has_map a s : has a (map s) = has (preim f a) s.
Proof.
by elim: s => //= x s ->. Qed.
Lemma all_map a s : all a (map s) = all (preim f a) s.
Proof.
by elim: s => //= x s ->. Qed.
Lemma all_mapT (a : pred T2) s : (forall x, a (f x)) -> all a (map s).
Lemma count_map a s : count a (map s) = count (preim f a) s.
Proof.
by elim: s => //= x s ->. Qed.
Lemma map_take s : map (take n0 s) = take n0 (map s).
Proof.
Lemma map_drop s : map (drop n0 s) = drop n0 (map s).
Proof.
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).
Proof.
by elim: m s => [|[|] m IHm] [|x p] //=; rewrite IHm. Qed.
Lemma inj_map : injective f -> injective map.
Proof.
by move=> injf; elim=> [|x s IHs] [|y t] //= [/injf-> /IHs->]. Qed.
Lemma inj_in_map (A : {pred T1}) :
{in A &, injective f} -> {in [pred s | all [in A] s] &, injective map}.
Proof.
End Map.
Section onth.
Variable T : Type.
Implicit Types x y z : T.
Implicit Types m n : nat.
Implicit Type s : seq T.
Fixpoint onth s n {struct n} : option T :=
if s isn't x :: s then None else
if n isn't n.+1 then Some x else onth s n.
Lemma odflt_onth x0 s n : odflt x0 (onth s n) = nth x0 s n.
Proof.
by elim: n s => [|? ?] []. Qed.
Lemma onthE s : onth s =1 nth None (map Some s).
Proof.
by move=> n; elim: n s => [|? ?] []. Qed.
Lemma onth_nth x0 x t n : onth t n = Some x -> nth x0 t n = x.
Proof.
Lemma onth0n n : onth [::] n = None
Proof.
by case: n. Qed.
Lemma onth1P x y n : onth [:: x] n = Some y <-> n = 0 /\ x = y.
Proof.
by case: n => [|[]]; split=> // -[] // _ ->. Qed.
Lemma onthTE s n : onth s n = (n < size s) :> bool.
Proof.
by elim: n s => [|? ?] []. Qed.
Lemma onthNE s n: ~~ onth s n = (size s <= n).
Lemma onth_default n s : size s <= n -> onth s n = None.
Lemma onth_cat s1 s2 n :
onth (s1 ++ s2) n = if n < size s1 then onth s1 n else onth s2 (n - size s1).
Proof.
by elim: n s1 => [|? ?] []. Qed.
Lemma onth_nseq x n m : onth (nseq n x) m = if m < n then Some x else None.
Lemma eq_onthP {s1 s2} :
[<-> s1 = s2;
forall i : nat, i < maxn (size s1) (size s2) -> onth s1 i = onth s2 i;
forall i : nat, onth s1 i = onth s2 i].
Proof.
tfae=> [->//|eqs12 i|eqs12].
have := eqs12 i; case: ltnP => [_ ->//|].
by rewrite geq_max => /andP[is1 is2] _; rewrite !onth_default.
have /eqP eq_size_12 : size s1 == size s2.
by rewrite eqn_leq -!onthNE eqs12 onthNE -eqs12 onthNE !leqnn.
apply/(inj_map Some_inj)/(@eq_from_nth _ None); rewrite !size_map//.
by move=> i _; rewrite -!onthE eqs12.
Qed.
have := eqs12 i; case: ltnP => [_ ->//|].
by rewrite geq_max => /andP[is1 is2] _; rewrite !onth_default.
have /eqP eq_size_12 : size s1 == size s2.
by rewrite eqn_leq -!onthNE eqs12 onthNE -eqs12 onthNE !leqnn.
apply/(inj_map Some_inj)/(@eq_from_nth _ None); rewrite !size_map//.
by move=> i _; rewrite -!onthE eqs12.
Qed.
Lemma eq_from_onth [s1 s2 : seq T] :
(forall i : nat, onth s1 i = onth s2 i) -> s1 = s2.
Proof.
Lemma eq_from_onth_le [s1 s2 : seq T] :
(forall i : nat, i < maxn (size s1) (size s2) -> onth s1 i = onth s2 i) ->
s1 = s2.
Proof.
End onth.
Lemma onth_map {T S} n (s : seq T) (f : T -> S) :
onth (map f s) n = omap f (onth s n).
Proof.
by elim: s n => [|x s IHs] []. Qed.
Lemma inj_onth_map {T S} n (s : seq T) (f : T -> S) x :
injective f -> onth (map f s) n = Some (f x) -> onth s n = Some x.
Section onthEqType.
Variables T : eqType.
Implicit Types x y z : T.
Implicit Types i m n : nat.
Implicit Type s : seq T.
Lemma onthP s x : reflect (exists i, onth s i = Some x) (x \in s).
Proof.
Lemma onthPn s x : reflect (forall i, onth s i != Some x) (x \notin s).
Proof.
Lemma onth_inj s n m : uniq s -> minn m n < size s ->
onth s n = onth s m -> n = m.
Proof.
End onthEqType.
Arguments onthP {T s x}.
Arguments onthPn {T s x}.
Arguments onth_nth {T}.
Arguments onth_inj {T}.
Notation "[ 'seq' E | i <- s ]" := (map (fun i => E) s)
(i binder, format "[ '[hv' 'seq' E '/ ' | i <- s ] ']'") : seq_scope.
Notation "[ 'seq' E | i <- s & C ]" := [seq E | i <- [seq i <- s | C]]
(i binder,
format "[ '[hv' 'seq' E '/ ' | i <- s '/ ' & C ] ']'") : seq_scope.
Notation "[ 'seq' E : R | i <- s ]" := (@map _ R (fun i => E) s)
(i binder, only parsing) : seq_scope.
Notation "[ 'seq' E : R | i <- s & C ]" := [seq E : R | i <- [seq i <- s | C]]
(i binder, only parsing) : seq_scope.
Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
Proof.
by elim: s => //= x s <-; case: (a x). Qed.
Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | s = map sval s'}.
Proof.
Section MiscMask.
Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s.
Proof.
Variable (T : eqType).
Implicit Types (s : seq T) (m : bitseq).
Lemma mask_filter s m : uniq s -> mask m s = [seq i <- s | i \in mask m s].
Proof.
Lemma leq_count_subseq P s1 s2 : subseq s1 s2 -> count P s1 <= count P s2.
Proof.
Lemma count_maskP s1 s2 :
(forall x, count_mem x s1 <= count_mem x s2) <->
exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2).
Proof.
split=> [s1_le|[m _ /permP s1ms2 x]]; last by rewrite s1ms2 leq_count_mask.
suff [m mP]: exists m, perm_eq s1 (mask m s2).
by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm.
elim: s2 => [|x s2 IHs]//= in s1 s1_le *.
by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le.
have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR.
exists ((x \in s1) :: m); have [|/rem_id<-//] := boolP (x \in s1).
by move/perm_to_rem/permPl->; rewrite perm_cons.
Qed.
suff [m mP]: exists m, perm_eq s1 (mask m s2).
by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm.
elim: s2 => [|x s2 IHs]//= in s1 s1_le *.
by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le.
have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR.
exists ((x \in s1) :: m); have [|/rem_id<-//] := boolP (x \in s1).
by move/perm_to_rem/permPl->; rewrite perm_cons.
Qed.
Lemma count_subseqP s1 s2 :
(forall x, count_mem x s1 <= count_mem x s2) <->
exists2 s, subseq s s2 & perm_eq s1 s.
Proof.
split=> [/count_maskP[m _]|]; first by exists (mask m s2); rewrite ?mask_subseq.
by move=> -[_/subseqP[m sm ->] ?]; apply/count_maskP; exists m.
Qed.
by move=> -[_/subseqP[m sm ->] ?]; apply/count_maskP; exists m.
Qed.
End MiscMask.
Section FilterSubseq.
Variable T : eqType.
Implicit Types (s : seq T) (a : pred T).
Lemma filter_subseq a s : subseq (filter a s) s.
Proof.
Lemma subset_memP s1 s2 : {subset s1 <= s2} -> {s3 | subseq s3 s2 & s1 =i s3}.
Proof.
move=> s12; exists (filter [in s1] s2); first by rewrite filter_subseq.
by move=> x; rewrite mem_filter andb_idr//; apply: s12.
Qed.
by move=> x; rewrite mem_filter andb_idr//; apply: s12.
Qed.
Lemma subseq_filter s1 s2 a :
subseq s1 (filter a s2) = all a s1 && subseq s1 s2.
Proof.
Lemma subseq_uniqP s1 s2 :
uniq s2 -> reflect (s1 = filter [in s1] s2) (subseq s1 s2).
Proof.
move=> uniq_s2; apply: (iffP idP) => [ss12 | ->]; last exact: filter_subseq.
apply/eqP; rewrite -size_subseq_leqif ?subseq_filter ?(introT allP) //.
apply/eqP/esym/perm_size.
rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x.
by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12).
Qed.
apply/eqP; rewrite -size_subseq_leqif ?subseq_filter ?(introT allP) //.
apply/eqP/esym/perm_size.
rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x.
by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12).
Qed.
Lemma uniq_subseq_pivot x (s1 s2 s3 s4 : seq T) (s := s3 ++ x :: s4) :
uniq s -> subseq (s1 ++ x :: s2) s = (subseq s1 s3 && subseq s2 s4).
Proof.
move=> uniq_s; apply/idP/idP => [sub_s'_s|/andP[? ?]]; last first.
by rewrite cat_subseq //= eqxx.
have uniq_s' := subseq_uniq sub_s'_s uniq_s.
have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s.
rewrite !filter_cat /= mem_cat inE eqxx orbT /=.
rewrite uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->].
by rewrite !filter_subseq.
Qed.
by rewrite cat_subseq //= eqxx.
have uniq_s' := subseq_uniq sub_s'_s uniq_s.
have/eqP {sub_s'_s uniq_s} := subseq_uniqP _ uniq_s sub_s'_s.
rewrite !filter_cat /= mem_cat inE eqxx orbT /=.
rewrite uniq_eqseq_pivotl // => /andP [/eqP -> /eqP ->].
by rewrite !filter_subseq.
Qed.
Lemma perm_to_subseq s1 s2 :
subseq s1 s2 -> {s3 | perm_eq s2 (s1 ++ s3)}.
Proof.
elim Ds2: s2 s1 => [|y s2' IHs] [|x s1] //=; try by exists s2; rewrite Ds2.
case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}.
by exists s3; rewrite perm_cons.
by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r.
Qed.
case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}.
by exists s3; rewrite perm_cons.
by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r.
Qed.
Lemma subseq_rem x : {homo rem x : s1 s2 / @subseq T s1 s2}.
Proof.
move=> s1 s2; elim: s2 s1 => [|x2 s2 IHs2] [|x1 s1]; rewrite ?sub0seq //=.
have [->|_] := eqVneq x1 x2; first by case: eqP => //= _ /IHs2; rewrite eqxx.
move=> /IHs2/subseq_trans->//.
by have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons].
Qed.
have [->|_] := eqVneq x1 x2; first by case: eqP => //= _ /IHs2; rewrite eqxx.
move=> /IHs2/subseq_trans->//.
by have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons].
Qed.
End FilterSubseq.
Arguments subseq_uniqP [T s1 s2].
Section EqMap.
Variables (n0 : nat) (T1 : eqType) (x1 : T1).
Variables (T2 : eqType) (x2 : T2) (f : T1 -> T2).
Implicit Type s : seq T1.
Lemma map_f s x : x \in s -> f x \in map f s.
Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s).
Proof.
Lemma subset_mapP (s : seq T1) (s' : seq T2) :
{subset s' <= map f s} <-> exists2 t, all (mem s) t & s' = map f t.
Proof.
Lemma map_uniq s : uniq (map f s) -> uniq s.
Proof.
Lemma map_inj_in_uniq s : {in s &, injective f} -> uniq (map f s) = uniq s.
Proof.
Lemma map_subseq s1 s2 : subseq s1 s2 -> subseq (map f s1) (map f s2).
Lemma index_map_in s x :
{in s &, injective f} -> x \in s -> index (f x) (map f s) = index x s.
Proof.
move=> f_inj x_in_s; rewrite /index find_map.
by apply: eq_in_find => y /= y_s; rewrite (inj_in_eq f_inj).
Qed.
by apply: eq_in_find => y /= y_s; rewrite (inj_in_eq f_inj).
Qed.
Lemma index_map_inW s x : {in s, injective f} -> index (f x) (map f s) = index x s.
Proof.
Lemma uniq_map_inj_in s : uniq (map f s) -> {in s &, injective f}.
Proof.
Lemma nth_index_map s x0 x :
{in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x.
Proof.
Lemma perm_map s t : perm_eq s t -> perm_eq (map f s) (map f t).
Lemma sub_map s1 s2 : {subset s1 <= s2} -> {subset map f s1 <= map f s2}.
Lemma eq_mem_map s1 s2 : s1 =i s2 -> map f s1 =i map f s2.
Hypothesis Hf : injective f.
Lemma mem_map s x : (f x \in map f s) = (x \in s).
Lemma index_map s x : index (f x) (map f s) = index x s.
Proof.
Lemma map_inj_uniq s : uniq (map f s) = uniq s.
Proof.
Lemma undup_map_inj s : undup (map f s) = map f (undup s).
Lemma perm_map_inj s t : perm_eq (map f s) (map f t) -> perm_eq s t.
Proof.
End EqMap.
Arguments mapP {T1 T2 f s y}.
Arguments subset_mapP {T1 T2}.
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}.
Proof.
exists (fun x => nth y0 fs (index x s)) => uAs eq_sz.
apply/esym/(@eq_from_nth _ y0); rewrite ?size_map eq_sz // => i ltis.
by have x0 : T1 by [case: (s) ltis]; rewrite (nth_map x0) // index_uniq.
Qed.
apply/esym/(@eq_from_nth _ y0); rewrite ?size_map eq_sz // => i ltis.
by have x0 : T1 by [case: (s) ltis]; rewrite (nth_map x0) // index_uniq.
Qed.
Section MapComp.
Variable S T U : Type.
Lemma map_id (s : seq T) : map id s = s.
Proof.
by elim: s => //= x s ->. Qed.
Lemma eq_map (f g : S -> T) : f =1 g -> map f =1 map g.
Proof.
by move=> Ef; elim=> //= x s ->; rewrite Ef. Qed.
Lemma map_comp (f : T -> U) (g : S -> T) s : map (f \o g) s = map f (map g s).
Proof.
by elim: s => //= x s ->. Qed.
Lemma mapK (f : S -> T) (g : T -> S) : cancel f g -> cancel (map f) (map g).
Proof.
by move=> fK; elim=> //= x s ->; rewrite fK. Qed.
Lemma mapK_in (A : {pred S}) (f : S -> T) (g : T -> S) :
{in A, cancel f g} -> {in [pred s | all [in A] s], cancel (map f) (map g)}.
Proof.
End MapComp.
Lemma eq_in_map (S : eqType) T (f g : S -> T) (s : seq S) :
{in s, f =1 g} <-> map f s = map g s.
Proof.
elim: s => //= x s IHs; split=> [/forall_cons[-> ?]|]; first by rewrite IHs.1.
by move=> -[? ?]; apply/forall_cons; split=> [//|]; apply: IHs.2.
Qed.
by move=> -[? ?]; apply/forall_cons; split=> [//|]; apply: IHs.2.
Qed.
Lemma map_id_in (T : eqType) f (s : seq T) : {in s, f =1 id} -> map f s = s.
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.
Proof.
by move=> gK; elim=> //= x s ->; rewrite gK. Qed.
Lemma size_pmap s : size (pmap s) = count [eta f] s.
Proof.
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.
Proof.
Lemma all_pmap (p : pred rT) s :
all p (pmap s) = all [pred i | oapp p true (f i)] s.
Proof.
End Pmap.
Lemma eq_in_pmap (aT : eqType) rT (f1 f2 : aT -> option rT) s :
{in s, f1 =1 f2} -> pmap f1 s = pmap f2 s.
Proof.
Lemma eq_pmap aT rT (f1 f2 : aT -> option rT) :
f1 =1 f2 -> pmap f1 =1 pmap f2.
Proof.
by move=> Ef; elim => //= a s ->; rewrite Ef. Qed.
Section EqPmap.
Variables (aT rT : eqType) (f : aT -> option rT) (g : rT -> aT).
Lemma mem_pmap s u : (u \in pmap f s) = (Some u \in map f s).
Hypothesis fK : ocancel f g.
Lemma can2_mem_pmap : pcancel g f -> forall s u, (u \in pmap f s) = (g u \in s).
Proof.
Lemma pmap_uniq s : uniq s -> uniq (pmap f s).
Proof.
Lemma perm_pmap s t : perm_eq s t -> perm_eq (pmap f s) (pmap f t).
Proof.
move=> eq_st; apply/(perm_map_inj Some_inj); rewrite !pmapS_filter.
exact/perm_map/perm_filter.
Qed.
exact/perm_map/perm_filter.
Qed.
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.
Proof.
End PmapSub.
Section EqPmapSub.
Variables (T : eqType) (p : pred T) (sT : subEqType p).
Let insT : T -> option sT := insub.
Lemma mem_pmap_sub s u : (u \in pmap insT s) = (val u \in s).
Proof.
Lemma pmap_sub_uniq s : uniq s -> uniq (pmap insT s).
End EqPmapSub.
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.
Proof.
by elim: n m => //= n IHn m; rewrite IHn. Qed.
Lemma iotaD m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
Lemma iotaDl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
Proof.
Lemma nth_iota p m n i : i < n -> nth p (iota m n) i = m + i.
Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n).
Proof.
Lemma iota_uniq m n : uniq (iota m n).
Lemma take_iota k m n : take k (iota m n) = iota m (minn k n).
Proof.
have [lt_k_n|le_n_k] := ltnP.
by elim: k n lt_k_n m => [|k IHk] [|n] //= H m; rewrite IHk.
by apply: take_oversize; rewrite size_iota.
Qed.
by elim: k n lt_k_n m => [|k IHk] [|n] //= H m; rewrite IHk.
by apply: take_oversize; rewrite size_iota.
Qed.
Lemma drop_iota k m n : drop k (iota m n) = iota (m + k) (n - k).
Lemma filter_iota_ltn m n j : j <= n ->
[seq i <- iota m n | i < m + j] = iota m j.
Proof.
Lemma filter_iota_leq n m j : j < n ->
[seq i <- iota m n | i <= m + j] = iota m j.+1.
Proof.
Definition mindex m := nth (size m) (mask m (iota 0 (size m))).
Lemma nth_mask {T} m x0 (s : seq T) : size m >= size s ->
forall i, nth x0 (mask m s) i = nth x0 s (mindex m i).
Proof.
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 mkseqS f n :
mkseq f n.+1 = rcons (mkseq f n) (f n).
Lemma eq_mkseq f g : f =1 g -> mkseq f =1 mkseq g.
Proof.
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.
Proof.
Variant mkseq_spec s : seq T -> Type :=
| MapIota n f : s = mkseq f n -> mkseq_spec s (mkseq f n).
Lemma mkseqP s : mkseq_spec s s.
Proof.
Lemma map_nth_iota0 s i :
i <= size s -> [seq nth x0 s j | j <- iota 0 i] = take i s.
Lemma map_nth_iota s i j : j <= size s - i ->
[seq nth x0 s k | k <- iota i j] = take j (drop i s).
Proof.
Lemma take_mkseq f n i : take i (mkseq f n) = mkseq f (minn i n).
Lemma drop_mkseq f n i :
drop i (mkseq f n) = mkseq (fun k => f (i + k)) (n - i).
End MakeSeq.
Section MakeEqSeq.
Variable T : eqType.
Lemma mkseq_uniqP (f : nat -> T) n :
reflect {in gtn n &, injective f} (uniq (mkseq f n)).
Proof.
apply: (equivP (uniqP (f 0))); rewrite size_mkseq.
by split=> injf i j lti ltj; have:= injf i j lti ltj; rewrite !nth_mkseq.
Qed.
by split=> injf i j lti ltj; have:= injf i j lti ltj; rewrite !nth_mkseq.
Qed.
Lemma mkseq_uniq (f : nat -> T) n : injective f -> uniq (mkseq f n).
Proof.
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).
Proof.
apply: (iffP idP) => [Est | [Is eqIst ->]]; last first.
by rewrite -{2}[t](mkseq_nth x0) perm_map.
elim: t => [|x t IHt] in s It Est *.
by rewrite (perm_small_eq _ Est) //; exists [::].
have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head.
have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot.
exists (rotr k (0 :: map succn Is1)).
by rewrite perm_rot /It /= perm_cons (iotaDl 1) perm_map.
by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK.
Qed.
by rewrite -{2}[t](mkseq_nth x0) perm_map.
elim: t => [|x t IHt] in s It Est *.
by rewrite (perm_small_eq _ Est) //; exists [::].
have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head.
have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot.
exists (rotr k (0 :: map succn Is1)).
by rewrite perm_rot /It /= perm_cons (iotaDl 1) perm_map.
by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK.
Qed.
End MakeEqSeq.
Arguments perm_iotaP {T s t}.
Section FoldRight.
Variables (T : Type) (R : Type) (f : T -> R -> R) (z0 : R).
Fixpoint foldr s := if s is x :: s' then f x (foldr s') else z0.
End FoldRight.
Section FoldRightComp.
Variables (T1 T2 : Type) (h : T1 -> T2).
Variables (R : Type) (f : T2 -> R -> R) (z0 : R).
Lemma foldr_cat s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.
Proof.
by elim: s1 => //= x s1 ->. Qed.
Lemma foldr_rcons s x : foldr f z0 (rcons s x) = foldr f (f x z0) s.
Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s.
Proof.
by elim: s => //= x s ->. Qed.
End FoldRightComp.
Definition sumn := foldr addn 0.
Lemma sumn_ncons x n s : sumn (ncons n x s) = x * n + sumn s.
Lemma sumn_nseq x n : sumn (nseq n x) = x * n.
Proof.
Lemma sumn_cat s1 s2 : sumn (s1 ++ s2) = sumn s1 + sumn s2.
Proof.
Lemma sumn_count T (a : pred T) s : sumn [seq a i : nat | i <- s] = count a s.
Proof.
by elim: s => //= s0 s /= ->. Qed.
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.
Proof.
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).
Proof.
Lemma sumn_set_nth s x0 n x :
sumn (set_nth x0 s n x) =
sumn s + x - (nth x0 s n) * (n < size s) + x0 * (n - size s).
Proof.
rewrite set_nthE; case: ltnP => [nlts|nges]; last first.
by rewrite sumn_cat sumn_ncons /= addn0 muln0 subn0 addnAC addnA.
have -> : n - size s = 0 by apply/eqP; rewrite subn_eq0 ltnW.
rewrite -[in sumn s](cat_take_drop n s) [drop n s](drop_nth x0)//.
by rewrite !sumn_cat /= muln1 muln0 addn0 addnAC !addnA [in RHS]addnAC addnK.
Qed.
by rewrite sumn_cat sumn_ncons /= addn0 muln0 subn0 addnAC addnA.
have -> : n - size s = 0 by apply/eqP; rewrite subn_eq0 ltnW.
rewrite -[in sumn s](cat_take_drop n s) [drop n s](drop_nth x0)//.
by rewrite !sumn_cat /= muln1 muln0 addn0 addnAC !addnA [in RHS]addnAC addnK.
Qed.
Lemma sumn_set_nth_ltn s x0 n x : n < size s ->
sumn (set_nth x0 s n x) = sumn s + x - nth x0 s n.
Proof.
Lemma sumn_set_nth0 s n x : sumn (set_nth 0 s n x) = sumn s + x - nth 0 s n.
Proof.
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.
Lemma foldl_rcons z s x : foldl z (rcons s x) = f (foldl z s) x.
End FoldLeft.
Section Folds.
Variables (T : Type) (f : T -> T -> T).
Hypotheses (fA : associative f) (fC : commutative f).
Lemma foldl_foldr x0 l : foldl f x0 l = foldr f x0 l.
Proof.
End Folds.
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.
Proof.
by elim: s x => //= y s IHs x; rewrite IHs. Qed.
Lemma pairmap_cat x s1 s2 :
pairmap x (s1 ++ s2) = pairmap x s1 ++ pairmap (last x s1) s2.
Proof.
by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed.
Lemma nth_pairmap s n : n < size s ->
forall x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n).
Proof.
by elim: s n => [|y s IHs] [|n] //= Hn x; apply: IHs. Qed.
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.
Proof.
by elim: s x => //= y s IHs x; rewrite IHs. Qed.
Lemma scanl_cat x s1 s2 :
scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2.
Proof.
by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed.
Lemma scanl_rcons x s1 y :
scanl x (rcons s1 y) = rcons (scanl x s1) (foldl g x (rcons s1 y)).
Lemma nth_cons_scanl s n : n <= size s ->
forall x, nth x1 (x :: scanl x s) n = foldl g x (take n s).
Proof.
by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite IHs. Qed.
Lemma nth_scanl s n : n < size s ->
forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s).
Proof.
Lemma scanlK :
(forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x).
Proof.
by move=> Hfg x s; elim: s x => //= y s IHs x; rewrite Hfg IHs. Qed.
Lemma pairmapK :
(forall x, cancel (f x) (g x)) -> forall x, cancel (pairmap x) (scanl x).
Proof.
by move=> Hgf x s; elim: s x => //= y s IHs x; rewrite Hgf IHs. Qed.
End Scan.
Prenex Implicits mask map pmap foldr foldl scanl pairmap.
Section Zip.
Variables (S T : Type) (r : S -> T -> bool).
Fixpoint zip (s : seq S) (t : seq T) {struct t} :=
match s, t with
| x :: s', y :: t' => (x, y) :: zip s' t'
| _, _ => [::]
end.
Definition unzip1 := map (@fst S T).
Definition unzip2 := map (@snd S T).
Fixpoint all2 s t :=
match s, t with
| [::], [::] => true
| x :: s, y :: t => r x y && all2 s t
| _, _ => false
end.
Lemma zip_unzip s : zip (unzip1 s) (unzip2 s) = s.
Proof.
by elim: s => [|[x y] s /= ->]. Qed.
Lemma unzip1_zip s t : size s <= size t -> unzip1 (zip s t) = s.
Proof.
by elim: s t => [|x s IHs] [|y t] //= le_s_t; rewrite IHs. Qed.
Lemma unzip2_zip s t : size t <= size s -> unzip2 (zip s t) = t.
Proof.
by elim: s t => [|x s IHs] [|y t] //= le_t_s; rewrite IHs. Qed.
Lemma size1_zip s t : size s <= size t -> size (zip s t) = size s.
Proof.
by elim: s t => [|x s IHs] [|y t] //= Hs; rewrite IHs. Qed.
Lemma size2_zip s t : size t <= size s -> size (zip s t) = size t.
Proof.
by elim: s t => [|x s IHs] [|y t] //= Hs; rewrite IHs. Qed.
Lemma size_zip s t : size (zip s t) = minn (size s) (size t).
Proof.
Lemma zip_cat s1 s2 t1 t2 :
size s1 = size t1 -> zip (s1 ++ s2) (t1 ++ t2) = zip s1 t1 ++ zip s2 t2.
Proof.
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).
Proof.
by elim: i s t => [|i IHi] [|y1 s1] [|y2 t] //= [/IHi->]. Qed.
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).
Proof.
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).
Proof.
Lemma all2E s t :
all2 s t = (size s == size t) && all [pred xy | r xy.1 xy.2] (zip s t).
Proof.
Lemma zip_map I f g (s : seq I) :
zip (map f s) (map g s) = [seq (f i, g i) | i <- s].
Proof.
by elim: s => //= i s ->. Qed.
Lemma unzip1_map_nth_zip x y s t l :
size s = size t ->
unzip1 [seq nth (x, y) (zip s t) i | i <- l] = [seq nth x s i | i <- l].
Proof.
Lemma unzip2_map_nth_zip x y s t l :
size s = size t ->
unzip2 [seq nth (x, y) (zip s t) i | i <- l] = [seq nth y t i | i <- l].
Proof.
End Zip.
Lemma zip_uniql (S T : eqType) (s : seq S) (t : seq T) :
uniq s -> uniq (zip s t).
Proof.
Lemma zip_uniqr (S T : eqType) (s : seq S) (t : seq T) :
uniq t -> uniq (zip s t).
Proof.
Lemma perm_zip_sym (S T : eqType) (s1 s2 : seq S) (t1 t2 : seq T) :
perm_eq (zip s1 t1) (zip s2 t2) -> perm_eq (zip t1 s1) (zip t2 s2).
Proof.
Lemma perm_zip1 {S T : eqType} (t1 t2 : seq T) (s1 s2 : seq S):
size s1 = size t1 -> size s2 = size t2 ->
perm_eq (zip s1 t1) (zip s2 t2) -> perm_eq s1 s2.
Proof.
wlog [x y] : s1 s2 t1 t2 / (S * T)%type => [hwlog|].
case: s2 t2 => [|x s2] [|y t2] //; last exact: hwlog.
by case: s1 t1 => [|u s1] [|v t1]//= _ _ /perm_nilP.
move=> eq1 eq2 /(perm_iotaP (x, y))[ns nsP /(congr1 (@unzip1 _ _))].
rewrite unzip1_zip ?unzip1_map_nth_zip -?eq1// => ->.
by apply/(perm_iotaP x); exists ns; rewrite // size_zip -eq2 minnn in nsP.
Qed.
case: s2 t2 => [|x s2] [|y t2] //; last exact: hwlog.
by case: s1 t1 => [|u s1] [|v t1]//= _ _ /perm_nilP.
move=> eq1 eq2 /(perm_iotaP (x, y))[ns nsP /(congr1 (@unzip1 _ _))].
rewrite unzip1_zip ?unzip1_map_nth_zip -?eq1// => ->.
by apply/(perm_iotaP x); exists ns; rewrite // size_zip -eq2 minnn in nsP.
Qed.
Lemma perm_zip2 {S T : eqType} (s1 s2 : seq S) (t1 t2 : seq T) :
size s1 = size t1 -> size s2 = size t2 ->
perm_eq (zip s1 t1) (zip s2 t2) -> perm_eq t1 t2.
Proof.
Prenex Implicits zip unzip1 unzip2 all2.
Lemma eqseq_all (T : eqType) (s t : seq T) : (s == t) = all2 eq_op s t.
Proof.
by elim: s t => [|x s +] [|y t]//= => <-. Qed.
Lemma eq_map_all I (T : eqType) (f g : I -> T) (s : seq I) :
(map f s == map g s) = all [pred xy | xy.1 == xy.2] [seq (f i, g i) | i <- s].
Section Flatten.
Variable T : Type.
Implicit Types (s : seq T) (ss : seq (seq T)).
Definition flatten := foldr cat (Nil T).
Definition shape := map (@size T).
Fixpoint reshape sh s :=
if sh is n :: sh' then take n s :: reshape sh' (drop n s) else [::].
Definition flatten_index sh r c := sumn (take r sh) + c.
Definition reshape_index sh i := find (pred1 0) (scanl subn i.+1 sh).
Definition reshape_offset sh i := i - sumn (take (reshape_index sh i) sh).
Lemma size_flatten ss : size (flatten ss) = sumn (shape ss).
Proof.
Lemma flatten_cat ss1 ss2 : flatten (ss1 ++ ss2) = flatten ss1 ++ flatten ss2.
Proof.
Lemma size_reshape sh s : size (reshape sh s) = size sh.
Proof.
by elim: sh s => //= s0 sh IHsh s; rewrite IHsh. Qed.
Lemma nth_reshape (sh : seq nat) l n :
nth [::] (reshape sh l) n = take (nth 0 sh n) (drop (sumn (take n sh)) l).
Proof.
Lemma flattenK ss : reshape (shape ss) (flatten ss) = ss.
Proof.
Lemma reshapeKr sh s : size s <= sumn sh -> flatten (reshape sh s) = s.
Proof.
elim: sh s => [[]|n sh IHsh] //= s sz_s; rewrite IHsh ?cat_take_drop //.
by rewrite size_drop leq_subLR.
Qed.
by rewrite size_drop leq_subLR.
Qed.
Lemma reshapeKl sh s : size s >= sumn sh -> shape (reshape sh s) = sh.
Proof.
Lemma flatten_rcons ss s : flatten (rcons ss s) = flatten ss ++ s.
Proof.
Lemma flatten_seq1 s : flatten [seq [:: x] | x <- s] = s.
Proof.
by elim: s => //= s0 s ->. Qed.
Lemma count_flatten ss P :
count P (flatten ss) = sumn [seq count P x | x <- ss].
Proof.
Lemma filter_flatten ss (P : pred T) :
filter P (flatten ss) = flatten [seq filter P i | i <- ss].
Proof.
Lemma rev_flatten ss :
rev (flatten ss) = flatten (rev (map rev ss)).
Proof.
Lemma nth_shape ss i : nth 0 (shape ss) i = size (nth [::] ss i).
Proof.
Lemma shape_rev ss : shape (rev ss) = rev (shape ss).
Proof.
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)).
Proof.
move=> sz_s; apply/(canLR revK)/eq_from_flatten_shape.
rewrite reshapeKr ?sz_s // -rev_flatten reshapeKr ?revK //.
by rewrite size_rev sumn_rev sz_s.
transitivity (rev (shape (reshape (rev sh) (rev s)))).
by rewrite !reshapeKl ?revK ?size_rev ?sz_s ?sumn_rev.
rewrite shape_rev; congr (rev _); rewrite -[RHS]map_comp.
by under eq_map do rewrite /= size_rev.
Qed.
rewrite reshapeKr ?sz_s // -rev_flatten reshapeKr ?revK //.
by rewrite size_rev sumn_rev sz_s.
transitivity (rev (shape (reshape (rev sh) (rev s)))).
by rewrite !reshapeKl ?revK ?size_rev ?sz_s ?sumn_rev.
rewrite shape_rev; congr (rev _); rewrite -[RHS]map_comp.
by under eq_map do rewrite /= size_rev.
Qed.
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).
Proof.
move=> Dmn; apply/(can_inj revK); rewrite rev_reshape ?rev_rcons ?sumn_rcons //.
rewrite /= take_rev drop_rev -Dmn addnK revK -rev_reshape //.
by rewrite size_takel // -Dmn leq_addr.
Qed.
rewrite /= take_rev drop_rev -Dmn addnK revK -rev_reshape //.
by rewrite size_takel // -Dmn leq_addr.
Qed.
Lemma flatten_indexP sh r c :
c < nth 0 sh r -> flatten_index sh r c < sumn sh.
Proof.
move=> lt_c_sh; rewrite -[sh in sumn sh](cat_take_drop r) sumn_cat ltn_add2l.
suffices lt_r_sh: r < size sh by rewrite (drop_nth 0 lt_r_sh) ltn_addr.
by case: ltnP => // le_sh_r; rewrite nth_default in lt_c_sh.
Qed.
suffices lt_r_sh: r < size sh by rewrite (drop_nth 0 lt_r_sh) ltn_addr.
by case: ltnP => // le_sh_r; rewrite nth_default in lt_c_sh.
Qed.
Lemma reshape_indexP sh i : i < sumn sh -> reshape_index sh i < size sh.
Proof.
rewrite /reshape_index; elim: sh => //= n sh IHsh in i *; rewrite subn_eq0.
by have [// | le_n_i] := ltnP i n; rewrite -leq_subLR subSn // => /IHsh.
Qed.
by have [// | le_n_i] := ltnP i n; rewrite -leq_subLR subSn // => /IHsh.
Qed.
Lemma reshape_offsetP sh i :
i < sumn sh -> reshape_offset sh i < nth 0 sh (reshape_index sh i).
Proof.
rewrite /reshape_offset /reshape_index; elim: sh => //= n sh IHsh in i *.
rewrite subn_eq0; have [| le_n_i] := ltnP i n; first by rewrite subn0.
by rewrite -leq_subLR /= subnDA subSn // => /IHsh.
Qed.
rewrite subn_eq0; have [| le_n_i] := ltnP i n; first by rewrite subn0.
by rewrite -leq_subLR /= subnDA subSn // => /IHsh.
Qed.
Lemma reshape_indexK sh i :
flatten_index sh (reshape_index sh i) (reshape_offset sh i) = i.
Proof.
rewrite /reshape_offset /reshape_index /flatten_index -subSKn.
elim: sh => //= n sh IHsh in i *; rewrite subn_eq0; have [//|le_n_i] := ltnP.
by rewrite /= subnDA subSn // -addnA IHsh subnKC.
Qed.
elim: sh => //= n sh IHsh in i *; rewrite subn_eq0; have [//|le_n_i] := ltnP.
by rewrite /= subnDA subSn // -addnA IHsh subnKC.
Qed.
Lemma flatten_indexKl sh r c :
c < nth 0 sh r -> reshape_index sh (flatten_index sh r c) = r.
Proof.
rewrite /reshape_index /flatten_index.
elim: sh r => [|n sh IHsh] [|r] //= lt_c_sh; first by rewrite ifT.
by rewrite -addnA -addnS addKn IHsh.
Qed.
elim: sh r => [|n sh IHsh] [|r] //= lt_c_sh; first by rewrite ifT.
by rewrite -addnA -addnS addKn IHsh.
Qed.
Lemma flatten_indexKr sh r c :
c < nth 0 sh r -> reshape_offset sh (flatten_index sh r c) = c.
Proof.
rewrite /reshape_offset /reshape_index /flatten_index.
elim: sh r => [|n sh IHsh] [|r] //= lt_c_sh; first by rewrite ifT ?subn0.
by rewrite -addnA -addnS addKn /= subnDl IHsh.
Qed.
elim: sh r => [|n sh IHsh] [|r] //= lt_c_sh; first by rewrite ifT ?subn0.
by rewrite -addnA -addnS addKn /= subnDl IHsh.
Qed.
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).
Proof.
rewrite /reshape_offset -subSKn {}/r /reshape_index.
elim: ss => //= s ss IHss in i *; rewrite subn_eq0 nth_cat.
by have [//|le_s_i] := ltnP; rewrite subnDA subSn /=.
Qed.
elim: ss => //= s ss IHss in i *; rewrite subn_eq0 nth_cat.
by have [//|le_s_i] := ltnP; rewrite subnDA subSn /=.
Qed.
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))).
Proof.
rewrite {}/r1 {}/c1 {}/r2 {}/c2 /reshape_offset /reshape_index.
elim: sh => [|s0 s IHs] /= in i1 i2 *; rewrite ?subn0 ?subn_eq0 //.
have [[] i1s0 [] i2s0] := (ltnP i1 s0, ltnP i2 s0); first by rewrite !subn0.
- by apply: leq_trans i2s0; apply/ltnW.
- by apply/negP => /(leq_trans i1s0); rewrite leqNgt i2s0.
by rewrite !subSn // !eqSS !ltnS !subnDA -IHs leq_subLR subnKC.
Qed.
elim: sh => [|s0 s IHs] /= in i1 i2 *; rewrite ?subn0 ?subn_eq0 //.
have [[] i1s0 [] i2s0] := (ltnP i1 s0, ltnP i2 s0); first by rewrite !subn0.
- by apply: leq_trans i2s0; apply/ltnW.
- by apply/negP => /(leq_trans i1s0); rewrite leqNgt i2s0.
by rewrite !subSn // !eqSS !ltnS !subnDA -IHs leq_subLR subnKC.
Qed.
End Flatten.
Prenex Implicits flatten shape reshape.
Lemma map_flatten S T (f : T -> S) ss :
map f (flatten ss) = flatten (map (map f) ss).
Proof.
Lemma flatten_map1 (S T : Type) (f : S -> T) s :
flatten [seq [:: f x] | x <- s] = map f s.
Proof.
by elim: s => //= s0 s ->. Qed.
Lemma undup_flatten_nseq n (T : eqType) (s : seq T) : 0 < n ->
undup (flatten (nseq n s)) = undup s.
Proof.
elim: n => [|[|n]/= IHn]//= _; rewrite ?cats0// undup_cat {}IHn//.
rewrite (@eq_in_filter _ _ pred0) ?filter_pred0// => x.
by rewrite mem_undup mem_cat => ->.
Qed.
rewrite (@eq_in_filter _ _ pred0) ?filter_pred0// => x.
by rewrite mem_undup mem_cat => ->.
Qed.
Lemma sumn_flatten (ss : seq (seq nat)) :
sumn (flatten ss) = sumn (map sumn ss).
Proof.
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).
Proof.
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)).
Proof.
Lemma perm_flatten (ss1 ss2 : seq (seq T)) :
perm_eq ss1 ss2 -> perm_eq (flatten ss1) (flatten ss2).
Proof.
move=> eq_ss; apply/permP=> a; apply/catCA_perm_subst: ss1 ss2 eq_ss.
by move=> ss1 ss2 ss3; rewrite !flatten_cat !count_cat addnCA.
Qed.
by move=> ss1 ss2 ss3; rewrite !flatten_cat !count_cat addnCA.
Qed.
End EqFlatten.
Arguments flattenP {T A x}.
Arguments flatten_mapP {S T A s y}.
Notation "[ 'seq' E | x <- s , y <- t ]" :=
(flatten [seq [seq E | y <- t] | x <- s])
(x binder, y binder,
format "[ '[hv' 'seq' E '/ ' | x <- s , '/ ' y <- t ] ']'")
: seq_scope.
Notation "[ 'seq' E : R | x <- s , y <- t ]" :=
(flatten [seq [seq E : R | y <- t] | x <- s])
(x binder, y binder, only parsing) : seq_scope.
Section PrefixSuffixInfix.
Variables T : eqType.
Implicit Type s : seq T.
Fixpoint prefix s1 s2 {struct s2} :=
if s1 isn't x :: s1' then true else
if s2 isn't y :: s2' then false else
(x == y) && prefix s1' s2'.
Lemma prefixE s1 s2 : prefix s1 s2 = (take (size s1) s2 == s1).
Proof.
Lemma prefix_refl s : prefix s s
Lemma prefixs0 s : prefix s [::] = (s == [::])
Proof.
by case: s. Qed.
Lemma prefix0s s : prefix [::] s
Proof.
by case: s. Qed.
Lemma prefix_cons s1 s2 x y :
prefix (x :: s1) (y :: s2) = (x == y) && prefix s1 s2.
Proof.
by []. Qed.
Lemma prefix_catr s1 s2 s1' s3 : size s1 = size s1' ->
prefix (s1 ++ s2) (s1' ++ s3) = (s1 == s1') && prefix s2 s3.
Proof.
Lemma prefix_prefix s1 s2 : prefix s1 (s1 ++ s2).
Hint Resolve prefix_prefix : core.
Lemma prefixP {s1 s2} :
reflect (exists s2' : seq T, s2 = s1 ++ s2') (prefix s1 s2).
Proof.
apply: (iffP idP) => [|[{}s2 ->]]; last exact: prefix_prefix.
by rewrite prefixE => /eqP<-; exists (drop (size s1) s2); rewrite cat_take_drop.
Qed.
by rewrite prefixE => /eqP<-; exists (drop (size s1) s2); rewrite cat_take_drop.
Qed.
Lemma prefix_trans : transitive prefix.
Lemma prefixs1 s x : prefix s [:: x] = (s == [::]) || (s == [:: x]).
Proof.
Lemma catl_prefix s1 s2 s3 : prefix (s1 ++ s3) s2 -> prefix s1 s2.
Lemma prefix_catl s1 s2 s3 : prefix s1 s2 -> prefix s1 (s2 ++ s3).
Lemma prefix_rcons s x : prefix s (rcons s x).
Proof.
Definition suffix s1 s2 := prefix (rev s1) (rev s2).
Lemma suffixE s1 s2 : suffix s1 s2 = (drop (size s2 - size s1) s2 == s1).
Lemma suffix_refl s : suffix s s.
Proof.
Lemma suffixs0 s : suffix s [::] = (s == [::]).
Lemma suffix0s s : suffix [::] s.
Proof.
Lemma prefix_rev s1 s2 : prefix (rev s1) (rev s2) = suffix s1 s2.
Proof.
by []. Qed.
Lemma prefix_revLR s1 s2 : prefix (rev s1) s2 = suffix s1 (rev s2).
Proof.
Lemma suffix_rev s1 s2 : suffix (rev s1) (rev s2) = prefix s1 s2.
Proof.
Lemma suffix_revLR s1 s2 : suffix (rev s1) s2 = prefix s1 (rev s2).
Proof.
Lemma suffix_suffix s1 s2 : suffix s2 (s1 ++ s2).
Proof.
Lemma suffixP {s1 s2} :
reflect (exists s2' : seq T, s2 = s2' ++ s1) (suffix s1 s2).
Proof.
Lemma suffix_trans : transitive suffix.
Lemma suffix_rcons s1 s2 x y :
suffix (rcons s1 x) (rcons s2 y) = (x == y) && suffix s1 s2.
Proof.
Lemma suffix_catl s1 s2 s3 s3' : size s3 = size s3' ->
suffix (s1 ++ s3) (s2 ++ s3') = (s3 == s3') && suffix s1 s2.
Lemma suffix_catr s1 s2 s3 : suffix s1 s2 -> suffix s1 (s3 ++ s2).
Proof.
Lemma catl_suffix s s1 s2 : suffix (s ++ s1) s2 -> suffix s1 s2.
Proof.
Lemma suffix_cons s x : suffix s (x :: s).
Proof.
Fixpoint infix s1 s2 :=
if s2 is y :: s2' then prefix s1 s2 || infix s1 s2' else s1 == [::].
Fixpoint infix_index s1 s2 :=
if prefix s1 s2 then 0
else if s2 is y :: s2' then (infix_index s1 s2').+1 else 1.
Lemma infix0s s : infix [::] s
Proof.
by case: s. Qed.
Lemma infixs0 s : infix s [::] = (s == [::])
Proof.
by case: s. Qed.
Lemma infix_consl s1 y s2 :
infix s1 (y :: s2) = prefix s1 (y :: s2) || infix s1 s2.
Proof.
by []. Qed.
Lemma infix_indexss s : infix_index s s = 0.
Proof.
Lemma infix_index_le s1 s2 : infix_index s1 s2 <= (size s2).+1.
Proof.
Lemma infixTindex s1 s2 : (infix_index s1 s2 <= size s2) = infix s1 s2.
Proof.
Lemma infixPn s1 s2 :
reflect (infix_index s1 s2 = (size s2).+1) (~~ infix s1 s2).
Proof.
rewrite -infixTindex -ltnNge; apply: (iffP idP) => [s2lt|->//].
by apply/eqP; rewrite eqn_leq s2lt infix_index_le.
Qed.
by apply/eqP; rewrite eqn_leq s2lt infix_index_le.
Qed.
Lemma infix_index0s s : infix_index [::] s = 0.
Proof.
by case: s. Qed.
Lemma infix_indexs0 s : infix_index s [::] = (s != [::]).
Proof.
by case: s. Qed.
Lemma infixE s1 s2 : infix s1 s2 =
(take (size s1) (drop (infix_index s1 s2) s2) == s1).
Proof.
Lemma infix_refl s : infix s s.
Proof.
Lemma prefixW s1 s2 : prefix s1 s2 -> infix s1 s2.
Proof.
by elim: s2 s1 => [|y s2 IHs2] [|x s1]//=->. Qed.
Lemma prefix_infix s1 s2 : infix s1 (s1 ++ s2).
Proof.
Lemma infix_infix s1 s2 s3 : infix s2 (s1 ++ s2 ++ s3).
Proof.
Lemma suffix_infix s1 s2 : infix s2 (s1 ++ s2).
Hint Resolve suffix_infix : core.
Lemma infixP {s1 s2} :
reflect (exists s s' : seq T, s2 = s ++ s1 ++ s') (infix s1 s2).
Proof.
Lemma infix_rev s1 s2 : infix (rev s1) (rev s2) = infix s1 s2.
Proof.
Lemma suffixW s1 s2 : suffix s1 s2 -> infix s1 s2.
Lemma infix_trans : transitive infix.
Proof.
Lemma infix_revLR s1 s2 : infix (rev s1) s2 = infix s1 (rev s2).
Lemma infix_rconsl s1 s2 y :
infix s1 (rcons s2 y) = suffix s1 (rcons s2 y) || infix s1 s2.
Proof.
Lemma infix_cons s x : infix s (x :: s).
Proof.
Lemma infixs1 s x : infix s [:: x] = (s == [::]) || (s == [:: x]).
Proof.
Lemma catl_infix s s1 s2 : infix (s ++ s1) s2 -> infix s1 s2.
Proof.
Lemma catr_infix s s1 s2 : infix (s1 ++ s) s2 -> infix s1 s2.
Proof.
Lemma cons2_infix s1 s2 x : infix (x :: s1) (x :: s2) -> infix s1 s2.
Proof.
Lemma rcons2_infix s1 s2 x : infix (rcons s1 x) (rcons s2 x) -> infix s1 s2.
Proof.
Lemma catr2_infix s s1 s2 : infix (s ++ s1) (s ++ s2) -> infix s1 s2.
Proof.
Lemma catl2_infix s s1 s2 : infix (s1 ++ s) (s2 ++ s) -> infix s1 s2.
Proof.
Lemma infix_catl s1 s2 s3 : infix s1 s2 -> infix s1 (s3 ++ s2).
Proof.
Lemma infix_catr s1 s2 s3 : infix s1 s2 -> infix s1 (s2 ++ s3).
Proof.
case: s3 => [|x s /infixP [p [sf]] ->]; first by rewrite cats0.
by rewrite -catA; apply: infix_catl; rewrite -catA prefix_infix.
Qed.
by rewrite -catA; apply: infix_catl; rewrite -catA prefix_infix.
Qed.
Lemma prefix_infix_trans s2 s1 s3 :
prefix s1 s2 -> infix s2 s3 -> infix s1 s3.
Proof.
Lemma suffix_infix_trans s2 s1 s3 :
suffix s1 s2 -> infix s2 s3 -> infix s1 s3.
Proof.
Lemma infix_prefix_trans s2 s1 s3 :
infix s1 s2 -> prefix s2 s3 -> infix s1 s3.
Proof.
Lemma infix_suffix_trans s2 s1 s3 :
infix s1 s2 -> suffix s2 s3 -> infix s1 s3.
Proof.
Lemma prefix_suffix_trans s2 s1 s3 :
prefix s1 s2 -> suffix s2 s3 -> infix s1 s3.
Proof.
Lemma suffix_prefix_trans s2 s1 s3 :
suffix s1 s2 -> prefix s2 s3 -> infix s1 s3.
Proof.
Lemma infixW s1 s2 : infix s1 s2 -> subseq s1 s2.
Proof.
Lemma mem_infix s1 s2 : infix s1 s2 -> {subset s1 <= s2}.
Proof.
Lemma infix1s s x : infix [:: x] s = (x \in s).
Lemma prefix1s s x : prefix [:: x] s -> x \in s.
Lemma suffix1s s x : suffix [:: x] s -> x \in s.
Lemma infix_rcons s x : infix s (rcons s x).
Proof.
Lemma infix_uniq s1 s2 : infix s1 s2 -> uniq s2 -> uniq s1.
Proof.
Lemma prefix_uniq s1 s2 : prefix s1 s2 -> uniq s2 -> uniq s1.
Proof.
Lemma suffix_uniq s1 s2 : suffix s1 s2 -> uniq s2 -> uniq s1.
Proof.
Lemma prefix_take s i : prefix (take i s) s.
Proof.
Lemma suffix_drop s i : suffix (drop i s) s.
Proof.
Lemma infix_take s i : infix (take i s) s.
Proof.
Lemma prefix_drop_gt0 s i : ~~ prefix (drop i s) s -> i > 0.
Proof.
Lemma infix_drop s i : infix (drop i s) s.
Proof.
Lemma consr_infix s1 s2 x : infix (x :: s1) s2 -> infix [:: x] s2.
Proof.
Lemma consl_infix s1 s2 x : infix (x :: s1) s2 -> infix s1 s2.
Proof.
Lemma prefix_index s1 s2 : prefix s1 s2 -> infix_index s1 s2 = 0.
Proof.
by case: s1 s2 => [|x s1] [|y s2] //= ->. Qed.
Lemma size_infix s1 s2 : infix s1 s2 -> size s1 <= size s2.
Proof.
Lemma size_prefix s1 s2 : prefix s1 s2 -> size s1 <= size s2.
Proof.
Lemma size_suffix s1 s2 : suffix s1 s2 -> size s1 <= size s2.
Proof.
End PrefixSuffixInfix.
Section AllPairsDep.
Variables (S S' : Type) (T T' : S -> Type) (R : Type).
Implicit Type f : forall x, T x -> R.
Definition allpairs_dep f s t := [seq f x y | x <- s, y <- t x].
Lemma size_allpairs_dep f s t :
size [seq f x y | x <- s, y <- t x] = sumn [seq size (t x) | x <- s].
Lemma allpairs0l f t : [seq f x y | x <- [::], y <- t x] = [::].
Proof.
by []. Qed.
Lemma allpairs0r f s : [seq f x y | x <- s, y <- [::]] = [::].
Proof.
by elim: s. Qed.
Lemma allpairs1l f x t :
[seq f x y | x <- [:: x], y <- t x] = [seq f x y | y <- t x].
Proof.
Lemma allpairs1r f s y :
[seq f x y | x <- s, y <- [:: y x]] = [seq f x (y x) | x <- s].
Proof.
Lemma allpairs_cons f x s t :
[seq f x y | x <- x :: s, y <- t x] =
[seq f x y | y <- t x] ++ [seq f x y | x <- s, y <- t x].
Proof.
by []. Qed.
Lemma eq_allpairs (f1 f2 : forall x, T x -> R) s t :
(forall x, f1 x =1 f2 x) ->
[seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].
Lemma eq_allpairsr (f : forall x, T x -> R) s t1 t2 : (forall x, t1 x = t2 x) ->
[seq f x y | x <- s, y <- t1 x] = [seq f x y | x <- s, y <- t2 x].
Proof.
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].
Proof.
Lemma allpairs_rcons f x s t :
[seq f x y | x <- rcons s x, y <- t x] =
[seq f x y | x <- s, y <- t x] ++ [seq f x y | y <- t x].
Proof.
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)].
Proof.
Lemma allpairs_mapr f (g : forall x, T' x -> T x) s t :
[seq f x y | x <- s, y <- map (g x) (t x)] =
[seq f x (g x y) | x <- s, y <- t x].
End AllPairsDep.
Arguments allpairs_dep {S T R} f s t /.
Lemma map_allpairs S T R R' (g : R' -> R) f s t :
map g [seq f x y | x : S <- s, y : T x <- t x] =
[seq g (f x y) | x <- s, y <- t x].
Proof.
Section AllPairsNonDep.
Variables (S T R : Type) (f : S -> T -> R).
Implicit Types (s : seq S) (t : seq T).
Definition allpairs s t := [seq f x y | x <- s, y <- t].
Lemma size_allpairs s t : size [seq f x y | x <- s, y <- t] = size s * size t.
End AllPairsNonDep.
Arguments allpairs {S T R} f s t /.
Section EqAllPairsDep.
Variables (S : eqType) (T : S -> eqType).
Implicit Types (R : eqType) (s : seq S) (t : forall x, seq (T x)).
Lemma allpairsPdep R (f : forall x, T x -> R) s t (z : R) :
reflect (exists x y, [/\ x \in s, y \in t x & z = f x y])
(z \in [seq f x y | x <- s, y <- t x]).
Proof.
apply: (iffP flatten_mapP); first by case=> x sx /mapP[y ty ->]; exists x, y.
by case=> x [y [sx ty ->]]; exists x; last apply: map_f.
Qed.
by case=> x [y [sx ty ->]]; exists x; last apply: map_f.
Qed.
Variable R : eqType.
Implicit Type f : forall 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].
Proof.
Lemma eq_in_allpairs_dep f1 f2 s t :
{in s, forall 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].
Proof.
Lemma perm_allpairs_dep f s1 t1 s2 t2 :
perm_eq s1 s2 -> {in s1, forall x, perm_eq (t1 x) (t2 x)} ->
perm_eq [seq f x y | x <- s1, y <- t1 x] [seq f x y | x <- s2, y <- t2 x].
Proof.
elim: s1 s2 t1 t2 => [s2 t1 t2 |a s1 IH s2 t1 t2 perm_s2 perm_t1].
by rewrite perm_sym => /perm_nilP->.
have mem_a : a \in s2 by rewrite -(perm_mem perm_s2) inE eqxx.
rewrite -[s2](cat_take_drop (index a s2)).
rewrite allpairs_cat (drop_nth a) ?index_mem //= nth_index //=.
rewrite perm_sym perm_catC -catA perm_cat //; last first.
rewrite perm_catC -allpairs_cat.
rewrite -remE perm_sym IH // => [|x xI]; last first.
by apply: perm_t1; rewrite inE xI orbT.
by rewrite -(perm_cons a) (perm_trans perm_s2 (perm_to_rem _)).
have /perm_t1 : a \in a :: s1 by rewrite inE eqxx.
rewrite perm_sym; elim: (t2 a) (t1 a) => /= [s4|b s3 IH1 s4 perm_s4].
by rewrite perm_sym => /perm_nilP->.
have mem_b : b \in s4 by rewrite -(perm_mem perm_s4) inE eqxx.
rewrite -[s4](cat_take_drop (index b s4)).
rewrite map_cat /= (drop_nth b) ?index_mem //= nth_index //=.
rewrite perm_sym perm_catC /= perm_cons // perm_catC -map_cat.
rewrite -remE perm_sym IH1 // -(perm_cons b).
by apply: perm_trans perm_s4 (perm_to_rem _).
Qed.
by rewrite perm_sym => /perm_nilP->.
have mem_a : a \in s2 by rewrite -(perm_mem perm_s2) inE eqxx.
rewrite -[s2](cat_take_drop (index a s2)).
rewrite allpairs_cat (drop_nth a) ?index_mem //= nth_index //=.
rewrite perm_sym perm_catC -catA perm_cat //; last first.
rewrite perm_catC -allpairs_cat.
rewrite -remE perm_sym IH // => [|x xI]; last first.
by apply: perm_t1; rewrite inE xI orbT.
by rewrite -(perm_cons a) (perm_trans perm_s2 (perm_to_rem _)).
have /perm_t1 : a \in a :: s1 by rewrite inE eqxx.
rewrite perm_sym; elim: (t2 a) (t1 a) => /= [s4|b s3 IH1 s4 perm_s4].
by rewrite perm_sym => /perm_nilP->.
have mem_b : b \in s4 by rewrite -(perm_mem perm_s4) inE eqxx.
rewrite -[s4](cat_take_drop (index b s4)).
rewrite map_cat /= (drop_nth b) ?index_mem //= nth_index //=.
rewrite perm_sym perm_catC /= perm_cons // perm_catC -map_cat.
rewrite -remE perm_sym IH1 // -(perm_cons b).
by apply: perm_trans perm_s4 (perm_to_rem _).
Qed.
Lemma mem_allpairs_dep f s1 t1 s2 t2 :
s1 =i s2 -> {in s1, forall 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].
Proof.
move=> eq_s eq_t z; apply/allpairsPdep/allpairsPdep=> -[x [y [sx ty ->]]];
by exists x, y; rewrite -eq_s in sx *; rewrite eq_t in ty *.
Qed.
by exists x, y; rewrite -eq_s in sx *; rewrite eq_t in ty *.
Qed.
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, forall x, uniq (t x)} -> {in st &, injective g} ->
uniq [seq f x y | x <- s, y <- t x].
Proof.
move=> g Us Ut; rewrite -(map_allpairs g (existT T)) => /map_inj_in_uniq->{f g}.
elim: s Us => //= x s IHs /andP[s'x Us] in st Ut *; rewrite {st}cat_uniq.
rewrite {}IHs {Us}// ?andbT => [x1 s_s1|]; first exact/Ut/mem_behead.
have injT: injective (existT T x) by move=> y z /eqP; rewrite eq_Tagged => /eqP.
rewrite (map_inj_in_uniq (in2W injT)) {injT}Ut ?mem_head // has_sym has_map.
by apply: contra s'x => /hasP[y _ /allpairsPdep[z [_ [? _ /(congr1 tag)/=->]]]].
Qed.
elim: s Us => //= x s IHs /andP[s'x Us] in st Ut *; rewrite {st}cat_uniq.
rewrite {}IHs {Us}// ?andbT => [x1 s_s1|]; first exact/Ut/mem_behead.
have injT: injective (existT T x) by move=> y z /eqP; rewrite eq_Tagged => /eqP.
rewrite (map_inj_in_uniq (in2W injT)) {injT}Ut ?mem_head // has_sym has_map.
by apply: contra s'x => /hasP[y _ /allpairsPdep[z [_ [? _ /(congr1 tag)/=->]]]].
Qed.
End EqAllPairsDep.
Arguments allpairsPdep {S T R f s t z}.
Section MemAllPairs.
Variables (S : Type) (T : S -> Type) (R : eqType).
Implicit Types (f : forall x, T x -> R) (s : seq S).
Lemma perm_allpairs_catr f s t1 t2 :
perm_eql [seq f x y | x <- s, y <- t1 x ++ t2 x]
([seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x]).
Proof.
apply/permPl; rewrite perm_sym; elim: s => //= x s ihs.
by rewrite perm_catACA perm_cat ?map_cat.
Qed.
by rewrite perm_catACA perm_cat ?map_cat.
Qed.
Lemma mem_allpairs_catr f s y0 t :
[seq f x y | x <- s, y <- y0 x ++ t x] =i
[seq f x y | x <- s, y <- y0 x] ++ [seq f x y | x <- s, y <- t x].
Proof.
Lemma perm_allpairs_consr f s y0 t :
perm_eql [seq f x y | x <- s, y <- y0 x :: t x]
([seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x]).
Proof.
Lemma mem_allpairs_consr f s t y0 :
[seq f x y | x <- s, y <- y0 x :: t x] =i
[seq f x (y0 x) | x <- s] ++ [seq f x y | x <- s, y <- t x].
Proof.
Lemma allpairs_rconsr f s y0 t :
perm_eql [seq f x y | x <- s, y <- rcons (t x) (y0 x)]
([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]).
Proof.
apply/permPl; rewrite -(eq_allpairsr _ _ (fun=> cats1 _ _)).
by rewrite perm_allpairs_catr allpairs1r.
Qed.
by rewrite perm_allpairs_catr allpairs1r.
Qed.
Lemma mem_allpairs_rconsr f s t y0 :
[seq f x y | x <- s, y <- rcons (t x) (y0 x)] =i
([seq f x y | x <- s, y <- t x] ++ [seq f x (y0 x) | x <- s]).
Proof.
End MemAllPairs.
Lemma all_allpairsP
(S : eqType) (T : S -> eqType) (R : Type)
(p : pred R) (f : forall x : S, T x -> R)
(s : seq S) (t : forall x : S, seq (T x)) :
reflect (forall (x : S) (y : T x), x \in s -> y \in t x -> p (f x y))
(all p [seq f x y | x <- s, y <- t x]).
Proof.
elim: s => [|x s IHs]; first by constructor.
rewrite /= all_cat all_map /preim.
apply/(iffP andP)=> [[/allP /= ? ? x' y x'_in_xs]|p_xs_t].
by move: x'_in_xs y => /[1!inE] /predU1P [-> //|? ?]; exact: IHs.
split; first by apply/allP => ?; exact/p_xs_t/mem_head.
by apply/IHs => x' y x'_in_s; apply: p_xs_t; rewrite inE x'_in_s orbT.
Qed.
rewrite /= all_cat all_map /preim.
apply/(iffP andP)=> [[/allP /= ? ? x' y x'_in_xs]|p_xs_t].
by move: x'_in_xs y => /[1!inE] /predU1P [-> //|? ?]; exact: IHs.
split; first by apply/allP => ?; exact/p_xs_t/mem_head.
by apply/IHs => x' y x'_in_s; apply: p_xs_t; rewrite inE x'_in_s orbT.
Qed.
Arguments all_allpairsP {S T R p f s t}.
Section EqAllPairs.
Variables S T R : eqType.
Implicit Types (f : S -> T -> R) (s : seq S) (t : seq T).
Lemma allpairsP f s t (z : R) :
reflect (exists 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]).
Proof.
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].
Proof.
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].
Proof.
split=> [eq_f | /eq_in_allpairs_dep-eq_f x y /eq_f/(_ y)//].
by apply/eq_in_allpairs_dep=> x /eq_f.
Qed.
by apply/eq_in_allpairs_dep=> x /eq_f.
Qed.
Lemma perm_allpairs f s1 t1 s2 t2 :
perm_eq s1 s2 -> perm_eq t1 t2 ->
perm_eq [seq f x y | x <- s1, y <- t1] [seq f x y | x <- s2, y <- t2].
Proof.
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].
Proof.
Lemma allpairs_uniq f s t (st := [seq (x, y) | x <- s, y <- t]) :
uniq s -> uniq t -> {in st &, injective (uncurry f)} ->
uniq [seq f x y | x <- s, y <- t].
Proof.
move=> Us Ut inj_f; rewrite -(map_allpairs (uncurry f) (@pair S T)) -/st.
rewrite map_inj_in_uniq // allpairs_uniq_dep {Us Ut st inj_f}//.
by apply: in2W => -[x1 y1] [x2 y2] /= [-> ->].
Qed.
rewrite map_inj_in_uniq // allpairs_uniq_dep {Us Ut st inj_f}//.
by apply: in2W => -[x1 y1] [x2 y2] /= [-> ->].
Qed.
End EqAllPairs.
Arguments allpairsP {S T R f s t z}.
Arguments perm_nilP {T s}.
Arguments perm_consP {T x s t}.
Section AllRel.
Variables (T S : Type) (r : T -> S -> bool).
Implicit Types (x : T) (y : S) (xs : seq T) (ys : seq S).
Definition allrel xs ys := all [pred x | all (r x) ys] xs.
Lemma allrel0l ys : allrel [::] ys
Proof.
by []. Qed.
Lemma allrel0r xs : allrel xs [::]
Proof.
by elim: xs. Qed.
Lemma allrel_consl x xs ys : allrel (x :: xs) ys = all (r x) ys && allrel xs ys.
Proof.
by []. Qed.
Lemma allrel_consr xs y ys :
allrel xs (y :: ys) = all (r^~ y) xs && allrel xs ys.
Proof.
Lemma allrel_cons2 x y xs ys :
allrel (x :: xs) (y :: ys) =
[&& r x y, all (r x) ys, all (r^~ y) xs & allrel xs ys].
Proof.
Lemma allrel1l x ys : allrel [:: x] ys = all (r x) ys
Proof.
Lemma allrel1r xs y : allrel xs [:: y] = all (r^~ y) xs.
Proof.
Lemma allrel_catl xs xs' ys :
allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys.
Proof.
Lemma allrel_catr xs ys ys' :
allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'.
Proof.
Lemma allrel_maskl m xs ys : allrel xs ys -> allrel (mask m xs) ys.
Proof.
Lemma allrel_maskr m xs ys : allrel xs ys -> allrel xs (mask m ys).
Lemma allrel_filterl a xs ys : allrel xs ys -> allrel (filter a xs) ys.
Proof.
Lemma allrel_filterr a xs ys : allrel xs ys -> allrel xs (filter a ys).
Proof.
Lemma allrel_allpairsE xs ys :
allrel xs ys = all id [seq r x y | x <- xs, y <- ys].
End AllRel.
Arguments allrel {T S} r xs ys : simpl never.
Arguments allrel0l {T S} r ys.
Arguments allrel0r {T S} r xs.
Arguments allrel_consl {T S} r x xs ys.
Arguments allrel_consr {T S} r xs y ys.
Arguments allrel1l {T S} r x ys.
Arguments allrel1r {T S} r xs y.
Arguments allrel_catl {T S} r xs xs' ys.
Arguments allrel_catr {T S} r xs ys ys'.
Arguments allrel_maskl {T S} r m xs ys.
Arguments allrel_maskr {T S} r m xs ys.
Arguments allrel_filterl {T S} r a xs ys.
Arguments allrel_filterr {T S} r a xs ys.
Arguments allrel_allpairsE {T S} r xs ys.
Notation all2rel r xs := (allrel r xs xs).
Lemma sub_in_allrel
{T S : Type} (P : {pred T}) (Q : {pred S}) (r r' : T -> S -> bool) :
{in P & Q, forall x y, r x y -> r' x y} ->
forall xs ys, all P xs -> all Q ys -> allrel r xs ys -> allrel r' xs ys.
Proof.
Lemma sub_allrel {T S : Type} (r r' : T -> S -> bool) :
(forall x y, r x y -> r' x y) ->
forall xs ys, allrel r xs ys -> allrel r' xs ys.
Proof.
Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' :
{in P & Q, r =2 r'} ->
forall xs ys, all P xs -> all Q ys -> allrel r xs ys = allrel r' xs ys.
Proof.
move=> rr' xs ys Pxs Qys.
by apply/idP/idP; apply/sub_in_allrel/Qys/Pxs => ? ? ? ?; rewrite rr'.
Qed.
by apply/idP/idP; apply/sub_in_allrel/Qys/Pxs => ? ? ? ?; rewrite rr'.
Qed.
Lemma eq_allrel {T S : Type} (r r' : T -> S -> bool) :
r =2 r' -> allrel r =2 allrel r'.
Proof.
Lemma allrelC {T S : Type} (r : T -> S -> bool) xs ys :
allrel r xs ys = allrel (fun y => r^~ y) ys xs.
Proof.
Lemma allrel_mapl {T T' S : Type} (f : T' -> T) (r : T -> S -> bool) xs ys :
allrel r (map f xs) ys = allrel (fun x => r (f x)) xs ys.
Proof.
Lemma allrel_mapr {T S S' : Type} (f : S' -> S) (r : T -> S -> bool) xs ys :
allrel r xs (map f ys) = allrel (fun x y => r x (f y)) xs ys.
Proof.
Lemma allrelP {T S : eqType} {r : T -> S -> bool} {xs ys} :
reflect {in xs & ys, forall x y, r x y} (allrel r xs ys).
Proof.
Lemma allrelT {T S : Type} (xs : seq T) (ys : seq S) :
allrel (fun _ _ => true) xs ys = true.
Proof.
Lemma allrel_relI {T S : Type} (r r' : T -> S -> bool) xs ys :
allrel (fun x y => r x y && r' x y) xs ys = allrel r xs ys && allrel r' xs ys.
Lemma allrel_revl {T S : Type} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) :
allrel r (rev s1) s2 = allrel r s1 s2.
Proof.
Lemma allrel_revr {T S : Type} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) :
allrel r s1 (rev s2) = allrel r s1 s2.
Proof.
Lemma allrel_rev2 {T S : Type} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) :
allrel r (rev s1) (rev s2) = allrel r s1 s2.
Proof.
Lemma eq_allrel_meml {T : eqType} {S} (r : T -> S -> bool) (s1 s1' : seq T) s2 :
s1 =i s1' -> allrel r s1 s2 = allrel r s1' s2.
Proof.
Lemma eq_allrel_memr {T} {S : eqType} (r : T -> S -> bool) s1 (s2 s2' : seq S) :
s2 =i s2' -> allrel r s1 s2 = allrel r s1 s2'.
Proof.
Lemma eq_allrel_mem2 {T S : eqType} (r : T -> S -> bool)
(s1 s1' : seq T) (s2 s2' : seq S) :
s1 =i s1' -> s2 =i s2' -> allrel r s1 s2 = allrel r s1' s2'.
Proof.
Section All2Rel.
Variable (T : nonPropType) (r : rel T).
Implicit Types (x y z : T) (xs : seq T).
Hypothesis (rsym : symmetric r).
Lemma all2rel1 x : all2rel r [:: x] = r x x.
Lemma all2rel2 x y : all2rel r [:: x; y] = r x x && r y y && r x y.
Lemma all2rel_cons x xs :
all2rel r (x :: xs) = [&& r x x, all (r x) xs & all2rel r xs].
Proof.
End All2Rel.
Section Pairwise.
Variables (T : Type) (r : T -> T -> bool).
Implicit Types (x y : T) (xs ys : seq T).
Fixpoint pairwise xs : bool :=
if xs is x :: xs then all (r x) xs && pairwise xs else true.
Lemma pairwise_cons x xs : pairwise (x :: xs) = all (r x) xs && pairwise xs.
Proof.
by []. Qed.
Lemma pairwise_cat xs ys :
pairwise (xs ++ ys) = [&& allrel r xs ys, pairwise xs & pairwise ys].
Lemma pairwise_rcons xs x :
pairwise (rcons xs x) = all (r^~ x) xs && pairwise xs.
Proof.
Lemma pairwise2 x y : pairwise [:: x; y] = r x y.
Proof.
Lemma pairwise_mask m xs : pairwise xs -> pairwise (mask m xs).
Lemma pairwise_filter a xs : pairwise xs -> pairwise (filter a xs).
Proof.
Lemma pairwiseP x0 xs :
reflect {in gtn (size xs) &, {homo nth x0 xs : i j / i < j >-> r i j}}
(pairwise xs).
Proof.
elim: xs => /= [|x xs IHxs]; first exact: (iffP idP).
apply: (iffP andP) => [[r_x_xs pxs] i j|Hnth]; rewrite -?topredE /= ?ltnS.
by case: i j => [|i] [|j] //= gti gtj ij; [exact/all_nthP | exact/IHxs].
split; last by apply/IHxs => // i j; apply/(Hnth i.+1 j.+1).
by apply/(all_nthP x0) => i gti; apply/(Hnth 0 i.+1).
Qed.
apply: (iffP andP) => [[r_x_xs pxs] i j|Hnth]; rewrite -?topredE /= ?ltnS.
by case: i j => [|i] [|j] //= gti gtj ij; [exact/all_nthP | exact/IHxs].
split; last by apply/IHxs => // i j; apply/(Hnth i.+1 j.+1).
by apply/(all_nthP x0) => i gti; apply/(Hnth 0 i.+1).
Qed.
Lemma pairwise_all2rel :
reflexive r -> symmetric r -> forall xs, pairwise xs = all2rel r xs.
Proof.
End Pairwise.
Arguments pairwise {T} r xs.
Arguments pairwise_cons {T} r x xs.
Arguments pairwise_cat {T} r xs ys.
Arguments pairwise_rcons {T} r xs x.
Arguments pairwise2 {T} r x y.
Arguments pairwise_mask {T r} m {xs}.
Arguments pairwise_filter {T r} a {xs}.
Arguments pairwiseP {T r} x0 {xs}.
Arguments pairwise_all2rel {T r} r_refl r_sym xs.
Lemma sub_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) :
{in P &, subrel r r'} ->
forall xs, all P xs -> pairwise r xs -> pairwise r' xs.
Proof.
Lemma sub_pairwise {T : Type} (r r' : rel T) xs :
subrel r r' -> pairwise r xs -> pairwise r' xs.
Proof.
Lemma eq_in_pairwise {T : Type} (P : {pred T}) (r r' : rel T) :
{in P &, r =2 r'} -> forall xs, all P xs -> pairwise r xs = pairwise r' xs.
Proof.
Lemma eq_pairwise {T : Type} (r r' : rel T) :
r =2 r' -> pairwise r =i pairwise r'.
Proof.
Lemma pairwise_map {T T' : Type} (f : T' -> T) (r : rel T) xs :
pairwise r (map f xs) = pairwise (relpre f r) xs.
Proof.
Lemma pairwise_relI {T : Type} (r r' : rel T) (s : seq T) :
pairwise [rel x y | r x y && r' x y] s = pairwise r s && pairwise r' s.
Section EqPairwise.
Variables (T : eqType) (r : T -> T -> bool).
Implicit Types (xs ys : seq T).
Lemma subseq_pairwise xs ys : subseq xs ys -> pairwise r ys -> pairwise r xs.
Proof.
Lemma uniq_pairwise xs : uniq xs = pairwise [rel x y | x != y] xs.
Proof.
Lemma pairwise_uniq xs : irreflexive r -> pairwise r xs -> uniq xs.
Proof.
move=> r_irr; rewrite uniq_pairwise; apply/sub_pairwise => x y.
by apply: contraTneq => ->; rewrite r_irr.
Qed.
by apply: contraTneq => ->; rewrite r_irr.
Qed.
Lemma pairwise_eq : antisymmetric r ->
forall xs ys, pairwise r xs -> pairwise r ys -> perm_eq xs ys -> xs = ys.
Proof.
move=> r_asym; elim=> [|x xs IHxs] [|y ys] //=; try by move=> ? ? /perm_size.
move=> /andP [r_x_xs pxs] /andP [r_y_ys pys] eq_xs_ys.
move: (mem_head y ys) (mem_head x xs).
rewrite -(perm_mem eq_xs_ys) [x \in _](perm_mem eq_xs_ys) !inE.
case: eqVneq eq_xs_ys => /= [->|ne_xy] eq_xs_ys ys_x xs_y.
by rewrite (IHxs ys) // -(perm_cons x).
by case/eqP: ne_xy; apply: r_asym; rewrite (allP r_x_xs) ?(allP r_y_ys).
Qed.
move=> /andP [r_x_xs pxs] /andP [r_y_ys pys] eq_xs_ys.
move: (mem_head y ys) (mem_head x xs).
rewrite -(perm_mem eq_xs_ys) [x \in _](perm_mem eq_xs_ys) !inE.
case: eqVneq eq_xs_ys => /= [->|ne_xy] eq_xs_ys ys_x xs_y.
by rewrite (IHxs ys) // -(perm_cons x).
by case/eqP: ne_xy; apply: r_asym; rewrite (allP r_x_xs) ?(allP r_y_ys).
Qed.
Lemma pairwise_trans s : antisymmetric r ->
pairwise r s -> {in s & &, transitive r}.
Proof.
move=> /(_ _ _ _)/eqP r_anti + y x z => /pairwiseP-/(_ y) ltP ys xs zs.
have [-> //|neqxy] := eqVneq x y; have [-> //|neqzy] := eqVneq z y.
move=> lxy lyz; move: ys xs zs lxy neqxy lyz neqzy.
move=> /(nthP y)[j jlt <-] /(nthP y)[i ilt <-] /(nthP y)[k klt <-].
have [ltij|ltji|->] := ltngtP i j; last 2 first.
- by move=> leij; rewrite r_anti// leij ltP.
- by move=> lejj; rewrite r_anti// lejj.
move=> _ _; have [ltjk|ltkj|->] := ltngtP j k; last 2 first.
- by move=> lejk; rewrite r_anti// lejk ltP.
- by move=> lekk; rewrite r_anti// lekk.
by move=> _ _; apply: (ltP) => //; apply: ltn_trans ltjk.
Qed.
have [-> //|neqxy] := eqVneq x y; have [-> //|neqzy] := eqVneq z y.
move=> lxy lyz; move: ys xs zs lxy neqxy lyz neqzy.
move=> /(nthP y)[j jlt <-] /(nthP y)[i ilt <-] /(nthP y)[k klt <-].
have [ltij|ltji|->] := ltngtP i j; last 2 first.
- by move=> leij; rewrite r_anti// leij ltP.
- by move=> lejj; rewrite r_anti// lejj.
move=> _ _; have [ltjk|ltkj|->] := ltngtP j k; last 2 first.
- by move=> lejk; rewrite r_anti// lejk ltP.
- by move=> lekk; rewrite r_anti// lekk.
by move=> _ _; apply: (ltP) => //; apply: ltn_trans ltjk.
Qed.
End EqPairwise.
Arguments subseq_pairwise {T r xs ys}.
Arguments uniq_pairwise {T} xs.
Arguments pairwise_uniq {T r xs}.
Arguments pairwise_eq {T r} r_asym {xs ys}.
Section Permutations.
Variable T : eqType.
Implicit Types (x : T) (s t : seq T) (bs : seq (T * nat)) (acc : seq (seq T)).
Fixpoint incr_tally bs x :=
if bs isn't b :: bs then [:: (x, 1)] else
if x == b.1 then (x, b.2.+1) :: bs else b :: incr_tally bs x.
Definition tally s := foldl incr_tally [::] s.
Definition wf_tally :=
[qualify a bs : seq (T * nat) | uniq (unzip1 bs) && (0 \notin unzip2 bs)].
Definition tally_seq bs := flatten [seq nseq b.2 b.1 | b <- bs].
Local Notation tseq := tally_seq.
Lemma size_tally_seq bs : size (tally_seq bs) = sumn (unzip2 bs).
Proof.
Lemma tally_seqK : {in wf_tally, cancel tally_seq tally}.
Proof.
move=> bs /andP[]; elim: bs => [|[x [|n]] bs IHbs] //= /andP[bs'x Ubs] bs'0.
rewrite inE /tseq /tally /= -[n.+1]addn1 in bs'0 *.
elim: n 1 => /= [|n IHn] m; last by rewrite eqxx IHn addnS.
rewrite -{}[in RHS]IHbs {Ubs bs'0}// /tally /tally_seq add0n.
elim: bs bs'x [::] => [|[y n] bs IHbs] //= /[1!inE] /norP[y'x bs'x].
by elim: n => [|n IHn] bs1 /=; [rewrite IHbs | rewrite eq_sym ifN // IHn].
Qed.
rewrite inE /tseq /tally /= -[n.+1]addn1 in bs'0 *.
elim: n 1 => /= [|n IHn] m; last by rewrite eqxx IHn addnS.
rewrite -{}[in RHS]IHbs {Ubs bs'0}// /tally /tally_seq add0n.
elim: bs bs'x [::] => [|[y n] bs IHbs] //= /[1!inE] /norP[y'x bs'x].
by elim: n => [|n IHn] bs1 /=; [rewrite IHbs | rewrite eq_sym ifN // IHn].
Qed.
Lemma incr_tallyP x : {homo incr_tally^~ x : bs / bs \in wf_tally}.
Proof.
move=> bs /andP[]; rewrite unfold_in.
elim: bs => [|[y [|n]] bs IHbs] //= /andP[bs'y Ubs] /[1!inE] /= bs'0.
have [<- | y'x] /= := eqVneq y; first by rewrite bs'y Ubs.
rewrite -andbA {}IHbs {Ubs bs'0}// andbT.
elim: bs bs'y => [|b bs IHbs] /=; rewrite inE ?y'x // => /norP[b'y bs'y].
by case: ifP => _; rewrite /= inE negb_or ?y'x // b'y IHbs.
Qed.
elim: bs => [|[y [|n]] bs IHbs] //= /andP[bs'y Ubs] /[1!inE] /= bs'0.
have [<- | y'x] /= := eqVneq y; first by rewrite bs'y Ubs.
rewrite -andbA {}IHbs {Ubs bs'0}// andbT.
elim: bs bs'y => [|b bs IHbs] /=; rewrite inE ?y'x // => /norP[b'y bs'y].
by case: ifP => _; rewrite /= inE negb_or ?y'x // b'y IHbs.
Qed.
Lemma tallyP s : tally s \is a wf_tally.
Proof.
rewrite /tally; set bs := [::]; have: bs \in wf_tally by [].
by elim: s bs => //= x s IHs bs /(incr_tallyP x)/IHs.
Qed.
by elim: s bs => //= x s IHs bs /(incr_tallyP x)/IHs.
Qed.
Lemma tallyK s : perm_eq (tally_seq (tally s)) s.
Proof.
rewrite -[s in perm_eq _ s]cats0 -[nil]/(tseq [::]) /tally.
elim: s [::] => //= x s IHs bs; rewrite {IHs}(permPl (IHs _)).
rewrite perm_sym -cat1s perm_catCA {s}perm_cat2l.
elim: bs => //= b bs IHbs; case: eqP => [-> | _] //=.
by rewrite -cat1s perm_catCA perm_cat2l.
Qed.
elim: s [::] => //= x s IHs bs; rewrite {IHs}(permPl (IHs _)).
rewrite perm_sym -cat1s perm_catCA {s}perm_cat2l.
elim: bs => //= b bs IHbs; case: eqP => [-> | _] //=.
by rewrite -cat1s perm_catCA perm_cat2l.
Qed.
Lemma tallyEl s : perm_eq (unzip1 (tally s)) (undup s).
Proof.
Lemma tallyE s : perm_eq (tally s) [seq (x, count_mem x s) | x <- undup s].
Proof.
have /andP[Ubs _] := tallyP s; pose b := [fun s x => (x, count_mem x (tseq s))].
suffices /permPl->: perm_eq (tally s) (map (b (tally s)) (unzip1 (tally s))).
congr perm_eq: (perm_map (b (tally s)) (tallyEl s)).
by under eq_map do rewrite /= (permP (tallyK s)).
elim: (tally s) Ubs => [|[x m] bs IH] //= /andP[bs'x /IH-IHbs {IH}].
rewrite /tseq /= -/(tseq _) count_cat count_nseq /= eqxx mul1n.
rewrite (count_memPn _) ?addn0 ?perm_cons.
apply: contra bs'x; elim: {b IHbs}bs => //= b bs IHbs.
by rewrite mem_cat mem_nseq inE andbC; case: (_ == _).
congr perm_eq: IHbs; apply/eq_in_map=> y bs_y; congr (y, _).
by rewrite count_cat count_nseq /= (negPf (memPnC bs'x y bs_y)).
Qed.
suffices /permPl->: perm_eq (tally s) (map (b (tally s)) (unzip1 (tally s))).
congr perm_eq: (perm_map (b (tally s)) (tallyEl s)).
by under eq_map do rewrite /= (permP (tallyK s)).
elim: (tally s) Ubs => [|[x m] bs IH] //= /andP[bs'x /IH-IHbs {IH}].
rewrite /tseq /= -/(tseq _) count_cat count_nseq /= eqxx mul1n.
rewrite (count_memPn _) ?addn0 ?perm_cons.
apply: contra bs'x; elim: {b IHbs}bs => //= b bs IHbs.
by rewrite mem_cat mem_nseq inE andbC; case: (_ == _).
congr perm_eq: IHbs; apply/eq_in_map=> y bs_y; congr (y, _).
by rewrite count_cat count_nseq /= (negPf (memPnC bs'x y bs_y)).
Qed.
Lemma perm_tally s1 s2 : perm_eq s1 s2 -> perm_eq (tally s1) (tally s2).
Proof.
Lemma perm_tally_seq bs1 bs2 :
perm_eq bs1 bs2 -> perm_eq (tally_seq bs1) (tally_seq bs2).
Proof.
Lemma perm_count_undup s :
perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s.
Local Fixpoint cons_perms_ perms_rec (s : seq T) bs bs2 acc :=
if bs isn't b :: bs1 then acc else
if b isn't (x, m.+1) then cons_perms_ perms_rec s bs1 bs2 acc else
let acc_xs := perms_rec (x :: s) ((x, m) :: bs1 ++ bs2) acc in
cons_perms_ perms_rec s bs1 (b :: bs2) acc_xs.
Local Fixpoint perms_rec n s bs acc :=
if n isn't n.+1 then s :: acc else cons_perms_ (perms_rec n) s bs [::] acc.
Local Notation cons_perms n := (cons_perms_ (perms_rec n) [::]).
Definition permutations s := perms_rec (size s) [::] (tally s) [::].
Let permsP s : exists n bs,
[/\ permutations s = perms_rec n [::] bs [::],
size (tseq bs) == n, perm_eq (tseq bs) s & uniq (unzip1 bs)].
Proof.
Local Notation bsCA := (permEl (perm_catCA _ [:: _] _)).
Let cons_permsE : forall 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 [::]].
Proof.
pose is_acc f := forall acc, f acc = f [::] ++ acc. (* f is accumulating. *)
have cpE: forall f & forall s bs, is_acc (f s bs), is_acc (cons_perms_ f _ _ _).
move=> s bs bs2 f fE acc; elim: bs => [|[x [|m]] bs IHbs] //= in s bs2 acc *.
by rewrite fE IHbs catA -IHbs.
have prE: is_acc (perms_rec _ _ _) by elim=> //= n IHn s bs; apply: cpE.
pose has_suffix f := forall s : seq T, f s = [seq t ++ s | t <- f [::]].
suffices prEs n bs: has_suffix (fun s => perms_rec n s bs [::]).
move=> n x bs bs1 bs2 /=; rewrite cpE // prEs.
by under eq_map do rewrite cats1.
elim: n bs => //= n IHn bs s; elim: bs [::] => [|[x [|m]] bs IHbs] //= bs1.
rewrite cpE // IHbs IHn [in RHS]cpE // [in RHS]IHn map_cat -map_comp.
by congr (_ ++ _); apply: eq_map => t /=; rewrite -catA.
Qed.
have cpE: forall f & forall s bs, is_acc (f s bs), is_acc (cons_perms_ f _ _ _).
move=> s bs bs2 f fE acc; elim: bs => [|[x [|m]] bs IHbs] //= in s bs2 acc *.
by rewrite fE IHbs catA -IHbs.
have prE: is_acc (perms_rec _ _ _) by elim=> //= n IHn s bs; apply: cpE.
pose has_suffix f := forall s : seq T, f s = [seq t ++ s | t <- f [::]].
suffices prEs n bs: has_suffix (fun s => perms_rec n s bs [::]).
move=> n x bs bs1 bs2 /=; rewrite cpE // prEs.
by under eq_map do rewrite cats1.
elim: n bs => //= n IHn bs s; elim: bs [::] => [|[x [|m]] bs IHbs] //= bs1.
rewrite cpE // IHbs IHn [in RHS]cpE // [in RHS]IHn map_cat -map_comp.
by congr (_ ++ _); apply: eq_map => t /=; rewrite -catA.
Qed.
Lemma mem_permutations s t : (t \in permutations s) = perm_eq t s.
Proof.
have{s} [n [bs [-> Dn /permPr<- _]]] := permsP s.
elim: n => [|n IHn] /= in t bs Dn *.
by rewrite inE (nilP Dn); apply/eqP/perm_nilP.
rewrite -[bs in tseq bs]cats0 in Dn *; have x0 : T by case: (tseq _) Dn.
rewrite -[RHS](@andb_idl (last x0 t \in tseq bs)).
case/lastP: t {IHn} => [|t x] Dt; first by rewrite -(perm_size Dt) in Dn.
by rewrite -[bs]cats0 -(perm_mem Dt) last_rcons mem_rcons mem_head.
elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn *.
rewrite cons_permsE -!cat_cons !mem_cat (mem_nseq m.+1) orbC andb_orl.
rewrite {}IHbs ?(perm_size (perm_tseq bsCA)) //= (permPr (perm_tseq bsCA)).
congr (_ || _); apply/mapP/andP=> [[t1 Dt1 ->] | [/eqP]].
by rewrite last_rcons perm_rcons perm_cons IHn in Dt1 *.
case/lastP: t => [_ /perm_size//|t y]; rewrite last_rcons perm_rcons => ->.
by rewrite perm_cons; exists t; rewrite ?IHn.
Qed.
elim: n => [|n IHn] /= in t bs Dn *.
by rewrite inE (nilP Dn); apply/eqP/perm_nilP.
rewrite -[bs in tseq bs]cats0 in Dn *; have x0 : T by case: (tseq _) Dn.
rewrite -[RHS](@andb_idl (last x0 t \in tseq bs)).
case/lastP: t {IHn} => [|t x] Dt; first by rewrite -(perm_size Dt) in Dn.
by rewrite -[bs]cats0 -(perm_mem Dt) last_rcons mem_rcons mem_head.
elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn *.
rewrite cons_permsE -!cat_cons !mem_cat (mem_nseq m.+1) orbC andb_orl.
rewrite {}IHbs ?(perm_size (perm_tseq bsCA)) //= (permPr (perm_tseq bsCA)).
congr (_ || _); apply/mapP/andP=> [[t1 Dt1 ->] | [/eqP]].
by rewrite last_rcons perm_rcons perm_cons IHn in Dt1 *.
case/lastP: t => [_ /perm_size//|t y]; rewrite last_rcons perm_rcons => ->.
by rewrite perm_cons; exists t; rewrite ?IHn.
Qed.
Lemma permutations_uniq s : uniq (permutations s).
Proof.
have{s} [n [bs [-> Dn _ Ubs]]] := permsP s.
elim: n => //= n IHn in bs Dn Ubs *; rewrite -[bs]cats0 /unzip1 in Dn Ubs.
elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn Ubs *.
by case/andP: Ubs => _ /IHbs->.
rewrite /= cons_permsE cat_uniq has_sym andbCA andbC.
rewrite {}IHbs; first 1 last; last by rewrite (perm_size (perm_tseq bsCA)).
by rewrite (perm_uniq (perm_map _ bsCA)).
rewrite (map_inj_uniq (rcons_injl x)) {}IHn {Dn}//=.
have: x \notin unzip1 bs by apply: contraL Ubs; rewrite map_cat mem_cat => ->.
move: {bs2 m Ubs}(perms_rec n _ _ _) (_ :: bs2) => ts.
elim: bs => [|[y [|m]] bs IHbs] //= /[1!inE] bs2 /norP[x'y /IHbs//].
rewrite cons_permsE has_cat negb_or has_map => ->.
by apply/hasPn=> t _; apply: contra x'y => /mapP[t1 _ /rcons_inj[_ ->]].
Qed.
elim: n => //= n IHn in bs Dn Ubs *; rewrite -[bs]cats0 /unzip1 in Dn Ubs.
elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn Ubs *.
by case/andP: Ubs => _ /IHbs->.
rewrite /= cons_permsE cat_uniq has_sym andbCA andbC.
rewrite {}IHbs; first 1 last; last by rewrite (perm_size (perm_tseq bsCA)).
by rewrite (perm_uniq (perm_map _ bsCA)).
rewrite (map_inj_uniq (rcons_injl x)) {}IHn {Dn}//=.
have: x \notin unzip1 bs by apply: contraL Ubs; rewrite map_cat mem_cat => ->.
move: {bs2 m Ubs}(perms_rec n _ _ _) (_ :: bs2) => ts.
elim: bs => [|[y [|m]] bs IHbs] //= /[1!inE] bs2 /norP[x'y /IHbs//].
rewrite cons_permsE has_cat negb_or has_map => ->.
by apply/hasPn=> t _; apply: contra x'y => /mapP[t1 _ /rcons_inj[_ ->]].
Qed.
Notation perms := permutations.
Lemma permutationsE s :
0 < size s ->
perm_eq (perms s) [seq x :: t | x <- undup s, t <- perms (rem x s)].
Proof.
move=> nt_s; apply/uniq_perm=> [||t]; first exact: permutations_uniq.
apply/allpairs_uniq_dep=> [|x _|]; rewrite ?undup_uniq ?permutations_uniq //.
by case=> [_ _] [x t] _ _ [-> ->].
rewrite mem_permutations; apply/idP/allpairsPdep=> [Dt | [x [t1 []]]].
rewrite -(perm_size Dt) in nt_s; case: t nt_s => // x t _ in Dt *.
have s_x: x \in s by rewrite -(perm_mem Dt) mem_head.
exists x, t; rewrite mem_undup mem_permutations; split=> //.
by rewrite -(perm_cons x) (permPl Dt) perm_to_rem.
rewrite mem_undup mem_permutations -(perm_cons x) => s_x Dt1 ->.
by rewrite (permPl Dt1) perm_sym perm_to_rem.
Qed.
apply/allpairs_uniq_dep=> [|x _|]; rewrite ?undup_uniq ?permutations_uniq //.
by case=> [_ _] [x t] _ _ [-> ->].
rewrite mem_permutations; apply/idP/allpairsPdep=> [Dt | [x [t1 []]]].
rewrite -(perm_size Dt) in nt_s; case: t nt_s => // x t _ in Dt *.
have s_x: x \in s by rewrite -(perm_mem Dt) mem_head.
exists x, t; rewrite mem_undup mem_permutations; split=> //.
by rewrite -(perm_cons x) (permPl Dt) perm_to_rem.
rewrite mem_undup mem_permutations -(perm_cons x) => s_x Dt1 ->.
by rewrite (permPl Dt1) perm_sym perm_to_rem.
Qed.
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].
Proof.
have take'x t i: i <= index x t -> i <= size t /\ x \notin take i t.
move=> le_i_x; have le_i_t: i <= size t := leq_trans le_i_x (index_size x t).
case: (nthP x) => // -[j lt_j_i /eqP]; rewrite size_takel // in lt_j_i.
by rewrite nth_take // [_ == _](before_find x (leq_trans lt_j_i le_i_x)).
pose xrot t i := rot i (x :: t); pose xrotV t := index x (rev (rot 1 t)).
have xrotK t: {in le_x t, cancel (xrot t) xrotV}.
move=> i; rewrite mem_iota addn1 /xrotV => /take'x[le_i_t ti'x].
rewrite -rotD ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev.
by rewrite ifN // size_takel //= eqxx addn0.
apply/uniq_perm=> [||t]; first exact: permutations_uniq.
apply/allpairs_uniq_dep=> [|t _|]; rewrite ?permutations_uniq ?iota_uniq //.
move=> _ _ /allpairsPdep[t [i [_ ? ->]]] /allpairsPdep[u [j [_ ? ->]]] Etu.
have Eij: i = j by rewrite -(xrotK t i) // /xrot Etu xrotK.
by move: Etu; rewrite Eij => /rot_inj[->].
rewrite mem_permutations; apply/esym; apply/allpairsPdep/idP=> [[u [i]] | Dt].
rewrite mem_permutations => -[Du _ /(canLR (rotK i))]; rewrite /rotr.
by set j := (j in rot j _) => Dt; apply/perm_consP; exists j, u.
pose r := rev (rot 1 t); pose i := index x r; pose u := rev (take i r).
have r_x: x \in r by rewrite mem_rev mem_rot (perm_mem Dt) mem_head.
have [v Duv]: {v | rot i (x :: u ++ v) = t}; first exists (rev (drop i.+1 r)).
rewrite -rev_cat -rev_rcons -rot1_cons -cat_cons -(nth_index x r_x).
by rewrite -drop_nth ?index_mem // rot_rot !rev_rot revK rotK rotrK.
exists (u ++ v), i; rewrite mem_permutations -(perm_cons x) -(perm_rot i) Duv.
rewrite mem_iota addn1 ltnS /= index_cat mem_rev size_rev.
by have /take'x[le_i_t ti'x] := leqnn i; rewrite ifN ?size_takel ?leq_addr.
Qed.
move=> le_i_x; have le_i_t: i <= size t := leq_trans le_i_x (index_size x t).
case: (nthP x) => // -[j lt_j_i /eqP]; rewrite size_takel // in lt_j_i.
by rewrite nth_take // [_ == _](before_find x (leq_trans lt_j_i le_i_x)).
pose xrot t i := rot i (x :: t); pose xrotV t := index x (rev (rot 1 t)).
have xrotK t: {in le_x t, cancel (xrot t) xrotV}.
move=> i; rewrite mem_iota addn1 /xrotV => /take'x[le_i_t ti'x].
rewrite -rotD ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev.
by rewrite ifN // size_takel //= eqxx addn0.
apply/uniq_perm=> [||t]; first exact: permutations_uniq.
apply/allpairs_uniq_dep=> [|t _|]; rewrite ?permutations_uniq ?iota_uniq //.
move=> _ _ /allpairsPdep[t [i [_ ? ->]]] /allpairsPdep[u [j [_ ? ->]]] Etu.
have Eij: i = j by rewrite -(xrotK t i) // /xrot Etu xrotK.
by move: Etu; rewrite Eij => /rot_inj[->].
rewrite mem_permutations; apply/esym; apply/allpairsPdep/idP=> [[u [i]] | Dt].
rewrite mem_permutations => -[Du _ /(canLR (rotK i))]; rewrite /rotr.
by set j := (j in rot j _) => Dt; apply/perm_consP; exists j, u.
pose r := rev (rot 1 t); pose i := index x r; pose u := rev (take i r).
have r_x: x \in r by rewrite mem_rev mem_rot (perm_mem Dt) mem_head.
have [v Duv]: {v | rot i (x :: u ++ v) = t}; first exists (rev (drop i.+1 r)).
rewrite -rev_cat -rev_rcons -rot1_cons -cat_cons -(nth_index x r_x).
by rewrite -drop_nth ?index_mem // rot_rot !rev_rot revK rotK rotrK.
exists (u ++ v), i; rewrite mem_permutations -(perm_cons x) -(perm_rot i) Duv.
rewrite mem_iota addn1 ltnS /= index_cat mem_rev size_rev.
by have /take'x[le_i_t ti'x] := leqnn i; rewrite ifN ?size_takel ?leq_addr.
Qed.
Lemma size_permutations s : uniq s -> size (permutations s) = (size s)`!.
Proof.
Lemma permutations_all_uniq s : uniq s -> all uniq (permutations s).
Proof.
Lemma perm_permutations s t :
perm_eq s t -> perm_eq (permutations s) (permutations t).
Proof.
move=> Est; apply/uniq_perm; try exact: permutations_uniq.
by move=> u; rewrite !mem_permutations (permPr Est).
Qed.
by move=> u; rewrite !mem_permutations (permPr Est).
Qed.
End Permutations.