...
 
Commits (3)
This diff is collapsed.
......@@ -191,7 +191,7 @@ Proof.
Qed.
Instance coPset_elem_of_dec : RelDecision (@{coPset}).
Proof. solve_decision. Defined.
Proof. unfold elem_of. solve_decision. Defined.
Instance coPset_equiv_dec : RelDecision (@{coPset}).
Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
......
......@@ -233,7 +233,7 @@ Proof.
Qed.
Global Instance map_subseteq_po : PartialOrder (@{M A}).
Proof.
split; [apply _|].
split; [apply map_included_preorder, _|].
intros m1 m2; rewrite !map_subseteq_spec.
intros; apply map_eq; intros i; apply option_eq; naive_solver.
Qed.
......@@ -1534,8 +1534,10 @@ Qed.
End union_with.
(** ** Properties of the [union] operation *)
Global Instance: LeftId (=@{M A}) () := _.
Global Instance: RightId (=@{M A}) () := _.
Global Instance: LeftId (=@{M A}) ().
Proof. unfold union; apply _. Qed.
Global Instance: RightId (=@{M A}) ().
Proof. unfold union; apply _. Qed.
Global Instance: Assoc (=@{M A}) ().
Proof.
intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
......
......@@ -130,8 +130,4 @@ Proof.
Qed.
End mapset.
(** [mapset_elem_of] internally contains an equality; make sure that tactics do
not unfold it and try to unify [∈] against goals with [=]. *)
Opaque mapset_elem_of.
Arguments mapset_eq_dec : simpl never.