From fee2a24e836388565c295db5843f7b7e72399e6a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 May 2020 12:37:15 +0200
Subject: [PATCH] test setoid_rewrite on inv_mapsto

---
 tests/heap_lang.ref |  9 +++++++++
 tests/heap_lang.v   | 12 ++++++++++--
 2 files changed, 19 insertions(+), 2 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 8d19418d3..80cab8e26 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -113,6 +113,15 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   l ↦∗{1 / 2} vs ∗ l ↦∗{1 / 2} vs
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  f : val → Prop
+  Heq : ∀ v : val, f v ↔ f #true
+  ============================
+  ⊢ l ↦□ (λ _ : val, f #true)
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 6b88e361c..1b16d6733 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -220,13 +220,21 @@ Section tests.
 
 End tests.
 
-Section notation_tests.
+Section inv_mapsto_tests.
   Context `{!heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
   Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
-End notation_tests.
+
+  (* Make sure [setoid_rewrite] works. *)
+  Lemma inv_mapsto_setoid_rewrite (l : loc) (f : val → Prop) :
+    (∀ v, f v ↔ f #true) →
+    ⊢ l ↦□ (λ v, f v).
+  Proof.
+    iIntros (Heq). setoid_rewrite Heq. Show.
+  Abort.
+End inv_mapsto_tests.
 
 Section printing_tests.
   Context `{!heapG Σ}.
-- 
GitLab