From f112bfcdaeb7f664feaed93ff04957734b421643 Mon Sep 17 00:00:00 2001
From: Sanjit Bhat <sanjit.bhat@gmail.com>
Date: Thu, 15 Aug 2024 13:42:12 -0400
Subject: [PATCH] update changelog and add tests

---
 CHANGELOG.md        |  4 ++++
 tests/proofmode.ref |  7 +++++++
 tests/proofmode.v   | 33 +++++++++++++++++++++++++++++++++
 3 files changed, 44 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b01c05afb..fcb4635c6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,10 @@ lemma.
 
 * Add support for compiling the packages with dune. (by Rodolphe Lepigre) 
 
+**Changes in `bi`:**
+
+* For derived connectives, add TC hints to destruct matches. (by Sanjit Bhat)
+
 ## Iris 4.2.0 (2024-04-12)
 
 The highlights of this release are:
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index f13abe06a..f2e42b0db 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -784,6 +784,13 @@ No applicable tactic.
      : string
 The command has indeed failed with message:
 x is already used.
+"test_TC_hint_for_connective_on_match"
+     : string
+The command has indeed failed with message:
+Cannot infer this placeholder of type "Persistent (match_foo b)" (no type
+class instance found) in environment:
+PROP : bi
+b : bool
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 068950e62..45e87559d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1652,6 +1652,39 @@ Proof.
   Fail iIntros (? x).
 Abort.
 
+Check "test_TC_hint_for_connective_on_match".
+
+Lemma test_match_persistent :
+  Persistent (∃ b : bool, if b then False else False : PROP).
+Proof. apply _. Qed.
+Lemma test_match_affine : Affine (∃ b : bool, if b then False else False : PROP).
+Proof. apply _. Qed.
+Lemma test_match_absorbing :
+  Absorbing (∃ b : bool, if b then False else False : PROP).
+Proof. apply _. Qed.
+Lemma test_match_timeless :
+  Timeless (∃ b : bool, if b then False else False : PROP).
+Proof. apply _. Qed.
+Lemma test_match_plain `{!BiPlainly PROP} :
+  Plain (PROP:=PROP) (∃ b : bool, if b then False else False).
+Proof. apply _. Qed.
+
+Lemma test_match_list :
+  Persistent (PROP:=PROP)
+    (∃ l : list nat, match l with _ => False end).
+Proof. apply _. Qed.
+
+(* From https://gitlab.mpi-sws.org/iris/iris/-/issues/576. *)
+Lemma test_match_pair `{!Timeless (emp%I : PROP)} (m : gset (nat * nat)) :
+  Timeless ([∗ set] '(k1, k2) ∈ m, False : PROP).
+Proof. apply _. Qed.
+
+(* Don't want hint to unfold def's. *)
+Definition match_foo (b : bool) : PROP := if b then False%I else False%I.
+Lemma test_match_def_unfold_fail b :
+  Persistent (match_foo b).
+Proof. Fail apply _. Abort.
+
 End tests.
 
 Section parsing_tests.
-- 
GitLab