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

We define a few simple operations on lists that return zero for empty lists: max0, first0, and last0.
Definition max0 := foldl maxn 0.
Definition last0 := last 0.

Section Last0.

Let xs be a non-empty sequence and x be an arbitrary element, then we prove that last0 (x::xs) = last0 xs.
Lemma last0_cons :
x xs,
xs [::]
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 also prove that last0 xs = xs [| size xs -1 |] .
Lemma last0_nth :
xs,
last0 xs = nth 0 xs (size xs).-1.

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.
Section Max0.

First we prove that max0 (x::xs) is equal to max {x, max0 xs}.
Lemma max0_cons : x xs, max0 (x :: xs) = maxn x (max0 xs).

Next, we prove that if all the numbers of a seq xs are equal to a constant k, then max0 xs = k.
We prove that no element in a sequence xs is greater than max0 xs.
Lemma in_max0_le :
xs x, x \in xs x max0 xs.

We prove that for a non-empty sequence xs, max0 xs xs.
Lemma max0_in_seq :
xs,
xs [::]
max0 xs \in xs.

We prove a technical lemma stating that one can remove duplicating element from the head of a sequence.
Lemma max0_2cons_eq :
x xs,
max0 (x::x::xs) = max0 (x::xs).

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.
Lemma max0_2cons_le :
x1 x2 xs,
x1 x2
max0 (x1::x2::xs) = max0 (x2::xs).

We prove that max0 of a sequence xs is equal to max0 of sequence xs without 0s.
Lemma max0_rem0 :
xs,
max0 ([seq x <- xs | 0 < x]) = max0 xs.

Note that the last element is at most the max element.
Let's introduce the notion of the nth element of a sequence.
Notation "xs [| n |]" := (nth 0 xs n) (at level 30).

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.
Section RemList.

We prove that if x lies in xs excluding y, then x also lies in xs.
Lemma rem_in :
{X : eqType} (x y : X) (xs : seq X),
x \in rem y xs x \in xs.

Similarly, we prove that if x y and x lies in xs, then x lies in xs excluding y.
Lemma in_neq_impl_rem_in :
{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.

First, we prove that x::xs = ys is a sufficient condition for x to be in ys.
{X : eqType} (x : X) (xs ys : seq X),
x::xs = ys
x \in ys.

We show that if n > 0, then nth (x::xs) n = nth xs (n-1).
Lemma nth0_cons :
x xs n,
n > 0
nth 0 (x :: xs) n = nth 0 xs n.-1.

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.

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.

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.

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.
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).
Given two sequences xs and ys of equal size and without duplicates, the fact that xs ys implies that ys 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 = [::].

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.

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.

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.

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.

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

Section Last.

First, we show that the default element does not change the value of last for non-empty sequences.
Lemma nonnil_last :
{X : eqType} (xs : seq X) (d1 d2 : X),
xs != [::]
last d1 xs = last d2 xs.

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.

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.

Section RemAllList.

First we prove that x rem_all x xs.
Lemma nin_rem_all :
{X : eqType} (x : X) (xs : seq X),
¬ (x \in rem_all x xs).

Next we show that rem_all x xs xs.
Lemma in_rem_all :
{X : eqType} (a x : X) (xs : seq X),
a \in rem_all x xs a \in xs.

If an element x is smaller than any element of a sequence xs, then rem_all x xs = xs.
Lemma rem_lt_id :
x xs,
( y, y \in xs x < y)
rem_all x xs = xs.

End RemAllList.

To have a more intuitive naming, we introduce the definition of range a b which is equal to index_iota a b.+1.
Definition range (a b : nat) := index_iota a b.+1.

Section IotaRange.

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.
Next, we prove that index_iota a b = a :: index_iota a.+1 b for a < b.
We prove that one can remove duplicating element from the head of a sequence by which range is filtered.
Consider a, b, and x s.t. a x < b, then filter of iota_index a b with predicate (_ == x) yields ::x.
As a corollary we prove that filter of iota_index a b with predicate (_ [::x]) yields ::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).
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).
For convenience, we define a special case of lemma index_iota_filter_step for a = 0 and b = k.+1.
We prove that if x < a, then x < P a b))[idx] for any predicate P.
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.
Definition prefix_of {T : eqType} (xs ys : seq T) := xs_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.
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.
Definition shift_points_pos (xs : seq nat) (s : nat) : seq nat :=