From 5f26f6cd4b1510a34a427c27cd92ef64aca2fb80 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 24 Feb 2020 15:11:08 +0100
Subject: [PATCH] Add tests for `set_solver` on `dom`.

---
 tests/fin_maps.v | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/tests/fin_maps.v b/tests/fin_maps.v
index 842c20a8..b81d06ae 100644
--- a/tests/fin_maps.v
+++ b/tests/fin_maps.v
@@ -1,4 +1,4 @@
-From stdpp Require Import fin_maps.
+From stdpp Require Import fin_maps fin_map_dom.
 
 Section map_disjoint.
   Context `{FinMap K M}.
@@ -11,3 +11,14 @@ Section map_disjoint.
     m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → m2 ##ₘ <[i:=x]> m1 ∧ m1 !! i = None.
   Proof. intros. solve_map_disjoint. Qed.
 End map_disjoint.
+
+Section map_dom.
+  Context `{FinMapDom K M D}.
+
+  Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
+    {[i; j]} ⊆ dom D (<[i:=x]> (<[j:=y]> (∅ : M A))).
+  Proof. set_solver. Qed.
+
+  Lemma set_solver_dom_disjoint {A} (X : D) : dom D (∅ : M A) ## X.
+  Proof. set_solver. Qed.
+End map_dom.
-- 
GitLab