From 2776d930d9d03f3833ad5d21095a6275d08f3fda Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Nov 2018 10:31:02 +0100
Subject: [PATCH] Support singletons in `solve_map_disjoint`.
---
tests/fin_maps.ref | 0
tests/fin_maps.v | 13 +++++++++++++
theories/fin_maps.v | 2 ++
3 files changed, 15 insertions(+)
create mode 100644 tests/fin_maps.ref
create mode 100644 tests/fin_maps.v
diff --git a/tests/fin_maps.ref b/tests/fin_maps.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/fin_maps.v b/tests/fin_maps.v
new file mode 100644
index 00000000..842c20a8
--- /dev/null
+++ b/tests/fin_maps.v
@@ -0,0 +1,13 @@
+From stdpp Require Import fin_maps.
+
+Section map_disjoint.
+ Context `{FinMap K M}.
+
+ Lemma solve_map_disjoint_singleton_1 {A} (m1 m2 : M A) i x :
+ m1 ##ₘ <[i:=x]> m2 → {[ i:= x ]} ∪ m2 ##ₘ m1 ∧ m2 ##ₘ ∅.
+ Proof. intros. solve_map_disjoint. Qed.
+
+ Lemma solve_map_disjoint_singleton_2 {A} (m1 m2 : M A) i x :
+ m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → m2 ##ₘ <[i:=x]> m1 ∧ m1 !! i = None.
+ Proof. intros. solve_map_disjoint. Qed.
+End map_disjoint.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index bcce9efd..d4cdfd3e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1932,6 +1932,8 @@ Hint Extern 2 (_ ##ₘ {[ _ := _ ]}) =>
apply map_disjoint_singleton_r_2 : map_disjoint.
Hint Extern 2 (_ ∪ _ ##ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
Hint Extern 2 (_ ##ₘ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint.
+Hint Extern 2 ({[_:= _]} ##ₘ _) => apply map_disjoint_singleton_l : map_disjoint.
+Hint Extern 2 (_ ##ₘ {[_:= _]}) => apply map_disjoint_singleton_r : map_disjoint.
Hint Extern 2 (<[_:=_]>_ ##ₘ _) => apply map_disjoint_insert_l_2 : map_disjoint.
Hint Extern 2 (_ ##ₘ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
Hint Extern 2 (delete _ _ ##ₘ _) => apply map_disjoint_delete_l : map_disjoint.
--
GitLab