...
 
Commits (3)
This diff is collapsed.
...@@ -191,7 +191,7 @@ Proof. ...@@ -191,7 +191,7 @@ Proof.
Qed. Qed.
Instance coPset_elem_of_dec : RelDecision (@{coPset}). Instance coPset_elem_of_dec : RelDecision (@{coPset}).
Proof. solve_decision. Defined. Proof. unfold elem_of. solve_decision. Defined.
Instance coPset_equiv_dec : RelDecision (@{coPset}). Instance coPset_equiv_dec : RelDecision (@{coPset}).
Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined. Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
Instance mapset_disjoint_dec : RelDecision (##@{coPset}). Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
......
...@@ -233,7 +233,7 @@ Proof. ...@@ -233,7 +233,7 @@ Proof.
Qed. Qed.
Global Instance map_subseteq_po : PartialOrder (@{M A}). Global Instance map_subseteq_po : PartialOrder (@{M A}).
Proof. Proof.
split; [apply _|]. split; [apply map_included_preorder, _|].
intros m1 m2; rewrite !map_subseteq_spec. intros m1 m2; rewrite !map_subseteq_spec.
intros; apply map_eq; intros i; apply option_eq; naive_solver. intros; apply map_eq; intros i; apply option_eq; naive_solver.
Qed. Qed.
...@@ -1534,8 +1534,10 @@ Qed. ...@@ -1534,8 +1534,10 @@ Qed.
End union_with. End union_with.
(** ** Properties of the [union] operation *) (** ** Properties of the [union] operation *)
Global Instance: LeftId (=@{M A}) () := _. Global Instance: LeftId (=@{M A}) ().
Global Instance: RightId (=@{M A}) () := _. Proof. unfold union; apply _. Qed.
Global Instance: RightId (=@{M A}) ().
Proof. unfold union; apply _. Qed.
Global Instance: Assoc (=@{M A}) (). Global Instance: Assoc (=@{M A}) ().
Proof. Proof.
intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with. intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
......
...@@ -130,8 +130,4 @@ Proof. ...@@ -130,8 +130,4 @@ Proof.
Qed. Qed.
End mapset. 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. Arguments mapset_eq_dec : simpl never.