Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export mathcomp.zify.zify.Require Import prosa.util.tactics.Require Export prosa.util.supremum.(** We define a few simple operations on lists that return zero for empty lists: [max0], [first0], and [last0]. *)Definitionmax0 := foldl maxn 0.Definitionfirst0 := head 0.Definitionlast0 := last0.(** Additional lemmas about [last0]. *)SectionLast0.(** Let [xs] be a non-empty sequence and [x] be an arbitrary element, then we prove that [last0 (x::xs) = last0 xs]. *)
byinduction xs; lastunfold last0.Qed.(** Similarly, let [xs_r] be a non-empty sequence and [xs_l] be any sequence, we prove that [last0 (xs_l ++ xs_r) = last0 xs_r]. *)
x, a, n: nat xs: seq nat NEQ: [:: a, n & xs] <> [::] LAST: last0 [:: a, n & xs] = x IHxs: n :: xs <> [::] ->
last0 (n :: xs) = x ->
existsxsh : seq nat, xsh ++ [:: x] = n :: xs
existsxsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat xs: seq nat NEQ: [:: a, n & xs] <> [::] LAST: last0 [:: a, n & xs] = x IHxs: n :: xs <> [::] ->
last0 (n :: xs) = x ->
existsxsh : seq nat, xsh ++ [:: x] = n :: xs
existsxsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat xs: seq nat NEQ: [:: a, n & xs] <> [::] LAST: last0 [:: a, n & xs] = x IHxs: n :: xs <> [::] ->
last0 (n :: xs) = x ->
existsxsh : seq nat, xsh ++ [:: x] = n :: xs
existsxsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat xs: seq nat NEQ: [:: a, n & xs] <> [::] LAST: last0 [:: a, n & xs] = x IHxs: existsxsh : seq nat, xsh ++ [:: x] = n :: xs
existsxsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat xs: seq nat NEQ: [:: a, n & xs] <> [::] LAST: last0 [:: a, n & xs] = x xsh: seq nat EQ: xsh ++ [:: x] = n :: xs
existsxsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
byexists (a::xsh); rewrite //= EQ.Qed.(** We prove that if [x] is the last element of a sequence [xs] and [x] satisfies a predicate, then [x] remains the last element in the filtered sequence. *)
forall (x : nat) (xs : seq nat) (P : nat -> bool),
xs <> [::] ->
last0 xs = x -> P x -> last0 [seq x0 <- xs | P x0] = x
forall (x : nat) (xs : seq nat) (P : nat -> bool),
xs <> [::] ->
last0 xs = x -> P x -> last0 [seq x0 <- xs | P x0] = x
x: nat xs: seq nat P: nat -> bool NEQ: xs <> [::] LAST: last0 xs = x PX: P x
last0 [seq x <- xs | P x] = x
x: nat P: nat -> bool xsh: seq nat LAST: last0 (xsh ++ [:: x]) = x NEQ: xsh ++ [:: x] <> [::] PX: P x
last0 [seq x <- xsh ++ [:: x] | P x] = x
x: nat P: nat -> bool xsh: seq nat LAST: last0 (xsh ++ [:: x]) = x NEQ: xsh ++ [:: x] <> [::] PX: P x
last0 [seq x <- [:: x] | P x] = x
x: nat P: nat -> bool xsh: seq nat LAST: last0 (xsh ++ [:: x]) = x NEQ: xsh ++ [:: x] <> [::] PX: P x
[seq x <- [:: x] | P x] <> [::]
all:rewrite //= PX //=.Qed.EndLast0.(** Additional lemmas about [max0]. *)SectionMax0.(** First we prove that [max0 (x::xs)] is equal to [max {x, max0 xs}]. *)
byintros; unfold max; apply L.Qed.(** Next, we prove that if all the numbers of a seq [xs] are equal to a constant [k], then [max0 xs = k]. *)
forall (k : nat_eqType) (xs : seq nat_eqType),
0 < size xs ->
(forallx : nat_eqType, x \in xs -> x = k) ->
max0 xs = k
forall (k : nat_eqType) (xs : seq nat_eqType),
0 < size xs ->
(forallx : nat_eqType, x \in xs -> x = k) ->
max0 xs = k
k: nat_eqType xs: seq nat_eqType SIZE: 0 < size xs ALL: forallx : nat_eqType, x \in xs -> x = k
max0 xs = k
k, a: nat_eqType xs: seq nat_eqType SIZE: 0 < size (a :: xs) ALL: forallx : nat_eqType, x \in a :: xs -> x = k IHxs: 0 < size xs ->
(forallx : nat_eqType, x \in xs -> x = k) ->
max0 xs = k
max0 (a :: xs) = k
k, a: nat_eqType SIZE: 0 < size [:: a] ALL: forallx : nat_eqType, x \in [:: a] -> x = k IHxs: 0 < size [::] ->
(forallx : nat_eqType, x \in [::] -> x = k) ->
max0 [::] = k
max0 [:: a] = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a: nat_eqType SIZE: 0 < size [:: a] ALL: forallx : nat_eqType, x \in [:: a] -> x = k IHxs: 0 < size [::] ->
(forallx : nat_eqType, x \in [::] -> x = k) ->
max0 [::] = k
max0 [:: a] = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a: nat_eqType SIZE: 0 < size [:: a] ALL: forallx : nat_eqType, x \in [:: a] -> x = k IHxs: 0 < size [::] ->
(forallx : nat_eqType, x \in [::] -> x = k) ->
max0 [::] = k
a \in [:: a]
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
maxn a k = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
forallx : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
maxn a k = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
forallx : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
forallx : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k
forallx : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k x: nat_eqType H: x \in s :: xs
x \in [:: a, s & xs]
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k x: nat_eqType EQ: x = s
x \in [:: a, s & xs]
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k x: nat_eqType IN: x \in xs
x \in [:: a, s & xs]
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k x: nat_eqType EQ: x = s
x \in [:: a, s & xs]
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k x: nat_eqType IN: x \in xs
x \in [:: a, s & xs]
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k x: nat_eqType IN: x \in xs
x \in [:: a, s & xs]
k, a, s: nat_eqType xs: seq nat_eqType SIZE: 0 < size [:: a, s & xs] ALL: forallx : nat_eqType,
x \in [:: a, s & xs] -> x = k IHxs: 0 < size (s :: xs) ->
(forallx : nat_eqType, x \in s :: xs -> x = k) ->
max0 (s :: xs) = k x: nat_eqType IN: x \in xs
x \in [:: a, s & xs]
byrewrite !in_cons; apply/orP; right; apply/orP; right.Qed.(** We prove that no element in a sequence [xs] is greater than [max0 xs]. *)
forall (xs : seq_predType nat_eqType) (x : nat),
x \in xs -> x <= max0 xs
forall (xs : seq_predType nat_eqType) (x : nat),
x \in xs -> x <= max0 xs
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs
forallx : nat, x \in a :: xs -> x <= max0 (a :: xs)
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs
a <= max0 (a :: xs)
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs x: nat IN: x \in xs
x <= max0 (a :: xs)
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs
a <= max0 (a :: xs)
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs x: nat IN: x \in xs
x <= max0 (a :: xs)
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs x: nat IN: x \in xs
x <= max0 (a :: xs)
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs x: nat IN: x \in xs
x <= max0 (a :: xs)
a: nat_eqType xs: seq nat_eqType IHxs: forallx : nat, x \in xs -> x <= max0 xs x: nat IN: x \in xs
max0 xs <= max0 (a :: xs)
byrewrite max0_cons; apply leq_maxr.Qed.(** We prove that for a non-empty sequence [xs], [max0 xs ∈ xs]. *)
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs]
a: nat IHxs: [::] <> [::] -> max0 [::] \in [::]
max0 [:: a] \in [:: a]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs]
a: nat IHxs: [::] <> [::] -> max0 [::] \in [::]
max0 [:: a.+1] \in [:: a.+1]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs LE: a <= max0 (n :: xs)
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs LE: max0 (n :: xs) <= a
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs LE: a <= max0 (n :: xs)
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs LE: max0 (n :: xs) <= a
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs LE: max0 (n :: xs) <= a
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs LE: max0 (n :: xs) <= a
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat xs: seq nat IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs EQ: max0 (n :: xs) - a = 0
a + (max0 (n :: xs) - a) \in [:: a, n & xs]
byrewrite EQ addn0 in_cons; apply/orP; left.Qed.(** We prove a technical lemma stating that one can remove duplicating element from the head of a sequence. *)
byintros; rewrite !max0_cons maxnA maxnn.Qed.(** Similarly, we prove that one can remove the first element of a sequence if it is not greater than the second element of this sequence. *)
byintros; rewrite !max0_cons maxnA [maxn x1 x2]maxnE subnKC.Qed.(** We prove that [max0] of a sequence [xs] is equal to [max0] of sequence [xs] without 0s. *)
bysubst.Qed.(** Let's introduce the notion of the nth element of a sequence. *)Notation"xs [| n |]" := (nth 0 xs n) (at level30).(** If any element of a sequence [xs] is less-than-or-equal-to the corresponding element of a sequence [ys], then [max0] of [xs] is less-than-or-equal-to max of [ys]. *)
byintros; specialize (H n1.+1); simplin H.}}Qed.EndMax0.(** Additional lemmas about [rem] for lists. *)SectionRemList.(** We prove that if [x] lies in [xs] excluding [y], then [x] also lies in [xs]. *)
forall (X : eqType) (xy : X) (xs : seq X),
x \in rem (T:=X) y xs -> x \in xs
forall (X : eqType) (xy : X) (xs : seq X),
x \in rem (T:=X) y xs -> x \in xs
X: eqType x, y: X H: x \in [::]
x \in [::]
X: eqType x, y, a: X xs: seq X H: x
\in (if a == y then xs else a :: rem (T:=X) y xs) IHxs: x \in rem (T:=X) y xs -> x \in xs
x \in a :: xs
X: eqType x, y: X H: x \in [::]
x \in [::]
byrewrite in_nil in H.
X: eqType x, y, a: X xs: seq X H: x
\in (if a == y then xs else a :: rem (T:=X) y xs) IHxs: x \in rem (T:=X) y xs -> x \in xs
x \in a :: xs
X: eqType x, y, a: X xs: seq X H: x
\in (if a == y then xs else a :: rem (T:=X) y xs) IHxs: x \in rem (T:=X) y xs -> x \in xs
x \in a :: xs
X: eqType x, y, a: X xs: seq X H: x
\in (if a == y then xs else a :: rem (T:=X) y xs) IHxs: x \in rem (T:=X) y xs -> x \in xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = true H: x \in xs IHxs: x \in rem (T:=X) y xs -> x \in xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false H: x \in a :: rem (T:=X) y xs IHxs: x \in rem (T:=X) y xs -> x \in xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = true H: x \in xs IHxs: x \in rem (T:=X) y xs -> x \in xs
x == a \/ x \in xs
bymove: EQ => /eqP EQ; subst a; right.
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false H: x \in a :: rem (T:=X) y xs IHxs: x \in rem (T:=X) y xs -> x \in xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false H: x \in a :: rem (T:=X) y xs IHxs: x \in rem (T:=X) y xs -> x \in xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false IHxs: x \in rem (T:=X) y xs -> x \in xs H: x = a
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false IHxs: x \in rem (T:=X) y xs -> x \in xs H: x \in rem (T:=X) y xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false IHxs: x \in rem (T:=X) y xs -> x \in xs H: x = a
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false IHxs: x \in rem (T:=X) y xs -> x \in xs H: x \in rem (T:=X) y xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false IHxs: x \in rem (T:=X) y xs -> x \in xs H: x \in rem (T:=X) y xs
x == a \/ x \in xs
X: eqType x, y, a: X xs: seq X EQ: (a == y) = false IHxs: x \in rem (T:=X) y xs -> x \in xs H: x \in rem (T:=X) y xs
x == a \/ x \in xs
byright; apply IHxs.}}Qed.(** Similarly, we prove that if [x <> y] and [x] lies in [xs], then [x] lies in [xs] excluding [y]. *)
forall (X : eqType) (xy : X) (xs : seq X),
x \in xs -> x != y -> x \in rem (T:=X) y xs
forall (X : eqType) (xy : X) (xs : seq X),
x \in xs -> x != y -> x \in rem (T:=X) y xs
X: eqType x, y: X
x \in [::] -> x != y -> x \in rem (T:=X) y [::]
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
x \in a :: xs ->
x != y -> x \in rem (T:=X) y (a :: xs)
X: eqType x, y: X
x \in [::] -> x != y -> x \in rem (T:=X) y [::]
intros ?; bydone.
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
x \in a :: xs ->
x != y -> x \in rem (T:=X) y (a :: xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
x \in a :: xs ->
x != y -> x \in rem (T:=X) y (a :: xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs EQ: x = a NEQ: x != y
x \in rem (T:=X) y (a :: xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs IN: x \in xs NEQ: x != y
x \in rem (T:=X) y (a :: xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs EQ: x = a NEQ: x != y
x \in rem (T:=X) y (a :: xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs EQ: x = a NEQ: x != y
x \in (if x == y then xs else x :: rem (T:=X) y xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs EQ: x = a
x \in x :: rem (T:=X) y xs
byrewrite in_cons; apply/orP; left.
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs IN: x \in xs NEQ: x != y
x \in rem (T:=X) y (a :: xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs IN: x \in xs NEQ: x != y
x \in rem (T:=X) y (a :: xs)
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs IN: x \in xs NEQ: x != y AD: (a == y) = false
x \in a :: rem (T:=X) y xs
X: eqType x, y, a: X xs: seq X IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs IN: x \in xs NEQ: x != y AD: (a == y) = false
x \in rem (T:=X) y xs
byapply IHxs.}}Qed.(** We prove that if we remove an element [x] for which [P x] from a filter, then the size of the filter decreases by [1]. *)
forall (X : eqType) (x : X) (xs : seq X) (P : pred X),
x \in xs ->
P x ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
forall (X : eqType) (x : X) (xs : seq X) (P : pred X),
x \in xs ->
P x ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H: x \in a :: xs H0: P x IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
X: eqType a: X xs: seq X P: pred X IHxs: a \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) a xs | P y] + 1 H0: P a
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) a (a :: xs) | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
X: eqType a: X xs: seq X P: pred X IHxs: a \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) a xs | P y] + 1 H0: P a
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) a (a :: xs) | P y] + 1
bysimpl; rewrite H0 -[X in X = _]addn1 eq_refl.
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs
size
(if P a
then a :: [seq y <- xs | P y]
else [seq y <- xs | P y]) =
size
[seq y <- if a == x
then xs
else a :: rem (T:=X) x xs
| P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = true
size
(if P a
then a :: [seq y <- xs | P y]
else [seq y <- xs | P y]) =
size [seq y <- xs | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false
size
(if P a
then a :: [seq y <- xs | P y]
else [seq y <- xs | P y]) =
size
(if P a
then a :: [seq y <- rem (T:=X) x xs | P y]
else [seq y <- rem (T:=X) x xs | P y]) + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = true
size
(if P a
then a :: [seq y <- xs | P y]
else [seq y <- xs | P y]) =
size [seq y <- xs | P y] + 1
X: eqType x: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs
size
(if P x
then x :: [seq y <- xs | P y]
else [seq y <- xs | P y]) =
size [seq y <- xs | P y] + 1
byrewrite H0 addn1.
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false
size
(if P a
then a :: [seq y <- xs | P y]
else [seq y <- xs | P y]) =
size
(if P a
then a :: [seq y <- rem (T:=X) x xs | P y]
else [seq y <- rem (T:=X) x xs | P y]) + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false
size
(if P a
then a :: [seq y <- xs | P y]
else [seq y <- xs | P y]) =
size
(if P a
then a :: [seq y <- rem (T:=X) x xs | P y]
else [seq y <- rem (T:=X) x xs | P y]) + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false Pa: P a = true
(size [seq y <- xs | P y]).+1 =
(size [seq y <- rem (T:=X) x xs | P y]).+1 + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false Pa: P a = false
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false Pa: P a = true
(size [seq y <- xs | P y]).+1 =
(size [seq y <- rem (T:=X) x xs | P y]).+1 + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false Pa: P a = false
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false Pa: P a = false
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
X: eqType x, a: X xs: seq X P: pred X H0: P x IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 H: x \in xs EQab: (a == x) = false Pa: P a = false
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
byrewrite IHxs.}}Qed.EndRemList.(** Additional lemmas about sequences. *)SectionAdditionalLemmas.(** First, we prove that [x::xs = ys] is a sufficient condition for [x] to be in [ys]. *)
forall (X : eqType) (x : X) (xsys : seq X),
x :: xs = ys -> x \in ys
forall (X : eqType) (x : X) (xsys : seq X),
x :: xs = ys -> x \in ys
X: eqType x: X xs: seq X y: X ys: seq X EQ: x :: xs = y :: ys
x \in y :: ys
X: eqType x: X xs: seq X y: X ys: seq X EQ: x = y
x \in y :: ys
bysubst y; rewrite in_cons; apply/orP; left.Qed.(** We show that if [n > 0], then [nth (x::xs) n = nth xs (n-1)]. *)
byintros; destruct n.Qed.(** We prove that a sequence [xs] of size [n.+1] can be destructed into a sequence [xs_l] of size [n] and an element [x] such that [x = xs ++ [::x]]. *)
bysubst; exists (a::xsl), xsr.Qed.(** We prove that for any two sequences [xs] and [ys] the fact that [xs] is a sub-sequence of [ys] implies that the size of [xs] is at most the size of [ys]. *)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs EQ: (a == x) = true
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs ->
(forallx : X, x \in xs -> x \in ys) ->
size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs EQ: (a == x) = false
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs EQ: (a == x) = true
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs EQ: (a == x) = true
False
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs EQ: a = x NIN: x \notin xs UNIQ: uniq xs
False
bysubst; move: NIN => /negP NIN; apply: NIN.
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs EQ: (a == x) = false
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) SUB: forallx0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr a: X IN: a \in xs EQ: (a == x) = false
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X SUB: a \in x :: xs -> a \in ysl ++ [:: x] ++ ysr IN: a \in xs EQ: (a == x) = false
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X SUB: a \in ysl ++ [:: x] ++ ysr IN: a \in xs EQ: (a == x) = false
a \in ysr ++ ysl
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysl
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs ->
(forallx : X, x \in xs -> x \in ys) ->
size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in [:: x]
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs ->
(forallx : X, x \in xs -> x \in ys) ->
size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysr
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysl
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs ->
(forallx : X, x \in xs -> x \in ys) ->
size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in [:: x]
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs ->
(forallx : X, x \in xs -> x \in ys) ->
size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysr
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in [:: x]
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs ->
(forallx : X, x \in xs -> x \in ys) ->
size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysr
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in [:: x]
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs ->
(forallx : X, x \in xs -> x \in ys) ->
size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysr
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysr
(a \in ysr) || (a \in ysl)
X: eqType m: nat IHm: forallxsys : seq X,
size ys <= m ->
uniq xs -> (forallx : X, x \in xs -> x \in ys) -> size xs <= size ys x: X xs, ysl, ysr: seq X SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1 UNIQ: uniq (x :: xs) a: X EQ: (a == x) = false IN: a \in ysr
(a \in ysr) || (a \in ysl)
byapply/orP; left.}}Qed.(** Given two sequences [xs] and [ys], two elements [x] and [y], and an index [idx] such that [nth xs idx = x, nth ys idx = y], we show that the pair [(x, y)] is in [zip xs ys]. *)
byexistsidx; repeatsplit; eauto.}Qed.(** This lemma allows us to check proposition of the form [forall x ∈ xs, exists y ∈ ys, P x y] using a boolean expression [all P (zip xs ys)]. *)
forall (XY : eqType) (P_bool : X * Y -> bool)
(P_prop : X -> Y -> Prop) (xs : seq X),
(forall (x : X) (y : Y), P_bool (x, y) <-> P_prop x y) ->
(existsys : seq Y,
size xs = size ys /\ all P_bool (zip xs ys) == true) ->
forallx : X, x \in xs -> existsy : Y, P_prop x y
forall (XY : eqType) (P_bool : X * Y -> bool)
(P_prop : X -> Y -> Prop) (xs : seq X),
(forall (x : X) (y : Y), P_bool (x, y) <-> P_prop x y) ->
(existsys : seq Y,
size xs = size ys /\ all P_bool (zip xs ys) == true) ->
forallx : X, x \in xs -> existsy : Y, P_prop x y
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y TR: existsys : seq Y,
size xs = size ys /\
all P_bool (zip xs ys) == true x: X IN: x \in xs
existsy : Y, P_prop x y
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y ys: seq Y SIZE: size xs = size ys ALL: all P_bool (zip xs ys) == true x: X IN: x \in xs
existsy : Y, P_prop x y
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y ys: seq Y SIZE: size xs = size ys ALL: all P_bool (zip xs ys) == true x: X IN: x \in xs idx:= index x xs: nat
existsy : Y, P_prop x y
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y ys: seq Y SIZE: size xs = size ys ALL: all P_bool (zip xs ys) == true x: X IN: x \in xs idx:= index x xs: nat x__d: Y
existsy : Y, P_prop x y
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y ys: seq Y SIZE: size xs = size ys ALL: all P_bool (zip xs ys) == true x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
existsy : Y, P_prop x y
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys ALL: all P_bool (zip xs ys) == true x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
P_bool (x, nth y__d ys idx)
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
(x, nth y__d ys idx) \in zip xs ys
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
idx < size xs
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
nth ?x__d xs idx = x
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
idx < size xs
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
nth ?x__d xs idx = x
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
nth ?x__d xs idx = x
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
nth ?x__d xs idx = x
byapply nth_index.-
X, Y: eqType P_bool: X * Y -> bool P_prop: X -> Y -> Prop xs: seq X ys: seq Y SIZE: size xs = size ys x: X IN: x \in xs idx:= index x xs: nat x__d, y__d: Y
X
bydone.Qed.(** Given two sequences [xs] and [ys] of equal size and without duplicates, the fact that [xs ⊆ ys] implies that [ys ⊆ xs]. *)
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
uniq (rem (T:=X) x ys)
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
size xs = size (rem (T:=X) x ys)
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
a \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
uniq (rem (T:=X) x ys)
byapply rem_uniq.
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
size xs = size (rem (T:=X) x ys)
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
a \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
size xs = size (rem (T:=X) x ys)
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
size xs = (size ys).-1
byrewrite -EQ //=.
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
a \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs
b \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs
b \in ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs
b != x
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs
b \in x :: xs
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X,
x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs
b != x
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs
b != x
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs
uniq (x :: xs) -> b != x
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a b: X INb: b \in xs NIN: x \notin xs
b != x
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a INb: x \in xs NIN: x \notin xs
False
bymove: NIN => /negP NIN; apply: NIN.
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
a \in rem (T:=X) x ys
X: eqType m: nat x: X xs, ys: seq X IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forallx0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forallx0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs SIZEm: size ys <= m.+1 UNIQx: uniq (x :: xs) UNIQy: uniq ys EQ: size (x :: xs) = size ys SUB: forallx0 : X, x0 \in x :: xs -> x0 \in ys a: X IN: a \in ys NEQ: x != a
a \in rem (T:=X) x ys
byapply in_neq_impl_rem_in; lastrewrite eq_sym.}}}Qed.(** We prove that if no element of a sequence [xs] satisfies a predicate [P], then [filter P xs] is equal to an empty sequence. *)
forall (X : eqType) (xs : seq X) (P : pred X),
(forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
forall (X : eqType) (xs : seq X) (P : pred X),
(forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
X: eqType xs: seq X P: pred X ALLF: forallx : X, x \in xs -> ~~ P x
[seq x <- xs | P x] = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
[seq x <- a :: xs | P x] = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
forallx : X, x \in xs -> ~~ P x
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
(if P a then [:: a] else [::]) = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
forallx : X, x \in xs -> ~~ P x
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
(if P a then [:: a] else [::]) = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
(if P a then [:: a] else [::]) = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
(if P a then [:: a] else [::]) = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::] EQ: P a = true
[:: a] = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::] T: ~ ~~ P a
[:: a] = [::]
X: eqType a: X xs: seq X P: pred X ALLF: forallx : X, x \in a :: xs -> ~~ P x IHxs: (forallx : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
~~ P a
byapply ALLF; apply/orP; left.Qed.(** We show that any two elements having the same index in a sequence must be equal. *)
forall (X : eqType) (ab : X) (xs : seq X),
index a xs = index b xs ->
a \in xs -> b \in xs -> a = b
forall (X : eqType) (ab : X) (xs : seq X),
index a xs = index b xs ->
a \in xs -> b \in xs -> a = b
X: eqType a, b: X xs: seq X EQ: index a xs = index b xs IN_a: a \in xs IN_b: b \in xs
a = b
X: eqType a, b: X xs: seq X EQ: index a xs = index b xs IN_a: a \in xs IN_b: b \in xs EQ_a: nth a xs (index a xs) = a
a = b
X: eqType a, b: X xs: seq X EQ: index a xs = index b xs IN_a: a \in xs IN_b: b \in xs EQ_a: nth a xs (index a xs) = a EQ_b: nth a xs (index b xs) = b
a = b
byrewrite -EQ_a -EQ_b EQ.Qed.(** We show that the nth element in a sequence is either in the sequence or is the default element. *)
forall (X : eqType) (n : nat) (d : X) (xs : seq X),
nth d xs n = d \/ nth d xs n \in xs
forall (X : eqType) (n : nat) (d : X) (xs : seq X),
nth d xs n = d \/ nth d xs n \in xs
X: eqType n: nat d: X xs: seq X i: size xs <= n
nth d xs n = d \/ nth d xs n \in xs
X: eqType n: nat d: X xs: seq X i: n < size xs
nth d xs n = d \/ nth d xs n \in xs
X: eqType n: nat d: X xs: seq X i: size xs <= n
nth d xs n = d \/ nth d xs n \in xs
X: eqType n: nat d: X xs: seq X i: n < size xs
nth d xs n = d \/ nth d xs n \in xs
X: eqType n: nat d: X xs: seq X i: n < size xs
nth d xs n = d \/ nth d xs n \in xs
X: eqType n: nat d: X xs: seq X i: n < size xs
nth d xs n = d \/ nth d xs n \in xs
byright; apply mem_nth.Qed.(** We show that in a unique sequence of size greater than one there exist two unique elements. *)
forall (X : eqType) (xs : seq X),
1 < size xs ->
uniq xs ->
existsab : X, a <> b /\ a \in xs /\ b \in xs
forall (X : eqType) (xs : seq X),
1 < size xs ->
uniq xs ->
existsab : X, a <> b /\ a \in xs /\ b \in xs
T: eqType xs: seq T GT1: 1 < size xs UNIQ: uniq xs HEAD: existsx : T, ohead xs = Some x x0: T GT0: 0 < size xs
nth x0 xs 0 <> nth x0 xs 1
T: eqType xs: seq T GT1: 1 < size xs UNIQ: uniq xs HEAD: existsx : T, ohead xs = Some x x0: T GT0: 0 < size xs
nth x0 xs 0 == nth x0 xs 1 -> 0 == 1
byrewrite nth_uniq.Qed.(** The predicate [all] implies the predicate [has], if the sequence is not empty. *)
T: eqType
forall (s : seq T) (P : pred T),
all P s -> ~~ nilp s -> has P s
T: eqType
forall (s : seq T) (P : pred T),
all P s -> ~~ nilp s -> has P s
T: eqType a: T s: seq T P: pred T ALL: {in a :: s, forallx : T, P x}
has P (a :: s)
byapply /hasP; existsa; [|move: (ALL a); apply]; exact: mem_head.Qed.EndAdditionalLemmas.(** Additional lemmas about [sorted]. *)SectionSorted.(** We show that if [[x | x ∈ xs : P x]] is sorted with respect to values of some function [f], then it can be split into two parts: [[x | x ∈ xs : P x /\ f x <= t]] and [[x | x ∈ xs : P x /\ f x <= t]]. *)
forall (X : eqType) (xs : seq X) (P : X -> bool)
(f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
forall (X : eqType) (xs : seq X) (P : X -> bool)
(f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs
(if P a
then a :: [seq x <- xs | P x]
else [seq x <- xs | P x]) =
(if P a && (f a <= t)
then a :: [seq x <- xs | P x & f x <= t]
else [seq x <- xs | P x & f x <= t]) ++
(if P a && (t < f a)
then a :: [seq x <- xs | P x & t < f x]
else [seq x <- xs | P x & t < f x])
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs
transitive (T:=X) (funxy : X => f x <= f y)
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y)
(if P a
then a :: [seq x <- xs | P x]
else [seq x <- xs | P x]) =
(if P a && (f a <= t)
then a :: [seq x <- xs | P x & f x <= t]
else [seq x <- xs | P x & f x <= t]) ++
(if P a && (t < f a)
then a :: [seq x <- xs | P x & t < f x]
else [seq x <- xs | P x & t < f x])
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs
transitive (T:=X) (funxy : X => f x <= f y)
intros ? ? ? LE1 LE2; lia.
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y)
(if P a
then a :: [seq x <- xs | P x]
else [seq x <- xs | P x]) =
(if P a && (f a <= t)
then a :: [seq x <- xs | P x & f x <= t]
else [seq x <- xs | P x & f x <= t]) ++
(if P a && (t < f a)
then a :: [seq x <- xs | P x & t < f x]
else [seq x <- xs | P x & t < f x])
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: f a <= t
a :: [seq x <- xs | P x] =
a
:: [seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: t < f a
a :: [seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: f a <= t
a :: [seq x <- xs | P x] =
a
:: [seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: f a <= t
sorted (funxy : X => f x <= f y) xs
byeapply path_sorted; eauto.
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: t < f a
a :: [seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: t < f a
a :: [seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: t < f a
a
:: [seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: t < f a
[::] = [seq x <- xs | P x & f x <= t]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: t < f a ALL: all (funy : X => f a <= f y) xs SORT: sorted (funxy : X => f x <= f y) xs
[seq x <- xs | P x & f x <= t] = [::]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = true R1: t < f a ALL: all (funy : X => f a <= f y) xs SORT: sorted (funxy : X => f x <= f y) xs x: X IN: x \in xs Px: P x LEx: f x <= t
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
byeapply IHxs, path_sorted; eauto.
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType a: X xs: seq X IHxs: forall (P : X -> bool) (f : X -> nat) (t : nat),
sorted (funxy : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] P: X -> bool f: X -> nat t: nat SORT: path (funxy : X => f x <= f y) a xs TR: transitive (T:=X) (funxy : X => f x <= f y) Pa: P a = false R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
byeapply IHxs, path_sorted; eauto.}Qed.(** We show that if a sequence [xs1 ++ xs2] is sorted, then both subsequences [xs1] and [xs2] are sorted as well. *)
forall (X : eqType) (R : rel X) (xs1xs2 : seq X),
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) -> sorted R xs1 /\ sorted R xs2
forall (X : eqType) (R : rel X) (xs1xs2 : seq X),
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) -> sorted R xs1 /\ sorted R xs2
X: eqType R: rel X a: X xs1: seq X IHxs1: forallxs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2 xs2: seq X TR: transitive (T:=X) R SORT: sorted R ((a :: xs1) ++ xs2)
sorted R (a :: xs1)
X: eqType R: rel X a: X xs1: seq X IHxs1: forallxs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2 xs2: seq X TR: transitive (T:=X) R SORT: sorted R ((a :: xs1) ++ xs2)
sorted R xs2
X: eqType R: rel X a: X xs1: seq X IHxs1: forallxs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2 xs2: seq X TR: transitive (T:=X) R SORT: sorted R ((a :: xs1) ++ xs2)
sorted R (a :: xs1)
X: eqType R: rel X a: X xs1: seq X IHxs1: forallxs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2 xs2: seq X TR: transitive (T:=X) R ALL1: all (R a) xs1 ALL2: all (R a) xs2 SORT: sorted R (xs1 ++ xs2)
X: eqType R: rel X a: X xs1: seq X IHxs1: forallxs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2 xs2: seq X TR: transitive (T:=X) R SORT: sorted R ((a :: xs1) ++ xs2)
sorted R xs2
X: eqType R: rel X a: X xs1: seq X IHxs1: forallxs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2 xs2: seq X TR: transitive (T:=X) R SORT: sorted R ((a :: xs1) ++ xs2)
sorted R xs2
X: eqType R: rel X a: X xs1: seq X IHxs1: forallxs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2 xs2: seq X TR: transitive (T:=X) R ALL1: all (R a) xs1 ALL2: all (R a) xs2 SORT: sorted R (xs1 ++ xs2)
sorted R xs2
byapply IHxs1.}Qed.EndSorted.(** Additional lemmas about [last]. *)SectionLast.(** First, we show that the default element does not change the value of [last] for non-empty sequences. *)
X: eqType a: X xs: seq X IHxs: foralld1d2 : X,
xs != [::] -> last d1 xs = last d2 xs
foralld1d2 : X,
a :: xs != [::] ->
last d1 (a :: xs) = last d2 (a :: xs)
byintros * _; destruct xs.Qed.(** We show that if a sequence [xs] contains an element that satisfies a predicate [P], then the last element of [filter P xs] is in [xs]. *)
forall (X : eqType) (xs : seq X) (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
forall (X : eqType) (xs : seq X) (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
forall (d : X) (P : pred X),
has P (a :: xs) ->
last d [seq x <- a :: xs | P x] \in a :: xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x EQ: x = a
last d [seq x <- a :: xs | P x] \in a :: xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x IN: x \in xs
last d [seq x <- a :: xs | P x] \in a :: xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x EQ: x = a
last d [seq x <- a :: xs | P x] \in a :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x
last x [seq x <- xs | P x] \in x :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = true
last x [seq x <- xs | P x] \in x :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
last x [seq x <- xs | P x] \in x :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = true
last x [seq x <- xs | P x] \in x :: xs
byrewrite in_cons; apply/orP; right; apply IHxs.
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
last x [seq x <- xs | P x] \in x :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
last x [seq x <- xs | P x] \in x :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
last x [::] \in x :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
[::] = [seq x <- xs | P x]
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
last x [::] \in x :: xs
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
[::] = [seq x <- xs | P x]
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
[::] = [seq x <- xs | P x]
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false
[::] = [seq x <- xs | P x]
X: eqType xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x HAS: has P xs = false y: X IN: y \in xs
~~ P y
bymove: HAS => /negP/negP/hasPn ALLN; apply: ALLN.}
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x IN: x \in xs
last d [seq x <- a :: xs | P x] \in a :: xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x IN: x \in xs
last d [seq x <- a :: xs | P x] \in a :: xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x IN: x \in xs
last d [seq x <- a :: xs | P x] \in xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x IN: x \in xs
has P xs
X: eqType a: X xs: seq X IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs d: X P: pred X x: X Px: P x IN: x \in xs
has P xs
all: byapply/hasP; existsx.}Qed.EndLast.(** Function [rem] from [ssreflect] removes only the first occurrence of an element in a sequence. We define function [rem_all] which removes all occurrences of an element in a sequence. *)Fixpointrem_all {X : eqType} (x : X) (xs : seq X) :=
match xs with
| [::] => [::]
| a :: xs =>
if a == x then rem_all x xs else a :: rem_all x xs
end.(** Additional lemmas about [rem_all] for lists. *)SectionRemAllList.(** First we prove that [x ∉ rem_all x xs]. *)
forall (X : eqType) (x : X) (xs : seq X),
~ x \in rem_all x xs
forall (X : eqType) (x : X) (xs : seq X),
~ x \in rem_all x xs
X: eqType x: X xs: seq X IN: x \in rem_all x xs
False
X: eqType x, a: X xs: seq X IN: x \in rem_all x (a :: xs) IHxs: x \in rem_all x xs -> False
False
X: eqType x, a: X xs: seq X IN: x \in rem_all x (a :: xs)
x \in rem_all x xs
X: eqType x, a: X xs: seq X EQ: (a == x) = false IN: x \in a :: rem_all x xs
x \in rem_all x xs
X: eqType x, a: X xs: seq X EQ: (a == x) = false EQ2: x = a
x \in rem_all x xs
bysubst; exfalso; rewrite eq_refl in EQ.Qed.(** Next we show that [rem_all x xs ⊆ xs]. *)
forall (X : eqType) (ax : X) (xs : seq X),
a \in rem_all x xs -> a \in xs
forall (X : eqType) (ax : X) (xs : seq X),
a \in rem_all x xs -> a \in xs
X: eqType a, x: X xs: seq X IN: a \in rem_all x xs
a \in xs
X: eqType a, x, a0: X xs: seq X IN: a \in rem_all x (a0 :: xs) IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X IN: a
\in (if a0 == x
then rem_all x xs
else a0 :: rem_all x xs) IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = true IN: a \in rem_all x xs IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IN: a \in a0 :: rem_all x xs IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = true IN: a \in rem_all x xs IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IN: a \in a0 :: rem_all x xs IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IN: a \in a0 :: rem_all x xs IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IN: a \in a0 :: rem_all x xs IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IHxs: a \in rem_all x xs -> a \in xs EQ2: a == a0
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IHxs: a \in rem_all x xs -> a \in xs IN: a \in rem_all x xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IHxs: a \in rem_all x xs -> a \in xs EQ2: a == a0
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IHxs: a \in rem_all x xs -> a \in xs IN: a \in rem_all x xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IHxs: a \in rem_all x xs -> a \in xs IN: a \in rem_all x xs
a \in a0 :: xs
X: eqType a, x, a0: X xs: seq X EQ: (a0 == x) = false IHxs: a \in rem_all x xs -> a \in xs IN: a \in rem_all x xs
a \in a0 :: xs
byrewrite in_cons; apply/orP; right; auto.Qed.(** If an element [x] is smaller than any element of a sequence [xs], then [rem_all x xs = xs]. *)
forall (x : nat) (xs : seq_predType nat_eqType),
(forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
forall (x : nat) (xs : seq_predType nat_eqType),
(forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
x: nat a: nat_eqType xs: seq nat_eqType MIN: forally : nat, y \in a :: xs -> x < y IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
rem_all x (a :: xs) = a :: xs
x: nat a: nat_eqType xs: seq nat_eqType MIN: forally : nat, y \in a :: xs -> x < y IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
(a == x) = false
x: nat a: nat_eqType xs: seq nat_eqType MIN: forally : nat, y \in a :: xs -> x < y IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
a :: rem_all x xs = a :: xs
x: nat a: nat_eqType xs: seq nat_eqType MIN: forally : nat, y \in a :: xs -> x < y IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
(a == x) = false
x: nat a: nat_eqType xs: seq nat_eqType MIN: forally : nat, y \in a :: xs -> x < y IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
x < a
byapply MIN; rewrite in_cons; apply/orP; left.
x: nat a: nat_eqType xs: seq nat_eqType MIN: forally : nat, y \in a :: xs -> x < y IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
a :: rem_all x xs = a :: xs
x: nat a: nat_eqType xs: seq nat_eqType MIN: forally : nat, y \in a :: xs -> x < y IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs
forally : nat, y \in xs -> x < y
x: nat a: nat_eqType xs: seq nat_eqType IHxs: (forally : nat, y \in xs -> x < y) ->
rem_all x xs = xs y: nat H: y \in xs
y \in a :: xs
byrewrite in_cons; apply/orP; right.Qed.EndRemAllList.(** To have a more intuitive naming, we introduce the definition of [range a b] which is equal to [index_iota a b.+1]. *)Definitionrange (ab : nat) := index_iota a b.+1.(** Additional lemmas about [index_iota] and [range] for lists. *)SectionIotaRange.(** First, we show that [iota m n] can be split into two parts [iota m nle] and [iota (m + nle) (n - nle)] for any [nle <= n]. *)
foralln_lemn : nat,
n_le <= n ->
iota m n = iota m n_le ++ iota (m + n_le) (n - n_le)
foralln_lemn : nat,
n_le <= n ->
iota m n = iota m n_le ++ iota (m + n_le) (n - n_le)
n_le, m, n: nat LE: n_le <= n
iota m n = iota m n_le ++ iota (m + n_le) (n - n_le)
n_le, m, k: nat
iota m (n_le + k) =
iota m n_le ++ iota (m + n_le) (n_le + k - n_le)
n_le, m, k: nat
iota m n_le ++ iota (m + n_le) k =
iota m n_le ++ iota (m + n_le) (n_le + k - n_le)
byreplace (_ + _ - _) with k; lastlia.Qed.(** Next, we prove that [index_iota a b = a :: index_iota a.+1 b] for [a < b]. *)
forallab : nat,
a < b -> index_iota a b = a :: index_iota a.+1 b
forallab : nat,
a < b -> index_iota a b = a :: index_iota a.+1 b
a, b: nat LT: a < b
iota a (b - a) = a :: iota a.+1 (b - a.+1)
a, b: nat LT: a < b.+1
iota a (b.+1 - a) = a :: iota a.+1 (b.+1 - a.+1)
a, b: nat LT: a <= b
iota a (b.+1 - a) = a :: iota a.+1 (b.+1 - a.+1)
byrewrite subSn //.Qed.(** We prove that one can remove duplicating element from the head of a sequence by which [range] is filtered. *)
forall (x : nat_eqType) (xs : seq nat_eqType)
(k : nat),
[seq ρ <- range 0 k | ρ \in [:: x, x & xs]] =
[seq ρ <- range 0 k | ρ \in x :: xs]
forall (x : nat_eqType) (xs : seq nat_eqType)
(k : nat),
[seq ρ <- range 0 k | ρ \in [:: x, x & xs]] =
[seq ρ <- range 0 k | ρ \in x :: xs]
x: nat_eqType xs: seq nat_eqType k: nat
[seq ρ <- range 0 k | ρ \in [:: x, x & xs]] =
[seq ρ <- range 0 k | ρ \in x :: xs]
bydestruct (x0 == x), (x0 \in xs).Qed.(** Consider [a], [b], and [x] s.t. [a ≤ x < b], then filter of [iota_index a b] with predicate [(_ == x)] yields [::x]. *)
forallxab : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
forallxab : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
existsk : nat, b - a <= k
x, a, b: nat EX: existsk : nat, b - a <= k
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
existsk : nat, b - a <= k
exists (b-a); bysimpl.
x, a, b: nat EX: existsk : nat, b - a <= k
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b, k: nat BO: b - a <= k
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat BO: b - a <= 0 GE: a <= x LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a <= k.+1 GE: a <= x LT: x < b
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a <= k.+1 GE: a <= x LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a <= k.+1 GE: a <= x LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b - 0 <= k.+1 GE: 0 <= x LT: x < b
[seq ρ <- index_iota 0 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b
[seq ρ <- index_iota a.+1 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b - 0 <= k.+1 GE: 0 <= x LT: x < b
[seq ρ <- index_iota 0 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b.+1 - 0 <= k.+1 GE: 0 <= x LT: x < b.+1
[seq ρ <- index_iota 0 b.+1 | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b.+1 - 0 <= k.+1 GE: 0 <= x LT: x < b.+1
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b.+1 - 0 <= k.+1 GE: 0 <= x LT: x < b.+1 EQ: (0 == x) = false
[seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] b: nat BO: b.+1 - 0 <= k.+1 LT: 0 < b.+1 GE: 0 <= 0
forallx : nat_eqType,
x \in index_iota 1 b.+1 -> x != 0
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b.+1 - 0 <= k.+1 GE: 0 <= x LT: x < b.+1 EQ: (0 == x) = false
[seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b.+1 - 0 <= k.+1 GE: 0 <= x LT: x < b.+1 EQ: (0 == x) = false
[seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, b: nat BO: b.+1 - 0 <= k.+1 GE: 0 <= x LT: x < b.+1 EQ: (0 == x) = false
[seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]
byapply IHk; lia.
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b
[seq ρ <- index_iota a.+1 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = true
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = true
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] a, b: nat BO: b - a.+1 <= k.+1 LT: a.+1 < b GE: a < a.+1
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] a, b: nat BO: b - a.+1 <= k.+1 LT: a.+1 < b GE: a < a.+1
forallx : nat_eqType,
x \in index_iota a.+2 b -> x != a.+1
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] a, b: nat BO: b - a.+1 <= k.+1 LT: a.+1 < b GE: a < a.+1 x: nat_eqType T1: a.+1 < x
x != a.+1
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
k: nat IHk: forallxab : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x] x, a, b: nat BO: b - a.+1 <= k.+1 GE: a < x LT: x < b EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
byrewrite IHk //; lia.}Qed.(** As a corollary we prove that filter of [iota_index a b] with predicate [(_ ∈ [::x])] yields [::x]. *)
forallxab : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]
forallxab : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]
x, a, b: nat NEQ: a <= x < b
[seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]
x, a, b: nat NEQ: a <= x < b
[seq ρ <- index_iota a b | ρ \in [:: x]] =
[seq ρ <- index_iota a b | ρ == x]
x, a, b: nat NEQ: a <= x < b x0: nat_eqType
(x0 \in [:: x]) = (x0 == x)
byrepeatrewrite in_cons; rewrite in_nil Bool.orb_false_r.Qed.(** Next we prove that if an element [x] is not in a sequence [xs], then [iota_index a b] filtered with predicate [(_ ∈ xs)] is equal to [iota_index a b] filtered with predicate [(_ ∈ rem_all x xs)]. *)
forall (abx : nat) (xs : seq_predType nat_eqType),
x < a ->
[seq ρ <- index_iota a b | ρ \in xs] =
[seq ρ <- index_iota a b | ρ \in rem_all x xs]
forall (abx : nat) (xs : seq_predType nat_eqType),
x < a ->
[seq ρ <- index_iota a b | ρ \in xs] =
[seq ρ <- index_iota a b | ρ \in rem_all x xs]
a, b, x: nat xs: seq_predType nat_eqType LT: x < a
[seq ρ <- index_iota a b | ρ \in xs] =
[seq ρ <- index_iota a b | ρ \in rem_all x xs]
a, b, x: nat xs: seq_predType nat_eqType LT: x < a
a, b, x: nat xs: seq_predType nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b
(y \in xs) = (y \in rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b IHxs: (y \in xs) = (y \in rem_all x xs)
(y \in y' :: xs) = (y \in rem_all x (y' :: xs))
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b
(y == y') || (y \in rem_all x xs) =
(y
\in (if y' == x
then rem_all x xs
else y' :: rem_all x xs))
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = true EQ2: (y' == x) = true
true || (y \in rem_all x xs) = (y \in rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = true EQ2: (y' == x) = false
true || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = false EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = true EQ2: (y' == x) = true
true || (y \in rem_all x xs) = (y \in rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = true EQ2: (y' == x) = false
true || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = false EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = true EQ2: (y' == x) = false
true || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = false EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = true EQ2: (y' == x) = false
true || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = false EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = false EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat y': nat_eqType xs: seq nat_eqType LT: x < a y: nat_eqType LE: a <= y GT: y < b EQ1: (y == y') = false EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
byrewrite in_cons EQ1.Qed.(** We prove that if an element [x] is a min of a sequence [xs], then [iota_index a b] filtered with predicate [(_ ∈ x::xs)] is equal to [x :: iota_index a b] filtered with predicate [(_ ∈ rem_all x xs)]. *)
forall (x : nat) (xs : seq_predType nat_eqType)
(ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
forall (x : nat) (xs : seq_predType nat_eqType)
(ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat xs: seq_predType nat_eqType a, b: nat B: a <= x < b MIN: forally : nat, y \in xs -> x <= y
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat xs: seq_predType nat_eqType a, b: nat B: a <= x < b MIN: forally : nat, y \in xs -> x <= y
existsk : nat, b - a <= k
x: nat xs: seq_predType nat_eqType a, b: nat B: a <= x < b MIN: forally : nat, y \in xs -> x <= y EX: existsk : nat, b - a <= k
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat xs: seq_predType nat_eqType a, b: nat B: a <= x < b MIN: forally : nat, y \in xs -> x <= y
existsk : nat, b - a <= k
exists (b-a); bysimpl.
x: nat xs: seq_predType nat_eqType a, b: nat B: a <= x < b MIN: forally : nat, y \in xs -> x <= y EX: existsk : nat, b - a <= k
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat xs: seq_predType nat_eqType a, b: nat B: a <= x < b MIN: forally : nat, y \in xs -> x <= y k: nat BO: b - a <= k
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat
forall (x : nat) (xs : seq_predType nat_eqType)
(ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat xs: seq_predType nat_eqType a, b: nat LE: a <= x GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= 0
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat LE: a <= x GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat xs: seq_predType nat_eqType a, b: nat LE: a <= x GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= 0
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat LE: a <= x GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat LE: a <= x GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat LE: a <= x GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 EQ: a = x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 EQ: a = x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
[seq ρ <- index_iota x b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota x b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
[seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- x :: index_iota x.+1 b
| ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
[seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- x :: index_iota x.+1 b
| ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
[seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
true = (x \in x :: xs)
all: byauto; rewrite in_cons eq_refl.
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- x :: index_iota x.+1 b
| ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x
:: [seq ρ <- index_iota x.+1 b
| ρ
\in (if x == x
then rem_all x xs
else x :: rem_all x xs)] =
x
:: (if x \in rem_all x xs
then
x
:: [seq ρ <- index_iota x.+1 b
| ρ \in rem_all x xs]
else
[seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs])
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs] =
x
:: (if x \in rem_all x xs
then
x
:: [seq ρ <- index_iota x.+1 b
| ρ \in rem_all x xs]
else
[seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs])
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
false = (x \in rem_all x xs)
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs] =
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x \notin rem_all x xs
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs] =
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs] =
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- a :: index_iota a.+1 b
| ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- a :: index_iota a.+1 b
| ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
false = (a \in x :: xs)
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
a \notin x :: xs
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a = x
False
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a \in xs
False
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a = x
False
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a \in xs
False
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a \in xs
False
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a \in xs
False
by move_neq_down LT; apply MIN.
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- a :: index_iota a.+1 b
| ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs]
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
false = (a \in rem_all x xs)
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a \in rem_all x xs
False
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x C: a \in xs
False
by move_neq_down LT; apply MIN.
k: nat IHk: forall (x : nat) (xs : seq_predType nat_eqType) (ab : nat),
a <= x < b ->
(forally : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] x: nat xs: seq_predType nat_eqType a, b: nat GT: x < b MIN: forally : nat, y \in xs -> x <= y BO: b - a <= k.+1 LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]
byrewrite IHk //; lia.Qed.(** For convenience, we define a special case of lemma [index_iota_filter_step] for [a = 0] and [b = k.+1]. *)
forall (x : nat) (xs : seq_predType nat_eqType)
(k : nat),
x <= k ->
(forally : nat, y \in xs -> x <= y) ->
[seq ρ <- range 0 k | ρ \in x :: xs] =
x :: [seq ρ <- range 0 k | ρ \in rem_all x xs]
forall (x : nat) (xs : seq_predType nat_eqType)
(k : nat),
x <= k ->
(forally : nat, y \in xs -> x <= y) ->
[seq ρ <- range 0 k | ρ \in x :: xs] =
x :: [seq ρ <- range 0 k | ρ \in rem_all x xs]
x: nat xs: seq_predType nat_eqType k: nat LE: x <= k MIN: forally : nat, y \in xs -> x <= y
[seq ρ <- range 0 k | ρ \in x :: xs] =
x :: [seq ρ <- range 0 k | ρ \in rem_all x xs]
byapply index_iota_filter_step; auto.Qed.(** We prove that if [x < a], then [x < (filter P (index_iota a b))[idx]] for any predicate [P]. *)
forall (xabidx : nat) (P : nat -> bool),
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat P: nat -> bool
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx
x, a, b, idx: nat P: nat -> bool
existsk : nat, b - a <= k
x, a, b, idx: nat P: nat -> bool EX: existsk : nat, b - a <= k
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx
x, a, b, idx: nat P: nat -> bool
existsk : nat, b - a <= k
exists (b-a); bysimpl.
x, a, b, idx: nat P: nat -> bool EX: existsk : nat, b - a <= k
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx
x, a, b, idx: nat P: nat -> bool k: nat BO: b - a <= k
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= 0 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= 0 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat P: nat -> bool BO: b - a <= 0 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x]
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat P: nat -> bool LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] BO: b - a = 0
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (xabidx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x]
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: b <= a
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: b <= a
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] EQ: b - a = 0
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b
x < nth 0 [seq x <- a :: index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = true
x <
nth 0 (a :: [seq x <- index_iota a.+1 b | P x]) idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = true
x <
nth 0 (a :: [seq x <- index_iota a.+1 b | P x]) idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx.+1 < size [seq x <- index_iota a b | P x] N: a < b PA: P a = true
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx.+1 < size [seq x <- index_iota a b | P x] N: a < b PA: P a = true
idx < size [seq x <- index_iota a.+1 b | P x]
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
k: nat IHk: forall (xabidx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx x, a, b, idx: nat P: nat -> bool BO: b - a <= k.+1 LT1: x < a LT2: idx < size [seq x <- index_iota a b | P x] N: a < b PA: P a = false
idx < size [seq x <- index_iota a.+1 b | P x]
byrewrite index_iota_lt_step // //= PA //= in LT2.Qed.EndIotaRange.(** A sequence [xs] is a prefix of another sequence [ys] iff there exists a sequence [xs_tail] such that [ys] is a concatenation of [xs] and [xs_tail]. *)Definitionprefix_of {T : eqType} (xsys : seq T) := existsxs_tail, xs ++ xs_tail = ys.(** Furthermore, every prefix of a sequence is said to be strict if it is not equal to the sequence itself. *)Definitionstrict_prefix_of {T : eqType} (xsys : seq T) :=
existsxs_tail, xs_tail <> [::] /\ xs ++ xs_tail = ys.(** We define a helper function that shifts a sequence of numbers forward by a constant offset, and an analogous version that shifts them backwards, removing any number that, in the absence of Coq' s saturating subtraction, would become negative. These functions are very useful in transforming abstract RTA's search space. *)Definitionshift_points_pos (xs : seq nat) (s : nat) : seq nat :=
map (addn s) xs.Definitionshift_points_neg (xs : seq nat) (s : nat) : seq nat :=
letnonsmall := filter (funx => x >= s) xs in
map (funx => x - s) nonsmall.