Commit 0571115a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add type class `IntoFUpd`.

parent 79a11082
......@@ -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.
......@@ -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.
......@@ -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.
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. *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment