Skip to content
Snippets Groups Projects
Commit 453f5e30 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add distributive laws for multisets.

parent 47d57144
No related branches found
No related tags found
No related merge requests found
......@@ -169,6 +169,21 @@ Proof.
intros X. apply gmultiset_eq; intros x. rewrite !multiplicity_intersection; lia.
Qed.
Lemma gmultiset_union_intersection_l X Y Z : X (Y Z) = (X Y) (X Z).
Proof.
apply gmultiset_eq; intros y.
rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia.
Qed.
Lemma gmultiset_union_intersection_r X Y Z : (X Y) Z = (X Z) (Y Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_union_intersection_l. Qed.
Lemma gmultiset_intersection_union_l X Y Z : X (Y Z) = (X Y) (X Z).
Proof.
apply gmultiset_eq; intros y.
rewrite multiplicity_union, !multiplicity_intersection, !multiplicity_union. lia.
Qed.
Lemma gmultiset_intersection_union_r X Y Z : (X Y) Z = (X Z) (Y Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_intersection_union_l. Qed.
(** For disjoint union (aka sum) *)
Global Instance gmultiset_disj_union_comm : Comm (=@{gmultiset A}) ().
Proof.
......@@ -194,6 +209,24 @@ Qed.
Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) ( X).
Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
Lemma gmultiset_disj_union_intersection_l X Y Z : X (Y Z) = (X Y) (X Z).
Proof.
apply gmultiset_eq; intros y.
rewrite multiplicity_disj_union, !multiplicity_intersection,
!multiplicity_disj_union. lia.
Qed.
Lemma gmultiset_disj_union_intersection_r X Y Z : (X Y) Z = (X Z) (Y Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_intersection_l. Qed.
Lemma gmultiset_disj_union_union_l X Y Z : X (Y Z) = (X Y) (X Z).
Proof.
apply gmultiset_eq; intros y.
rewrite multiplicity_disj_union, !multiplicity_union,
!multiplicity_disj_union. lia.
Qed.
Lemma gmultiset_disj_union_union_r X Y Z : (X Y) Z = (X Z) (Y Z).
Proof. by rewrite <-!(comm_L _ Z), gmultiset_disj_union_union_l. Qed.
(** Misc *)
Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠@{gmultiset A} ∅.
Proof.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment