From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.ssreflect.seq.html | 1822 ++++++++++++++++++------------
1 file changed, 1116 insertions(+), 706 deletions(-)
(limited to 'docs/htmldoc/mathcomp.ssreflect.seq.html')
diff --git a/docs/htmldoc/mathcomp.ssreflect.seq.html b/docs/htmldoc/mathcomp.ssreflect.seq.html
index 8f7211f..6709b82 100644
--- a/docs/htmldoc/mathcomp.ssreflect.seq.html
+++ b/docs/htmldoc/mathcomp.ssreflect.seq.html
@@ -21,7 +21,6 @@
@@ -88,29 +87,45 @@
first padded with 0's to size i+1, if needed).
Predicates:
- nilp s == s is [:: ].
+ nilp s <=> s is [:: ].
:= (size s == 0).
x \in s == x appears in s (this requires an eqType for T).
index x s == the first index at which x appears in s, or size s if
x \notin s.
- has p s == the (applicative, boolean) predicate p holds for some
- item in s.
- all p s == p holds for all items in s.
+ 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 number of times x occurs in s := count (pred1 x) s.
- constant s == all items in s are identical (trivial if s = [:: ])
- uniq s == all the items in s are pairwise different.
- subseq s1 s2 == s1 is a subsequence of s2, i.e., s1 = mask m s2 for
+ count_mem x s == the multiplicity of x in s, i.e., count (pred1 x) s.
+ tally s == a tally of s, i.e., a sequence of (item, multiplicity)
+ pairs for all items in sequence s (without duplicates).
+ incr_tally bs x == increment the multiplicity of x in the tally bs, or add
+ x with multiplicity 1 at then end if x is not in bs.
+ bs \is a wf_tally <=> bs is well-formed tally, with no duplicate items or
+ null multiplicities.
+ tally_seq bs == the expansion of a tally bs into a sequence where each
+ (x, n) pair expands into a sequence of n x's.
+ constant s <=> all items in s are identical (trivial if s = [:: ]).
+ uniq s <=> all the items in s are pairwise different.
+ subseq s1 s2 <=> s1 is a subsequence of s2, i.e., s1 = mask m s2 for
some m : bitseq (see below).
- perm_eq s1 s2 == s2 is a permutation of s1, i.e., s1 and s2 have the
+ 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.
+> 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
@@ -136,12 +151,21 @@
rev s == the (linear time) reversal of s.
catrev s1 s2 == the reversal of s1 followed by s2 (this is the
recursive form of rev).
-Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m],
-
- map f s == the sequence [:: f x_1, ..., f x_n].
- allpairs f s t == the sequence of all the f x y, with x and y drawn from
- s and t, respectively, in row-major order.
+Dependent iterator: for s : seq S and t : S -> seq T
+
+ [seq E | x <- s, y <- t] := flatten [seq [seq E | x <- t] | y <- s]
+ == the sequence of all the f x y, with x and y drawn from
+ s and t, respectively, in row-major order,
+ and where t is possibly dependent in elements of s
+ allpairs_dep f s t := self expanding definition for
+ [seq f x y | x <- s, y <- t i]
+Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m],
+
+ allpairs f s t := same as allpairs_dep but where t is non dependent,
+ i.e. self expanding definition for
+ [seq f x y | x <- s, y <- t]
:= [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m]
+ map f s == the sequence [:: f x_1, ..., f x_n].
pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik,
pf x_i = Some y_i, and pf x_j = None iff j is not in
{i1, ..., ik}.
@@ -162,7 +186,7 @@
reshape r s == s reshaped into a sequence of sequences whose sizes are
given by r (truncating if s is too long or too short).
:= [:: [:: x_1; ...; x_r1];
- [:: x(r1 + 1); ...; x(r0 + r1) ];
+ [:: x(r1 + 1); ...; x(r0 + r1) ];
...;
[:: x(r1 + ... + r(k-1) + 1); ...; x(r0 + ... rk) ]#]
flatten_index sh r c == the index, in flatten ss, of the item of indexes
@@ -172,11 +196,10 @@
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:
+Notation for manifest comprehensions:
[seq x <- s | C] := filter (fun x => C) s.
[seq E | x <- s] := map (fun x => E) s.
- [seq E | x <- s, y <- t] := allpairs (fun x y => E) s t.
[seq x <- s | C1 & C2] := [seq x <- s | C1 && C2].
[seq E | x <- s & C] := [seq E | x <- [seq x | C] ].
> The above allow optional type casts on the eigenvariables, as in
@@ -184,7 +207,14 @@
needed as type inference considers E or C before s.
We are quite systematic in providing lemmas to rewrite any composition
of two operations. "rev", whose simplifications are not natural, is
- protected with nosimpl.
+ protected with nosimpl.
+The following are equivalent:
+
+ [<-> P0; P1; ..; Pn] <-> P0, P1, ..., Pn are all equivalent.
+ := P0 -> P1 -> ... -> Pn -> P0
+ if T : [<-> P0; P1; ..; Pn] is such an equivalence, and i, j are in nat
+ then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj;
+ when i (resp. j) is out of bounds, Pi (resp. Pj) defaults to P0.
@@ -202,11 +232,9 @@
Inductive seq (T : Type) : Type := Nil | Cons of T & seq T.
-
Notation seq :=
list.
-
Notation Cons T := (@
cons T) (
only parsing).
-
Notation Nil T := (@
nil T) (
only parsing).
-
-
+
Notation seq :=
list.
+
Notation Cons T := (@
cons T) (
only parsing).
+
Notation Nil T := (@
nil T) (
only parsing).
-
Infix "::" :=
cons :
seq_scope.
+
Infix "::" :=
cons :
seq_scope.
-
- GG - this triggers a camlp4 warning, as if this Notation had been Reserved
-
-
-
Notation "[ :: ]" :=
nil (
at level 0,
format "[ :: ]") :
seq_scope.
+
Notation "[ :: ]" :=
nil (
at level 0,
format "[ :: ]") :
seq_scope.
-
Notation "[ :: x1 ]" := (
x1 :: [::])
+
Notation "[ :: x1 ]" := (
x1 :: [::])
(
at level 0,
format "[ :: x1 ]") :
seq_scope.
-
Notation "[ :: x & s ]" := (
x :: s) (
at level 0,
only parsing) :
seq_scope.
+
Notation "[ :: x & s ]" := (
x :: s) (
at level 0,
only parsing) :
seq_scope.
-
Notation "[ :: x1 , x2 , .. , xn & s ]" := (
x1 :: x2 :: .. (
xn :: s) ..)
+
Notation "[ :: x1 , x2 , .. , xn & s ]" := (
x1 :: x2 :: .. (
xn :: s) ..)
(
at level 0,
format
"'[hv' [ :: '[' x1 , '/' x2 , '/' .. , '/' xn ']' '/ ' & s ] ']'"
) :
seq_scope.
-
Notation "[ :: x1 ; x2 ; .. ; xn ]" := (
x1 :: x2 :: ..
[:: xn] ..)
+
Notation "[ :: x1 ; x2 ; .. ; xn ]" := (
x1 :: x2 :: ..
[:: xn] ..)
(
at level 0,
format "[ :: '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]"
) :
seq_scope.
@@ -249,36 +271,36 @@
Section Sequences.
-
Variable n0 :
nat.
+
Variable n0 :
nat.
Variable T :
Type.
Variable x0 :
T.
Implicit Types x y z :
T.
-
Implicit Types m n :
nat.
+
Implicit Types m n :
nat.
Implicit Type s :
seq T.
-
Fixpoint size s :=
if s is _ :: s' then (size s').+1 else 0.
+
Fixpoint size s :=
if s is _ :: s' then (size s').+1 else 0.
-
Lemma size0nil s :
size s = 0
→ s = [::].
+
Lemma size0nil s :
size s = 0
→ s = [::].
-
Definition nilp s :=
size s == 0.
+
Definition nilp s :=
size s == 0.
-
Lemma nilP s :
reflect (
s = [::]) (
nilp s).
+
Lemma nilP s :
reflect (
s = [::]) (
nilp s).
-
Definition ohead s :=
if s is x :: _ then Some x else None.
-
Definition head s :=
if s is x :: _ then x else x0.
+
Definition 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 [::].
+
Definition behead s :=
if s is _ :: s' then s' else [::].
-
Lemma size_behead s :
size (
behead s)
= (size s).-1.
+
Lemma size_behead s :
size (
behead s)
= (size s).-1.
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.
+ 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].
+ if s is x :: s' then if n is n'.+1 then x :: @set_nth s' n' y else y :: s'
+ else ncons n x0 [:: y].
-Lemma nth0 s : nth s 0 = head s.
+Lemma nth0 s : nth s 0 = head s.
-Lemma nth_default s n : size s ≤ n → nth s n = x0.
+Lemma nth_default s n : size s ≤ n → nth s n = x0.
-Lemma nth_nil n : nth [::] n = x0.
+Lemma nth_nil n : nth [::] n = x0.
-Lemma last_nth x s : last x s = nth (x :: s) (size s).
+Lemma last_nth x s : last x s = nth (x :: s) (size s).
-Lemma nth_last s : nth s (size s).-1 = last x0 s.
+Lemma nth_last s : nth s (size s).-1 = last x0 s.
-Lemma nth_behead s n : nth (behead s) n = nth s n.+1.
+Lemma nth_behead s n : nth (behead s) n = nth s n.+1.
Lemma nth_cat s1 s2 n :
- nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1).
+ nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1).
Lemma nth_rcons s x n :
- nth (rcons s x) n =
- if n < size s then nth s n else if n == size s then x else x0.
+ nth (rcons s x) n =
+ if n < size s then nth s n else if n == size s then x else x0.
Lemma nth_ncons m x s n :
- nth (ncons m x s) n = if n < m then x else nth s (n - m).
+ nth (ncons m x s) n = if n < m then x else nth s (n - m).
-Lemma nth_nseq m x n : nth (nseq m x) n = (if n < m then x else x0).
+Lemma nth_nseq m x n : nth (nseq m x) n = (if n < m then x else x0).
Lemma eq_from_nth s1 s2 :
- size s1 = size s2 → (∀ i, i < size s1 → nth s1 i = nth s2 i) →
- s1 = s2.
+ size s1 = size s2 → (∀ i, i < size s1 → nth s1 i = nth s2 i) →
+ s1 = s2.
-Lemma size_set_nth s n y : size (set_nth s n y) = maxn n.+1 (size s).
+Lemma size_set_nth s n y : size (set_nth s n y) = maxn n.+1 (size s).
-Lemma set_nth_nil n y : set_nth [::] n y = ncons n x0 [:: y].
+Lemma set_nth_nil n y : set_nth [::] n y = ncons n x0 [:: y].
-Lemma nth_set_nth s n y : nth (set_nth s n y) =1 [eta nth s with n |-> y].
+Lemma nth_set_nth s n y : nth (set_nth s n y) =1 [eta nth s with n |-> y].
Lemma set_set_nth s n1 y1 n2 y2 (s2 := set_nth s n2 y2) :
- set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1.
+ set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1.
@@ -490,198 +512,204 @@
Section SeqFind.
-Variable a : pred T.
+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 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 [::].
+ 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 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 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.
+Fixpoint all s := if s is x :: s' then a x && all s' else true.
-Lemma size_filter s : size (filter s) = count s.
+Lemma size_filter s : size (filter s) = count s.
-Lemma has_count s : has s = (0 < count s).
+Lemma has_count s : has s = (0 < count s).
-Lemma count_size s : count s ≤ size s.
+Lemma count_size s : count s ≤ size s.
-Lemma all_count s : all s = (count s == size s).
+Lemma all_count s : all s = (count s == size s).
Lemma filter_all s : all (filter s).
-Lemma all_filterP s : reflect (filter s = s) (all s).
+Lemma all_filterP s : reflect (filter s = s) (all s).
-Lemma filter_id s : filter (filter s) = filter s.
+Lemma filter_id s : filter (filter s) = filter s.
-Lemma has_find s : has s = (find s < size s).
+Lemma has_find s : has s = (find s < size s).
-Lemma find_size s : find s ≤ size s.
+Lemma find_size s : find s ≤ size s.
Lemma find_cat s1 s2 :
- find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2.
+ find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2.
-Lemma has_nil : has [::] = false.
+Lemma has_nil : has [::] = false.
-Lemma has_seq1 x : has [:: x] = a x.
+Lemma has_seq1 x : has [:: x] = a x.
-Lemma has_nseq n x : has (nseq n x) = (0 < n) && a x.
+Lemma has_nseq n x : has (nseq n x) = (0 < n) && a x.
-Lemma has_seqb (b : bool) x : has (nseq b x) = b && a x.
+Lemma has_seqb (b : bool) x : has (nseq b x) = b && a x.
-Lemma all_nil : all [::] = true.
+Lemma all_nil : all [::] = true.
-Lemma all_seq1 x : all [:: x] = a x.
+Lemma all_seq1 x : all [:: x] = a x.
-Lemma all_nseq n x : all (nseq n x) = (n == 0) || a x.
+Lemma all_nseq n x : all (nseq n x) = (n == 0) || a x.
-Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x.
+Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x.
-Lemma find_nseq n x : find (nseq n x) = ~~ a x × n.
+Lemma filter_nseq n x : filter (nseq n x) = nseq (a x × n) x.
-Lemma nth_find s : has s → a (nth s (find s)).
+Lemma count_nseq n x : count (nseq n x) = a x × n.
-Lemma before_find s i : i < find s → a (nth s i) = false.
-
+Lemma find_nseq n x : find (nseq n x) = ~~ a x × n.
+
+
+Lemma nth_find s : has s → a (nth s (find s)).
+
-Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
+Lemma before_find s i : i < find s → a (nth s i) = false.
+
+
+Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
Lemma filter_rcons s x :
- filter (rcons s x) = if a x then rcons (filter s) x else filter s.
+ filter (rcons s x) = if a x then rcons (filter s) x else filter s.
-Lemma count_cat s1 s2 : count (s1 ++ s2) = count s1 + count s2.
+Lemma count_cat s1 s2 : count (s1 ++ s2) = count s1 + count s2.
-Lemma has_cat s1 s2 : has (s1 ++ s2) = has s1 || has s2.
+Lemma has_cat s1 s2 : has (s1 ++ s2) = has s1 || has s2.
-Lemma has_rcons s x : has (rcons s x) = a x || has s.
+Lemma has_rcons s x : has (rcons s x) = a x || has s.
-Lemma all_cat s1 s2 : all (s1 ++ s2) = all s1 && all s2.
+Lemma all_cat s1 s2 : all (s1 ++ s2) = all s1 && all s2.
-Lemma all_rcons s x : all (rcons s x) = a x && all s.
+Lemma all_rcons s x : all (rcons s x) = a x && all s.
End SeqFind.
-Lemma eq_find a1 a2 : a1 =1 a2 → find a1 =1 find a2.
+Lemma eq_find a1 a2 : a1 =1 a2 → find a1 =1 find a2.
-Lemma eq_filter a1 a2 : a1 =1 a2 → filter a1 =1 filter a2.
+Lemma eq_filter a1 a2 : a1 =1 a2 → filter a1 =1 filter a2.
-Lemma eq_count a1 a2 : a1 =1 a2 → count a1 =1 count a2.
+Lemma eq_count a1 a2 : a1 =1 a2 → count a1 =1 count a2.
-Lemma eq_has a1 a2 : a1 =1 a2 → has a1 =1 has a2.
+Lemma eq_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 eq_all a1 a2 : a1 =1 a2 → all a1 =1 all a2.
Section SubPred.
-Variable (a1 a2 : pred T).
-Hypothesis s12 : subpred a1 a2.
+Variable (a1 a2 : pred T).
+Hypothesis s12 : subpred a1 a2.
-Lemma sub_find s : find a2 s ≤ find a1 s.
+Lemma sub_find s : find a2 s ≤ find a1 s.
-Lemma sub_has s : has a1 s → has a2 s.
+Lemma sub_has s : has a1 s → has a2 s.
-Lemma sub_count s : count a1 s ≤ count a2 s.
+Lemma sub_count s : count a1 s ≤ count a2 s.
-Lemma sub_all s : all a1 s → all a2 s.
+Lemma sub_all s : all a1 s → all a2 s.
End SubPred.
-Lemma filter_pred0 s : filter pred0 s = [::].
+Lemma filter_pred0 s : filter pred0 s = [::].
-Lemma filter_predT s : filter predT s = s.
+Lemma filter_predT s : filter predT s = s.
-Lemma filter_predI a1 a2 s : filter (predI a1 a2) s = filter a1 (filter a2 s).
+Lemma filter_predI a1 a2 s : filter (predI a1 a2) s = filter a1 (filter a2 s).
-Lemma count_pred0 s : count pred0 s = 0.
+Lemma count_pred0 s : count pred0 s = 0.
-Lemma count_predT s : count predT s = size s.
+Lemma count_predT s : count predT s = size s.
Lemma count_predUI a1 a2 s :
- count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
+ count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
-Lemma count_predC a s : count a s + count (predC a) s = size s.
+Lemma count_predC a s : count a s + count (predC a) s = size s.
-Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s.
+Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s.
-Lemma has_pred0 s : has pred0 s = false.
+Lemma has_pred0 s : has pred0 s = false.
-Lemma has_predT s : has predT s = (0 < size s).
+Lemma has_predT s : has predT s = (0 < size s).
-Lemma has_predC a s : has (predC a) s = ~~ all a s.
+Lemma has_predC a s : has (predC a) s = ~~ all a s.
-Lemma has_predU a1 a2 s : has (predU a1 a2) s = has a1 s || has a2 s.
+Lemma has_predU a1 a2 s : has (predU a1 a2) s = has a1 s || has a2 s.
-Lemma all_pred0 s : all pred0 s = (size s == 0).
+Lemma all_pred0 s : all pred0 s = (size s == 0).
-Lemma all_predT s : all predT s.
+Lemma all_predT s : all predT s.
-Lemma all_predC a s : all (predC a) s = ~~ has a s.
+Lemma all_predC a s : all (predC a) s = ~~ has a s.
-Lemma all_predI a1 a2 s : all (predI a1 a2) s = all a1 s && all a2 s.
+Lemma all_predI a1 a2 s : all (predI a1 a2) s = all a1 s && all a2 s.
@@ -694,97 +722,95 @@
Fixpoint drop n s {struct s} :=
match s, n with
- | _ :: s', n'.+1 ⇒ drop n' s'
+ | _ :: s', n'.+1 ⇒ drop n' s'
| _, _ ⇒ s
end.
-Lemma drop_behead : drop n0 =1 iter n0 behead.
+Lemma drop_behead : drop n0 =1 iter n0 behead.
-Lemma drop0 s : drop 0 s = s.
+Lemma drop0 s : drop 0 s = s.
-Lemma drop1 : drop 1 =1 behead.
+Lemma drop1 : drop 1 =1 behead.
-Lemma drop_oversize n s : size s ≤ n → drop n s = [::].
+Lemma drop_oversize n s : size s ≤ n → drop n s = [::].
-Lemma drop_size s : drop (size s) s = [::].
+Lemma drop_size s : drop (size s) s = [::].
Lemma drop_cons x s :
- drop n0 (x :: s) = if n0 is n.+1 then drop n s else x :: s.
+ drop n0 (x :: s) = if n0 is n.+1 then drop n s else x :: s.
-Lemma size_drop s : size (drop n0 s) = size s - n0.
+Lemma size_drop s : size (drop n0 s) = size s - n0.
Lemma drop_cat s1 s2 :
- drop n0 (s1 ++ s2) =
- if n0 < size s1 then drop n0 s1 ++ s2 else drop (n0 - size s1) s2.
+ drop n0 (s1 ++ s2) =
+ if n0 < size s1 then drop n0 s1 ++ s2 else drop (n0 - size s1) s2.
-Lemma drop_size_cat n s1 s2 : size s1 = n → drop n (s1 ++ s2) = s2.
+Lemma drop_size_cat n s1 s2 : size s1 = n → drop n (s1 ++ s2) = s2.
-Lemma nconsK n x : cancel (ncons n x) (drop n).
+Lemma nconsK n x : cancel (ncons n x) (drop n).
-Lemma drop_drop s n1 n2 : drop n1 (drop n2 s) = drop (n1 + n2) s.
+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'
- | _, _ ⇒ [::]
+ | x :: s', n'.+1 ⇒ x :: take n' s'
+ | _, _ ⇒ [::]
end.
-Lemma take0 s : take 0 s = [::].
+Lemma take0 s : take 0 s = [::].
-Lemma take_oversize n s : size s ≤ n → take n s = s.
+Lemma take_oversize n s : size s ≤ n → take n s = s.
-Lemma take_size s : take (size s) s = s.
+Lemma take_size s : take (size s) s = s.
Lemma take_cons x s :
- take n0 (x :: s) = if n0 is n.+1 then x :: (take n s) else [::].
+ take n0 (x :: s) = if n0 is n.+1 then x :: (take n s) else [::].
-Lemma drop_rcons s : n0 ≤ size s →
- ∀ x, drop n0 (rcons s x) = rcons (drop n0 s) x.
+Lemma drop_rcons s : n0 ≤ size s →
+ ∀ x, drop n0 (rcons s x) = rcons (drop n0 s) x.
-Lemma cat_take_drop s : take n0 s ++ drop n0 s = s.
+Lemma cat_take_drop s : take n0 s ++ drop n0 s = s.
-Lemma size_takel s : n0 ≤ size s → size (take n0 s) = n0.
+Lemma size_takel s : n0 ≤ size s → size (take n0 s) = n0.
-Lemma size_take s : size (take n0 s) = if n0 < size s then n0 else size s.
+Lemma size_take s : size (take n0 s) = if n0 < size s then n0 else size s.
Lemma take_cat s1 s2 :
- take n0 (s1 ++ s2) =
- if n0 < size s1 then take n0 s1 else s1 ++ take (n0 - size s1) s2.
+ take n0 (s1 ++ s2) =
+ if n0 < size s1 then take n0 s1 else s1 ++ take (n0 - size s1) s2.
-Lemma take_size_cat n s1 s2 : size s1 = n → take n (s1 ++ s2) = s1.
+Lemma take_size_cat n s1 s2 : size s1 = n → take n (s1 ++ s2) = s1.
-Lemma takel_cat s1 :
- n0 ≤ size s1 →
- ∀ s2, take n0 (s1 ++ s2) = take n0 s1.
+Lemma takel_cat s1 s2 : n0 ≤ size s1 → take n0 (s1 ++ s2) = take n0 s1.
-Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
+Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
-Lemma nth_take i : i < n0 → ∀ s, nth (take n0 s) i = nth s i.
+Lemma nth_take i : i < n0 → ∀ s, nth (take n0 s) i = nth s i.
@@ -797,10 +823,10 @@
@@ -811,38 +837,35 @@
@@ -852,43 +875,73 @@
-
-
- rev must be defined outside a Section because Coq's end of section
- "cooking" removes the nosimpl guard.
-
-
+
Lemma catrev_catl s t u :
catrev (
s ++ t)
u = catrev t (
catrev s u).
+
+
+
Lemma catrev_catr s t u :
catrev s (
t ++ u)
= catrev s t ++ u.
+
+
+
Lemma catrevE s t :
catrev s t = rev s ++ t.
+
+
+
Lemma rev_cons x s :
rev (
x :: s)
= rcons (
rev s)
x.
+
+
+
Lemma size_rev s :
size (
rev s)
= size s.
+
+
+
Lemma rev_cat s t :
rev (
s ++ t)
= rev t ++ rev s.
+
+
+
Lemma rev_rcons s x :
rev (
rcons s x)
= x :: rev s.
+
+
+
Lemma revK :
involutive rev.
+
+
+
Lemma nth_rev n s :
n < size s → nth (
rev s)
n = nth s (
size s - n.+1).
-
Definition rev T (
s :
seq T) :=
nosimpl (
catrev s [::]).
+
Lemma filter_rev a s :
filter a (
rev s)
= rev (
filter a s).
+
+
+
Lemma count_rev a s :
count a (
rev s)
= count a s.
+
+
+
Lemma has_rev a s :
has a (
rev s)
= has a s.
+
+
+
Lemma all_rev a s :
all a (
rev s)
= all a s.
+
+
+
End Sequences.
-
Notation count_mem x := (
count (
pred_of_simpl (
pred1 x))).
+
Notation count_mem x := (
count (
pred_of_simpl (
pred1 x))).
-
Infix "++" :=
cat :
seq_scope.
+
Infix "++" :=
cat :
seq_scope.
-
Notation "[ 'seq' x <- s | C ]" := (
filter (
fun x ⇒
C%
B)
s)
+
Notation "[ 'seq' x <- s | C ]" := (
filter (
fun x ⇒
C%
B)
s)
(
at level 0,
x at level 99,
format "[ '[hv' 'seq' x <- s '/ ' | C ] ']'") :
seq_scope.
-
Notation "[ 'seq' x <- s | C1 & C2 ]" :=
[seq x <- s | C1 && C2]
+
Notation "[ 'seq' x <- s | C1 & C2 ]" :=
[seq x <- s | C1 && C2]
(
at level 0,
x at level 99,
format "[ '[hv' 'seq' x <- s '/ ' | C1 '/ ' & C2 ] ']'") :
seq_scope.
-
Notation "[ 'seq' x : T <- s | C ]" := (
filter (
fun x :
T ⇒
C%
B)
s)
+
Notation "[ 'seq' x : T <- s | C ]" := (
filter (
fun x :
T ⇒
C%
B)
s)
(
at level 0,
x at level 99,
only parsing).
-
Notation "[ 'seq' x : T <- s | C1 & C2 ]" :=
[seq x : T <- s | C1 && C2]
+
Notation "[ 'seq' x : T <- s | C1 & C2 ]" :=
[seq x : T <- s | C1 && C2]
(
at level 0,
x at level 99,
only parsing).
@@ -898,65 +951,33 @@
Double induction/recursion.
-
Lemma seq2_ind T1 T2 (
P :
seq T1 → seq T2 → Type) :
-
P [::] [::] → (∀ x1 x2 s1 s2,
P s1 s2 → P (
x1 :: s1) (
x2 :: s2)
) →
-
∀ s1 s2,
size s1 = size s2 → P s1 s2.
-
-
-
Section Rev.
+
Lemma seq_ind2 {
S T} (
P :
seq S → seq T → Type) :
+
P [::] [::] →
+
(∀ x y s t,
size s = size t → P s t → P (
x :: s) (
y :: t)
) →
+
∀ s t,
size s = size t → P s t.
-
Variable T :
Type.
-
Implicit Types s t :
seq T.
+
Section RotRcons.
-
Lemma catrev_catl s t u :
catrev (
s ++ t)
u = catrev t (
catrev s u).
-
-
-
Lemma catrev_catr s t u :
catrev s (
t ++ u)
= catrev s t ++ u.
-
-
-
Lemma catrevE s t :
catrev s t = rev s ++ t.
-
-
-
Lemma rev_cons x s :
rev (
x :: s)
= rcons (
rev s)
x.
-
-
-
Lemma size_rev s :
size (
rev s)
= size s.
-
-
-
Lemma rev_cat s t :
rev (
s ++ t)
= rev t ++ rev s.
-
-
-
Lemma rev_rcons s x :
rev (
rcons s x)
= x :: rev s.
-
-
-
Lemma revK :
involutive (@
rev T).
-
-
-
Lemma nth_rev x0 n s :
-
n < size s → nth x0 (
rev s)
n = nth x0 s (
size s - n.+1).
+
Variable T :
Type.
+
Implicit Types (
x :
T) (
s :
seq T).
-
Lemma filter_rev a s :
filter a (
rev s)
= rev (
filter a s).
+
Lemma rot1_cons x s :
rot 1 (
x :: s)
= rcons s x.
-
Lemma count_rev a s :
count a (
rev s)
= count a s.
+
Lemma rcons_inj s1 s2 x1 x2 :
+
rcons s1 x1 = rcons s2 x2 :> seq T → (s1, x1) = (s2, x2).
-
Lemma has_rev a s :
has a (
rev s)
= has a s.
+
Lemma rcons_injl x :
injective (
rcons^~ x).
-
Lemma all_rev a s :
all a (
rev s)
= all a s.
+
Lemma rcons_injr s :
injective (
rcons s).
-
Lemma take_rev s n :
take n (
rev s)
= rev (
drop (
size s - n)
s).
-
-
-
Lemma drop_rev s n :
drop n (
rev s)
= rev (
take (
size s - n)
s).
-
-
-
End Rev.
+
End RotRcons.
@@ -972,16 +993,15 @@
Section EqSeq.
-
Variables (
n0 :
nat) (
T :
eqType) (
x0 :
T).
-
Implicit Type s :
seq T.
-
Implicit Types x y z :
T.
+
Variables (
n0 :
nat) (
T :
eqType) (
x0 :
T).
+
Implicit Types (
x y z :
T) (
s :
seq T).
Fixpoint eqseq s1 s2 {
struct s2} :=
match s1,
s2 with
- |
[::],
[::] ⇒
true
- |
x1 :: s1',
x2 :: s2' ⇒
(x1 == x2) && eqseq s1' s2'
- |
_,
_ ⇒
false
+ |
[::],
[::] ⇒
true
+ |
x1 :: s1',
x2 :: s2' ⇒
(x1 == x2) && eqseq s1' s2'
+ |
_,
_ ⇒
false
end.
@@ -992,25 +1012,25 @@
Canonical seq_eqType :=
Eval hnf in EqType (
seq T)
seq_eqMixin.
-
Lemma eqseqE :
eqseq = eq_op.
+
Lemma eqseqE :
eqseq = eq_op.
Lemma eqseq_cons x1 x2 s1 s2 :
-
(x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).
+
(x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).
Lemma eqseq_cat s1 s2 s3 s4 :
-
size s1 = size s2 → (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).
+
size s1 = size s2 → (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).
Lemma eqseq_rcons s1 s2 x1 x2 :
-
(rcons s1 x1 == rcons s2 x2) = (s1 == s2) && (x1 == x2).
+
(rcons s1 x1 == rcons s2 x2) = (s1 == s2) && (x1 == x2).
-
Lemma size_eq0 s :
(size s == 0
) = (s == [::]).
+
Lemma size_eq0 s :
(size s == 0
) = (s == [::]).
-
Lemma has_filter a s :
has a s = (filter a s != [::]).
+
Lemma has_filter a s :
has a s = (filter a s != [::]).
Fixpoint mem_seq (s : seq T) :=
- if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
-
-
-Definition eqseq_class := seq T.
-Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
+ if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
-Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].
+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 := @mkPredType T (seq T) pred_of_eq_seq.
+Canonical seq_predType := PredType (pred_of_seq : seq T → pred T).
The line below makes mem_seq a canonical instance of topred.
-
Canonical mem_seq_predType :=
mkPredType mem_seq.
+
Canonical mem_seq_predType :=
PredType mem_seq.
-
Lemma in_cons y s x :
(x \in y :: s) = (x == y) || (x \in s).
+
Lemma in_cons y s x :
(x \in y :: s) = (x == y) || (x \in s).
-
Lemma in_nil x :
(x \in [::]) = false.
+
Lemma in_nil x :
(x \in [::]) = false.
-
Lemma mem_seq1 x y :
(x \in [:: y]) = (x == y).
+
Lemma mem_seq1 x y :
(x \in [:: y]) = (x == y).
-
Let inE :=
(mem_seq1, in_cons, inE).
+
Let inE :=
(mem_seq1, in_cons, inE).
-
Lemma mem_seq2 x y1 y2 :
(x \in [:: y1; y2]) = xpred2 y1 y2 x.
+
Lemma mem_seq2 x y z :
(x \in [:: y; z]) = xpred2 y z x.
-
Lemma mem_seq3 x y1 y2 y3 :
(x \in [:: y1; y2; y3]) = xpred3 y1 y2 y3 x.
+
Lemma mem_seq3 x y z t :
(x \in [:: y; z; t]) = xpred3 y z t x.
-
Lemma mem_seq4 x y1 y2 y3 y4 :
-
(x \in [:: y1; y2; y3; y4]) = xpred4 y1 y2 y3 y4 x.
+
Lemma mem_seq4 x y z t u :
(x \in [:: y; z; t; u]) = xpred4 y z t u x.
-
Lemma mem_cat x s1 s2 :
(x \in s1 ++ s2) = (x \in s1) || (x \in s2).
+
Lemma mem_cat x s1 s2 :
(x \in s1 ++ s2) = (x \in s1) || (x \in s2).
-
Lemma mem_rcons s y :
rcons s y =i y :: s.
+
Lemma mem_rcons s y :
rcons s y =i y :: s.
-
Lemma mem_head x s :
x \in x :: s.
+
Lemma mem_head x s :
x \in x :: s.
-
Lemma mem_last x s :
last x s \in x :: s.
+
Lemma mem_last x s :
last x s \in x :: s.
-
Lemma mem_behead s :
{subset behead s ≤ s}.
+
Lemma mem_behead s :
{subset behead s ≤ s}.
-
Lemma mem_belast s y :
{subset belast y s ≤ y :: s}.
+
Lemma mem_belast s y :
{subset belast y s ≤ y :: s}.
-
Lemma mem_nth s n :
n < size s → nth s n \in s.
+
Lemma mem_nth s n :
n < size s → nth s n \in s.
-
Lemma mem_take s x :
x \in take n0 s → x \in s.
+
Lemma mem_take s x :
x \in take n0 s → x \in s.
-
Lemma mem_drop s x :
x \in drop n0 s → x \in s.
+
Lemma mem_drop s x :
x \in drop n0 s → x \in s.
+
+
+
Lemma last_eq s z x y :
x != y → z != y → (last x s == y) = (last z s == y).
Section Filters.
-
Variable a :
pred T.
+
Implicit Type a :
pred T.
-
Lemma hasP s :
reflect (
exists2 x, x \in s & a x) (
has a s).
+
Lemma hasP {
a s} :
reflect (
exists2 x, x \in s & a x) (
has a s).
-
Lemma hasPn s :
reflect (
∀ x,
x \in s → ~~ a x) (
~~ has a s).
+
Lemma allP {
a s} :
reflect {in s, ∀ x,
a x} (
all a s).
-
Lemma allP s :
reflect (
∀ x,
x \in s → a x) (
all a s).
-
+
Lemma hasPn a s :
reflect {in s, ∀ x,
~~ a x} (
~~ has a s).
+
+
+
Lemma allPn a s :
reflect (
exists2 x, x \in s & ~~ a x) (
~~ all a s).
+
-
Lemma allPn s :
reflect (
exists2 x, x \in s & ~~ a x) (
~~ all a s).
+
Lemma mem_filter a x s :
(x \in filter a s) = a x && (x \in s).
-
Lemma mem_filter x s :
(x \in filter a s) = a x && (x \in s).
+
Variables (
a :
pred T) (
s :
seq T) (
A :
T → Prop).
+
Hypothesis aP :
∀ x,
reflect (
A x) (
a x).
+
+
Lemma hasPP :
reflect (
exists2 x, x \in s & A x) (
has a s).
+
+
+
Lemma allPP :
reflect {in s, ∀ x,
A x} (
all a s).
+
End Filters.
+
+
Notation "'has_ view" := (
hasPP _ (
fun _ ⇒
view))
+ (
at level 4,
right associativity,
format "''has_' view").
+
Notation "'all_ view" := (
allPP _ (
fun _ ⇒
view))
+ (
at level 4,
right associativity,
format "''all_' view").
+
Section EqIn.
-
Variables a1 a2 :
pred T.
+
Variables a1 a2 :
pred T.
-
Lemma eq_in_filter s :
{in s, a1 =1 a2} → filter a1 s = filter a2 s.
+
Lemma eq_in_filter s :
{in s, a1 =1 a2} → filter a1 s = filter a2 s.
-
Lemma eq_in_find s :
{in s, a1 =1 a2} → find a1 s = find a2 s.
+
Lemma eq_in_find s :
{in s, a1 =1 a2} → find a1 s = find a2 s.
-
Lemma eq_in_count s :
{in s, a1 =1 a2} → count a1 s = count a2 s.
+
Lemma eq_in_count s :
{in s, a1 =1 a2} → count a1 s = count a2 s.
-
Lemma eq_in_all s :
{in s, a1 =1 a2} → all a1 s = all a2 s.
+
Lemma eq_in_all s :
{in s, a1 =1 a2} → all a1 s = all a2 s.
-
Lemma eq_in_has s :
{in s, a1 =1 a2} → has a1 s = has a2 s.
+
Lemma eq_in_has s :
{in s, a1 =1 a2} → has a1 s = has a2 s.
End EqIn.
-
Lemma eq_has_r s1 s2 :
s1 =i s2 → has^~ s1 =1 has^~ s2.
+
Lemma eq_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 eq_all_r s1 s2 :
s1 =i s2 → all^~ s1 =1 all^~ s2.
+
-
Lemma has_sym s1 s2 :
has (
mem s1)
s2 = has (
mem s2)
s1.
+
Lemma has_sym s1 s2 :
has (
mem s1)
s2 = has (
mem s2)
s1.
-
Lemma has_pred1 x s :
has (
pred1 x)
s = (x \in s).
+
Lemma has_pred1 x s :
has (
pred1 x)
s = (x \in s).
-
Lemma mem_rev s :
rev s =i s.
+
Lemma mem_rev s :
rev s =i s.
Fixpoint undup s :=
- if s is x :: s' then if x \in s' then undup s' else x :: undup s' else [::].
+ 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 size_undup s : size (undup s) ≤ size s.
-Lemma mem_undup s : undup s =i s.
+Lemma mem_undup s : undup s =i s.
Lemma undup_uniq s : uniq (undup s).
-Lemma undup_id s : uniq s → undup s = s.
+Lemma undup_id s : uniq s → undup s = s.
-Lemma ltn_size_undup s : (size (undup s) < size s) = ~~ uniq s.
+Lemma ltn_size_undup s : (size (undup s) < size s) = ~~ uniq s.
-Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
+Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
-Lemma undup_nil s : undup s = [::] → s = [::].
+Lemma undup_nil s : undup s = [::] → s = [::].
@@ -1280,55 +1319,58 @@
Definition index x := find (pred1 x).
-Lemma index_size x s : index x s ≤ size s.
+Lemma index_size x s : index x s ≤ size s.
-Lemma index_mem x s : (index x s < size s) = (x \in s).
+Lemma index_mem x s : (index x s < size s) = (x \in s).
-Lemma nth_index x s : x \in s → nth s (index x s) = x.
+Lemma nth_index x s : x \in s → nth s (index x s) = x.
Lemma index_cat x s1 s2 :
- index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2.
+ index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2.
-Lemma index_uniq i s : i < size s → uniq s → index (nth s i) s = i.
+Lemma nthK s: uniq s → {in gtn (size s), cancel (nth s) (index^~ s)}.
-Lemma index_head x s : index x (x :: s) = 0.
+Lemma index_uniq i s : i < size s → uniq s → index (nth s i) s = i.
-Lemma index_last x s : uniq (x :: s) → index (last x s) (x :: s) = size s.
+Lemma index_head x s : index x (x :: s) = 0.
+
+
+Lemma index_last x s : uniq (x :: s) → index (last x s) (x :: s) = size s.
Lemma nth_uniq s i j :
- i < size s → j < size s → uniq s → (nth s i == nth s j) = (i == j).
-
+ i < size s → j < size s → uniq s → (nth s i == nth s j) = (i == j).
+
Lemma uniqPn s :
- reflect (∃ i j, [/\ i < j, j < size s & nth s i = nth s j]) (~~ uniq s).
+ reflect (∃ i j, [/\ i < j, j < size s & nth s i = nth s j]) (~~ uniq s).
-Lemma uniqP s : reflect {in [pred i | i < size s] &, injective (nth s)} (uniq s).
+Lemma uniqP s : reflect {in gtn (size s) &, injective (nth s)} (uniq s).
-Lemma mem_rot s : rot n0 s =i s.
+Lemma mem_rot s : rot n0 s =i s.
-Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
+Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
-CoInductive rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
+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.
+Lemma rot_to s x : x \in s → rot_to_spec s x.
End EqSeq.
-Definition inE := (mem_seq1, in_cons, inE).
+Definition inE := (mem_seq1, in_cons, inE).
@@ -1339,34 +1381,34 @@
Lemma nthP (T : eqType) (s : seq T) x x0 :
- reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s).
+ reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s).
Variable T : Type.
-Lemma has_nthP (a : pred T) s x0 :
- reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).
+Lemma has_nthP (a : pred T) s x0 :
+ reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).
-Lemma all_nthP (a : pred T) s x0 :
- reflect (∀ i, i < size s → a (nth x0 s i)) (all a s).
+Lemma all_nthP (a : pred T) s x0 :
+ reflect (∀ i, i < size s → a (nth x0 s i)) (all a s).
End NthTheory.
-Lemma set_nth_default T s (y0 x0 : T) n : n < size s → nth x0 s n = nth y0 s n.
+Lemma set_nth_default T s (y0 x0 : T) n : n < size s → nth x0 s n = nth y0 s n.
-Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x).
+Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x).
-Definition bitseq := seq bool.
-Canonical bitseq_eqType := Eval hnf in [eqType of bitseq].
-Canonical bitseq_predType := Eval hnf in [predType of bitseq].
+Definition bitseq := seq bool.
+Canonical bitseq_eqType := Eval hnf in [eqType of bitseq].
+Canonical bitseq_predType := Eval hnf in [predType of bitseq].
@@ -1379,22 +1421,22 @@
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].
+ if v is n :: v' then if i is i'.+1 then n :: incr_nth v' i' else n.+1 :: v'
+ else ncons i 0 [:: 1].
-Lemma nth_incr_nth v i j : nth 0 (incr_nth v i) j = (i == j) + nth 0 v j.
+Lemma nth_incr_nth v i j : nth 0 (incr_nth v i) j = (i == j) + nth 0 v j.
Lemma size_incr_nth v i :
- size (incr_nth v i) = if i < size v then size v else i.+1.
+ size (incr_nth v i) = if i < size v then size v else i.+1.
-Lemma incr_nth_inj v : injective (incr_nth v).
+Lemma incr_nth_inj v : injective (incr_nth v).
Lemma incr_nthC v i j :
- incr_nth (incr_nth v i) j = incr_nth (incr_nth v j) i.
+ incr_nth (incr_nth v i) j = incr_nth (incr_nth v j) i.
@@ -1413,54 +1455,64 @@
Definition perm_eq s1 s2 :=
- all [pred x | count_mem x s1 == count_mem x s2] (s1 ++ s2).
+ all [pred x | count_mem x s1 == count_mem x s2] (s1 ++ s2).
-Lemma perm_eqP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).
+Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).
-Lemma perm_eq_refl s : perm_eq s s.
- Hint Resolve perm_eq_refl.
+Lemma perm_refl s : perm_eq s s.
+ Hint Resolve perm_refl : core.
-Lemma perm_eq_sym : symmetric perm_eq.
+Lemma perm_sym : symmetric perm_eq.
-Lemma perm_eq_trans : transitive 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).
+Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
+Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2).
-Lemma perm_eqlE s1 s2 : perm_eql s1 s2 → perm_eq s1 s2.
+Lemma permEl s1 s2 : perm_eql s1 s2 → perm_eq s1 s2.
-Lemma perm_eqlP s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
+Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
-Lemma perm_eqrP s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2).
+Lemma 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_catC s1 s2 : perm_eql (s1 ++ s2) (s2 ++ s1).
-Lemma perm_cat2l s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.
+Lemma perm_cat2l s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.
-Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.
+Lemma perm_catl s t1 t2 : perm_eq t1 t2 → perm_eql (s ++ t1) (s ++ t2).
+
+
+Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.
+
+
+Lemma perm_cat2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.
+
+
+Lemma perm_catr s1 s2 t : perm_eq s1 s2 → perm_eql (s1 ++ t) (s2 ++ t).
-Lemma perm_cat2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.
+Lemma perm_cat s1 s2 t1 t2 :
+ perm_eq s1 s2 → perm_eq t1 t2 → perm_eq (s1 ++ t1) (s2 ++ t2).
-Lemma perm_catAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).
+Lemma perm_catAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).
-Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).
+Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).
-Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s).
+Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s).
Lemma perm_rot n s : perm_eql (rot n s) s.
@@ -1469,115 +1521,137 @@
Lemma perm_rotr n s : perm_eql (rotr n s) s.
-Lemma perm_eq_rev s : perm_eq s (rev s).
+Lemma perm_rev s : perm_eql (rev s) s.
-Lemma perm_filter s1 s2 P :
- perm_eq s1 s2 → perm_eq (filter P s1) (filter P s2).
+Lemma perm_filter s1 s2 a :
+ perm_eq s1 s2 → perm_eq (filter a s1) (filter a s2).
-Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
+Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
-Lemma perm_eq_mem s1 s2 : perm_eq s1 s2 → s1 =i s2.
+Lemma perm_size s1 s2 : perm_eq s1 s2 → size s1 = size s2.
-Lemma perm_eq_all s1 s2 P : perm_eq s1 s2 → all P s1 = all P s2.
+Lemma perm_mem s1 s2 : perm_eq s1 s2 → s1 =i s2.
-Lemma perm_eq_size s1 s2 : perm_eq s1 s2 → size s1 = size s2.
+Lemma perm_nilP s : reflect (s = [::]) (perm_eq s [::]).
-Lemma perm_eq_small s1 s2 : size s2 ≤ 1 → perm_eq s1 s2 → s1 = s2.
+Lemma perm_consP x s t :
+ reflect (∃ i u, rot i t = x :: u ∧ perm_eq u s)
+ (perm_eq t (x :: s)).
-Lemma uniq_leq_size s1 s2 : uniq s1 → {subset s1 ≤ s2} → size s1 ≤ size s2.
+Lemma perm_has s1 s2 a : perm_eq s1 s2 → has a s1 = has a s2.
+
+
+Lemma perm_all s1 s2 a : perm_eq s1 s2 → all a s1 = all a s2.
+
+
+Lemma perm_small_eq s1 s2 : size s2 ≤ 1 → perm_eq s1 s2 → s1 = s2.
+
+
+Lemma uniq_leq_size s1 s2 : uniq s1 → {subset s1 ≤ s2} → size s1 ≤ size s2.
Lemma leq_size_uniq s1 s2 :
- uniq s1 → {subset s1 ≤ s2} → size s2 ≤ size s1 → uniq s2.
+ uniq s1 → {subset s1 ≤ s2} → size s2 ≤ size s1 → uniq s2.
Lemma uniq_size_uniq s1 s2 :
- uniq s1 → s1 =i s2 → uniq s2 = (size s2 == size s1).
+ uniq s1 → s1 =i s2 → uniq s2 = (size s2 == size s1).
-Lemma leq_size_perm s1 s2 :
- uniq s1 → {subset s1 ≤ s2} → size s2 ≤ size s1 →
- s1 =i s2 ∧ size s1 = size s2.
+Lemma uniq_min_size s1 s2 :
+ uniq s1 → {subset s1 ≤ s2} → size s2 ≤ size s1 →
+ (size s1 = size s2) × (s1 =i s2).
-Lemma perm_uniq s1 s2 : s1 =i s2 → size s1 = size s2 → uniq s1 = uniq s2.
+Lemma eq_uniq s1 s2 : size s1 = size s2 → s1 =i s2 → uniq s1 = uniq s2.
-Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 → uniq s1 = uniq s2.
+Lemma perm_uniq s1 s2 : perm_eq s1 s2 → uniq s1 = uniq s2.
+
+
+Lemma uniq_perm s1 s2 : uniq s1 → uniq s2 → s1 =i s2 → perm_eq s1 s2.
-Lemma uniq_perm_eq s1 s2 : uniq s1 → uniq s2 → s1 =i s2 → perm_eq s1 s2.
+Lemma perm_undup s1 s2 : s1 =i s2 → perm_eq (undup s1) (undup s2).
-Lemma count_mem_uniq s : (∀ x, count_mem x s = (x \in s)) → uniq s.
+Lemma count_mem_uniq s : (∀ x, count_mem x s = (x \in s)) → uniq s.
Lemma catCA_perm_ind P :
- (∀ s1 s2 s3, P (s1 ++ s2 ++ s3) → P (s2 ++ s1 ++ s3)) →
- (∀ s1 s2, perm_eq s1 s2 → P s1 → P s2).
+ (∀ s1 s2 s3, P (s1 ++ s2 ++ s3) → P (s2 ++ s1 ++ s3)) →
+ (∀ s1 s2, perm_eq s1 s2 → P s1 → P s2).
Lemma catCA_perm_subst R F :
- (∀ s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R) →
- (∀ s1 s2, perm_eq s1 s2 → F s1 = F s2).
+ (∀ s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R) →
+ (∀ s1 s2, perm_eq s1 s2 → F s1 = F s2).
End PermSeq.
-Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
-Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2).
+Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
+Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2).
-Hint Resolve perm_eq_refl.
+Hint Resolve perm_refl : core.
Section RotrLemmas.
-Variables (n0 : nat) (T : Type) (T' : eqType).
-Implicit Type s : seq T.
+Variables (n0 : nat) (T : Type) (T' : eqType).
+Implicit Types (x : T) (s : seq T).
-Lemma size_rotr s : size (rotr n0 s) = size s.
+Lemma size_rotr s : size (rotr n0 s) = size s.
-Lemma mem_rotr (s : seq T') : rotr n0 s =i s.
+Lemma mem_rotr (s : seq T') : rotr n0 s =i s.
-Lemma rotr_size_cat s1 s2 : rotr (size s2) (s1 ++ s2) = s2 ++ s1.
+Lemma rotr_size_cat s1 s2 : rotr (size s2) (s1 ++ s2) = s2 ++ s1.
-Lemma rotr1_rcons x s : rotr 1 (rcons s x) = x :: s.
+Lemma rotr1_rcons x s : rotr 1 (rcons s x) = x :: s.
-Lemma has_rotr a s : has a (rotr n0 s) = has a s.
+Lemma has_rotr a s : has a (rotr n0 s) = has a s.
-Lemma rotr_uniq (s : seq T') : uniq (rotr n0 s) = uniq s.
+Lemma rotr_uniq (s : seq T') : uniq (rotr n0 s) = uniq s.
-Lemma rotrK : cancel (@rotr T n0) (rot n0).
+Lemma rotrK : cancel (@rotr T n0) (rot n0).
-Lemma rotr_inj : injective (@rotr T n0).
+Lemma rotr_inj : injective (@rotr T n0).
-Lemma rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).
+Lemma take_rev s : take n0 (rev s) = rev (drop (size s - n0) s).
+
+
+Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).
+
+
+Lemma rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).
-Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).
+Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).
End RotrLemmas.
+
+
Section RotCompLemmas.
@@ -1586,23 +1660,23 @@
Implicit Type s : seq T.
-Lemma rot_addn m n s : m + n ≤ size s → rot (m + n) s = rot m (rot n s).
+Lemma rot_addn m n s : m + n ≤ size s → rot (m + n) s = rot m (rot n s).
-Lemma rotS n s : n < size s → rot n.+1 s = rot 1 (rot n s).
+Lemma rotS n s : n < size s → rot n.+1 s = rot 1 (rot n s).
-Lemma rot_add_mod m n s : n ≤ size s → m ≤ size s →
- rot m (rot n s) = rot (if m + n ≤ size s then m + n else m + n - size s) s.
+Lemma rot_add_mod m n s : n ≤ size s → m ≤ size s →
+ rot m (rot n s) = rot (if m + n ≤ size s then m + n else m + n - size s) s.
-Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s).
+Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s).
-Lemma rot_rotr m n s : rot m (rotr n s) = rotr n (rot m s).
+Lemma 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).
+Lemma rotr_rotr m n s : rotr m (rotr n s) = rotr n (rotr m s).
End RotCompLemmas.
@@ -1611,51 +1685,51 @@
Section Mask.
-Variables (n0 : nat) (T : Type).
+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'
- | _, _ ⇒ [::]
+ | b :: m', x :: s' ⇒ if b then x :: mask m' s' else mask m' s'
+ | _, _ ⇒ [::]
end.
-Lemma mask_false s n : mask (nseq n false) s = [::].
+Lemma mask_false s n : mask (nseq n false) s = [::].
-Lemma mask_true s n : size s ≤ n → mask (nseq n true) s = s.
+Lemma mask_true s n : size s ≤ n → mask (nseq n true) s = s.
-Lemma mask0 m : mask m [::] = [::].
+Lemma mask0 m : mask m [::] = [::].
-Lemma mask1 b x : mask [:: b] [:: x] = nseq b x.
+Lemma mask1 b x : mask [:: b] [:: x] = nseq b x.
-Lemma mask_cons b m x s : mask (b :: m) (x :: s) = nseq b x ++ mask m s.
+Lemma mask_cons b m x s : mask (b :: m) (x :: s) = nseq b x ++ mask m s.
-Lemma size_mask m s : size m = size s → size (mask m s) = count id m.
+Lemma size_mask m s : size m = size s → size (mask m s) = count id m.
Lemma mask_cat m1 m2 s1 s2 :
- size m1 = size s1 → mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.
+ size m1 = size s1 → mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.
Lemma has_mask_cons a b m x s :
- has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).
+ has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).
-Lemma has_mask a m s : has a (mask m s) → has a s.
+Lemma has_mask a m s : has a (mask m s) → has a s.
-Lemma mask_rot m s : size m = size s →
- mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s).
+Lemma mask_rot m s : size m = size s →
+ mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s).
-Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s}.
+Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s}.
End Mask.
@@ -1664,22 +1738,22 @@
Section EqMask.
-Variables (n0 : nat) (T : eqType).
+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).
+ (x \in mask (b :: m) (y :: s)) = b && (x == y) || (x \in mask m s).
-Lemma mem_mask x m s : x \in mask m s → x \in s.
+Lemma mem_mask x m s : x \in mask m s → x \in s.
-Lemma mask_uniq s : uniq s → ∀ m, uniq (mask m s).
+Lemma mask_uniq s : uniq s → ∀ m, uniq (mask m s).
Lemma mem_mask_rot m s :
- size m = size s → mask (rot n0 m) (rot n0 s) =i mask m s.
+ size m = size s → mask (rot n0 m) (rot n0 s) =i mask m s.
End EqMask.
@@ -1693,61 +1767,67 @@
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 == [::].
+ if s2 is y :: s2' then
+ if s1 is x :: s1' then subseq (if x == y then s1' else s1) s2' else true
+ else s1 == [::].
-Lemma sub0seq s : subseq [::] s.
+Lemma sub0seq s : subseq [::] s.
-Lemma subseq0 s : subseq s [::] = (s == [::]).
+Lemma subseq0 s : subseq s [::] = (s == [::]).
+
+
+Lemma subseq_refl s : subseq s s.
+ Hint Resolve subseq_refl : core.
Lemma subseqP s1 s2 :
- reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2).
+ reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2).
Lemma mask_subseq m s : subseq (mask m s) s.
-Lemma subseq_trans : transitive subseq.
-
-
-Lemma subseq_refl s : subseq s s.
- Hint Resolve subseq_refl.
+Lemma subseq_trans : transitive subseq.
Lemma cat_subseq s1 s2 s3 s4 :
- subseq s1 s3 → subseq s2 s4 → subseq (s1 ++ s2) (s3 ++ s4).
+ subseq s1 s3 → subseq s2 s4 → subseq (s1 ++ s2) (s3 ++ s4).
-Lemma prefix_subseq s1 s2 : subseq s1 (s1 ++ s2).
+Lemma prefix_subseq s1 s2 : subseq s1 (s1 ++ s2).
-Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2).
+Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2).
-Lemma mem_subseq s1 s2 : subseq s1 s2 → {subset s1 ≤ s2}.
+Lemma take_subseq s i : subseq (take i s) s.
-Lemma sub1seq x s : subseq [:: x] s = (x \in s).
+Lemma drop_subseq s i : subseq (drop i s) s.
+
+
+Lemma mem_subseq s1 s2 : subseq s1 s2 → {subset s1 ≤ s2}.
+
+
+Lemma sub1seq x s : subseq [:: x] s = (x \in s).
-Lemma size_subseq s1 s2 : subseq s1 s2 → size s1 ≤ size s2.
+Lemma size_subseq s1 s2 : subseq s1 s2 → size s1 ≤ size s2.
Lemma size_subseq_leqif s1 s2 :
- subseq s1 s2 → size s1 ≤ size s2 ?= iff (s1 == s2).
+ subseq s1 s2 → size s1 ≤ size s2 ?= iff (s1 == s2).
-Lemma subseq_cons s x : subseq s (x :: s).
+Lemma subseq_cons s x : subseq s (x :: s).
Lemma subseq_rcons s x : subseq s (rcons s x).
-Lemma subseq_uniq s1 s2 : subseq s1 s2 → uniq s2 → uniq s1.
+Lemma subseq_uniq s1 s2 : subseq s1 s2 → uniq s2 → uniq s1.
End Subseq.
@@ -1755,7 +1835,7 @@
-Hint Resolve subseq_refl.
+Hint Resolve subseq_refl : core.
Section Rem.
@@ -1764,31 +1844,34 @@
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.
+Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s.
-Lemma rem_id s : x \notin s → rem s = s.
+Lemma rem_id s : x \notin s → rem s = s.
-Lemma perm_to_rem s : x \in s → perm_eq s (x :: rem s).
+Lemma perm_to_rem s : x \in s → perm_eq s (x :: rem s).
-Lemma size_rem s : x \in s → size (rem s) = (size s).-1.
+Lemma size_rem s : x \in s → size (rem s) = (size s).-1.
Lemma rem_subseq s : subseq (rem s) s.
-Lemma rem_uniq s : uniq s → uniq (rem s).
+Lemma rem_uniq s : uniq s → uniq (rem s).
-Lemma mem_rem s : {subset rem s ≤ s}.
+Lemma mem_rem s : {subset rem s ≤ s}.
-Lemma rem_filter s : uniq s → rem s = filter (predC1 x) s.
+Lemma rem_filter s : uniq s → rem s = filter (predC1 x) s.
-Lemma mem_rem_uniq s : uniq s → rem s =i [predD1 s & x].
+Lemma mem_rem_uniq s : uniq s → rem s =i [predD1 s & x].
+
+
+Lemma mem_rem_uniqF s : uniq s → x \in rem s = false.
End Rem.
@@ -1797,121 +1880,138 @@
Section Map.
-Variables (n0 : nat) (T1 : Type) (x1 : T1).
-Variables (T2 : Type) (x2 : T2) (f : T1 → T2).
+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 [::].
+Fixpoint map s := if s is x :: s' then f x :: map s' else [::].
-Lemma map_cons x s : map (x :: s) = f x :: map s.
+Lemma map_cons x s : map (x :: s) = f x :: map s.
-Lemma map_nseq x : map (nseq n0 x) = nseq n0 (f x).
+Lemma map_nseq x : map (nseq n0 x) = nseq n0 (f x).
-Lemma map_cat s1 s2 : map (s1 ++ s2) = map s1 ++ map s2.
+Lemma map_cat s1 s2 : map (s1 ++ s2) = map s1 ++ map s2.
-Lemma size_map s : size (map s) = size s.
+Lemma size_map s : size (map s) = size s.
-Lemma behead_map s : behead (map s) = map (behead s).
+Lemma behead_map s : behead (map s) = map (behead s).
-Lemma nth_map n s : n < size s → nth x2 (map s) n = f (nth x1 s n).
+Lemma nth_map n s : n < size s → nth x2 (map s) n = f (nth x1 s n).
-Lemma map_rcons s x : map (rcons s x) = rcons (map s) (f x).
+Lemma map_rcons s x : map (rcons s x) = rcons (map s) (f x).
-Lemma last_map s x : last (f x) (map s) = f (last x s).
+Lemma last_map s x : last (f x) (map s) = f (last x s).
-Lemma belast_map s x : belast (f x) (map s) = map (belast x s).
+Lemma belast_map s x : belast (f x) (map s) = map (belast x s).
-Lemma filter_map a s : filter a (map s) = map (filter (preim f a) s).
+Lemma filter_map a s : filter a (map s) = map (filter (preim f a) s).
-Lemma find_map a s : find a (map s) = find (preim f a) s.
+Lemma find_map a s : find a (map s) = find (preim f a) s.
-Lemma has_map a s : has a (map s) = has (preim f a) s.
+Lemma has_map a s : has a (map s) = has (preim f a) s.
-Lemma all_map a s : all a (map s) = all (preim f a) s.
+Lemma all_map a s : all a (map s) = all (preim f a) s.
-Lemma count_map a s : count a (map s) = count (preim f a) s.
+Lemma count_map a s : count a (map s) = count (preim f a) s.
-Lemma map_take s : map (take n0 s) = take n0 (map s).
+Lemma map_take s : map (take n0 s) = take n0 (map s).
-Lemma map_drop s : map (drop n0 s) = drop n0 (map s).
+Lemma map_drop s : map (drop n0 s) = drop n0 (map s).
-Lemma map_rot s : map (rot n0 s) = rot n0 (map s).
+Lemma map_rot s : map (rot n0 s) = rot n0 (map s).
-Lemma map_rotr s : map (rotr n0 s) = rotr 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_rev s : map (rev s) = rev (map s).
-Lemma map_mask m s : map (mask m s) = mask m (map s).
+Lemma map_mask m s : map (mask m s) = mask m (map s).
-Lemma inj_map : injective f → injective map.
+Lemma inj_map : injective f → injective map.
End Map.
-Notation "[ 'seq' E | i <- s ]" := (map (fun i ⇒ E) s)
+Notation "[ 'seq' E | i <- s ]" := (map (fun i ⇒ E) s)
(at level 0, E at level 99, i ident,
format "[ '[hv' 'seq' E '/ ' | i <- s ] ']'") : seq_scope.
-Notation "[ 'seq' E | i <- s & C ]" := [seq E | i <- [seq i <- s | C]]
+Notation "[ 'seq' E | i <- s & C ]" := [seq E | i <- [seq i <- s | C]]
(at level 0, E at level 99, i ident,
format "[ '[hv' 'seq' E '/ ' | i <- s '/ ' & C ] ']'") : seq_scope.
-Notation "[ 'seq' E | i : T <- s ]" := (map (fun i : T ⇒ E) s)
+Notation "[ 'seq' E | i : T <- s ]" := (map (fun i : T ⇒ E) s)
+ (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+
+Notation "[ 'seq' E | i : T <- s & C ]" :=
+ [seq E | i : T <- [seq i : T <- s | C]]
+ (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+
+Notation "[ 'seq' E : R | i <- s ]" := (@map _ R (fun i ⇒ E) s)
+ (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+
+Notation "[ 'seq' E : R | i <- s & C ]" := [seq E : R | i <- [seq i <- s | C]]
+ (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+
+Notation "[ 'seq' E : R | i : T <- s ]" := (@map T R (fun i : T ⇒ E) s)
(at level 0, E at level 99, i ident, only parsing) : seq_scope.
-Notation "[ 'seq' E | i : T <- s & C ]" :=
- [seq E | i : T <- [seq i : T <- s | C]]
+Notation "[ 'seq' E : R | i : T <- s & C ]" :=
+ [seq E : R | i : T <- [seq i : T <- s | C]]
(at level 0, E at level 99, i ident, only parsing) : seq_scope.
-Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
+Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
Section FilterSubseq.
Variable T : eqType.
-Implicit Types (s : seq T) (a : pred T).
+Implicit Types (s : seq T) (a : pred T).
Lemma filter_subseq a s : subseq (filter a s) s.
Lemma subseq_filter s1 s2 a :
- subseq s1 (filter a s2) = all a s1 && subseq s1 s2.
+ subseq s1 (filter a s2) = all a s1 && subseq s1 s2.
Lemma subseq_uniqP s1 s2 :
- uniq s2 → reflect (s1 = filter (mem s1) s2) (subseq s1 s2).
+ uniq s2 → reflect (s1 = filter (mem s1) s2) (subseq s1 s2).
Lemma perm_to_subseq s1 s2 :
- subseq s1 s2 → {s3 | perm_eq s2 (s1 ++ s3)}.
+ subseq s1 s2 → {s3 | perm_eq s2 (s1 ++ s3)}.
End FilterSubseq.
@@ -1922,44 +2022,47 @@
Section EqMap.
-Variables (n0 : nat) (T1 : eqType) (x1 : T1).
-Variables (T2 : eqType) (x2 : T2) (f : T1 → T2).
+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 map_f s x : x \in s → f x \in map f s.
-Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s).
+Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s).
-Lemma map_uniq s : uniq (map f s) → uniq s.
+Lemma map_uniq s : uniq (map f s) → uniq s.
-Lemma map_inj_in_uniq s : {in s &, injective f} → uniq (map f s) = uniq s.
+Lemma map_inj_in_uniq s : {in s &, injective f} → uniq (map f s) = uniq s.
-Lemma map_subseq s1 s2 : subseq s1 s2 → subseq (map f s1) (map f s2).
+Lemma map_subseq s1 s2 : subseq s1 s2 → subseq (map f s1) (map f s2).
Lemma nth_index_map s x0 x :
- {in s &, injective f} → x \in s → nth x0 s (index (f x) (map f s)) = x.
+ {in s &, injective f} → x \in s → nth x0 s (index (f x) (map f s)) = x.
-Lemma perm_map s t : perm_eq s t → perm_eq (map f s) (map f t).
+Lemma perm_map s t : perm_eq s t → perm_eq (map f s) (map f t).
-Hypothesis Hf : injective f.
+Hypothesis Hf : injective f.
-Lemma mem_map s x : (f x \in map f s) = (x \in s).
+Lemma mem_map s x : (f x \in map f s) = (x \in s).
-Lemma index_map s x : index (f x) (map f s) = index x s.
+Lemma index_map s x : index (f x) (map f s) = index x s.
-Lemma map_inj_uniq s : uniq (map f s) = uniq s.
+Lemma map_inj_uniq s : uniq (map f s) = uniq s.
+
+Lemma perm_map_inj s t : perm_eq (map f s) (map f t) → perm_eq s t.
+
End EqMap.
@@ -1967,7 +2070,7 @@
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}.
+ {f | uniq s → size fs = size s → map f s = fs}.
Section MapComp.
@@ -1976,28 +2079,28 @@
Variable T1 T2 T3 : Type.
-Lemma map_id (s : seq T1) : map id s = s.
+Lemma map_id (s : seq T1) : map id s = s.
-Lemma eq_map (f1 f2 : T1 → T2) : f1 =1 f2 → map f1 =1 map f2.
+Lemma eq_map (f1 f2 : T1 → T2) : f1 =1 f2 → map f1 =1 map f2.
-Lemma map_comp (f1 : T2 → T3) (f2 : T1 → T2) s :
- map (f1 \o f2) s = map f1 (map f2 s).
+Lemma map_comp (f1 : T2 → T3) (f2 : T1 → T2) s :
+ map (f1 \o f2) s = map f1 (map f2 s).
-Lemma mapK (f1 : T1 → T2) (f2 : T2 → T1) :
- cancel f1 f2 → cancel (map f1) (map f2).
+Lemma mapK (f1 : T1 → T2) (f2 : T2 → T1) :
+ cancel f1 f2 → cancel (map f1) (map f2).
End MapComp.
-Lemma eq_in_map (T1 : eqType) T2 (f1 f2 : T1 → T2) (s : seq T1) :
- {in s, f1 =1 f2} ↔ map f1 s = map f2 s.
+Lemma eq_in_map (T1 : eqType) T2 (f1 f2 : T1 → T2) (s : seq T1) :
+ {in s, f1 =1 f2} ↔ map f1 s = map f2 s.
-Lemma map_id_in (T : eqType) f (s : seq T) : {in s, f =1 id} → map f s = s.
+Lemma map_id_in (T : eqType) f (s : seq T) : {in s, f =1 id} → map f s = s.
@@ -2011,26 +2114,29 @@
Section Pmap.
-Variables (aT rT : Type) (f : aT → option rT) (g : rT → aT).
+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 [::].
+ if s is x :: s' then let r := pmap s' in oapp (cons^~ r) r (f x) else [::].
-Lemma map_pK : pcancel g f → cancel (map g) pmap.
+Lemma map_pK : pcancel g f → cancel (map g) pmap.
-Lemma size_pmap s : size (pmap s) = count [eta f] s.
+Lemma size_pmap s : size (pmap s) = count [eta f] s.
-Lemma pmapS_filter s : map some (pmap s) = map f (filter [eta f] s).
+Lemma pmapS_filter s : map some (pmap s) = map f (filter [eta f] s).
-Hypothesis fK : ocancel f g.
+Hypothesis fK : ocancel f g.
-Lemma pmap_filter s : map g (pmap s) = filter [eta f] s.
+Lemma pmap_filter s : map g (pmap s) = filter [eta f] s.
+
+
+Lemma pmap_cat s t : pmap (s ++ t) = pmap s ++ pmap t.
End Pmap.
@@ -2039,22 +2145,25 @@
Section EqPmap.
-Variables (aT rT : eqType) (f : aT → option rT) (g : rT → aT).
+Variables (aT rT : eqType) (f : aT → option rT) (g : rT → aT).
-Lemma eq_pmap (f1 f2 : aT → option rT) : f1 =1 f2 → pmap f1 =1 pmap f2.
+Lemma eq_pmap (f1 f2 : aT → option rT) : f1 =1 f2 → pmap f1 =1 pmap f2.
-Lemma mem_pmap s u : (u \in pmap f s) = (Some u \in map f s).
+Lemma mem_pmap s u : (u \in pmap f s) = (Some u \in map f s).
-Hypothesis fK : ocancel f g.
+Hypothesis fK : ocancel f g.
+
+
+Lemma can2_mem_pmap : pcancel g f → ∀ s u, (u \in pmap f s) = (g u \in s).
-Lemma can2_mem_pmap : pcancel g f → ∀ s u, (u \in pmap f s) = (g u \in s).
+Lemma pmap_uniq s : uniq s → uniq (pmap f s).
-Lemma pmap_uniq s : uniq s → uniq (pmap f s).
+Lemma perm_pmap s t : perm_eq s t → perm_eq (pmap f s) (pmap f t).
End EqPmap.
@@ -2063,10 +2172,10 @@
Section PmapSub.
-Variables (T : Type) (p : pred T) (sT : subType p).
+Variables (T : Type) (p : pred T) (sT : subType p).
-Lemma size_pmap_sub s : size (pmap (insub : T → option sT) s) = count p s.
+Lemma size_pmap_sub s : size (pmap (insub : T → option sT) s) = count p s.
End PmapSub.
@@ -2075,16 +2184,16 @@
Section EqPmapSub.
-Variables (T : eqType) (p : pred T) (sT : subType p).
+Variables (T : eqType) (p : pred T) (sT : subType p).
-Let insT : T → option sT := insub.
+Let insT : T → option sT := insub.
-Lemma mem_pmap_sub s u : (u \in pmap insT s) = (val u \in s).
+Lemma mem_pmap_sub s u : (u \in pmap insT s) = (val u \in s).
-Lemma pmap_sub_uniq s : uniq s → uniq (pmap insT s).
+Lemma pmap_sub_uniq s : uniq s → uniq (pmap insT s).
End EqPmapSub.
@@ -2098,22 +2207,22 @@
-
Fixpoint iota m n :=
if n is n'.+1 then m :: iota m.+1 n' else [::].
+
Fixpoint iota m n :=
if n is n'.+1 then m :: iota m.+1 n' else [::].
-
Lemma size_iota m n :
size (
iota m n)
= n.
+
Lemma size_iota m n :
size (
iota m n)
= n.
-
Lemma iota_add m n1 n2 :
iota m (
n1 + n2)
= iota m n1 ++ iota (
m + n1)
n2.
+
Lemma iota_add m n1 n2 :
iota m (
n1 + n2)
= iota m n1 ++ iota (
m + n1)
n2.
-
Lemma iota_addl m1 m2 n :
iota (
m1 + m2)
n = map (
addn m1) (
iota m2 n).
+
Lemma iota_addl m1 m2 n :
iota (
m1 + m2)
n = map (
addn m1) (
iota m2 n).
-
Lemma nth_iota p m n i :
i < n → nth p (
iota m n)
i = m + i.
+
Lemma nth_iota p m n i :
i < n → nth p (
iota m n)
i = m + i.
-
Lemma mem_iota m n i :
(i \in iota m n) = (m ≤ i) && (i < m + n).
+
Lemma mem_iota m n i :
(i \in iota m n) = (m ≤ i) && (i < m + n).
Lemma iota_uniq m n :
uniq (
iota m n).
@@ -2136,16 +2245,16 @@
Definition mkseq f n :
seq T :=
map f (
iota 0
n).
-
Lemma size_mkseq f n :
size (
mkseq f n)
= n.
+
Lemma size_mkseq f n :
size (
mkseq f n)
= n.
-
Lemma eq_mkseq f g :
f =1 g → mkseq f =1 mkseq g.
+
Lemma eq_mkseq f g :
f =1 g → mkseq f =1 mkseq g.
-
Lemma nth_mkseq f n i :
i < n → nth x0 (
mkseq f n)
i = f i.
+
Lemma 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.
+
Lemma mkseq_nth s :
mkseq (
nth x0 s) (
size s)
= s.
End MakeSeq.
@@ -2157,11 +2266,11 @@
Variable T :
eqType.
-
Lemma mkseq_uniq (
f :
nat → T)
n :
injective f → uniq (
mkseq f n).
+
Lemma mkseq_uniq (
f :
nat → T)
n :
injective f → uniq (
mkseq f n).
-
Lemma perm_eq_iotaP {
s t :
seq T}
x0 (
It :=
iota 0 (
size t)) :
-
reflect (
exists2 Is, perm_eq Is It & s = map (
nth x0 t)
Is) (
perm_eq s t).
+
Lemma perm_iotaP {
s t :
seq T}
x0 (
It :=
iota 0 (
size t)) :
+
reflect (
exists2 Is, perm_eq Is It & s = map (
nth x0 t)
Is) (
perm_eq s t).
End MakeEqSeq.
@@ -2172,10 +2281,10 @@
Section FoldRight.
-
Variables (
T :
Type) (
R :
Type) (
f :
T → R → R) (
z0 :
R).
+
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.
+
Fixpoint foldr s :=
if s is x :: s' then f x (
foldr s')
else z0.
End FoldRight.
@@ -2184,14 +2293,14 @@
Section FoldRightComp.
-
Variables (
T1 T2 :
Type) (
h :
T1 → T2).
-
Variables (
R :
Type) (
f :
T2 → R → R) (
z0 :
R).
+
Variables (
T1 T2 :
Type) (
h :
T1 → T2).
+
Variables (
R :
Type) (
f :
T2 → R → R) (
z0 :
R).
-
Lemma foldr_cat s1 s2 :
foldr f z0 (
s1 ++ s2)
= foldr f (
foldr f z0 s2)
s1.
+
Lemma foldr_cat s1 s2 :
foldr f z0 (
s1 ++ s2)
= foldr f (
foldr f z0 s2)
s1.
-
Lemma foldr_map s :
foldr f z0 (
map h s)
= foldr (
fun x z ⇒
f (
h x)
z)
z0 s.
+
Lemma foldr_map s :
foldr f z0 (
map h s)
= foldr (
fun x z ⇒
f (
h x)
z)
z0 s.
End FoldRightComp.
@@ -2208,38 +2317,43 @@
Definition sumn :=
foldr addn 0.
-
Lemma sumn_nseq x n :
sumn (
nseq n x)
= x × n.
+
Lemma sumn_nseq x n :
sumn (
nseq n x)
= x × n.
+
+
+
Lemma sumn_cat s1 s2 :
sumn (
s1 ++ s2)
= sumn s1 + sumn s2.
-
Lemma sumn_cat s1 s2 :
sumn (
s1 ++ s2)
= sumn s1 + sumn s2.
+
Lemma sumn_count T (
a :
pred T)
s :
sumn [seq a i : nat | i <- s] = count a s.
-
Lemma sumn_count T (
P :
pred T)
s :
-
sumn [seq (P i : nat) | i <- s] = count P s.
+
Lemma sumn_rcons s n :
sumn (
rcons s n)
= sumn s + n.
-
Lemma sumn_rcons s n :
sumn (
rcons s n)
= sumn s + n.
+
Lemma perm_sumn s1 s2 :
perm_eq s1 s2 → sumn s1 = sumn s2.
+
+
+
Lemma sumn_rot s n :
sumn (
rot n s)
= sumn s.
-
Lemma sumn_rev s :
sumn (
rev s)
= sumn s.
+
Lemma sumn_rev s :
sumn (
rev s)
= sumn s.
-
Lemma natnseq0P s :
reflect (
s = nseq (
size s) 0) (
sumn s == 0).
+
Lemma natnseq0P s :
reflect (
s = nseq (
size s) 0) (
sumn s == 0).
Section FoldLeft.
-
Variables (
T R :
Type) (
f :
R → T → R).
+
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.
+
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_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_cat z s1 s2 :
foldl z (
s1 ++ s2)
= foldl (
foldl z s1)
s2.
End FoldLeft.
@@ -2249,44 +2363,44 @@
Variables (
T1 :
Type) (
x1 :
T1) (
T2 :
Type) (
x2 :
T2).
-
Variables (
f :
T1 → T1 → T2) (
g :
T1 → T2 → T1).
+
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 [::].
+
Fixpoint pairmap x s :=
if s is y :: s' then f x y :: pairmap y s' else [::].
-
Lemma size_pairmap x s :
size (
pairmap x s)
= size s.
+
Lemma size_pairmap x s :
size (
pairmap x s)
= size s.
Lemma pairmap_cat x s1 s2 :
-
pairmap x (
s1 ++ s2)
= pairmap x s1 ++ pairmap (
last x s1)
s2.
+
pairmap x (
s1 ++ s2)
= pairmap x s1 ++ pairmap (
last x s1)
s2.
-
Lemma nth_pairmap s n :
n < size s →
-
∀ x,
nth x2 (
pairmap x s)
n = f (
nth x1 (
x :: s)
n) (
nth x1 s n).
+
Lemma nth_pairmap s n :
n < size s →
+
∀ x,
nth x2 (
pairmap x s)
n = f (
nth x1 (
x :: s)
n) (
nth x1 s n).
Fixpoint scanl x s :=
-
if s is y :: s' then let x' :=
g x y in x' :: scanl x' s' else [::].
+
if s is y :: s' then let x' :=
g x y in x' :: scanl x' s' else [::].
-
Lemma size_scanl x s :
size (
scanl x s)
= size s.
+
Lemma size_scanl x s :
size (
scanl x s)
= size s.
Lemma scanl_cat x s1 s2 :
-
scanl x (
s1 ++ s2)
= scanl x s1 ++ scanl (
foldl g x s1)
s2.
+
scanl x (
s1 ++ s2)
= scanl x s1 ++ scanl (
foldl g x s1)
s2.
-
Lemma nth_scanl s n :
n < size s →
-
∀ x,
nth x1 (
scanl x s)
n = foldl g x (
take n.+1 s).
+
Lemma nth_scanl s n :
n < size s →
+
∀ x,
nth x1 (
scanl x s)
n = foldl g x (
take n.+1 s).
Lemma scanlK :
-
(∀ x,
cancel (
g x) (
f x)
) → ∀ x,
cancel (
scanl x) (
pairmap x).
+
(∀ x,
cancel (
g x) (
f x)
) → ∀ x,
cancel (
scanl x) (
pairmap x).
Lemma pairmapK :
-
(∀ x,
cancel (
f x) (
g x)
) → ∀ x,
cancel (
pairmap x) (
scanl x).
+
(∀ x,
cancel (
f x) (
g x)
) → ∀ x,
cancel (
pairmap x) (
scanl x).
End Scan.
@@ -2302,54 +2416,64 @@
Fixpoint zip (
s :
seq S) (
t :
seq T) {
struct t} :=
match s,
t with
- |
x :: s',
y :: t' ⇒
(x, y) :: zip s' t'
- |
_,
_ ⇒
[::]
+ |
x :: s',
y :: t' ⇒
(x, y) :: zip s' t'
+ |
_,
_ ⇒
[::]
end.
-
Definition unzip1 :=
map (@
fst S T).
-
Definition unzip2 :=
map (@
snd S T).
+
Definition unzip1 :=
map (@
fst S T).
+
Definition unzip2 :=
map (@
snd S T).
+
+
+
Fixpoint all2 (
r :
S → T → bool)
s t :=
+
match s,
t with
+ |
[::],
[::] ⇒
true
+ |
x :: s,
y :: t ⇒
r x y && all2 r s t
+ |
_,
_ ⇒
false
+
end.
-
Lemma zip_unzip s :
zip (
unzip1 s) (
unzip2 s)
= s.
+
Lemma zip_unzip s :
zip (
unzip1 s) (
unzip2 s)
= s.
-
Lemma unzip1_zip s t :
size s ≤ size t → unzip1 (
zip s t)
= s.
+
Lemma unzip1_zip s t :
size s ≤ size t → unzip1 (
zip s t)
= s.
-
Lemma unzip2_zip s t :
size t ≤ size s → unzip2 (
zip s t)
= t.
+
Lemma unzip2_zip s t :
size t ≤ size s → unzip2 (
zip s t)
= t.
-
Lemma size1_zip s t :
size s ≤ size t → size (
zip s t)
= size s.
+
Lemma size1_zip s t :
size s ≤ size t → size (
zip s t)
= size s.
-
Lemma size2_zip s t :
size t ≤ size s → size (
zip s t)
= size t.
+
Lemma size2_zip s t :
size t ≤ size s → size (
zip s t)
= size t.
-
Lemma size_zip s t :
size (
zip s t)
= minn (
size s) (
size t).
+
Lemma size_zip s t :
size (
zip s t)
= minn (
size s) (
size t).
Lemma zip_cat s1 s2 t1 t2 :
-
size s1 = size t1 → zip (
s1 ++ s2) (
t1 ++ t2)
= zip s1 t1 ++ zip s2 t2.
+
size s1 = size t1 → zip (
s1 ++ s2) (
t1 ++ t2)
= zip s1 t1 ++ zip s2 t2.
Lemma nth_zip x y s t i :
-
size s = size t → nth (x, y) (
zip s t)
i = (nth x s i, nth y t i).
+
size s = size t → nth (x, y) (
zip s t)
i = (nth x s i, nth y t i).
Lemma nth_zip_cond p s t i :
nth p (
zip s t)
i
-
= (if i < size (
zip s t)
then (nth p.1 s i, nth p.2 t i) else p).
+
= (if i < size (
zip s t)
then (nth p.1 s i, nth p.2 t i) else p).
-
Lemma zip_rcons s1 s2 z1 z2 :
-
size s1 = size s2 →
-
zip (
rcons s1 z1) (
rcons s2 z2)
= rcons (
zip s1 s2)
(z1, z2).
+
Lemma 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 s1 s2 :
-
size s1 = size s2 → rev (
zip s1 s2)
= zip (
rev s1) (
rev s2).
+
Lemma rev_zip s t :
size s = size t → rev (
zip s t)
= zip (
rev s) (
rev t).
+
+
Lemma all2E r s t :
+
all2 r s t = (size s == size t) && all [pred xy | r xy.1 xy.2] (
zip s t).
+
End Zip.
@@ -2366,104 +2490,104 @@
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 [::].
+
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).
+
Definition flatten_index sh r c :=
sumn (
take r sh)
+ c.
+
Definition reshape_index sh i :=
find (
pred1 0) (
scanl subn i.+1 sh).
+
Definition reshape_offset sh i :=
i - sumn (
take (
reshape_index sh i)
sh).
-
Lemma size_flatten ss :
size (
flatten ss)
= sumn (
shape ss).
+
Lemma size_flatten ss :
size (
flatten ss)
= sumn (
shape ss).
-
Lemma flatten_cat ss1 ss2 :
flatten (
ss1 ++ ss2)
= flatten ss1 ++ flatten ss2.
+
Lemma flatten_cat ss1 ss2 :
flatten (
ss1 ++ ss2)
= flatten ss1 ++ flatten ss2.
-
Lemma size_reshape sh s :
size (
reshape sh s)
= size sh.
+
Lemma size_reshape sh s :
size (
reshape sh s)
= size sh.
-
Lemma nth_reshape (
sh :
seq nat)
l n :
-
nth [::] (
reshape sh l)
n = take (
nth 0
sh n) (
drop (
sumn (
take n sh))
l).
+
Lemma nth_reshape (
sh :
seq nat)
l n :
+
nth [::] (
reshape sh l)
n = take (
nth 0
sh n) (
drop (
sumn (
take n sh))
l).
-
Lemma flattenK ss :
reshape (
shape ss) (
flatten ss)
= ss.
+
Lemma flattenK ss :
reshape (
shape ss) (
flatten ss)
= ss.
-
Lemma reshapeKr sh s :
size s ≤ sumn sh → flatten (
reshape sh s)
= s.
+
Lemma reshapeKr sh s :
size s ≤ sumn sh → flatten (
reshape sh s)
= s.
-
Lemma reshapeKl sh s :
size s ≥ sumn sh → shape (
reshape sh s)
= sh.
+
Lemma reshapeKl sh s :
size s ≥ sumn sh → shape (
reshape sh s)
= sh.
-
Lemma flatten_rcons ss s :
flatten (
rcons ss s)
= flatten ss ++ s.
+
Lemma flatten_rcons ss s :
flatten (
rcons ss s)
= flatten ss ++ s.
-
Lemma flatten_seq1 s :
flatten [seq [:: x] | x <- s] = s.
+
Lemma flatten_seq1 s :
flatten [seq [:: x] | x <- s] = s.
Lemma count_flatten ss P :
-
count P (
flatten ss)
= sumn [seq count P x | x <- ss].
+
count P (
flatten ss)
= sumn [seq count P x | x <- ss].
-
Lemma filter_flatten ss (
P :
pred T) :
-
filter P (
flatten ss)
= flatten [seq filter P i | i <- ss].
+
Lemma filter_flatten ss (
P :
pred T) :
+
filter P (
flatten ss)
= flatten [seq filter P i | i <- ss].
Lemma rev_flatten ss :
-
rev (
flatten ss)
= flatten (
rev (
map rev ss)).
+
rev (
flatten ss)
= flatten (
rev (
map rev ss)).
-
Lemma nth_shape ss i :
nth 0 (
shape ss)
i = size (
nth [::] ss i).
+
Lemma nth_shape ss i :
nth 0 (
shape ss)
i = size (
nth [::] ss i).
-
Lemma shape_rev ss :
shape (
rev ss)
= rev (
shape ss).
+
Lemma shape_rev ss :
shape (
rev ss)
= rev (
shape ss).
Lemma eq_from_flatten_shape ss1 ss2 :
-
flatten ss1 = flatten ss2 → shape ss1 = shape ss2 → ss1 = ss2.
+
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)).
+
size s = sumn sh → rev (
reshape sh s)
= map rev (
reshape (
rev sh) (
rev s)).
Lemma reshape_rcons s sh n (
m :=
sumn sh) :
-
m + n = size s →
-
reshape (
rcons sh n)
s = rcons (
reshape sh (
take m s)) (
drop m s).
+
m + n = size s →
+
reshape (
rcons sh n)
s = rcons (
reshape sh (
take m s)) (
drop m s).
Lemma flatten_indexP sh r c :
-
c < nth 0
sh r → flatten_index sh r c < sumn sh.
+
c < nth 0
sh r → flatten_index sh r c < sumn sh.
-
Lemma reshape_indexP sh i :
i < sumn sh → reshape_index sh i < size sh.
+
Lemma reshape_indexP sh i :
i < sumn sh → reshape_index sh i < size sh.
Lemma reshape_offsetP sh i :
-
i < sumn sh → reshape_offset sh i < nth 0
sh (
reshape_index sh i).
+
i < sumn sh → reshape_offset sh i < nth 0
sh (
reshape_index sh i).
Lemma reshape_indexK sh i :
-
flatten_index sh (
reshape_index sh i) (
reshape_offset sh i)
= i.
+
flatten_index sh (
reshape_index sh i) (
reshape_offset sh i)
= i.
Lemma flatten_indexKl sh r c :
-
c < nth 0
sh r → reshape_index sh (
flatten_index sh r c)
= r.
+
c < nth 0
sh r → reshape_index sh (
flatten_index sh r c)
= r.
Lemma flatten_indexKr sh r c :
-
c < nth 0
sh r → reshape_offset sh (
flatten_index sh r c)
= c.
+
c < nth 0
sh r → reshape_offset sh (
flatten_index sh r c)
= c.
Lemma nth_flatten x0 ss i (
r :=
reshape_index (
shape ss)
i) :
-
nth x0 (
flatten ss)
i = nth x0 (
nth [::] ss r) (
reshape_offset (
shape ss)
i).
+
nth x0 (
flatten ss)
i = nth x0 (
nth [::] ss r) (
reshape_offset (
shape ss)
i).
Lemma reshape_leq sh i1 i2
(
r1 :=
reshape_index sh i1) (
c1 :=
reshape_offset sh i1)
(
r2 :=
reshape_index sh i2) (
c2 :=
reshape_offset sh i2) :
-
(i1 ≤ i2) = ((r1 < r2) || ((r1 == r2) && (c1 ≤ c2))).
+
(i1 ≤ i2) = ((r1 < r2) || ((r1 == r2) && (c1 ≤ c2))).
End Flatten.
@@ -2471,16 +2595,16 @@
-
Lemma map_flatten S T (
f :
T → S)
ss :
-
map f (
flatten ss)
= flatten (
map (
map f)
ss).
+
Lemma map_flatten S T (
f :
T → S)
ss :
+
map f (
flatten ss)
= flatten (
map (
map f)
ss).
-
Lemma sumn_flatten (
ss :
seq (
seq nat)) :
-
sumn (
flatten ss)
= sumn (
map sumn ss).
+
Lemma sumn_flatten (
ss :
seq (
seq nat)) :
+
sumn (
flatten ss)
= sumn (
map sumn ss).
-
Lemma map_reshape T S (
f :
T → S)
sh s :
-
map (
map f) (
reshape sh s)
= reshape sh (
map f s).
+
Lemma map_reshape T S (
f :
T → S)
sh s :
+
map (
map f) (
reshape sh s)
= reshape sh (
map f s).
Section EqFlatten.
@@ -2490,11 +2614,15 @@
Lemma flattenP (
A :
seq (
seq T))
x :
-
reflect (
exists2 s, s \in A & x \in s) (
x \in flatten A).
+
reflect (
exists2 s, s \in A & x \in s) (
x \in flatten A).
-
Lemma flatten_mapP (
A :
S → seq T)
s y :
-
reflect (
exists2 x, x \in s & y \in A x) (
y \in flatten (
map A s)).
+
Lemma flatten_mapP (
A :
S → seq T)
s y :
+
reflect (
exists2 x, x \in s & y \in A x) (
y \in flatten (
map A s)).
+
+
+
Lemma perm_flatten (
ss1 ss2 :
seq (
seq T)) :
+
perm_eq ss1 ss2 → perm_eq (
flatten ss1) (
flatten ss2).
End EqFlatten.
@@ -2502,68 +2630,350 @@
-
Lemma perm_undup_count (
T :
eqType) (
s :
seq T) :
-
perm_eq (
flatten [seq nseq (
count_mem x s)
x | x <- undup s])
s.
+
Notation "[ 'seq' E | x <- s , y <- t ]" :=
+ (
flatten [seq [seq E | y <- t] | x <- s])
+ (
at level 0,
E at level 99,
x ident,
y ident,
+
format "[ '[hv' 'seq' E '/ ' | x <- s , '/ ' y <- t ] ']'")
+ :
seq_scope.
+
Notation "[ 'seq' E | x : S <- s , y : T <- t ]" :=
+ (
flatten [seq [seq E | y : T <- t] | x : S <- s])
+ (
at level 0,
E at level 99,
x ident,
y ident,
only parsing) :
seq_scope.
+
Notation "[ 'seq' E : R | x : S <- s , y : T <- t ]" :=
+ (
flatten [seq [seq E : R | y : T <- t] | x : S <- s])
+ (
at level 0,
E at level 99,
x ident,
y ident,
only parsing) :
seq_scope.
+
Notation "[ 'seq' E : R | x <- s , y <- t ]" :=
+ (
flatten [seq [seq E : R | y <- t] | x <- s])
+ (
at level 0,
E at level 99,
x ident,
y ident,
only parsing) :
seq_scope.
-
Section AllPairs.
+
Section AllPairsDep.
-
Variables (
S T R :
Type) (
f :
S → T → R).
-
Implicit Types (
s :
seq S) (
t :
seq T).
+
Variables (
S S' :
Type) (
T T' :
S → Type) (
R :
Type).
+
Implicit Type f :
∀ x,
T x → R.
-
Definition allpairs s t :=
foldr (
fun x ⇒
cat (
map (
f x)
t))
[::] s.
+
Definition allpairs_dep f s t :=
[seq f x y | x <- s, y <- t x].
-
Lemma size_allpairs s t :
size (
allpairs s t)
= size s × size t.
+
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 allpairs_cat s1 s2 t :
-
allpairs (
s1 ++ s2)
t = allpairs s1 t ++ allpairs s2 t.
+
Lemma eq_allpairs (
f1 f2 :
∀ x,
T x → R)
s t :
+
(∀ x,
f1 x =1 f2 x) →
+
[seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].
-
End AllPairs.
+
Lemma allpairs_cat f s1 s2 t :
+
[seq f x y | x <- s1 ++ s2, y <- t x] =
+
[seq f x y | x <- s1, y <- t x] ++ [seq f x y | x <- s2, y <- t x].
+
+
+
Lemma allpairs_mapl f (
g :
S' → S)
s t :
+
[seq f x y | x <- map g s, y <- t x] = [seq f (
g x)
y | x <- s, y <- t (
g x)
].
+
+
+
Lemma allpairs_mapr f (
g :
∀ x,
T' x → T x)
s t :
+
[seq f x y | x <- s, y <- map (
g x) (
t x)
] =
+
[seq f x (
g x y)
| x <- s, y <- t x].
+
+
+
End AllPairsDep.
-
Notation "[ 'seq' E | i <- s , j <- t ]" := (
allpairs (
fun i j ⇒
E)
s t)
- (
at level 0,
E at level 99,
i ident,
j ident,
-
format "[ '[hv' 'seq' E '/ ' | i <- s , '/ ' j <- t ] ']'")
- :
seq_scope.
-
Notation "[ 'seq' E | i : T <- s , j : U <- t ]" :=
- (
allpairs (
fun (
i :
T) (
j :
U) ⇒
E)
s t)
- (
at level 0,
E at level 99,
i ident,
j ident,
only parsing) :
seq_scope.
+
Lemma map_allpairs S T R R' (
g :
R' → R)
f s t :
+
map g [seq f x y | x : S <- s, y : T x <- t x] =
+
[seq g (
f x y)
| x <- s, y <- t x].
+
+
+
Section AllPairsNonDep.
-
Section EqAllPairs.
+
Variables (
S T R :
Type) (
f :
S → T → R).
+
Implicit Types (
s :
seq S) (
t :
seq T).
+
+
+
Definition allpairs s t :=
[seq f x y | x <- s, y <- t].
+
+
+
Lemma size_allpairs s t :
size [seq f x y | x <- s, y <- t] = size s × size t.
+
+
+
End AllPairsNonDep.
+
+
+
+
+
Section EqAllPairsDep.
+
+
+
Variables (
S :
eqType) (
T :
S → eqType).
+
Implicit Types (
R :
eqType) (
s :
seq S) (
t :
∀ x,
seq (
T x)).
+
+
+
Lemma allpairsPdep R (
f :
∀ x,
T x → R)
s t (
z :
R) :
+
reflect (
∃ x y, [/\ x \in s, y \in t x & z = f x y])
+ (
z \in [seq f x y | x <- s, y <- t x]).
+
+
+
Variable R :
eqType.
+
Implicit Type f :
∀ x,
T x → R.
+
+
+
Lemma allpairs_f_dep f s t x y :
+
x \in s → y \in t x → f x y \in [seq f x y | x <- s, y <- t x].
+
+
+
Lemma eq_in_allpairs_dep f1 f2 s t :
+
{in s, ∀ x,
{in t x, f1 x =1 f2 x}} ↔
+
[seq f1 x y : R | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].
-
Variables S T :
eqType.
-
Implicit Types (
R :
eqType) (
s :
seq S) (
t :
seq T).
+
Lemma mem_allpairs_dep f s1 t1 s2 t2 :
+
s1 =i s2 → {in s1, ∀ x,
t1 x =i t2 x} →
+
[seq f x y | x <- s1, y <- t1 x] =i [seq f x y | x <- s2, y <- t2 x].
-
Lemma allpairsP R (
f :
S → T → R)
s t z :
-
reflect (
∃ p, [/\ p.1 \in s, p.2 \in t & z = f p.1 p.2])
- (
z \in allpairs f s t).
+
Lemma allpairs_catr f s t1 t2 :
+
[seq f x y | x <- s, y <- t1 x ++ t2 x] =i
+
[seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x].
-
Lemma mem_allpairs R (
f :
S → T → R)
s1 t1 s2 t2 :
-
s1 =i s2 → t1 =i t2 → allpairs f s1 t1 =i allpairs f s2 t2.
+
Lemma allpairs_uniq_dep f s t (
st :=
[seq Tagged T y | x <- s, y <- t x]) :
+
let g (
p :
{x : S & T x}) :
R :=
f (
tag p) (
tagged p)
in
+
uniq s → {in s, ∀ x,
uniq (
t x)
} → {in st &, injective g} →
+
uniq [seq f x y | x <- s, y <- t x].
-
Lemma allpairs_catr R (
f :
S → T → R)
s t1 t2 :
-
allpairs f s (
t1 ++ t2)
=i allpairs f s t1 ++ allpairs f s t2.
+
End EqAllPairsDep.
+
+
+
+
+
Section EqAllPairs.
-
Lemma allpairs_uniq R (
f :
S → T → R)
s t :
-
uniq s → uniq t →
-
{in [seq (x, y) | x <- s, y <- t] &, injective (
prod_curry f)
} →
-
uniq (
allpairs f s t).
+
Variables S T R :
eqType.
+
Implicit Types (
f :
S → T → R) (
s :
seq S) (
t :
seq T).
+
+
+
Lemma allpairsP f s t (
z :
R) :
+
reflect (
∃ p, [/\ p.1 \in s, p.2 \in t & z = f p.1 p.2])
+ (
z \in [seq f x y | x <- s, y <- t]).
+
+
+
Lemma allpairs_f f s t x y :
+
x \in s → y \in t → f x y \in [seq f x y | x <- s, y <- t].
+
+
+
Lemma eq_in_allpairs f1 f2 s t :
+
{in s & t, f1 =2 f2} ↔
+
[seq f1 x y : R | x <- s, y <- t] = [seq f2 x y | x <- s, y <- t].
+
+
+
Lemma mem_allpairs f s1 t1 s2 t2 :
+
s1 =i s2 → t1 =i t2 →
+
[seq f x y | x <- s1, y <- t1] =i [seq f x y | x <- s2, y <- t2].
+
+
+
Lemma allpairs_uniq f s t (
st :=
[seq (x, y) | x <- s, y <- t]) :
+
uniq s → uniq t → {in st &, injective (
prod_curry f)
} →
+
uniq [seq f x y | x <- s, y <- t].
End EqAllPairs.
+
+
+
+
+
Section Permutations.
+
+
+
Variable T :
eqType.
+
Implicit Types (
x :
T) (
s t :
seq T) (
bs :
seq (
T × nat)) (
acc :
seq (
seq T)).
+
+
+
Fixpoint incr_tally bs x :=
+
if bs isn't b :: bs then [:: (x, 1
)] else
+
if x == b.1 then (x, b.2.+1) :: bs else b :: incr_tally bs x.
+
+
+
Definition tally s :=
foldl incr_tally [::] s.
+
+
+
Definition wf_tally :=
+
[qualify a bs : seq (
T × nat)
| uniq (
unzip1 bs)
&& (0
\notin unzip2 bs)].
+
+
+
Definition tally_seq bs :=
flatten [seq nseq b.2 b.1 | b <- bs].
+
+
+
Lemma size_tally_seq bs :
size (
tally_seq bs)
= sumn (
unzip2 bs).
+
+
+
Lemma tally_seqK :
{in wf_tally, cancel tally_seq tally}.
+
+
+
Lemma incr_tallyP x :
{homo incr_tally^~ x : bs / bs \in wf_tally}.
+
+
+
Lemma tallyP s :
tally s \is a wf_tally.
+
+
+
Lemma tallyK s :
perm_eq (
tally_seq (
tally s))
s.
+
+
+
Lemma tallyEl s :
perm_eq (
unzip1 (
tally s)) (
undup s).
+
+
+
Lemma tallyE s :
perm_eq (
tally s)
[seq (x, count_mem x s) | x <- undup s].
+
+
+
Lemma perm_tally s1 s2 :
perm_eq s1 s2 → perm_eq (
tally s1) (
tally s2).
+
+
+
Lemma perm_tally_seq bs1 bs2 :
+
perm_eq bs1 bs2 → perm_eq (
tally_seq bs1) (
tally_seq bs2).
+
+
+
Lemma perm_count_undup s :
+
perm_eq (
flatten [seq nseq (
count_mem x s)
x | x <- undup s])
s.
+
+
+
+
+
+
+
Definition permutations s :=
perms_rec (
size s)
[::] (
tally s)
[::].
+
+
+
Let permsP s :
∃ n bs,
+
[/\ permutations s = perms_rec n [::] bs [::],
+
size (
tseq bs)
== n, perm_eq (
tseq bs)
s & uniq (
unzip1 bs)
].
+
+
+
Let cons_permsE :
∀ n x bs bs1 bs2,
+
let cp :=
cons_perms n bs bs2 in let perms s :=
perms_rec n s bs1 [::] in
+
cp (
perms [:: x])
= cp [::] ++ [seq rcons t x | t <- perms [::]].
+
+
+
Lemma mem_permutations s t :
(t \in permutations s) = perm_eq t s.
+
+
+
Lemma permutations_uniq s :
uniq (
permutations s).
+
+
+
Notation perms :=
permutations.
+
Lemma permutationsE s :
+ 0
< size s →
+
perm_eq (
perms s)
[seq x :: t | x <- undup s, t <- perms (
rem x s)
].
+
+
+
Lemma permutationsErot x s (
le_x :=
fun t ⇒
iota 0 (
index x t + 1)) :
+
perm_eq (
perms (
x :: s))
[seq rot i (
x :: t)
| t <- perms s, i <- le_x t].
+
+
+
Lemma size_permutations s :
uniq s → size (
permutations s)
= (size s)`!.
+
+
+
Lemma permutations_all_uniq s :
uniq s → all uniq (
permutations s).
+
+
+
Lemma perm_permutations s t :
+
perm_eq s t → perm_eq (
permutations s) (
permutations t).
+
+
+
End Permutations.
+
+
+
Section AllIff.
+
+
+
+ The Following Are Equivalent
+
+
+ We introduce a specific conjunction, used to chain the consecutive
+ items in a circular list of implications
+
+ This means "the following are all equivalent: P0, ... Pn"
+
+
+
Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (
all_iff P0 (
P1 :: ..
[:: Pn] ..))
+ (
at level 0,
format "[ '<->' '[' P0 ; '/' P1 ; '/' .. ; '/' Pn ']' ]")
+ :
form_scope.
+
+
+
+ Temporary backward compatibility.
+
+
--
cgit v1.2.3