Require Export fl.cfg.Base.

Module Lists.

  Import Base.

  Section Lists.

    Global Instance eq_dec_prod X Y (Dx : eq_dec X) (Dy : eq_dec Y) :
      eq_dec (X × Y).

    Global Instance filter_prod_dec X Y {D : eq_dec X} (x : X) :
      ∀ (e : X × Y) , dec ((fun e : X × Y ⇒ match e with (xe, _) ⇒ x = xe end) e).

    Global Instance splitList_dec X (D : eq_dec X) (xs ys : list X) : dec (∃ zs, xs = ys ++ zs).

    Fixpoint slists (X : Type) (p : X → Prop) {pdec : ∀ x, dec (p x)} (xs : list X) : list (list X) :=
      match xs with
        | [] ⇒ [[]]
| s::xs' ⇒
          let
            ys := @slists _ _ pdec xs'
          in let
            zs := map (cons s) ys
          in
          if decision (p s) then ys ++ zs else zs
      end.

    Inductive slist (X : Type) (p : X → Prop) {pdec : ∀ x, dec (p x)} : list X → list X → Prop :=
    | subnil : slist nil nil
    | subconsp s ys xs: p s → slist ys xs → slist ys (s :: xs)
    | subcons s ys xs : slist ys xs → slist (s :: ys) (s :: xs).
    Hint Constructors slist.

    Lemma slists_slist (X : Type) (xs ys : list X) (p : X → Prop) (D : ∀ x, dec (p x)) :
      ys el slists p xs ↔ slist p ys xs.

    Lemma slist_id (X : Type) (xs : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :
      slist p xs xs.

    Lemma slist_trans (X : Type) (xs ys zs : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :
      slist p zs ys → slist p ys xs → slist p zs xs.

    Lemma slist_append (X : Type) (xs1 xs2 ys1 ys2 : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :
      slist p ys1 xs1 → slist p ys2 xs2 → slist p (ys1 ++ ys2) (xs1 ++ xs2).

    Lemma slist_equiv_pred (X : Type) (xs ys : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} (p' : X → Prop) {pdec' : ∀ x, dec (p' x)}:
      (∀ x, p x ↔ p' x) → slist p xs ys → slist p' xs ys.

    Lemma slist_inv (X : Type) (xs ys : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :
      slist p ys xs → (∀ s, s el ys → p s) → ∀ s, s el xs → p s.

    Lemma slist_split (X : Type) (xs ys : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :
      slist p ys xs → ∀ xs1 xs2, xs = xs1 ++ xs2 → ∃ ys1 ys2, slist p ys1 xs1 ∧ slist p ys2 xs2 ∧ ys = ys1 ++ ys2.

    Lemma slist_subsumes X (p : X → Prop) {D : ∀ x, dec (p x)} xs ys :
      slist p xs ys → xs <<= ys.

    Lemma slist_length X (p : X → Prop) {D : ∀ x, dec (p x)} (xs ys : list X) :
      slist p xs ys → |xs| ≤ |ys|.

    Lemma slist_pred X (p p' : X → Prop) {D : ∀ x, dec (p' x)} (xs ys : list X) :
      slist p' xs ys → (∀ y, y el ys → p y) → ∀ x, x el xs → p x.

    Definition segment X (xs ys : list X) := ∃ xs1 xs2, xs = xs1 ++ ys ++ xs2.

    Fixpoint segms {X} {D : eq_dec X} (xs : list X) :=
      match xs with
          [] ⇒ [ [] ]
        | s :: xs ⇒
          let
            Ss := segms xs
          in
          map (cons s) (filter (fun ys ⇒ ∃ zs, xs = ys ++ zs) Ss) ++ Ss
      end.

    Lemma segment_nil X {D : eq_dec X} (xs : list X) :
      segment xs [].

    Lemma segment_refl X {D : eq_dec X} (xs : list X) :
      segment xs xs.

    Lemma segment_trans X {D : eq_dec X} (xs ys zs : list X) :
      segment ys zs → segment xs ys → segment xs zs.

    Lemma segms_corr1 X {D : eq_dec X} (xs ys : list X) :
      segment xs ys → ys el segms xs.

    Lemma segms_corr2 X {D : eq_dec X} (xs ys : list X) :
      ys el segms xs → segment xs ys.

    Lemma segms_corr X {D : eq_dec X} (xs ys : list X) :
      ys el segms xs ↔ segment xs ys.

    Fixpoint product X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) : list Z :=
      match xs with
          [] ⇒ []
        | s :: xs ⇒ map (f s) ys ++ product f xs ys
      end.

    Lemma prod_corr1 X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) (z : Z) :
      z el product f xs ys → ∃ sxs sys, f sxs sys = z ∧ sxs el xs ∧ sys el ys.

    Lemma prod_corr2 X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) (z : Z) :
      (∃ sxs sys, f sxs sys = z ∧ sxs el xs ∧ sys el ys) → z el product f xs ys.

    Lemma prod_corr X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) (z : Z) :
      z el product f xs ys ↔ ∃ sxs sys, f sxs sys = z ∧ sxs el xs ∧ sys el ys.

    Fixpoint fsts X Y (xs : list (X × Y)) :=
      match xs with
          [] ⇒ []
        | (x, y) :: xs ⇒ x :: fsts xs
      end.

    Lemma fsts_split X Y (xs ys : list (X × Y)) :
      fsts (xs ++ ys) = fsts xs ++ fsts ys.

    Fixpoint snds X Y (xs : list (X × Y)) :=
      match xs with
          [] ⇒ []
        | (x, y) :: xs ⇒ y :: snds xs
      end.

    Lemma snds_split X Y (xs ys : list (X × Y)) :
      snds (xs ++ ys) = snds xs ++ snds ys.

    Fixpoint concat X (xs : list (list X)) :=
      match xs with
          [] ⇒ []
        | ys :: xs ⇒ ys ++ (concat xs)
      end.

    Lemma concat_split X (xs ys : list (list X)) :
      concat (xs ++ ys) = concat xs ++ concat ys.

    Fixpoint substL X {D : eq_dec X} (xs : list X) (y : X) (ys : list X) :=
      match xs with
          [] ⇒ []
        | x :: xs ⇒ if decision (x = y) then ys ++ substL xs y ys else x :: substL xs y ys
      end.

    Lemma substL_split X {D : eq_dec X} (xs1 xs2 : list X) (y : X) (ys : list X) :
      substL (xs1 ++ xs2) y ys = substL xs1 y ys ++ substL xs2 y ys.

    Lemma substL_skip X {D : eq_dec X} (xs : list X) (y : X) (ys : list X) :
      ¬ y el xs → substL xs y ys = xs.

    Lemma substL_length_unit X {D : eq_dec X} (xs : list X) (x x' : X) :
      (|xs|) = | substL xs x [x'] |.

    Lemma substL_undo X {D : eq_dec X} (xs : list X) (x x' : X) :
      ¬ x' el xs → substL (substL xs x [x']) x' [x] = xs.

    Lemma list_unit (X : Type) (xs zs : list X) (x y : X) :
      [x] = xs ++ y :: zs → xs = [] ∧ zs = [] ∧ x = y.

  End Lists.

End Lists.