Library rt.util.list

Require Import rt.util.tactics.

(* Lemmas about lists without duplicates. *)
Section UniqList.

  Lemma idx_lt_rcons :
    ∀ {T: eqType} (l: seq T) i x0,
      uniq l →
      i < size l →
      [seq x <- l | index x l < i.+1] =
        rcons [seq x <- l | index x l < i] (nth x0 l i).

  Lemma filter_idx_lt_take :
    ∀ {T: eqType} (l: seq T) i,
      uniq l →
      i < size l →
      [seq x <- l | index x l < i] = take i l.

  Lemma filter_idx_le_takeS :
    ∀ {T: eqType} (l: seq T) i,
      uniq l →
      i < size l →
      [seq x <- l | index x l ≤ i] = take i.+1 l.

End UniqList.

(* Additional lemmas about list zip. *)
Section Zip.

  Lemma zipP {T: eqType} (x0: T) (P: _ → _ → bool) (X Y: seq T):
    size X = size Y →
    reflect (∀ i, i < size (zip X Y) → P (nth x0 X i) (nth x0 Y i))
            (all (fun p ⇒ P (fst p) (snd p)) (zip X Y)).

  Lemma mem_zip_exists :
    ∀ (T T': eqType) (x1: T) (x2: T') l1 l2 elem elem',
      size l1 = size l2 →
      (x1, x2) \in zip l1 l2 →
      ∃ idx,
        idx < size l1 ∧
        idx < size l2 ∧
        x1 = nth elem l1 idx ∧
        x2 = nth elem' l2 idx.

End Zip.

(* Restate nth_error function from Coq library. *)
Fixpoint nth_or_none {T: Type} (l: seq T) (n:nat) {struct n} : option T :=
  match n, l with
  | 0, x :: _ ⇒ Some x
  | n.+1, _ :: l ⇒ nth_or_none l n
  | _, _ ⇒ None
end.

(* Lemmas about nth_or_none. *)
Section NthOrNone.

  Context {T: eqType}.

  Lemma nth_or_none_mem :
    ∀ (l: seq T) n x, nth_or_none l n = Some x → x \in l.

  Lemma nth_or_none_mem_exists :
    ∀ (l: seq T) x, x \in l → ∃ n, nth_or_none l n = Some x.

  Lemma nth_or_none_size_none :
    ∀ (l: seq T) n,
      nth_or_none l n = None ↔ n ≥ size l.

  Lemma nth_or_none_size_some :
    ∀ (l: seq T) n x,
      nth_or_none l n = Some x → n < size l.

  Lemma nth_or_none_uniq :
    ∀ (l: seq T) i j x,
      uniq l →
      nth_or_none l i = Some x →
      nth_or_none l j = Some x →
      i = j.

Lemma nth_or_none_nth :
    ∀ (l: seq T) n x x0,
      nth_or_none l n = Some x →
      nth x0 l n = x.

End NthOrNone.