iModMasks.v

From iris.proofmode Require Import tactics.
From iris.bi Require Import bi.
Import bi.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Global Instance elim_modal_fupd_fupd_mask_frame_empty `{BiFUpd PROP} p E1 E1' E3 P Q :
  ElimModal (E1 ⊆ E1') p false (|={E1,∅}=> P) P
                               (|={E1',E3}=> Q) (|={E1'∖E1,E3}=> Q) | 2.
Proof.
  intros ?. rewrite intuitionistically_if_elim /= fupd_frame_r wand_elim_r.
  rewrite (fupd_mask_frame_r E1 _ (E1' ∖ E1)); last by set_solver.
  by rewrite left_id_L -union_difference_L // fupd_trans.
Qed.
Global Instance elim_modal_fupd_fupd_frame `{BiFUpd PROP} p E1 E1' E2 E3 P Q :
  ElimModal (E1 ⊆ E1') p false (|={E1,E2}=> P) P
                               (|={E1',E3}=> Q) (|={E2 ∪ E1'∖E1,E3}=> Q) | 3.
Proof.
  intros ?. rewrite intuitionistically_if_elim /= fupd_frame_r wand_elim_r.
  rewrite (fupd_mask_frame_r E1 _ (E1' ∖ E1)); last by set_solver.
  by rewrite -union_difference_L // fupd_trans.
Qed.
End sbi_instances.
From iris.program_logic Require Import weakestpre.
From iris.heap_lang Require Import notation proofmode.
Section types.
  Context `{heapG Σ}.
Lemma p (E E': coPset) (P: iProp Σ): E ⊆ E' -> ((|={E}=> P) ={E'}=∗ P)%I.
Proof.
iIntros (HSubset) ">HP".
Fail iModIntro.
Abort.