# Library CoLoR.Util.Multiset.MultisetTheory

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• William Delobel, 2005-10-07
This file provides a development of (part of) the theory of finite multisets.

Set Implicit Arguments.

Module Multiset (MC : MultisetCore).

Export MC.

Section NewOperations.

Definition member x M := (x/M)%msets > 0.

Definition insert x M : Multiset := {{x}}+M.

Definition pair a b : Multiset := insert a {{b}}.

Definition remove a A : Multiset := A - {{a}}.

Fixpoint list2multiset (l : list A) : Multiset :=
match l with
| List.nil => empty
| List.cons x xs => insert x (list2multiset xs)
end.

End NewOperations.

Notation "{{ x , y }}" := (pair x y) (at level 5) : msets_scope.
Notation "x 'in' M" := (member x M) (at level 10) : msets_scope.

Ltac mset_unfold := repeat progress unfold insert,remove,pair,member.

Ltac try_solve_meq :=
(intros;
match goal with
| |- _ =mul= _ =>
( apply multeq_meq
; intro
; try_solve_meq
)
| _ =>
( mset_unfold
; repeat progress (
try rewrite union_mult;
try rewrite diff_mult;
try rewrite empty_mult;
try rewrite intersection_mult
)
; try omega
; try congruence
; try solve [auto with multisets]
)
end
).

Ltac solve_meq :=
(solve [try_solve_meq] ||
fail "Goal is not an equality between multisets or fails to prove").

Ltac try_solve_meq_ext :=
(
let go x := (solve [clear x; try_solve_meq_ext]) in (
mset_unfold;
intros;
try solve_meq;
(match goal with
| H : ?A =mul= ?B |- _ =>
( (try_solve_meq; rewrite (meq_multeq H); go H)
|| (try_solve_meq; rewrite <- (meq_multeq H); go H)
)
| H : ?a =A= ?b |- _ =>
( (rewrite (singleton_mult_in H); go H)
|| (rewrite H; go H)
|| (rewrite <- H; go H)
|| (rewrite (mult_eqA_compat H); go H)
|| (rewrite <- (mult_eqA_compat H); go H)
)
| H : ~ ?a =A= ?b |- _ =>
(rewrite (singleton_mult_notin H); go H)
| |- _ =mul= _ =>
( apply multeq_meq; try_solve_meq_ext )
end || try_solve_meq))).

Ltac solve_meq_ext :=
(solve [try_solve_meq_ext] ||
fail "Couldn't show multisets equality").

Hint Unfold member
insert
pair
remove : multisets.

Section meq_equivalence.

Lemma meq_refl M : M =mul= M.

Lemma meq_trans M N P : M =mul= N -> N =mul= P -> M =mul= P.

Lemma meq_sym M N : M =mul= N -> N =mul= M.

End meq_equivalence.

Hint Resolve meq_refl meq_trans meq_sym : multisets.

Instance meq_Equivalence : Equivalence meq.

Instance union_morph : Proper (meq ==> meq ==> meq) union.

Instance singleton_morph : Proper (eqA ==> meq) singleton.

Instance pair_morph : Proper (eqA ==> eqA ==> meq) pair.

Instance mult_morph : Proper (eqA ==> meq ==> eq) mult.

Instance diff_morph : Proper (meq ==> meq ==> meq) diff.

Instance insert_morph : Proper (eqA ==> meq ==> meq) insert.

Instance member_morph : Proper (eqA ==> meq ==> iff) member.

Instance remove_morph : Proper (eqA ==> meq ==> meq) remove.

Instance intersection_morph : Proper (meq ==> meq ==> meq) intersection.

Section MultisetLemmas.

Lemma mset_ind : forall P : Multiset -> Prop,
P empty -> (forall M a, P M -> P (M + {{a}})) -> forall M, P M.

Lemma mset_ind_set : forall P : Multiset -> Set,
P empty -> (forall M a, P M -> P (M + {{a}})) -> forall M, P M.

Lemma union_comm M N : M + N =mul= N + M.

Lemma intersection_comm M N : M # N =mul= N # M.

Lemma union_assoc M N P : M + (N + P) =mul= (M + N) + P.

Lemma member_singleton x y : x in {{y}} -> x =A= y.

Lemma singleton_member_eqA a b : a in {{b}} -> a =A= b.

