Commit 677c3e3a authored by Robbert Krebbers's avatar Robbert Krebbers

Add iInv N as {x1 .. xn} "pat".

parent ab19e50e
...@@ -66,7 +66,7 @@ Lemma acquire_spec l R (Φ : val → iProp) : ...@@ -66,7 +66,7 @@ Lemma acquire_spec l R (Φ : val → iProp) :
Proof. Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)". iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E. iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iInv N as "Hinv". iDestruct "Hinv" as { [] } "[Hl HR]". iInv N as { [] } "[Hl HR]".
- wp_cas_fail. iSplitL "Hl". - wp_cas_fail. iSplitL "Hl".
+ iNext. iExists true. by iSplit. + iNext. iExists true. by iSplit.
+ wp_if. by iApply "IH". + wp_if. by iApply "IH".
...@@ -79,8 +79,7 @@ Lemma release_spec R l (Φ : val → iProp) : ...@@ -79,8 +79,7 @@ Lemma release_spec R l (Φ : val → iProp) :
(locked l R R Φ #()) WP release #l {{ Φ }}. (locked l R R Φ #()) WP release #l {{ Φ }}.
Proof. Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)". iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
rewrite /release. wp_let. rewrite /release. wp_let. iInv N as {b} "[Hl _]".
iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl _]".
wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ". wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
Qed. Qed.
End proof. End proof.
...@@ -65,7 +65,7 @@ Proof. ...@@ -65,7 +65,7 @@ Proof.
- wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle.
iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit. iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit.
- wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv". - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]". iInv N as {v'} "[Hl _]"; first wp_done.
wp_store. iSplit; [iNext|done]. wp_store. iSplit; [iNext|done].
iExists (InjRV v); iFrame "Hl"; iRight; iExists v; iSplit; [done|by iLeft]. iExists (InjRV v); iFrame "Hl"; iRight; iExists v; iSplit; [done|by iLeft].
Qed. Qed.
...@@ -74,8 +74,7 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) : ...@@ -74,8 +74,7 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
(join_handle l Ψ v, Ψ v - Φ v) WP join #l {{ Φ }}. (join_handle l Ψ v, Ψ v - Φ v) WP join #l {{ Φ }}.
Proof. Proof.
rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)". rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|]. - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
wp_case. wp_seq. iApply ("IH" with "Hγ Hv"). wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
......
...@@ -30,8 +30,7 @@ Proof. ...@@ -30,8 +30,7 @@ Proof.
Qed. Qed.
End invariants. End invariants.
Tactic Notation "iInv" constr(N) "as" constr(pat) := Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
let H := iFresh in
eapply tac_inv_fsa with _ _ _ _ N H _ _; eapply tac_inv_fsa with _ _ _ _ N H _ _;
[let P := match goal with |- FSASplit ?P _ _ _ _ => P end in [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P apply _ || fail "iInv: cannot viewshift in goal" P
...@@ -39,10 +38,25 @@ Tactic Notation "iInv" constr(N) "as" constr(pat) := ...@@ -39,10 +38,25 @@ Tactic Notation "iInv" constr(N) "as" constr(pat) :=
|done || eauto with ndisj (* [eauto with ndisj] is slow *) |done || eauto with ndisj (* [eauto with ndisj] is slow *)
|iAssumption || fail "iInv: invariant" N "not found" |iAssumption || fail "iInv: invariant" N "not found"
|env_cbv; reflexivity |env_cbv; reflexivity
|simpl (* get rid of FSAs *); iDestruct H as pat]. |simpl (* get rid of FSAs *)].
Tactic Notation "iInv>" constr(N) "as" constr(pat) := Tactic Notation "iInv" constr(N) "as" constr(pat) :=
let H := iFresh in let H := iFresh in iInvCore N as H; last iDestruct H as pat.
Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1) "}"
constr(pat) :=
let H := iFresh in iInvCore N as H; last iDestruct H as {x1} pat.
Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) "}" constr(pat) :=
let H := iFresh in iInvCore N as H; last iDestruct H as {x1 x2} pat.
Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
let H := iFresh in iInvCore N as H; last iDestruct H as {x1 x2 x3} pat.
Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
constr(pat) :=
let H := iFresh in iInvCore N as H; last iDestruct H as {x1 x2 x3 x4} pat.
Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _; eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
[let P := match goal with |- FSASplit ?P _ _ _ _ => P end in [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P apply _ || fail "iInv: cannot viewshift in goal" P
...@@ -52,4 +66,20 @@ Tactic Notation "iInv>" constr(N) "as" constr(pat) := ...@@ -52,4 +66,20 @@ Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
|let P := match goal with |- TimelessP ?P => P end in |let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iInv:" P "not timeless" apply _ || fail "iInv:" P "not timeless"
|env_cbv; reflexivity |env_cbv; reflexivity
|simpl (* get rid of FSAs *); iDestruct H as pat]. |simpl (* get rid of FSAs *)].
Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
let H := iFresh in iInvCore> N as H; last iDestruct H as pat.
Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1) "}"
constr(pat) :=
let H := iFresh in iInvCore> N as H; last iDestruct H as {x1} pat.
Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) "}" constr(pat) :=
let H := iFresh in iInvCore> N as H; last iDestruct H as {x1 x2} pat.
Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
let H := iFresh in iInvCore> N as H; last iDestruct H as {x1 x2 x3} pat.
Tactic Notation "iInv>" constr(N) "as" "{" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
constr(pat) :=
let H := iFresh in iInvCore> N as H; last iDestruct H as {x1 x2 x3 x4} pat.
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