From 3b1844866708771fd19bcdead11e2da8665c7a8c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Nov 2022 17:53:40 +0100
Subject: [PATCH] Add basic support for `gset_disj` to `set_solver`.

---
 iris/algebra/gset.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/iris/algebra/gset.v b/iris/algebra/gset.v
index 0e14bfeb9..2ac07daa8 100644
--- a/iris/algebra/gset.v
+++ b/iris/algebra/gset.v
@@ -237,6 +237,20 @@ Section gset_disj.
     intros. rewrite -{2}(right_id_L _ union Z).
     apply gset_disj_alloc_local_update; set_solver.
   Qed.
+
+  (** Add some basic support for [GSet X = GSet Y], [GSet X ≼ GSet Y], and
+  [✓ (GSet X ⋅ GSet Y)] to [set_solver]. There are probably more cases we could
+  cover (e.g., involving [GSetBot], or nesting of [â‹…]), but it is not clear
+  these are useful in practice, nor how to handle them effectively. *)
+  Global Instance set_unfold_gset_eq (X Y : gset K) Q :
+    SetUnfold (X = Y) Q → SetUnfold (GSet X = GSet Y) Q.
+  Proof. intros [?]; constructor. by rewrite (inj_iff _). Qed.
+  Global Instance set_unfold_gset_disj_included (X Y : gset K) Q :
+    SetUnfold (X ⊆ Y) Q → SetUnfold (GSet X ≼ GSet Y) Q.
+  Proof. intros [?]; constructor. by rewrite gset_disj_included. Qed.
+  Global Instance set_unfold_gset_disj_valid_op (X Y : gset K) Q :
+    SetUnfold (X ## Y) Q → SetUnfold (✓ (GSet X ⋅ GSet Y)) Q.
+  Proof. intros [?]; constructor. by rewrite gset_disj_valid_op. Qed.
 End gset_disj.
 
 Global Arguments gset_disjO _ {_ _}.
-- 
GitLab