Skip to content
GitLab
Commit cc1fa7b6 authored by Ralf Jung's avatar Ralf Jung
Browse files

bump Iris; update for new ElimInv

parent 7267315b
Pipeline #8781 failed with stage
in 18 minutes and 32 seconds
Hide whitespace changes
Inline Side-by-side
opam
View file @ cc1fa7b6
......@@ -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-05-09.1.c2b96095") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-17.0.0aeb4cdc") | (= "dev") }
]
theories/chan_lang/refine_heap.v
View file @ cc1fa7b6
......@@ -162,7 +162,7 @@ Section heap.
Proof.
iIntros (?) "[#Hinv HΦ]". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -208,7 +208,7 @@ Section heap.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -238,7 +238,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -267,7 +267,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -307,7 +307,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -349,7 +349,7 @@ Section heap.
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -391,7 +391,7 @@ Section heap.
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -434,7 +434,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -478,7 +478,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -522,7 +522,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -553,7 +553,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -585,7 +585,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -628,7 +628,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -671,7 +671,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -714,7 +714,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -760,7 +760,7 @@ Section heap.
Proof.
iIntros (? Hred Hdet ?) "(#Hinv&HΦ)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -784,7 +784,7 @@ Section heap.
Proof.
iIntros (Hstep ?) "(#Hinv&HΦ)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -805,7 +805,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ)". rewrite /scheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......
theories/heap_lang/refine_heap.v
View file @ cc1fa7b6
......@@ -127,7 +127,7 @@ Section heap.
Proof.
iIntros (??) "[#Hinv HΦ]". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -172,7 +172,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -202,7 +202,7 @@ Section heap.
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -243,7 +243,7 @@ Section heap.
Proof.
iIntros (????) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -276,7 +276,7 @@ Section heap.
Proof.
iIntros (???) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -318,7 +318,7 @@ Section heap.
Proof.
iIntros (??) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -361,7 +361,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ&Hpt)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -406,7 +406,7 @@ Section heap.
Proof.
iIntros (?? Hstep ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -430,7 +430,7 @@ Section heap.
Proof.
iIntros (? Hred Hdet ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -454,7 +454,7 @@ Section heap.
Proof.
iIntros (Hstep ?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......@@ -475,7 +475,7 @@ Section heap.
Proof.
iIntros (?) "(#Hinv&HΦ)". rewrite /sheap_ctx.
rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "(>Hγ&>Hφ)" "_".
iInv "Hinv" as (a') "(>Hγ&>Hφ)".
do 2 iApply affinely_elim in "Hφ".
iApply affinely_elim in "Hγ".
iCombine "HΦ" "Hφ" as "Hrefine".
......
theories/locks/lock_reln.v
View file @ cc1fa7b6
......@@ -1319,7 +1319,7 @@ Qed.
iDestruct "Hv1" as (l1 l1') "(%&%&Hv1)".
rewrite -/val_equiv_pre.
iInv "Hv1" as "Hinv" "_"; auto with fsaV.
iInv "Hv1" as "Hinv"; auto with fsaV.
iDestruct "Hinv" as (v v') "(>Hl1&>Hl2&Hvequiv)".
subst.
iDestruct "HS" as "(#?&#?&#?)".
......@@ -1359,7 +1359,7 @@ Qed.
iDestruct "Hv1" as (l1 l1') "(%&%&Hv1)".
rewrite -/val_equiv_pre.
iInv "Hv1" as "Hinv" "_"; auto with fsaV.
iInv "Hv1" as "Hinv"; auto with fsaV.
iDestruct "Hinv" as (v v') "(>Hl1&>Hl2&Hvequiv)".
iApply affinely_elim in "Hl1".
iApply affinely_elim in "Hl2".
......
theories/locks/ticket_clh_triples.v
View file @ cc1fa7b6
......@@ -638,7 +638,7 @@ Section proof.
* apply sts.closed_up. set_solver.
- iDestruct "Hx" as "#Hx".
wp_focus (! #lpred)%E.
iInv "Hx" as "Hspin" "_"; auto with fsaV.
iInv "Hx" as "Hspin"; auto with fsaV.
rewrite /spin_inv //=.
iDestruct "Hspin" as "[Hspin|Hspin]".
* (* Pred is still true, so we are going to spin and appeal to IH.
......@@ -778,7 +778,7 @@ Section proof.
wp_let. refine_delay (d-1).
wp_proj. refine_delay (d-2).
wp_focus (Swap _ _)%E.
iInv "Hnext" as "HnextOpen" "_"; auto with fsaV.
iInv "Hnext" as "HnextOpen"; auto with fsaV.
rewrite {2}/next_inv.
iDestruct "HnextOpen" as (n l) "(>Hn&>Htl&Hold&Htoks)".
iApply affinely_elim in "Hn".
......@@ -897,7 +897,7 @@ Section proof.
iModIntro.
rewrite (sts_up_dup γ (ticket_entered x)). iDestruct "Hsts" as "(Hsts0&Hsts)".
iApply wp_pvs. wp_proj.
iInv "Hinv" as "Hspin" "_"; auto with fsaV.
iInv "Hinv" as "Hspin"; auto with fsaV.
rewrite /spin_inv.
iDestruct "Hspin" as "[Hspin|Hspin]"; last first.
{ (* Impossible, because we own lmine ↦{1/2} # true *)
......@@ -956,7 +956,7 @@ Section proof.
wp_load. refine_op d.
(* Open invariants again to release *)
iInv "Hinv" as "Hspin" "_"; auto with fsaV.
iInv "Hinv" as "Hspin"; auto with fsaV.
iApply wp_pvs.
rewrite /spin_inv.
iDestruct "Hspin" as "[Hspin|Hspin]"; last first.
......
theories/program_logic/auth.v
View file @ cc1fa7b6
......@@ -106,7 +106,7 @@ Section auth.
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "[Hγ Hφ]" "_".
iInv "Hinv" as (a') "[Hγ Hφ]".
iMod "Hγ". iMod "Hγf". iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affinely_elim (own γ _)).
iDestruct (own_valid with "Hγ") as "#Hvalid".
......@@ -133,7 +133,7 @@ Section auth.
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv "Hinv" as (a') "[Hγ Hφ]" "_".
iInv "Hinv" as (a') "[Hγ Hφ]".
iMod "Hγ"; iMod "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
rewrite (affinely_elim (own γ _)).
iDestruct (own_valid with "Hγ") as "#Hvalid".
......
theories/program_logic/hoare.v
View file @ cc1fa7b6
......@@ -159,7 +159,7 @@ Lemma ht_inv N E P Φ R e :
(inv N R ★ {{ ⧆▷ R ★ P }} e @ E ∖ nclose N {{ v, ⧆▷ R ★ Φ v }})
⊢ {{ P }} e @ E {{ Φ }}.
Proof.
iIntros (??) "[#Hinv #Hwp] !# HP". iInv "Hinv" as "HR" "_". iApply "Hwp".
iIntros (??) "[#Hinv #Hwp] !# HP". iInv "Hinv" as "HR". iApply "Hwp".
by iSplitL "HR".
Qed.
End hoare.
theories/program_logic/invariants.v
View file @ cc1fa7b6
......@@ -118,31 +118,30 @@ Qed.
Global Instance into_inv_inv N P: IntoInv (inv N P) N.
Global Instance elim_inv_inv E N P Q:
ElimInv (↑N ⊆ E) (inv N P) emp (⧆▷ P) emp (|={E}=> Q) (|={E ∖ nclose N}=> ⧆▷ P ∗ Q)%I.
ElimInv (↑N ⊆ E) (inv N P) emp (λ _:(), ⧆▷ P)%I None (|={E}=> Q) (λ _, |={E ∖ nclose N}=> ⧆▷ P ∗ Q)%I.
Proof.
rewrite /ElimInv/ElimModal.
intros Hclose. rewrite //= !right_id !left_id.
intros Hclose. rewrite //= forall_unit !right_id !left_id.
iIntros "H".
iPoseProof (inv_afsa _ E _ _ (λ x, Q) with "[H]") as "H"; auto.
by rewrite /up_close in Hclose.
iPoseProof (inv_afsa _ E _ _ (λ x, Q) with "[H]") as "H"; eauto.
Qed.
Global Instance elim_inv_fsa {V: Type} (fsa : FSA Λ Σ V) fsaV E N P Ψ:
FrameShiftAssertion fsaV fsa →
ElimInv (↑N ⊆ E ∧ fsaV) (inv N P) emp
(⧆▷ P) emp (fsa E Ψ) (fsa (E ∖ nclose N) (λ a, ⧆▷ P ∗ Ψ a))%I.
(λ _:(), ⧆▷ P)%I None (fsa E Ψ) (λ _, fsa (E ∖ nclose N) (λ a, ⧆▷ P ∗ Ψ a))%I.
Proof.
rewrite /ElimInv => FSA [Hclose ?]. rewrite //= !right_id !left_id.
rewrite /ElimInv => FSA [Hclose ?]. rewrite //= forall_unit !right_id !left_id.
eapply inv_fsa; eauto.
Qed.
Global Instance elim_inv_afsa {A} (fsa : FSA Λ Σ A) fsaV E N P Ψ:
AffineFrameShiftAssertion fsaV fsa →
ElimInv (↑N ⊆ E ∧ fsaV) (inv N P) emp
(⧆▷ P) emp (fsa E Ψ) (fsa (E ∖ nclose N) (λ a, ⧆▷ P ∗ Ψ a))%I.
(λ _:(), ⧆▷ P)%I None (fsa E Ψ) (λ _, fsa (E ∖ nclose N) (λ a, ⧆▷ P ∗ Ψ a))%I.
Proof.
rewrite /ElimInv => FSA [Hclose ?]. rewrite //= !right_id !left_id.
rewrite /ElimInv => FSA [Hclose ?]. rewrite //= forall_unit !right_id !left_id.
eapply inv_afsa; eauto.
Qed.
End inv.
\ No newline at end of file
End inv.
theories/program_logic/pstepshifts.v
View file @ cc1fa7b6
......@@ -297,7 +297,7 @@ Proof.
Qed.
Global Instance elim_inv_psvs {Λ Σ} E N (P: iProp Λ Σ) Q:
ElimInv (↑N ⊆ E) (inv N P) emp (⧆▷ P) emp (|={E}=>> Q) (|={E ∖ nclose N}=>> ⧆▷ P ∗ Q)%I.
ElimInv (↑N ⊆ E) (inv N P) emp (λ _:(), ⧆▷ P)%I None (|={E}=>> Q) (λ _, |={E ∖ nclose N}=>> ⧆▷ P ∗ Q)%I.
Proof.
rewrite /ElimInv. iIntros (?) "(?&_&Hclose)".
iApply (elim_inv_afsa _ _ E N _ (λ _, Q) psvs_fsa_prf); auto.
......
theories/program_logic/sts.v
View file @ cc1fa7b6
......@@ -109,7 +109,7 @@ Section sts.
⊢ fsa E Ψ.
Proof.
iIntros (??) "(#Hinv & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
iInv "Hinv" as (s) "[Hγ Hφ]" "_"; iMod "Hγ".
iInv "Hinv" as (s) "[Hγ Hφ]"; iMod "Hγ".
rewrite (affinely_elim (own γ _)).
iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ") as %Hvalid.
assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
......
theories/program_logic/viewshifts.v
View file @ cc1fa7b6
......@@ -76,7 +76,7 @@ Lemma vs_inv N E P Q R :
nclose N ⊆ E → (inv N R ★ (⧆▷ R ★ P ={E ∖ nclose N}=> ⧆▷ R ★ Q)) ⊢ (P ={E}=> Q).
Proof.
iIntros (?) "[#Hinv #Hvs] !# HP".
iInv N as "HR" "_". iApply "Hvs". by iSplitL "HR".
iInv N as "HR". iApply "Hvs". by iSplitL "HR".
Qed.
Lemma vs_alloc N P : ⧆▷ P ={↑ N}=> inv N P.
......
theories/program_logic/weakestpre.v
View file @ cc1fa7b6
......@@ -360,11 +360,11 @@ Proof.
Qed.
Global Instance elim_inv_wp e E N P Φ:
ElimInv (↑N ⊆ E ∧ atomic e) (inv N P) emp (⧆▷ P) emp
(WP e @ E {{ Φ }}) (WP e @ (E ∖ nclose N) {{ v, (⧆▷ P ∗ Φ v)%I }})%I.
ElimInv (↑N ⊆ E ∧ atomic e) (inv N P) emp (λ _:(), ⧆▷ P)%I None
(WP e @ E {{ Φ }}) (λ _, WP e @ (E ∖ nclose N) {{ v, (⧆▷ P ∗ Φ v)%I }})%I.
Proof.
rewrite /ElimInv/ElimModal.
intros [Hclose ?]. rewrite //= !right_id !left_id.
intros [Hclose ?]. rewrite //= forall_unit !right_id !left_id.
iIntros "H".
iPoseProof (inv_afsa _ E _ _ _ with "[H]") as "H"; eauto.
Qed.
......
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