Commit 260b7508 authored by Robbert Krebbers's avatar Robbert Krebbers

Allow iMod to work under wands and foralls.

parent fc30ca08
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
Markdown is supported
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