Commit 42a87a40 authored by Robbert Krebbers's avatar Robbert Krebbers

`Equiv` instance for multisets.

This fixes issue #12.
parent 6d37f451
......@@ -25,6 +25,8 @@ Section definitions.
0 < multiplicity x X.
Global Instance gmultiset_subseteq : SubsetEq (gmultiset A) := λ X Y, x,
multiplicity x X multiplicity x Y.
Global Instance gmultiset_equiv : Equiv (gmultiset A) := λ X Y, x,
multiplicity x X = multiplicity x Y.
Global Instance gmultiset_elements : Elements A (gmultiset A) := λ X,
let (X) := X in ''(x,n) map_to_list X; replicate (S n) x.
......@@ -62,6 +64,8 @@ Proof.
specialize (HXY x); unfold multiplicity in *; simpl in *.
repeat case_match; naive_solver.
Qed.
Global Instance gmultiset_leibniz : LeibnizEquiv (gmultiset A).
Proof. intros X Y. by rewrite gmultiset_eq. Qed.
(* Multiplicity *)
Lemma multiplicity_empty x : multiplicity x = 0.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment