cleanup/move tests and improve changelog

CHANGELOG.md

@@ -38,7 +38,9 @@ lemma.
 
 **Changes in `bi`:**
 
-* For derived connectives, add TC hints to destruct matches. (by Sanjit Bhat)
+* Add hints for `match _ with _ end` (and thus `if _ then _ else` and
+  `'(_, _)` pair destructuring) for `Persistent`, `Affine`, `Absorbing`,
+  `Timeless`, and `Plain`. (by Sanjit Bhat)
 
 ## Iris 4.2.0 (2024-04-12)
 

tests/bi.ref

@@ -20,3 +20,10 @@ P : PROP
 
 ?p : "Persistent (■ P)"
 
+"match_def_unfold_fail"
+     : 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

tests/bi.v

+From stdpp Require Import strings.
 From iris.bi Require Import bi plainly big_op.
 
 Unset Mangle Names.
@@ -100,3 +101,40 @@ Section internal_eq_ne.
   Goal NonExpansive (λ x, (⌜a = x⌝ : PROP)%I).
   Proof. solve_proper. Qed.
 End internal_eq_ne.
+
+Section tc_match.
+  Context {PROP : bi}.
+
+  Lemma match_persistent :
+    Persistent (PROP:=PROP) (∃ b : bool, if b then False else False).
+  Proof. apply _. Qed.
+  Lemma match_affine :
+    Affine (PROP:=PROP) (∃ b : bool, if b then False else False).
+  Proof. apply _. Qed.
+  Lemma match_absorbing :
+    Absorbing (PROP:=PROP) (∃ b : bool, if b then False else False).
+  Proof. apply _. Qed.
+  Lemma match_timeless :
+    Timeless (PROP:=PROP) (∃ b : bool, if b then False else False).
+  Proof. apply _. Qed.
+  Lemma match_plain `{!BiPlainly PROP} :
+    Plain (PROP:=PROP) (∃ b : bool, if b then False else False).
+  Proof. apply _. Qed.
+
+  Lemma match_list_persistent :
+    Persistent (PROP:=PROP)
+      (∃ l : list nat, match l with [] => False | _ :: _ => False end).
+  Proof. apply _. Qed.
+
+  (* From https://gitlab.mpi-sws.org/iris/iris/-/issues/576. *)
+  Lemma pair_timeless `{!Timeless (emp%I : PROP)} (m : gset (nat * nat)) :
+    Timeless (PROP:=PROP) ([∗ set] '(k1, k2) ∈ m, False).
+  Proof. apply _. Qed.
+
+  Check "match_def_unfold_fail".
+  (* Don't want hint to unfold def's. *)
+  Definition match_foo (b : bool) : PROP := if b then False%I else False%I.
+  Lemma match_def_unfold_fail b :
+    Persistent (match_foo b).
+  Proof. Fail apply _. Abort.
+End tc_match.

tests/proofmode.ref

@@ -784,13 +784,6 @@ 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

tests/proofmode.v

@@ -1652,39 +1652,6 @@ 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.