# Library prosa.util.list

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Require Export mathcomp.zify.zify.

Require Import prosa.util.tactics.

Require Export prosa.util.supremum.

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.

Additional lemmas about last0.

Let xs be a non-empty sequence and x be an arbitrary element,
then we prove that last0 (x::xs) = last0 xs.

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.

We prove that for any non-empty sequence xs there is a sequence xsh
such that xsh ++ [::last0 x] = [xs].

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.

Lemma last0_filter :

∀ x xs (P : nat → bool),

xs ≠ [::] →

last0 xs = x →

P x →

last0 [seq x <- xs | P x] = x.

End Last0.

∀ x xs (P : nat → bool),

xs ≠ [::] →

last0 xs = x →

P x →

last0 [seq x <- xs | P x] = x.

End Last0.

Additional lemmas about max0.

We prove a technical lemma stating that one can remove
duplicating element from the head of a sequence.

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.

Note that the last element is at most the max element.

Let's introduce the notion of the nth element of a sequence.

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.

Additional lemmas about rem for lists.

Lemma in_neq_impl_rem_in :

∀ {X : eqType} (x y : X) (xs : seq X),

x \in xs →

x != y →

x \in rem y xs.

∀ {X : eqType} (x y : X) (xs : seq X),

x \in xs →

x != y →

x \in rem y xs.

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.

Lemma filter_size_rem :

∀ {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 x xs | P y] + 1.

End RemList.

∀ {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 x xs | P y] + 1.

End RemList.

Additional lemmas about sequences.

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

Lemma seq_elim_last :

∀ {X : Type} (n : nat) (xs : seq X),

size xs = n.+1 →

∃ x xs__c, xs = xs__c ++ [:: x] ∧ size xs__c = n.

∀ {X : Type} (n : nat) (xs : seq X),

size xs = n.+1 →

∃ x xs__c, xs = xs__c ++ [:: x] ∧ size xs__c = n.

Next, we prove that x ∈ xs implies that xs can be split
into two parts such that xs = xsl ++ [::x] ++ [xsr].

Lemma in_cat :

∀ {X : eqType} (x : X) (xs : list X),

x \in xs → ∃ xsl xsr, xs = xsl ++ [::x] ++ xsr.

∀ {X : eqType} (x : X) (xs : list X),

x \in xs → ∃ xsl xsr, xs = xsl ++ [::x] ++ xsr.

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.

Lemma subseq_leq_size :

∀ {X : eqType} (xs ys: seq X),

uniq xs →

(∀ x, x \in xs → x \in ys) →

size xs ≤ size ys.

∀ {X : eqType} (xs ys: seq X),

uniq xs →

(∀ x, x \in xs → x \in ys) →

size xs ≤ size ys.

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.

Lemma in_zip :

∀ {X Y : eqType} (xs : seq X) (ys : seq Y) (x x__d : X) (y y__d : Y),

size xs = size ys →

(∃ idx, idx < size xs ∧ nth x__d xs idx = x ∧ nth y__d ys idx = y) →

(x, y) \in zip xs ys.

∀ {X Y : eqType} (xs : seq X) (ys : seq Y) (x x__d : X) (y y__d : Y),

size xs = size ys →

(∃ idx, idx < size xs ∧ nth x__d xs idx = x ∧ nth y__d ys idx = y) →

(x, y) \in zip xs ys.

This lemma allows us to check proposition of the form
∀ x ∈ xs, ∃ y ∈ ys, P x y using a boolean expression
all P (zip xs ys).

Lemma forall_exists_implied_by_forall_in_zip:

∀ {X Y : eqType} (P_bool : X × Y → bool) (P_prop : X → Y → Prop) (xs : seq X),

(∀ x y, P_bool (x, y) ↔ P_prop x y) →

(∃ ys, size xs = size ys ∧ all P_bool (zip xs ys) == true) →

(∀ x, x \in xs → ∃ y, P_prop x y).

∀ {X Y : eqType} (P_bool : X × Y → bool) (P_prop : X → Y → Prop) (xs : seq X),

(∀ x y, P_bool (x, y) ↔ P_prop x y) →

(∃ ys, size xs = size ys ∧ all P_bool (zip xs ys) == true) →

(∀ x, x \in xs → ∃ y, P_prop x y).

Given two sequences xs and ys of equal size and without
duplicates, the fact that xs ⊆ ys implies that ys ⊆ xs.

Lemma subseq_eq:

∀ {X : eqType} (xs ys : seq X),

uniq xs →

uniq ys →

size xs = size ys →

(∀ x, x \in xs → x \in ys) →

(∀ x, x \in ys → x \in xs).

∀ {X : eqType} (xs ys : seq X),

uniq xs →

uniq ys →

size xs = size ys →

(∀ x, x \in xs → x \in ys) →

(∀ x, x \in ys → x \in xs).

We prove that if no element of a sequence xs satisfies a
predicate P, then filter P xs is equal to an empty
sequence.

Lemma filter_in_pred0 :

∀ {X : eqType} (xs : seq X) (P : pred X),

(∀ x, x \in xs → ~~ P x) →

filter P xs = [::].

∀ {X : eqType} (xs : seq X) (P : pred X),

(∀ x, x \in xs → ~~ P x) →

filter P xs = [::].

We show that any two elements having the same index in a
sequence must be equal.

Lemma eq_ind_in_seq :

∀ {X : eqType} (a b : 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),

index a xs = index b xs →

a \in xs →

b \in xs →

a = b.

