Commit 56a695de authored by Ralf Jung's avatar Ralf Jung
Browse files

bump Iris; fix SBI interface and other issues

parent dba5b164
Pipeline #8500 passed with stage
in 26 minutes and 38 seconds
......@@ -12,3 +12,4 @@
Makefile.coq
Makefile.coq.conf
build-dep/
.coqdeps.d
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-03-09.0") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-08.0.7af1bbd3") | (= "dev") }
]
From fri.algebra Require Import upred.
From iris.bi Require Export bi.
From iris.proofmode Require Import coq_tactics classes class_instances tactics.
From iris.proofmode Require Import coq_tactics classes class_instances_sbi tactics.
Import uPred.
......@@ -79,7 +79,7 @@ Proof.
- by unseal.
- by unseal.
- apply later_mono.
- apply löb.
- apply later_intro.
- intros. unseal; by split=> -[|n] x y.
- intros A Φ. unseal; split=> -[|[|n]] x y ?? Hsat /=; eauto.
* by left.
......@@ -109,7 +109,7 @@ Global Notation "■ φ" := (uPred_pure φ%stdpp%type)
(at level 20, right associativity) : bi_scope.
Global Notation "⧆ P" := (bi_affinely P%I)
(at level 20, right associativity) : bi_scope.
Global Notation "⧈ P" := (bi_affinely (bi_persistently P%I))
Global Notation "⧈ P" := (bi_intuitionistically P%I)
(at level 20, right associativity) : bi_scope.
Global Notation "✓ x" := (uPred_valid x) (at level 20) : bi_scope.
Infix "★" := bi_sep : bi_scope.
......@@ -301,7 +301,7 @@ Section ATimeless_uPred.
Qed.
Global Instance persistently_atimeless P : ATimeless P ATimeless ( P).
Proof.
rewrite /ATimeless.
rewrite /ATimeless /bi_intuitionistically.
rewrite -?uPred_affine_bi_affinely.
rewrite -unlimited_affine_persistent.
rewrite -relevant_affine affine_relevant_later.
......@@ -519,4 +519,4 @@ Section gmap.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
set_unfold. naive_solver.
Qed.
End gmap.
\ No newline at end of file
End gmap.
......@@ -534,8 +534,8 @@ Section proof.
⧆■(prot_mod pr' l (dual pl'))) prot_modc pl (left_state s) (prot_send Φ p)).
Proof.
iIntros "(Hinv&%)".
iSplit; iAlways; last done.
iNext.
iSplit; last by auto.
iAlways. iNext.
iDestruct "Hinv" as "[Hl|Hr]"; auto.
iDestruct "Hr" as (l pl' pr') "(%&%&H1&H2&H3&%)".
destruct l.
......@@ -570,9 +570,9 @@ Section proof.
⧆■(prot_mod pl' l (dual pr'))) prot_modc pr (right_state s) (prot_send Φ p)).
Proof.
iIntros "(Hinv&%)".
iSplit; iAlways; last done.
iSplit; last by auto.
rewrite /prot_inv.
iNext.
iAlways. iNext.
iDestruct "Hinv" as "[Hl|Hr]"; auto.
iDestruct "Hl" as (l pl' pr') "(%&%&H1&H2&H3&%)".
destruct l.
......@@ -1217,4 +1217,4 @@ Proof. by rewrite /Frame affine_elim=>->. Qed.
* eauto. solve_closed.
Qed.
End proof.
\ No newline at end of file
End proof.
......@@ -1308,7 +1308,7 @@ Tactic Notation "refine_unbind" constr(K) :=
}
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ iFrame "Hown". iFrame "Hheap". iFrame "Hscheap".
repeat iSplit; iPureIntro; eauto with ndisj. }
repeat iSplitL; iPureIntro; eauto with ndisj. }
iApply wp_wand_l. iFrame "Hwp".
iIntros "!#". iIntros (v) "Hpre".
iDestruct "Hpre" as (l c) "(%&Hleft&Hright&Hown)".
......
......@@ -33,7 +33,7 @@ Proof.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite affinely_persistently_elim assoc (refine_alloc _ d' _ _ E) //.
rewrite intuitionistically_elim assoc (refine_alloc _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite sep_exist_r.
......@@ -66,7 +66,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_recv_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -78,7 +78,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_recv_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -115,7 +115,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_recv_miss_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -127,7 +127,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_recv_miss_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -159,7 +159,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
destruct side.
- rewrite (refine_send_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
......@@ -198,7 +198,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
destruct side.
- rewrite (refine_select_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
......@@ -238,7 +238,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_rcase_left_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -250,7 +250,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_rcase_right_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -282,7 +282,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_rcase_left_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -294,7 +294,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_rcase_right_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -330,7 +330,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_rcase_miss_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -342,7 +342,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_rcase_miss_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -368,7 +368,7 @@ Proof.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc.
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite Hstep.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -507,7 +507,7 @@ Proof.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite affinely_persistently_elim assoc (refine_fork _ d' _ _ E) //.
rewrite intuitionistically_elim assoc (refine_fork _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite sep_exist_r.
......@@ -544,7 +544,7 @@ Proof.
intros Hgt Hl1 Hl2 Haff ? Hrep Hd.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite affinely_persistently_elim assoc.
rewrite intuitionistically_elim assoc.
rewrite (refine_delay _ d' _ _ E); eauto.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -1248,4 +1248,4 @@ Module Test.
Abort.
End Test.
*)
\ No newline at end of file
*)
......@@ -36,7 +36,7 @@ Proof.
intros ? Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite assoc (refine_alloc _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -64,7 +64,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_load _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -93,7 +93,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_store _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -123,7 +123,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_cas_fail _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -154,7 +154,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_cas_suc _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -182,7 +182,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_swap _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -210,7 +210,7 @@ Proof.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite (refine_fai _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -236,7 +236,7 @@ Proof.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc.
rewrite affinely_persistently_elim.
rewrite intuitionistically_elim.
rewrite Hstep.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -383,7 +383,7 @@ Proof.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite affinely_persistently_elim assoc (refine_fork _ d' _ _ E) //.
rewrite intuitionistically_elim assoc (refine_fork _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite sep_exist_r.
......@@ -420,7 +420,7 @@ Proof.
intros Hgt Hl1 Hl2 Haff ? Hrep Hd.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite affinely_persistently_elim assoc.
rewrite intuitionistically_elim assoc.
rewrite (refine_delay _ d' _ _ E); eauto.
rewrite Haff psvs_frame_r.
apply psvs_mono.
......@@ -1018,7 +1018,6 @@ Section Test.
refine_seq Kd.
wp_cas_suc; auto.
refine_cas_suc 0%nat; auto.
iFrame "Hown". auto.
Qed.
Definition heap_e_fork : expr :=
......@@ -1073,4 +1072,4 @@ Section Test.
by iApply ("IH" with "Hpts Hown").
Qed.
End Test.
\ No newline at end of file
End Test.
......@@ -179,7 +179,7 @@ Proof.
rewrite /big_op ?right_id; auto.
constructor; last constructor.
rewrite /ht in Hht.
rewrite bi.affinely_persistently_elim in Hht *=>Hht.
rewrite bi.intuitionistically_elim in Hht *=>Hht.
eapply uPred.wand_elim_l' in Hht.
rewrite left_id in Hht *=>Hht.
eapply Hht; eauto.
......
......@@ -558,7 +558,7 @@ Section bounded_nondet_hom2.
** rewrite Heq_b. auto.
- econstructor; [|econstructor].
rewrite /ht wp_eq in Hht *.
rewrite bi.affinely_persistently_elim in Hht * => Hht.
rewrite bi.intuitionistically_elim in Hht * => Hht.
eapply bi.wand_entails in Hht.
eapply Hht.
......@@ -584,4 +584,4 @@ Section bounded_nondet_hom2.
End bounded_nondet_hom2.
End adequacy_inf.
\ No newline at end of file
End adequacy_inf.
......@@ -221,17 +221,16 @@ Section proofmode_classes.
Affine (bi_affinely_if p P).
Proof. destruct p => //=; apply _. Qed.
Global Instance affinely_if_persistently_if_affine (P: iProp Λ Σ) (HA: Affine P) p :
Affine (bi_affinely_if p (bi_persistently_if p P)).
Global Instance intuitionistically_if_affine (P: iProp Λ Σ) (HA: Affine P) p :
Affine (bi_intuitionistically_if p P).
Proof. destruct p => //=; apply _. Qed.
Global Instance into_wand_psvs_persistent E1 E2 p q R P Q :
Affine P
IntoWand false q R P Q IntoWand p q (|={E1,E2}=>> R) P (|={E1,E2}=>> Q).
Proof.
rewrite /IntoWand /= => ? HR. rewrite affinely_persistently_if_elim HR.
apply wand_intro_l. rewrite -(affine_affinely (bi_affinely_if _ _)).
rewrite /IntoWand /= => ? HR. rewrite intuitionistically_if_elim HR.
apply wand_intro_l. rewrite -(affine_affinely (bi_intuitionistically_if _ _)).
by rewrite psvs_frame_l wand_elim_r.
Qed.
......@@ -259,7 +258,7 @@ Section proofmode_classes.
Affine R
Frame p R P Q Frame p R (|={E1,E2}=>> P) (|={E1,E2}=>> Q).
Proof.
rewrite /Frame=> ? <-. rewrite -(affine_affinely (bi_affinely_if _ _)).
rewrite /Frame=> ? <-. rewrite -(affine_affinely (bi_intuitionistically_if _ _)).
by rewrite psvs_frame_l.
Qed.
......@@ -302,7 +301,6 @@ Global Instance elim_inv_psvs {Λ Σ} E N (P: iProp Λ Σ) Q:
Proof.
rewrite /ElimInv. iIntros (?) "(?&_&Hclose)".
iApply (elim_inv_afsa _ _ E N _ (λ _, Q) psvs_fsa_prf); auto.
iFrame.
Qed.
Tactic Notation "iPsvs" open_constr(lem) :=
......@@ -311,4 +309,4 @@ Tactic Notation "iPsvs" open_constr(lem) :=
| ITrm ?t _ _ => t
| _ => lem
end in
iSpecialize lem; iApply psvs_pvs'; iApply (psvs_wand with t); iAlways; iIntros t.
\ No newline at end of file
iSpecialize lem; iApply psvs_pvs'; iApply (psvs_wand with t); iAlways; iIntros t.
......@@ -287,14 +287,14 @@ Section proofmode_classes.
IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
Proof.
rewrite /IntoWand /= => HR.
rewrite !affinely_persistently_if_elim HR.
rewrite !intuitionistically_if_elim HR.
apply wand_intro_l. by rewrite pvs_sep wand_elim_r.
Qed.
Global Instance into_wand_pvs_persistent E1 E2 p q R P Q :
IntoWand false q R P Q IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
Proof.
rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
apply wand_intro_l. by rewrite pvs_frame_l wand_elim_r.
Qed.
......@@ -302,7 +302,7 @@ Section proofmode_classes.
IntoWand p false R P Q IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof.
rewrite /IntoWand' /IntoWand /= => ->.
apply wand_intro_l. by rewrite affinely_persistently_if_elim pvs_wand_r.
apply wand_intro_l. by rewrite intuitionistically_if_elim pvs_wand_r.
Qed.
Global Instance from_sep_pvs E P Q1 Q2 :
......@@ -345,8 +345,11 @@ Section proofmode_classes.
Proof. rewrite /FromModal => //=. Qed.
Global Instance elim_modal_pvs_pvs E1 E2 E3 P Q :
ElimModal (E2 E1 E3) (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof. intros. rewrite /ElimModal => ?. rewrite pvs_frame_r wand_elim_r pvs_trans //=. Qed.
ElimModal (E2 E1 E3) p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof.
intros. rewrite /ElimModal bi.intuitionistically_if_elim => ?.
rewrite pvs_frame_r wand_elim_r pvs_trans //=.
Qed.
End proofmode_classes.
......@@ -483,20 +486,20 @@ Qed.
Global Instance elim_modal_fsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ:
FrameShiftAssertion fsaV fsa
ElimModal True (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
ElimModal True false false (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
Proof.
rewrite /ElimModal => FSA H.
rewrite /ElimModal /= => FSA H.
iIntros "(H1&H2)".
iApply fsa_pvs_fsa.
iMod "H1"; first by set_solver. iModIntro. by iApply "H2".
Qed.
Global Instance elim_modal_afsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ:
Global Instance elim_modal_afsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ p:
AffineFrameShiftAssertion fsaV fsa
ElimModal True (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
ElimModal True p false (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ).
Proof.
rewrite /ElimModal => FSA H.
rewrite /ElimModal intuitionistically_if_elim /= => FSA H.
iIntros "(H1&H2)".
iApply afsa_pvs_afsa.
iMod "H1"; first by set_solver. iModIntro. by iApply "H2".
Qed.
\ No newline at end of file
Qed.
......@@ -180,7 +180,7 @@ Proof.
rewrite ?envs_entails_eq.
intros ?? Hl1 Hl2 ? HΔ'. rewrite (is_afsa Q) -(sts_afsaS φ fsa) //.
rewrite envs_lookup_persistent_sound //; simpl.
rewrite bi.affinely_persistently_elim. apply sep_mono_r.
rewrite bi.intuitionistically_elim. apply sep_mono_r.
clear Hl1.
rewrite envs_lookup_sound //; simpl. apply sep_mono_r.
apply forall_intro=>s; apply wand_intro_l.
......@@ -205,4 +205,4 @@ Tactic Notation "iSts" constr(H) "as"
|iAssumptionCore || fail "iSts:" H "not found"
|solve_ndisj
|intros s Hs; eexists; split; [env_cbv; reflexivity|simpl]].
Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?.
\ No newline at end of file
Tactic Notation "iSts" constr(H) "as" simple_intropattern(s) := iSts H as s ?.
......@@ -352,10 +352,11 @@ Proof.
by setoid_rewrite affinely_elim.
Qed.
Global Instance elim_modal_pvs_wp e E P Φ :
ElimModal (True) (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. intros.
rewrite /ElimModal => ?. rewrite pvs_frame_r wand_elim_r pvs_wp //=.
Global Instance elim_modal_pvs_wp e E P Φ p :
ElimModal True p false (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof.
intros. rewrite /ElimModal intuitionistically_if_elim => ?.
rewrite pvs_frame_r wand_elim_r pvs_wp //=.
Qed.
Global Instance elim_inv_wp e E N P Φ:
......@@ -373,7 +374,7 @@ Global Instance frame_wp p E e R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v)) Frame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
Proof.
rewrite /Frame=> HA HR. rewrite -(affine_affinely R) => //=.
rewrite -{1}(affine_affinely (bi_affinely_if p _)) wp_frame_l. apply wp_mono => v.
rewrite -{1}(affine_affinely (bi_intuitionistically_if p _)) wp_frame_l. apply wp_mono => v.
rewrite ?affine_affinely. apply HR.
Qed.
......
......@@ -425,7 +425,6 @@ Section ClosedProofs.
iMod (heap_alloc with "Hσ") as (h) "[Hheap ?]"; first by done.
iMod (sheap_alloc with "Hsσ") as (h') "[Hsheap ?]"; first by done.
iPoseProof (heap_e_spec with "[Hheap Hsheap Hown]") as "Hspec"; eauto.
{ by iFrame. }
iApply wp_wand_l. iFrame "Hspec".
iAlways. iIntros (v) "(%&?)".
iExists #2.
......
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