Lemma singleton_mult_union_empty a a' M :
{{a}} =mul= {{a'}} + M -> M =mul= empty.

Lemma member_pair x y z : x in {{y,z}} -> x =A= y \/ x =A= z.

Lemma union_perm M N P : M + N + P =mul= M + P + N.

Lemma union_empty M : M + empty =mul= M.

Lemma notempty_member M : M <>mul empty -> exists N a, M =mul= {{a}} + N.

Lemma not_empty M x : x in M -> M =mul= empty -> False.

Lemma member_union_l a M N : a in M -> a in (M + N).

Lemma member_union_r a M N : a in N -> a in (M + N).

Lemma mult_insert : forall M a, (a/(M + {{a}}))%msets > 0.

Lemma singleton_member a : a in {{a}}.

Lemma member_insert a M : a in (insert a M).

Lemma member_member_union a M N : a in M -> a in (M+N).

Lemma member_diff_member a M N : a in (M-N) -> a in M.

Lemma diff_member_ly_rn a M N : a in M -> ~a in N -> a in (M - N).

Lemma diff_remove_both a M N :
a in M -> a in N -> M - N =mul= (remove a M) - (remove a N).

Lemma member_union a M N : a in (M+N) -> a in M \/ a in N.

Lemma member_meq_union a M N M' N' :
M + N =mul= M' + N' -> (a in M \/ a in N) -> ~a in N' -> a in M'.

Lemma meq_union_meq M N P : M + P =mul= N + P -> M =mul= N.

Lemma meq_meq_union M N P : M =mul= N -> M + P =mul= N + P.

Lemma meq_ins_ins_eq a a' M M' :
M + {{a}} =mul= M' + {{a'}} -> a =A= a' -> M =mul= M'.

Lemma meq_ins_ins a a' M M' :
M + {{a}} =mul= M' + {{a'}} -> M =mul= M' + {{a'}} - {{a}}.

Lemma member_ins_ins_meq a a' M M' :
M + {{a}} =mul= M' + {{a'}} -> ~a =A= a' -> a in M'.

Lemma meq_ins_rem a M : a in M -> M =mul= M - {{a}} + {{a}}.

Lemma meq_remove_insert a M : remove a (M + {{a}}) =mul= M.

Lemma meq_remove a M N : insert a M =mul= N -> M =mul= remove a N.

Lemma insert_meq M N a : insert a M =mul= insert a N -> M =mul= N.

Lemma insert_remove_eq a a' M : a =A= a' -> M =mul= remove a (insert a' M).

Lemma meq_insert_remove a M : a in M -> insert a (remove a M) =mul= M.

Lemma insert_remove_noteq a a' M :
~a =A= a' -> remove a (insert a' M) =mul= insert a' (remove a M).

Lemma meq_cons a M N :
M + {{a}} =mul= N -> exists N', N =mul= N' + {{a}} /\ M =mul= N'.

Lemma meq_diff_meq M N P : M =mul= N -> M - P =mul= N - P.

Section Decidability.

Lemma member_dec a M : {a in M}+{~a in M}.

Lemma empty_dec : forall M, {M =mul= empty}+{M <>mul empty}.

Lemma empty_decomp_dec : forall M,
{Ma: (Multiset * A) | M =mul= fst Ma + {{snd Ma}}} + {M =mul= empty}.

End Decidability.

Lemma insert_diff a M N :
insert a M - N =mul= empty -> a in N /\ M - remove a N =mul= empty.

Lemma diff_MM_empty M : M - M =mul= empty.

Lemma ins_meq_union M N P a :
M + {{a}} =mul= N + P -> a in N -> M =mul= N - {{a}} + P.

Lemma mem_memrem M a b : ~ a =A= b -> a in M -> a in (M - {{b}}).

Lemma member_notempty M x : x in M -> M <>mul empty.

Lemma singleton_notempty x : {{x}} <>mul empty.

Lemma union_isempty M N : M + N =mul= empty -> M =mul= empty.

Lemma union_notempty M N : M <>mul empty -> M + N <>mul empty.

Lemma remove_union a L R :
a in L -> remove a (L + R) =mul= (remove a L) + R.

Lemma meq_remove_elem_right a M L R :
M + {{a}} =mul= L + R -> a in R -> M =mul= L + (remove a R).

End MultisetLemmas.

Hint Immediate member_singleton
member_member_union
member_diff_member
member_union
member_meq_union
union_comm
intersection_comm
union_assoc : multisets.

Hint Resolve union_empty
not_empty
singleton_member
meq_union_meq
meq_meq_union
meq_ins_ins_eq
meq_ins_ins
member_ins_ins_meq
meq_ins_rem
meq_diff_meq
diff_MM_empty
ins_meq_union
mem_memrem
member_union_r
member_union_l
member_notempty
singleton_notempty
union_isempty
union_notempty : multisets.

Section MultisetLemmas2.