We show that the nth element in a sequence is either in the
sequence or is the default element.

Lemma default_or_in :

∀ {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),

nth d xs n = d ∨ nth d xs n \in xs.

We show that in a unique sequence of size greater than one
there exist two unique elements.

Lemma exists_two :

∀ {X : eqType} (xs : seq X),

size xs > 1 →

uniq xs →

∃ a b, a ≠ b ∧ a \in xs ∧ b \in xs.

∀ {X : eqType} (xs : seq X),

size xs > 1 →

uniq xs →

∃ a b, a ≠ b ∧ a \in xs ∧ b \in xs.

The predicate all implies the predicate has, if the sequence is not empty.

Lemma has_all_nilp {T : eqType}:

∀ (s : seq T) (P : pred T),

all P s →

~~ nilp s →

has P s.

End AdditionalLemmas.

∀ (s : seq T) (P : pred T),

all P s →

~~ nilp s →

has P s.

End AdditionalLemmas.

Additional lemmas about sorted.

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

Lemma sorted_split :

∀ {X : eqType} (xs : seq X) P f t,

sorted (fun x y ⇒ f x ≤ f y) xs →

[seq x <- xs | P x] = [seq x <- xs | P x & f x ≤ t] ++ [seq x <- xs | P x & f x > t].

∀ {X : eqType} (xs : seq X) P f t,

sorted (fun x y ⇒ f x ≤ f y) xs →

[seq x <- xs | P x] = [seq x <- xs | P x & f x ≤ t] ++ [seq x <- xs | P x & f x > t].

We show that if a sequence xs1 ++ xs2 is sorted, then both
subsequences xs1 and xs2 are sorted as well.

Lemma sorted_cat:

∀ {X : eqType} {R : rel X} (xs1 xs2 : seq X),

transitive R →

sorted R (xs1 ++ xs2) → sorted R xs1 ∧ sorted R xs2.

End Sorted.

∀ {X : eqType} {R : rel X} (xs1 xs2 : seq X),

transitive R →

sorted R (xs1 ++ xs2) → sorted R xs1 ∧ sorted R xs2.

End Sorted.

Additional lemmas about last.

First, we show that the default element does not change the
value of last for non-empty sequences.

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.

Lemma filter_last_mem :

∀ {X : eqType} (xs : seq X) (d : X) (P : pred X),

has P xs →

last d (filter P xs) \in xs.

End Last.

∀ {X : eqType} (xs : seq X) (d : X) (P : pred X),

has P xs →

last d (filter P xs) \in xs.

End Last.

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.

Fixpoint rem_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.

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.

To have a more intuitive naming, we introduce the definition of
range a b which is equal to index_iota a b.+1.

Additional lemmas about index_iota and range for lists.

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.

We prove that one can remove duplicating element from the
head of a sequence by which range is filtered.

Lemma range_filter_2cons :

∀ x xs k,

[seq ρ <- range 0 k | ρ \in x :: x :: xs] =

[seq ρ <- range 0 k | ρ \in x :: xs].

∀ x xs k,

[seq ρ <- range 0 k | ρ \in x :: x :: xs] =

[seq ρ <- range 0 k | ρ \in x :: xs].

Consider a, b, and x s.t. a ≤ x < b,
then filter of iota_index a b with predicate
(_ == x) yields ::x.

Corollary index_iota_filter_singl :

∀ x a b,

a ≤ x < b →

[seq ρ <- index_iota a b | ρ \in [:: x]] = [::x].

∀ x a b,

a ≤ x < b →

[seq ρ <- index_iota a b | ρ \in [:: x]] = [::x].

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

Lemma index_iota_filter_inxs :

∀ a b x xs,

x < a →

[seq ρ <- index_iota a b | ρ \in xs] =

[seq ρ <- index_iota a b | ρ \in rem_all x xs].

∀ a b x xs,

x < a →

[seq ρ <- index_iota a b | ρ \in xs] =

[seq ρ <- index_iota a b | ρ \in rem_all x xs].

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

Lemma index_iota_filter_step :

∀ x xs a b,

a ≤ x < b →

(∀ y, 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 xs a b,

a ≤ x < b →

(∀ y, y \in xs → x ≤ y) →

[seq ρ <- index_iota a b | ρ \in x :: xs] =

x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs].

Corollary range_iota_filter_step:

∀ x xs k,

x ≤ k →

(∀ y, y \in xs → x ≤ y) →

[seq ρ <- range 0 k | ρ \in x :: xs] =

x :: [seq ρ <- range 0 k | ρ \in rem_all x xs].

∀ x xs k,

x ≤ k →

(∀ y, y \in xs → x ≤ y) →

[seq ρ <- range 0 k | ρ \in x :: xs] =

x :: [seq ρ <- range 0 k | ρ \in rem_all x xs].

Lemma iota_filter_gt:

∀ x a b idx P,

x < a →

idx < size ([seq x <- index_iota a b | P x]) →

x < nth 0 [seq x <- index_iota a b | P x] idx.

End IotaRange.

∀ x a b idx P,

x < a →

idx < size ([seq x <- index_iota a b | P x]) →

x < nth 0 [seq x <- index_iota a b | P x] idx.

End IotaRange.

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.

Furthermore, every prefix of a sequence is said to be
strict if it is not equal to the sequence itself.

Definition strict_prefix_of {T : eqType} (xs ys : seq T) :=

∃ xs_tail, xs_tail ≠ [::] ∧ xs ++ xs_tail = ys.

∃ xs_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.