Merge branch 'tc-match-hints' into 'master'

Add instances for `match` on `Persistent`, `Affine`, `Absorbing`, `Plain`, `Timeless`

Closes #479

See merge request iris/iris!1068

CHANGELOG.md

@@ -37,6 +37,12 @@ lemma.
 
 * Add support for compiling the packages with dune. (by Rodolphe Lepigre) 
 
+**Changes in `bi`:**
+
+* Add instances 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)
 
 The highlights of this release are:

iris/bi/derived_connectives.v

@@ -19,6 +19,8 @@ Global Arguments Persistent {_} _%I : simpl never.
 Global Arguments persistent {_} _%I {_}.
 Global Hint Mode Persistent + ! : typeclass_instances.
 Global Instance: Params (@Persistent) 1 := {}.
+Global Hint Extern 100 (Persistent (match ?x with _ => _ end)) =>
+  destruct x : typeclass_instances.
 
 Definition bi_affinely {PROP : bi} (P : PROP) : PROP := emp ∧ P.
 Global Arguments bi_affinely {_} _%I : simpl never.
@@ -30,6 +32,8 @@ Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
 Global Arguments Affine {_} _%I : simpl never.
 Global Arguments affine {_} _%I {_}.
 Global Hint Mode Affine + ! : typeclass_instances.
+Global Hint Extern 100 (Affine (match ?x with _ => _ end)) =>
+  destruct x : typeclass_instances.
 
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
 Global Arguments bi_absorbingly {_} _%I : simpl never.
@@ -41,6 +45,8 @@ Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
 Global Arguments Absorbing {_} _%I : simpl never.
 Global Arguments absorbing {_} _%I.
 Global Hint Mode Absorbing + ! : typeclass_instances.
+Global Hint Extern 100 (Absorbing (match ?x with _ => _ end)) =>
+  destruct x : typeclass_instances.
 
 Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <pers> P else P)%I.
@@ -113,6 +119,8 @@ Global Arguments Timeless {_} _%I : simpl never.
 Global Arguments timeless {_} _%I {_}.
 Global Hint Mode Timeless + ! : typeclass_instances.
 Global Instance: Params (@Timeless) 1 := {}.
+Global Hint Extern 100 (Timeless (match ?x with _ => _ end)) =>
+  destruct x : typeclass_instances.
 
 (** An optional precondition [mP] to [Q].
     TODO: We may actually consider generalizing this to a list of preconditions,

iris/bi/plainly.v

@@ -107,6 +107,8 @@ Global Arguments Plain {_ _} _%I : simpl never.
 Global Arguments plain {_ _} _%I {_}.
 Global Hint Mode Plain + - ! : typeclass_instances.
 Global Instance: Params (@Plain) 1 := {}.
+Global Hint Extern 100 (Plain (match ?x with _ => _ end)) =>
+  destruct x : typeclass_instances.
 
 Definition plainly_if {PROP: bi} `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
   (if p then ■ P else P)%I.

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 instances_for_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 instances 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 instances_for_match.