Lemma double_split L R U D :
L + R =mul= U + D -> R =mul= (R # D) + (U - L).

Variables (P Q : A -> Prop) (PQ_dec : forall a, {P a}+{Q a}).

Definition comp_eqA P := forall a b, a =A= b -> P a -> P b.

Variables (P_comp : comp_eqA P) (Q_comp : comp_eqA Q).

Lemma partition : forall M, exists Mp, exists2 Mq, M =mul= Mp + Mq
& (forall p, p in Mp -> P p) /\ (forall q, q in Mq -> Q q).

End MultisetLemmas2.

Section List2Multiset.

Lemma member_list_multiset : forall l,
forall x, In x l -> member x (list2multiset l).

Lemma member_multiset_list : forall l,
forall x, member x (list2multiset l) -> exists2 y, In y l & x =A= y.

Lemma list2multiset_app : forall M1 M2,
list2multiset (M1 ++ M2) =mul= list2multiset M1 + list2multiset M2.

Lemma list2multiset_mult : forall l a,
a / (list2multiset l) = multiplicity (list_contents eqA_dec l) a.

Lemma meq_permutation l l' :
list2multiset l =mul= list2multiset l' -> permutation eqA_dec l l'.

Lemma permutation_meq l l' :
permutation eqA_dec l l' -> list2multiset l =mul= list2multiset l'.

Lemma list2multiset_eq_length l l' :
list2multiset l =mul= list2multiset l' -> length l = length l'.

Lemma list2multiset_cons_length l l' : forall a,
list2multiset l + {{a}} =mul= list2multiset l' ->
length l' = S (length l).

Lemma list2multiset_remove_in a : forall m,
remove a (list2multiset m)
=mul= list2multiset (removeElem eqA eqA_dec a m).

Lemma diff_empty : forall l m,
list2multiset l - list2multiset m =mul= empty ->
(length l - length m = 0)%nat.

Lemma list2multiset_union_length : forall l m n,
list2multiset l =mul= list2multiset m + list2multiset n ->
length l = (length m + length n)%nat.

Lemma list2multiset_diff_length : forall l m n,
list2multiset l =mul= list2multiset m - list2multiset n ->
length l >= length m - length n.

Lemma list2multiset_insert_nth a l p :
list2multiset (insert_nth l p a) =mul= insert a (list2multiset l).

End List2Multiset.

Section Multiset2List.
Definition mult_to_list : forall M, {l : list A | M =mul= list2multiset l}.

Definition multiset2list M :=
match mult_to_list M with @exist _ _ l _ => l end.

Lemma multiset2list_empty : multiset2list empty = nil.

Lemma double_convertion : forall M, list2multiset (multiset2list M) =mul= M.

End Multiset2List.

Section Multiset2List_Results.

Lemma multiset2list_meq_non_empty : forall M,
M <>mul empty -> multiset2list M <> nil.

Lemma multiset2list_meq_empty : forall M,
M =mul= empty -> multiset2list M = nil.

Lemma in_multiset_in_multiset2list : forall M x,
x in M -> exists y, x =A= y /\ In y (multiset2list M).

Lemma in_multiset2list_in_multiset : forall M x,
In x (multiset2list M) -> x in M.

Lemma multiset2list_insert a M :
exists a' p, a =A= a' /\
permutation eqA_dec (multiset2list M)
(drop_nth (multiset2list (insert a M)) p)
/\ nth_error (multiset2list (insert a M)) p = Some a'.

Lemma multiset2list_cons_length M a :
length (multiset2list (M + {{a}})) = S (length (multiset2list M)).

Lemma multiset2list_union_length M N :
length (multiset2list (M + N))
= (length (multiset2list M) + length (multiset2list N))%nat.

Lemma multiset2list_diff_length M N :
length (multiset2list (M - N))
>= length (multiset2list M) - length (multiset2list N).

Lemma multiset2list_meq_length M M' :
M =mul= M' -> length (multiset2list M) = length (multiset2list M').

Lemma cons_eq_cons_cons_absurd a a' a'' M :
{{a}} =mul= {{a'}} + {{a''}} + M -> False.

Lemma multiset2list_singleton a :
exists a', a =A= a' /\ multiset2list {{a}} = a' :: nil.

End Multiset2List_Results.

Section MultisetCardinality.

Definition card_def (M : Multiset) : { n | length (multiset2list M) = n}.

Definition card (M : Multiset) := proj1_sig (card_def M).

Lemma empty_card : card empty = 0.

Instance card_morph : Proper (meq ==> eq) card.

Lemma multiset2list_card M : length (multiset2list M) = card M.

Lemma card_non_empty M : M <>mul empty -> card M > 0.

Lemma singleton_card x : card {{x}} = 1.

Lemma pair_card x y : card {{x, y}} = 2.

Lemma union_card M N : card (M + N) = (card M + card N)%nat.

Lemma diff_card M N : card (M - N) >= card M - card N.

End MultisetCardinality.

Section Pair.

Lemma pair_eq a b c d :
{{a, b}} =mul= {{c, d}} -> (a =A= c /\ b =A= d) \/ (a =A= d /\ b =A= c).

Lemma pair_decomp a b X Y : {{a, b}} =mul= X + Y ->
(X =mul= {{a, b}} /\ Y =mul= empty) \/
(X =mul= empty /\ Y =mul= {{a, b}}) \/
(X =mul= {{a}} /\ Y =mul= {{b}}) \/
(X =mul= {{b}} /\ Y =mul= {{a}}).

End Pair.

Hint Immediate double_split : multisets.

End Multiset.