Commit 200f88a9 authored by Robbert Krebbers's avatar Robbert Krebbers

Intro pattern for framing.

parent facc902a
......@@ -33,7 +33,7 @@ Proof.
ef = None e' = Loc l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_head_step (Alloc e) φ σ) // /φ;
last (by intros; inv_head_step; eauto 8); last (by simpl; eauto).
iIntros "[HP HΦ]". iFrame "HP". iNext.
iIntros "[$ HΦ]". iNext.
iIntros {v2 σ2 ef} "[% HP]".
(* FIXME: I should not have to refer to "H0". *)
destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
......
......@@ -77,10 +77,10 @@ Lemma vs_impl E P Q : □ (P → Q) ⊢ (P ={E}=> Q).
Proof. iIntros "#HPQ ! HP". by iApply "HPQ". Qed.
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) (R P ={E1,E2}=> R Q).
Proof. iIntros "#Hvs ! [HR HP]". iFrame "HR". by iApply "Hvs". Qed.
Proof. iIntros "#Hvs ! [$ HP]". by iApply "Hvs". Qed.
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) (P R ={E1,E2}=> Q R).
Proof. iIntros "#Hvs ! [HP HR]". iFrame "HR". by iApply "Hvs". Qed.
Proof. iIntros "#Hvs ! [HP $]". by iApply "Hvs". Qed.
Lemma vs_mask_frame E1 E2 Ef P Q :
Ef E1 E2 (P ={E1,E2}=> Q) (P ={E1 Ef,E2 Ef}=> Q).
......
......@@ -5,6 +5,7 @@ Inductive intro_pat :=
| IAnom : intro_pat
| IAnomPure : intro_pat
| IClear : intro_pat
| IFrame : intro_pat
| IPersistent : intro_pat intro_pat
| IList : list (list intro_pat) intro_pat
| ISimpl : intro_pat
......@@ -16,6 +17,7 @@ Inductive token :=
| TAnom : token
| TAnomPure : token
| TClear : token
| TFrame : token
| TPersistent : token
| TBar : token
| TBracketL : token
......@@ -35,6 +37,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
| String "%" s => tokenize_go s (TAnomPure :: cons_name kn k) ""
| String "_" s => tokenize_go s (TClear :: cons_name kn k) ""
| String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
| String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
......@@ -99,6 +102,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TAnom :: ts => parse_go ts (SPat IAnom :: k)
| TAnomPure :: ts => parse_go ts (SPat IAnomPure :: k)
| TClear :: ts => parse_go ts (SPat IClear :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k)
| TPersistent :: ts => parse_go ts (SPersistent :: k)
| TBracketL :: ts => parse_go ts (SList :: k)
| TBar :: ts => parse_go ts (SBar :: k)
......
......@@ -551,6 +551,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IAnom => idtac
| IAnomPure => iPure Hz
| IClear => iClear Hz
| IFrame => iFrame Hz
| IName ?y => iRename Hz into y
| IPersistent ?pat => iPersistent Hz; go Hz pat
| IList [[]] => iContradiction Hz
......
......@@ -63,11 +63,11 @@ Proof.
+ iExists (InjRV #m). iFrame "Hl". iRight; iExists m; by iSplit. }
iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
iAssert (one_shot_inv γ l (v = InjLV #0 n : Z,
v = InjRV #n own γ (Shot (DecAgree n))))%I as "[Hl #Hv]" with "-".
v = InjRV #n own γ (Shot (DecAgree n))))%I as "[$ #Hv]" with "-".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". by iLeft.
+ iSplit. iRight; iExists m; by iSplitL "Hl". iRight; iExists m; by iSplit. }
iFrame "Hl". wp_let. iPvsIntro. iIntros "!". wp_seq.
wp_let. iPvsIntro. iIntros "!". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
{ wp_case. wp_seq. by iPvsIntro. }
wp_case. wp_let. wp_focus (! _)%E.
......
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