Require Export list_set list_multiset.

Section List_support.

  Variable A : Type.

  Variable aeq : eq_type A.

  Fixpoint list_support(l : list A) : list A :=
    match l with
      | [] ⇒ []
      | a :: l ⇒
        let sl := list_support l
        in
          if member aeq a sl then sl else a :: sl
    end.

  Lemma list_support_correct_no_dup :
    ∀(l : list A), NoDup (list_support l).

  Lemma list_support_correct_content :
    ∀(l : list A), incl l (list_support l).

  Lemma list_support_correct_subset :
    ∀(l : list A), multi_subset (list_support l) l.

  Lemma list_support_incl :
    ∀(l : list A), incl (list_support l) l.

  Lemma every_nth_list_support :
    ∀(P : A → Prop)(l : list A),
      every_nth P l →
        every_nth P (list_support l).

  Lemma list_support_destruct :
    ∀(l1 : list A), ∃(l2 : list A),
      list_reorder l1 (l2 ++ list_support l1) ∧
      incl l2 (list_support l1).

  Lemma list_support_of_no_dup : ∀(l : list A),
    NoDup l →
      list_support l = l.

  Lemma list_support_head_contract :
    ∀(a : A)(l : list A),
      list_support (a :: a :: l) = list_support (a :: l).

  Lemma multi_subset_list_support :
    ∀(l1 l2 : list A),
      incl l1 l2 →
        multi_subset (list_support l1) (list_support l2).

  Lemma list_support_same_set :
    ∀(l1 l2 : list A),
      (∀(a : A), In a l1 ↔ In a l2) →
        list_reorder (list_support l1) (list_support l2).

  Lemma list_support_reorder :
    ∀(l1 l2 : list A),
      list_reorder l1 l2 →
        list_reorder (list_support l1) (list_support l2).

  Lemma multi_subset_right_list_support :
    ∀(l1 l2 : list A),
      NoDup l1 →
      incl l1 l2 →
        multi_subset l1 (list_support l2).

End List_support.

Implicit Arguments list_support [A].

Lemma list_support_map :
  ∀{A B : Type}{aeq : eq_type A}{beq : eq_type B}
        {f : A → B}(l : list A),
    (∀(a1 a2 : A), In a1 l → In a2 l → f a1 = f a2 → a1 = a2) →
      list_support beq (map f l) = map f (list_support aeq l).