From 85d5c29956a09e59c01c7d2fbe7fa1304ce2f2fd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 May 2023 20:32:35 +0200
Subject: [PATCH] Simplify `dom` even further.
---
stdpp/mapset.v | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/stdpp/mapset.v b/stdpp/mapset.v
index 46f0c745..689f556d 100644
--- a/stdpp/mapset.v
+++ b/stdpp/mapset.v
@@ -128,11 +128,14 @@ Proof.
- destruct (Is_true_reflect (f a)); naive_solver.
- naive_solver.
Qed.
-Local Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+
+Local Instance mapset_dom {A} : Dom (M A) (mapset M) := λ m,
+ Mapset $ fmap (λ _, ()) m.
Local Instance mapset_dom_spec: FinMapDom K M (mapset M).
Proof.
- split; try apply _. intros. unfold dom, mapset_dom, is_Some.
- rewrite elem_of_mapset_dom_with; naive_solver.
+ split; try apply _. intros A m i.
+ unfold dom, mapset_dom, is_Some, elem_of, mapset_elem_of; simpl.
+ rewrite lookup_fmap. destruct (m !! i); naive_solver.
Qed.
End mapset.
--
GitLab