From 260b75083a71c8efd39c20f7dab8da73f13d3a15 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 Oct 2016 11:25:38 +0200
Subject: [PATCH] Allow iMod to work under wands and foralls.

---
 program_logic/fancy_updates.v | 16 +++++-----------
 program_logic/invariants.v    |  4 ++--
 proofmode/class_instances.v   | 12 ++++++++++++
 3 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/program_logic/fancy_updates.v b/program_logic/fancy_updates.v
index 4c21e0ee9..0bde1fff3 100644
--- a/program_logic/fancy_updates.v
+++ b/program_logic/fancy_updates.v
@@ -51,21 +51,15 @@ Proof. apply ne_proper, _. Qed.
 Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
 Proof.
   intros (E1''&->&?)%subseteq_disjoint_union_L.
-  rewrite fupd_eq /fupd_def ownE_op //. iIntros "H ($ & $ & HE) !>".
-  iApply except_0_intro. iIntros "[$ $] !>" . iApply except_0_intro.
-  by iFrame.
+  rewrite fupd_eq /fupd_def ownE_op //.
+  by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
 Qed.
 
 Lemma except_0_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=★ P.
-Proof.
-  rewrite fupd_eq. iIntros "H [Hw HE]". iMod "H". iApply "H"; by iFrame.
-Qed.
+Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
 
 Lemma bupd_fupd E P : (|==> P) ={E}=★ P.
-Proof.
-  rewrite fupd_eq /fupd_def. iIntros "H [$ $]"; iMod "H".
-  iModIntro. by iApply except_0_intro.
-Qed.
+Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
 
 Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=★ Q.
 Proof.
@@ -85,7 +79,7 @@ Proof.
   intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
   iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
   iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
-  iModIntro; iApply except_0_intro. by iApply "HP".
+  iIntros "!> !>". by iApply "HP".
 Qed.
 
 Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index d303886fb..5398da276 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -49,8 +49,8 @@ Proof.
   iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
   rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
   rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
-  iIntros "(Hw & [HE $] & $)"; iModIntro; iApply except_0_intro.
-  iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
+  iIntros "(Hw & [HE $] & $) !> !>".
+  iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)".
   iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
 Qed.
 
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 85add1c71..06cbcc6d0 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -366,6 +366,18 @@ Global Instance into_modal_except_0 P : IntoModal P (â—‡ P).
 Proof. apply except_0_intro. Qed.
 
 (* ElimModal *)
+Global Instance elim_modal_wand P P' Q Q' R :
+  ElimModal P P' Q Q' → ElimModal P P' (R -★ Q) (R -★ Q').
+Proof.
+  rewrite /ElimModal=> H. apply wand_intro_r.
+  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
+Qed.
+Global Instance forall_modal_wand {A} P P' (Φ Ψ : A → uPred M) :
+  (∀ x, ElimModal P P' (Φ x) (Ψ x)) → ElimModal P P' (∀ x, Φ x) (∀ x, Ψ x).
+Proof.
+  rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
+Qed.
+
 Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 
-- 
GitLab