# Library equiv_lst

Equivalence of lists

# Definitions

Definition equiv_lst l m := (x : Atom), In x l In x m.
Notation "l ≈ m" := (equiv_lst l m)(at level 60).

Global Instance equiv_lst_refl : Reflexive equiv_lst.
Global Instance equiv_lst_sym : Symmetric equiv_lst.
Global Instance equiv_lst_trans : Transitive equiv_lst.
Global Instance equiv_lst_Equiv : Equivalence equiv_lst.

Definition incl_lst l m := (x : Atom), In x l In x m.

Global Instance pre_incl_lst : PreOrder incl_lst.

Global Instance anti_incl_lst : PartialOrder equiv_lst incl_lst.

Global Instance antisym_incl_lst : Antisymmetric (list Atom)
equiv_lst incl_lst.
Notation "l ⊆ m" := (incl_lst l m)(at level 60).
Global Instance In_equiv a :
Proper (equiv_lst ==> Basics.impl) (In a).
Global Instance In_incl a :
Proper (incl_lst ==> Basics.impl) (In a).

Definition incl_lst_b l m :=
forallb (fun xinb x m) l.
Lemma incl_lst_b_spec l m : reflect (l m) (incl_lst_b l m).

Definition equiv_lst_b l m := (incl_lst_b l m && incl_lst_b m l)%bool.
Lemma equiv_lst_b_spec l m : reflect (l m) (equiv_lst_b l m).

# Simple Properties

Lemma cons_comm a b l m :
l m (a :: b :: l) (b :: a :: m).
Lemma purge_cong l1 l2 m1 m2 :
l1 l2 m1 m2 l1 -- m1 l2 -- m2.
Lemma app_cong l1 l2 m1 m2 :
l1 l2 m1 m2 (l1 ++ m1) (l2 ++ m2).
Lemma undup_equiv_lst l : l l.
Lemma inter_cong l1 l2 m1 m2 :
l1 l2 m1 m2 l1 m1 l2 m2.

Lemma cons_cong a l m : lm (a::l) (a::m).

Lemma rm_cong a l m : lm (rm a l) (rm a m).
Lemma mact_cong p l m : p l p m l m.

# The operators are morphims with respect to ≈ and ⊆.

Global Instance rm_equiv a : Proper (equiv_lst ==> equiv_lst) (rm a).
Global Instance cons_equiv a :
Proper (equiv_lst ==> equiv_lst) (cons a).
Global Instance purge_equiv :
Proper (equiv_lst ==> equiv_lst ==> equiv_lst) purge.
Global Instance purge_eq :
Proper (Logic.eq ==> equiv_lst ==> Logic.eq) purge.
Global Instance inter_equiv :
Proper (equiv_lst ==> equiv_lst ==> equiv_lst) inter.
Global Instance rm_incl a : Proper (incl_lst ==> incl_lst) (rm a).
Global Instance cons_incl a : Proper (incl_lst ==> incl_lst) (cons a).
Global Instance purge_incl :
Proper (incl_lst ==> equiv_lst ==> incl_lst) purge.
Global Instance inter_incl :
Proper (incl_lst ==> incl_lst ==> incl_lst) inter.
Global Instance mact_equiv p :
Proper (equiv_lst ==> equiv_lst) (mact p).
Global Instance mact_incl p : Proper (incl_lst ==> incl_lst) (mact p).
Global Instance undup_equiv : Proper (equiv_lst ==> equiv_lst) undup.
Global Instance app_equiv :
Proper (equiv_lst ==> equiv_lst ==> equiv_lst) (@app Atom).
Global Instance app_incl :
Proper (incl_lst ==> incl_lst ==> incl_lst) (@app Atom).

# More Properties.

Lemma cons_rm_eq a l m : ¬ In a m l (a::m) In a l rm a l m.

Lemma rm_cons_eq a l m : In a l rm a l m ¬ In a m l (a::m).

Lemma rm_cons_eq' a l : In a l l (a :: rm a l).
Lemma cons_rm_eq' a m : ¬ In a m rm a (a::m) m.
Lemma purge_l_m_nil l m : l m l -- m = [].
Lemma app_l_l l : (l++l) l.

Lemma map_act_inv_eq p l m : p l m l p m.

Lemma map1 p l m : l (p) m p l m.

Lemma map2 p l m : l p m (p) l m.
Lemma app_com l m : (l ++ m) (m ++ l).

To be sorted.

Fixpoint elements (p : perm) :=
match p with
| [][]
| (a,b)::pa::b::(elements p)
end.
Lemma elements_inv_act x p :
¬ In x (elements p) px = x.
Lemma elements_inv_mact x p :
( y, In y x ¬ In y (elements p)) px = x.
Lemma elements_app : p q,
elements (p++q) (elements p ++ elements q).
Lemma elements_inv_eq : q, elements q elements (q).

Lemma elements_act_in_equiv : q a,
In a (elements q) In (qa) (elements q).

Lemma elements_in_mact : l y q,
In y (q l) In y l In y (elements q).

Lemma mact_elements_equiv_perm p q :
p q
( x, In x (elements p ++ elements q) px = qx).

Definition bequiv_perm p q :=
forallb (fun xbeq_atom (px) (qx)) (elements p ++ elements q).
Lemma bequiv_perm_spec p q : reflect (p q) (bequiv_perm p q).