From 0571115a0102dc832b821465a17cbebee0e5b92b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jan 2021 09:58:00 +0100
Subject: [PATCH] Add type class `IntoFUpd`.

---
 iris/program_logic/total_weakestpre.v    |  4 ++++
 iris/program_logic/weakestpre.v          |  4 ++++
 iris/proofmode/class_instances_updates.v |  7 +++++++
 iris/proofmode/classes.v                 | 12 +++++++++++-
 4 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 5dadf421f..c196e5c90 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -303,4 +303,8 @@ Section proofmode_classes.
   Global Instance add_modal_fupd_twp s E e P Φ :
     AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_twp. Qed.
+
+  Global Instance into_fupd_twp E e s Φ :
+    IntoFUpd E (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof. apply fupd_intro. Qed.
 End proofmode_classes.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index c10cd66f5..a532b7031 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -321,4 +321,8 @@ Section proofmode_classes.
     iApply (wp_wand with "(Hinner Hα)").
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
   Qed.
+
+  Global Instance into_fupd_wp E e s Φ :
+    IntoFUpd E (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
+  Proof. apply fupd_intro. Qed.
 End proofmode_classes.
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 5fd7fea8b..232efd3c9 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -178,4 +178,11 @@ Proof.
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
 Qed.
+
+Global Instance into_fupd_default `{!BiFUpd PROP} E P :
+  IntoFUpd E (|={E}=> P) P | 100.
+Proof. by rewrite /IntoFUpd. Qed.
+Global Instance into_fupd_fupd `{!BiFUpd PROP} E1 E2 P :
+  IntoFUpd E1 (|={E1,E2}=> P) (|={E1,E2}=> P) | 1.
+Proof. apply fupd_intro. Qed.
 End class_instances_updates.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index dd4c2a2c6..0bf229bad 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -1,5 +1,5 @@
 From stdpp Require Import namespaces.
-From iris.bi Require Export bi.
+From iris.bi Require Export bi updates.
 From iris.proofmode Require Import base.
 From iris.proofmode Require Export ident_name modalities.
 From iris.prelude Require Import options.
@@ -263,6 +263,16 @@ Global Hint Mode AddModal + - ! ! : typeclass_instances.
 Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
 Proof. by rewrite /AddModal wand_elim_r. Qed.
 
+(** The [into_fupd E P Q] class is used to add an [|={E}=>] modality to the
+proposition [Q].
+
+The input are [E] and [Q], the output is [P]. *)
+Class IntoFUpd `{!BiFUpd PROP} E (P Q : PROP) :=
+  into_fupd : P ={E}=∗ Q.
+Arguments IntoFUpd {_ _} _ _%I _%I : simpl never.
+Arguments into_fupd {_ _} _ _%I _%I {_}.
+Global Hint Mode IntoFUpd + + ! - ! : typeclass_instances.
+
 (** We use the classes [IsCons] and [IsApp] to make sure that instances such as
 [frame_big_sepL_cons] and [frame_big_sepL_app] cannot be applied repeatedly
 often when having [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
-- 
GitLab