Support of lists
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).