Library probsa.util.seq

From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq.

Require Export prosa.util.list.

Lemma seq_split_take_drop :
  ∀ {X : eqType} (e : X) (xs : seq X),
    (e \in xs) →
    xs = take (index e xs) xs ++ [:: e] ++ drop (index e xs).+1 xs.
Lemma seq_split :
  ∀ {X : eqType} (e : X) (xs : seq X),
    (e \in xs) →
    ∃ xs1 xs2,
      xs = xs1 ++ [::e] ++ xs2
      ∧ (e \notin xs1).

Lemma choose_superior_default_or_in_seq :
  ∀ {X : eqType} (R : rel X) (a e : X) (ys : seq X),
    foldr (choose_superior R) (Some a) ys = Some e →
    a = e ∨ e \in ys.
Lemma foldr_choose_superior_not_none :
  ∀ {X : eqType} (R : rel X) (e : X) (ys : seq X),
    ¬ foldr (choose_superior R) (Some e) ys = None.
Lemma foldr_choose_superior_in_seq :
  ∀ {X : eqType} (R : rel X) (ys : seq X) (y e : X),
    (y \in ys) →
    (R y e) →
    foldr (choose_superior R) (Some e) ys = Some e →
    e \in ys.
Lemma supremum_monotone_wrt_subset :
  ∀ {X : eqType} (R : rel X) (e : X) (xs ys : seq X),
    reflexive R →
    total R →
    transitive R →
    uniq ys →
    subseq xs ys →
    (e \in xs) →
    supremum R ys = Some e →
    supremum R xs = Some e.
Lemma subseq_filter :
  ∀ {X : eqType} (xs : seq X) (P1 P2 : pred X),
    (∀ x, x \in xs → P1 x → P2 x) →
    subseq [seq x <- xs | P1 x] [seq x <- xs | P2 x].