Library prosa.classic.util.list

Require Export prosa.util.list.

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

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

  Lemma mapP2 (T: Type) (T': eqType) (s: seq T) (f: T T') y:
    reflect (exists2 x, List.In x s & y = f x) (y \in map f s).

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

  Lemma mem_zip :
     (T T': eqType) (x1: T) (x2: T') l1 l2,
      size l1 = size l2
      (x1, x2) \in zip l1 l2
      x1 \in l1 x2 \in l2.

  Lemma mem_zip_nseq_r :
     {T1 T2:eqType} (x: T1) (y: T2) n l,
      size l = n
      ((x, y) \in zip l (nseq n y)) = (x \in l).

  Lemma mem_zip_nseq_l :
     {T1 T2:eqType} (x: T1) (y: T2) n l,
      size l = n
      ((x, y) \in zip (nseq n x) l) = (y \in l).

  Lemma unzip1_pair:
     {T1 T2: eqType} (l: seq T1) (f: T1 T2),
      unzip1 [seq (x, f x) | x <- l] = l.

  Lemma unzip2_pair:
     {T1 T2: eqType} (l: seq T1) (f: T1 T2),
      unzip2 [seq (f x, x) | x <- l] = l.

  Lemma eq_unzip1:
     {T1 T2: eqType} (l1 l2: seq (T1 × T2)) x0,
      size l1 = size l2
      ( i, i < size l1 (fst (nth x0 l1 i)) = (fst (nth x0 l2 i)))
      unzip1 l1 = unzip1 l2.

  Lemma eq_unzip2:
     {T1 T2: eqType} (l1 l2: seq (T1 × T2)) x0,
      size l1 = size l2
      ( i, i < size l1 (snd (nth x0 l1 i)) = (snd (nth x0 l2 i)))
      unzip2 l1 = unzip2 l2.

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, _ :: lnth_or_none l n
  | _, _None
end.

(* Lemmas about nth. *)
Section Nth.

  Context {T: eqType}.

  Lemma nth_in_or_default:
     (l: seq T) x0 i,
      (nth x0 l i) \in l (nth x0 l i) = x0.

  Lemma nth_neq_default :
     (l: seq T) x0 i y,
      nth x0 l i = y
      y x0
      y \in l.

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

Section PartialMap.

  Lemma pmap_inj_in_uniq {T T': eqType} (s: seq T) (f: T option T') :
    {in s &, ssrfun.injective f}
    uniq s
    uniq (pmap f s).

  Lemma pmap_inj_uniq {T T': eqType} (s: seq T) (f: T option T') :
    ssrfun.injective f
    uniq s
    uniq (pmap f s).

End PartialMap.

(* Define a set_nth that does not grow the vector. *)
Program Definition set_nth_if_exists {T: Type} (l: seq T) n y :=
  if n < size l then
    set_nth _ l n y
  else l.

(* Define a function that replaces the first element that satisfies
   some predicate with using a mapping function f. *)

Fixpoint replace_first {T: Type} P f (l: seq T) :=
  if l is x0 :: l' then
    if P x0 then
      f x0 :: l'
    else x0 :: replace_first P f l'
  else [::].

(* Define a function that replaces the first element that satisfies
   some predicate with a constant. *)

Definition replace_first_const {T: Type} P y (l: seq T) :=
  replace_first P (fun xy) l.

Definition set_pair_1nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
  (fst p, y).

Definition set_pair_2nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
  (fst p, y).

Section Replace.

  Context {T: eqType}.

  Lemma replace_first_size P f (l: seq T) :
    size (replace_first P f l) = size l.

  Lemma replace_first_cases {P} {f} {l: seq T} {x}:
    x \in replace_first P f l
    x \in l ( y, x = f y P y y \in l).

  Lemma replace_first_no_change {P} {f} {l: seq T} {x}:
    x \in l
    ~~ P x
    x \in replace_first P f l.

  Lemma replace_first_idempotent {P} {f} {l: seq T} {x}:
    x \in l
    f x = x
    x \in replace_first P f l.

  Lemma replace_first_new :
     P f (l: seq T) x1 x2,
    x1 \notin l
    x2 \notin l
    x1 \in replace_first P f l
    x2 \in replace_first P f l
    x1 = x2.

  Lemma replace_first_previous P f {l: seq T} {x}:
    x \in l
      (x \in replace_first P f l)
      (P x f x \in replace_first P f l).

  Lemma replace_first_failed P f {l: seq T}:
    ( x, x \in l f x \notin replace_first P f l)
    ( x, x \in l ~~ P x).

End Replace.

Definition pairs_to_function {T1: eqType} {T2: Type} y0 (l: seq (T1×T2)) :=
  fun xnth y0 (unzip2 l) (index x (unzip1 l)).

Section Pairs.

  Lemma pairs_to_function_neq_default {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
    pairs_to_function y0 l x = y
    y y0
    (x,y) \in l.

  Lemma pairs_to_function_mem {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
    uniq (unzip1 l)
    (x,y) \in l
    pairs_to_function y0 l x = y.

End Pairs.

Section Order.

  Context {T: eqType}.
  Variable rel: T T bool.
  Variable l: seq T.

  Definition total_over_list :=
     x1 x2,
      x1 \in l
      x2 \in l
      (rel x1 x2 rel x2 x1).

  Definition antisymmetric_over_list :=
     x1 x2,
      x1 \in l
      x2 \in l
      rel x1 x2
      rel x2 x1
      x1 = x2.

End Order.

(* In this section we prove some additional lemmas about sequences. *)
Section AdditionalLemmas.

  (* First, 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 define a local function max over lists using foldl and maxn. *)
  Let max := foldl maxn 0.

  (* We prove that max {x, xs} is equal to max {x, max xs}. *)
  Lemma seq_max_cons: x xs, max (x :: xs) = maxn x (max xs).

  (* We prove that for any two sequences xs and ys the fact that xs is a subsequence 
     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.

End AdditionalLemmas.