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.

Maximum, First, and Last Element of Empty Lists

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.

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

Lemmas about 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.

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, (nth 0 xs n) ≤ (nth 0 ys n)) →
    max0 xs ≤ max0 ys.

Additional Lemmas about rem

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.

Misc. Additional Lemmas about Sequences

First, we show that a sequence xs contains the same elements as a sequence undup xs.
Lemma in_seq_equiv_undup :
  ∀ {X : eqType} (xs : seq X) (x : X),
    (x \in undup xs) = (x \in xs).

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.

Equality of singleton lists is identical to equality of option types.
Lemma seq1_some {T : eqType} :
  ∀ (x y : T),
    ([:: x] == [:: y]) = (Some x == Some y).

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.

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.

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

Additional Lemmas about 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.

Removing all Instances of a Given Value from a List

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.

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.

Range of Indices

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.

In the following, we establish some 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.
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.

Splitting index_iota t1 t2 at t yields two concatenated iotas.
Lemma index_iota_cat :
  ∀ t t1 t2,
    t1 ≤ t ≤ t2 →
    index_iota t1 t2 = index_iota t1 t ++ index_iota t t2.

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.

Additional Lemmas about count

If f implies g for all elements in xs, then the number of elements in xs satisfying f is less than or equal to the number of elements satisfying g.
Lemma sub_count_seq :
  ∀ {X : eqType} (f g : pred X) (xs : seq X),
    {in xs, ∀ x, f x → g x} →
    count f xs ≤ count g xs.

We adapt ssreflect’s count_predUI lemma for easier rewriting: the count of elements satisfying P1 ∪ P2 equals the sum of counts for P1 and P2, minus the count of elements satisfying both.
Lemma count_predUI' :
  ∀ (P1 P2 : pred nat) (xs : seq nat),
    count (predU P1 P2) xs = count P1 xs + count P2 xs - count (predI P1 P2) xs.

Prefix Definitions

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.
Definition strict_prefix_of {T : eqType} (xs ys : seq T) :=
  ∃ xs_tail, xs_tail ≠ [::] ∧ xs ++ xs_tail = ys.

Shifting Sequences of Natural Numbers

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 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 x ⇒ x ≥ s) xs in
  map (fun x ⇒ x - s) nonsmall.