Library atoms_ops

Lists of Atoms.

Operator definitions

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

Definition purge l m := filter (fun a ⇒ negb (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 a ⇒ inb 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 p ⇒ p ⧓ 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, l∩m, rm a l, and 〈l〉 are all smaller than l.

Lemma purge_length l m : length (l --m) ≤ length l.
Lemma inter_length l m : length (l ∩ m) ≤ length l.
Lemma rm_length a l : length (rm a l) ≤ length l.
Lemma undup_length l : length 〈l 〉 ≤ length l.

Whatever permutation p, the lists p⧓l and l always have the same length.

Lemma mact_length p l : length (p ⧓l) = 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.

Lemma NoDup_undup l : NoDup 〈l 〉.

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.

Lemma NoDup_undup_eq l : NoDup l → l = 〈l 〉.

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 〉.