diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 35b66fde026ffa48757a71f33c81094f7ecd5419..b0707a29cbb4ac752352a8fba695ed3875c4169a 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -66,7 +66,7 @@ Lemma acquire_spec l R (Φ : val → iProp) :
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
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".
+ iNext. iExists true. by iSplit.
+ wp_if. by iApply "IH".
@@ -79,8 +79,7 @@ Lemma release_spec R l (Φ : val → iProp) :
(locked l R ★ R ★ Φ #()) ⊢ WP release #l {{ Φ }}.
Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
- rewrite /release. wp_let.
- iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl _]".
+ rewrite /release. wp_let. iInv N as {b} "[Hl _]".
wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ".
Qed.
End proof.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 53fc6d6c7739cf44b1f488a8928ae0d35a115ba0..dd0515fe445afb4573c4341ec809fd360430d6e7 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -65,7 +65,7 @@ Proof.
- wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle.
iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit.
- 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].
iExists (InjRV v); iFrame "Hl"; iRight; iExists v; iSplit; [done|by iLeft].
Qed.
@@ -74,8 +74,7 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
(join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
Proof.
rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
- iLöb as "IH". wp_rec. wp_focus (! _)%E.
- iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
+ iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].
wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index d2161d80e68c22181c3fd6d77f2332c4df7ca698..ae13afe5bd8c0709f6dbd2f168ac54090599ffc0 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -30,8 +30,7 @@ Proof.
Qed.
End invariants.
-Tactic Notation "iInv" constr(N) "as" constr(pat) :=
- let H := iFresh in
+Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
eapply tac_inv_fsa with _ _ _ _ N H _ _;
[let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P
@@ -39,10 +38,25 @@ Tactic Notation "iInv" constr(N) "as" constr(pat) :=
|done || eauto with ndisj (* [eauto with ndisj] is slow *)
|iAssumption || fail "iInv: invariant" N "not found"
|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
+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.
+
+Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
[let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
apply _ || fail "iInv: cannot viewshift in goal" P
@@ -52,4 +66,20 @@ Tactic Notation "iInv>" constr(N) "as" constr(pat) :=
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iInv:" P "not timeless"
|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.