Lists of Atoms.

# Operator definitions

l -- m removes from the list l elements that appear in m.

Definition purge l m := filter (fun anegb (inb a m)) l.

Notation "l -- m" := (purge l m) (at level 40).

l is a list containing the same elements as l, but without duplication.

Definition undup l :=
fold_right (fun a acc
if inb a acc
then acc
else a::acc)
nil
l.

Notation " 〈 l 〉 " := (undup l) (at level 0).

The intersection of two lists.

Definition inter l m := filter (fun ainb a m) l.

Notation "l ∩ m" := (inter l m) (at level 40).

Removing an element from a list.

Definition rm := (@remove Atom Atom_eq_dec).

Applying a permutation to a list.

Definition mact p l :=map (act p) l.

Notation "p ⧓ l" := (mact p l) (at level 30).

If two permutations are equivalent, then they have the same effect on lists.

Global Instance equiv_perm_mact {a} :
Proper (equiv_perm ==> Logic.eq) (fun pp a).

# length of the operators.

Filtering out elements of a list yields a smaller list.

Lemma filter_length {A} (f : A bool) l :
length (filter f l) length l.

l--m, lm, rm a l, and l are all smaller than l.
Whatever permutation p, the lists pl and l always have the same length.

Lemma mact_length p l : length (pl) = length l.

# In predicate over operators

Lemma In_cons {A} : (a b : A) l,
In b (a::l) a=b In b l.

Lemma In_app_iff {A} : (a : A) l m,
In a (l ++ m) In a l In a m.

Lemma In_purge : a l m,
In a (l -- m) In a l ¬ In a m.

Lemma In_undup : a l,
In a l In a l.

Lemma In_inter : l m a,
In a (l m) In a l In a m.

Lemma In_rm : a b l,
In a (rm b l) In a l b a.

Lemma In_mact : a p l,
In a (p l) In (p a) l.

# NoDup predicate over operators

The 〈〉 operator always produces a duplication free list.
The list a::l is duplication free if and only if a doesn't appear in l and l is itself duplication free.

Lemma NoDup_cons_iff {A : Type} (a : A) l :
NoDup (a::l) ¬ In a l NoDup l.

The functions filter f, _ -- m, _ m, and rm a preserve the NoDup predicate.

Lemma NoDup_filter {A} f (l : list A) : NoDup l NoDup (filter f l).

Lemma NoDup_purge l m : NoDup l NoDup (l -- m).

Lemma NoDup_inter l m: NoDup l NoDup (l m).

Lemma NoDup_rm a l : NoDup l NoDup (rm a l).

If l and m don't share any element, then if both of them don't have duplications their concatenation won't either.

Lemma NoDup_app (l m : list Atom):
( a, In a l ¬ In a m) NoDup l NoDup m NoDup (l++m).

If the concatenation of two lists is duplication free, then so are they.

Lemma NoDup_app_inv {A} : (l m : list A),
NoDup (l++m) NoDup l NoDup m.

Applying a permutation to a list doesn't change its freeness from duplications.

Lemma NoDup_mact p l : NoDup l NoDup (p l).

The 〈〉 operator doesn't change duplication free lists.

# Simple properties of the list operators.

Lemma filter_id {A} f (l : list A) :
( a, In a l f a = true) filter f l = l.

Lemma rm_comm : a b l, rm a (rm b l) = rm b (rm a l).

Lemma purge_nil l : l -- [] = l.

Lemma purge_cons a l m : l -- (a::m) = (rm a l) -- m.

Lemma rm_app a l m : rm a (l++m) = rm a l ++ rm a m.

Lemma rm_purge a l m : (rm a l) -- m = rm a (l--m).
Lemma purge_l_l : ( l, l--l = []).

Lemma rm_id a l : ¬ In a l rm a l = l.

Lemma rm_cons a l : ¬ In a l rm a (a::l) = l.

Lemma filter_app {A} : f (l m : list A),
filter f (l ++ m) = filter f l ++ filter f m.

Lemma purge_app: l m n, (l ++ m) -- n = (l -- n) ++ (m -- n).

Lemma disjoint_In : l m,
l m = [] ( a, ¬ (In a l In a m)).

Lemma disjoint_com : l m, l m=[] m l=[].

Lemma disjoint_purge : l m, l m = [] l -- m = l.

Lemma purge_rm l m a : ¬ In a l l -- (rm a m) = l -- m.

Lemma undup_purge l m : l -- m = l -- m.

Lemma undup_app l m : l ++ m = l -- m ++ m.

Lemma undup_rm l a : rm a l = rm a l.

# Simple properties of ⧓.

Lemma mact_comp_app p q l : p (q l) = (p ++ q) l.

Lemma mact_inv_r p l : p (p l) = l.

Lemma mact_inv_l p l : p (p l) = l.

Lemma mact_rm p a l: rm a (p l) = p (rm (p a) l).

Lemma mact_purge p m l: (p l) -- m = p (l -- (p m)).

Lemma mact_id2 a b l : ¬ In a l ¬ In b l [a,b] l = l.

Lemma mact_nil : l, [] l = l.

Lemma mact_id1 a l : [a,a] l = l.

Lemma mact_app_distr : p l m, p (l ++ m) = p l ++ p m.

Lemma mact_undup p l : p l = p l.