Library prosa.util.list

Require Import prosa.util.ssrlia prosa.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Definition max0 := foldl maxn 0.
Definition first0 := head 0.
Definition last0 := last 0.

Section Last0.

  Lemma last0_cons:
    ∀ x xs,
      xs ≠ [::] →
      last0 (x::xs) = last0 xs.

  Lemma last0_cat:
    ∀ xs_l xs_r,
      xs_r ≠ [::] →
      last0 (xs_l ++ xs_r) = last0 xs_r.

  Lemma last0_nth:
    ∀ xs,
      last0 xs = nth 0 xs (size xs).-1.

  Lemma last0_ex_cat:
    ∀ x xs,
      xs ≠ [::] →
      last0 xs = x →
      ∃ xsh, xsh ++ [::x] = xs.

  Lemma last0_filter:
    ∀ x xs (P : nat → bool),
      xs ≠ [::] →
      last0 xs = x →
      P x →
      last0 [seq x <- xs | P x] = x.

End Last0.

Section Max0.

  Lemma max0_cons: ∀ x xs, max0 (x :: xs) = maxn x (max0 xs).

  Lemma max0_of_uniform_set:
    ∀ k xs,
      size xs > 0 →
      (∀ x, x \in xs → x = k) →
      max0 xs = k.

  Lemma in_max0_le:
    ∀ xs x, x \in xs → x ≤ max0 xs.

  Lemma max0_in_seq:
    ∀ xs,
      xs ≠ [::] →
      max0 xs \in xs.

  Lemma max0_2cons_eq:
    ∀ x xs,
      max0 (x::x::xs) = max0 (x::xs).

  Lemma max0_2cons_le:
    ∀ x1 x2 xs,
      x1 ≤ x2 →
      max0 (x1::x2::xs) = max0 (x2::xs).

  Lemma max0_rem0:
    ∀ xs,
      max0 ([seq x <- xs | 0 < x]) = max0 xs.

  Lemma last_of_seq_le_max_of_seq:
    ∀ xs, last0 xs ≤ max0 xs.

  Notation "xs [| n |]" := (nth 0 xs n) (at level 30).

  Lemma max_of_dominating_seq:
    ∀ (xs ys : seq nat),
      (∀ 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:
    ∀ (T: eqType) (x y: T) (xs: seq T),
      x \in rem y xs → x \in 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:
    ∀ (T: eqType) (x:T) (xs: seq T) (P: T → bool),
      (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 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.

  (* 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,
      (∀ x, x \in xs → ~~ P x) →
      filter P xs = [::].

  Lemma eq_ind_in_seq:
    ∀ (T : eqType) a b (xs : seq T),
      index a xs = index b xs →
      uniq xs →
      a \in xs →
      b \in xs →
      a = b.

  Lemma default_or_in:
    ∀ (T : eqType) (n : nat) (d : T) (xs : seq T),
      nth d xs n = d ∨ nth d xs n \in xs.

  Lemma exists_two:
    ∀ (T : eqType) (xs : seq T),
      size xs > 1 →
      uniq xs →
      ∃ a b, a ≠ b ∧ a \in xs ∧ b \in xs.

End AdditionalLemmas.

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.

  Lemma nin_rem_all:
    ∀ {X : eqType} (x : X) (xs : seq X),
      ¬ (x \in rem_all x xs).

  Lemma in_rem_all:
    ∀ {X : eqType} (a x : X) (xs : seq X),
      a \in rem_all x xs → a \in xs.

  Lemma rem_lt_id:
    ∀ x xs,
      (∀ y, y \in xs → x < y) →
      rem_all x xs = xs.

End RemAllList.

Definition range (a b : nat) := index_iota a b.+1.

Section IotaRange.

  Remark index_iota_lt_step:
    ∀ a b,
      a < b →
      index_iota a b = a :: index_iota a.+1 b.

  Lemma range_filter_2cons:
    ∀ x xs k,
      [seq ρ <- range 0 k | ρ \in x :: x :: xs] =
      [seq ρ <- range 0 k | ρ \in x :: xs].

  Lemma index_iota_filter_eqx:
    ∀ x a b,
      a ≤ x < b →
      [seq ρ <- index_iota a b | ρ == x] = [::x].

  Corollary index_iota_filter_singl:
    ∀ x a b,
      a ≤ x < b →
      [seq ρ <- index_iota a b | ρ \in [:: x]] = [::x].

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

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

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

  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.

Definition prefix (T : eqType) (xs ys : seq T) := ∃ xs_tail, xs ++ xs_tail = ys.

Definition strict_prefix (T : eqType) (xs ys : seq T) :=
  ∃ xs_tail, xs_tail ≠ [::] ∧ xs ++ xs_tail = ys.