Support of lists

The support of a list is the list of its elements each occuring exactly once. This is needed for sequent support.

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 : AProp)(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 : AB}(l : list A),
    ((a1 a2 : A), In a1 lIn a2 lf a1 = f a2a1 = a2) →
      list_support beq (map f l) = map f (list_support aeq l).