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 first0 := head 0.
Definition last0 := last 0.

Additional lemmas about last0.
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.
  Lemma last0_cat :
     xs_l xs_r,
      xs_r [::]
      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].
  Lemma last0_ex_cat :
     x xs,
      xs [::]
      last0 xs = x
       xsh, xsh ++ [::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.

Additional lemmas about max0.
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.
  Lemma max0_of_uniform_set :
     k xs,
      size xs > 0
      ( x, x \in xs x = k)
      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.
  Lemma last_of_seq_le_max_of_seq:
     xs, last0 xs max0 xs.

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.
  Lemma max_of_dominating_seq :
     xs ys,
      ( n, xs[|n|] ys[|n|])
      max0 xs max0 ys.

End Max0.

Additional lemmas about rem for lists.
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.

Additional lemmas about sequences.
Section AdditionalLemmas.

First, we prove that x::xs = ys is a sufficient condition for x to be in ys.
  Lemma mem_head_impl :
     {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.
  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.

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

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

End AdditionalLemmas.

Additional lemmas about sorted.
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].
  Lemma sorted_split :
     {X : eqType} (xs : seq X) P f t,
      sorted (fun x yf 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.

Additional lemmas about last.
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.

Additional lemmas about rem_all for lists.
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.

Additional lemmas about index_iota and range for lists.
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.
  Lemma iotaD_impl :
     n_le m n,
      n_le n
      iota m n = iota m n_le ++ iota (m + n_le) (n - n_le).

Next, we prove that index_iota a b = a :: index_iota a.+1 b for a < b.
  Remark index_iota_lt_step :
     a b,
      a < b
      index_iota a b = a :: index_iota a.+1 b.

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

Consider a, b, and x s.t. a x < b, then filter of iota_index a b with predicate (_ == x) yields ::x.
  Lemma index_iota_filter_eqx :
     x a b,
      a x < b
      [seq ρ <- index_iota a b | ρ == x] = [::x].

As a corollary we prove that 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].

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

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

For convenience, we define a special case of lemma index_iota_filter_step for a = 0 and b = k.+1.
  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].

We prove that if x < a, then x < (filter P (index_iota a b))[idx] for any predicate P.
  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.

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 :=
  map (addn s) xs.
Definition shift_points_neg (xs : seq nat) (s : nat) : seq nat :=
  let nonsmall := filter (fun xx s) xs in
  map (fun xx - s) nonsmall.