From 086cc92c8e5ea852d131db2ed2c2f86198748874 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 13 Jul 2016 13:45:04 +0200
Subject: [PATCH] Use round braces instead of curly braces in proof mode
tactics.
The intropattern {H} also meant clear (both in ssreflect, and the logic
part of the introduction pattern).
---
heap_lang/heap.v | 22 +-
heap_lang/lib/barrier/proof.v | 24 +-
heap_lang/lib/barrier/specification.v | 6 +-
heap_lang/lib/counter.v | 14 +-
heap_lang/lib/lock.v | 14 +-
heap_lang/lib/par.v | 10 +-
heap_lang/lib/spawn.v | 14 +-
heap_lang/lifting.v | 4 +-
program_logic/auth.v | 16 +-
program_logic/boxes.v | 28 +--
program_logic/ectx_lifting.v | 14 +-
program_logic/hoare.v | 22 +-
program_logic/hoare_lifting.v | 20 +-
program_logic/invariants.v | 8 +-
program_logic/lifting.v | 12 +-
program_logic/sts.v | 10 +-
program_logic/viewshifts.v | 6 +-
proofmode/invariants.v | 44 ++--
proofmode/pviewshifts.v | 46 ++--
proofmode/tactics.v | 322 +++++++++++++-------------
tests/barrier_client.v | 18 +-
tests/heap_lang.v | 8 +-
tests/joining_existentials.v | 18 +-
tests/one_shot.v | 22 +-
tests/proofmode.v | 14 +-
25 files changed, 368 insertions(+), 368 deletions(-)
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index a9dad2729..2f46b0eb9 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -153,13 +153,13 @@ Section heap.
to_val e = Some v → nclose N ⊆ E →
heap_ctx N ★ ▷ (∀ l, l ↦ v ={E}=★ Φ (LitV (LitLoc l))) ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
- iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
+ iIntros (??) "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
- iFrame "Hinv Hheap". iIntros {h}. rewrite left_id.
+ iFrame "Hinv Hheap". iIntros (h). rewrite left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
- iIntros {l} "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
+ iIntros (l) "[% Hheap]"; iPvsIntro; iExists {[ l := (1%Qp, DecAgree v) ]}.
rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
iFrame "Hheap". iSplitR; first iPureIntro.
{ by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
@@ -171,10 +171,10 @@ Section heap.
heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v ={E}=★ Φ v)
⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
- iIntros {?} "[#Hh [Hl HΦ]]".
+ iIntros (?) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
- iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+ iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
@@ -186,10 +186,10 @@ Section heap.
heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v ={E}=★ Φ (LitV LitUnit))
⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
- iIntros {??} "[#Hh [Hl HΦ]]".
+ iIntros (??) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
- iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+ iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v)]}; iSplit.
@@ -202,10 +202,10 @@ Section heap.
heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' ={E}=★ Φ (LitV (LitBool false)))
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
- iIntros {????} "[#Hh [Hl HΦ]]".
+ iIntros (????) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
- iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+ iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists _; iSplit; first done.
@@ -217,10 +217,10 @@ Section heap.
heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 ={E}=★ Φ (LitV (LitBool true)))
⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
- iIntros {???} "[#Hh [Hl HΦ]]".
+ iIntros (???) "[#Hh [Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iApply wp_pvs; iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
- iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+ iFrame "Hh Hl". iIntros (h) "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
rewrite insert_insert !of_heap_singleton_op; eauto. iFrame "Hl".
iIntros "> Hown". iPvsIntro. iExists {[l := (1%Qp, DecAgree v2)]}; iSplit.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 645347ed9..7b08ad632 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -81,7 +81,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
(Q -★ R1 ★ R2) ★ ress P I
⊢ ress P ({[i1;i2]} ∪ I ∖ {[i]}).
Proof.
- iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
+ iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
@@ -99,12 +99,12 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
heap_ctx heapN ★ (∀ l, recv l P ★ send l P -★ Φ #l)
⊢ WP newbarrier #() {{ Φ }}.
Proof.
- iIntros {HN} "[#? HΦ]".
+ iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
iApply "HΦ".
- iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
+ iPvs (saved_prop_alloc (F:=idCF) _ P) as (γ) "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
- as {γ'} "[#? Hγ']"; eauto.
+ as (γ') "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame.
iExists (const P). rewrite !big_sepS_singleton /=. eauto. }
iAssert (barrier_ctx γ' l P)%I as "#?".
@@ -125,14 +125,14 @@ Lemma signal_spec l P (Φ : val → iProp) :
send l P ★ P ★ Φ #() ⊢ WP signal #l {{ Φ }}.
Proof.
rewrite /signal /send /barrier_ctx.
- iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
+ iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_store. iPvsIntro. destruct p; [|done].
iExists (State High I), (∅ : set token).
iSplit; [iPureIntro; by eauto using signal_step|].
iSplitR "HΦ"; [iNext|by auto].
rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
- iDestruct "Hr" as {Ψ} "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
+ iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iIntros "> _"; by iApply "Hr".
Qed.
@@ -140,7 +140,7 @@ Lemma wait_spec l P (Φ : val → iProp) :
recv l P ★ (P -★ Φ #()) ⊢ WP wait #l {{ Φ }}.
Proof.
rename P into R; rewrite /recv /barrier_ctx.
- iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+ iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
wp_load. iPvsIntro. destruct p.
@@ -155,7 +155,7 @@ Proof.
return to the client *)
iExists (State High (I ∖ {[ i ]})), (∅ : set token).
iSplit; [iPureIntro; by eauto using wait_step|].
- iDestruct "Hr" as {Ψ} "[HΨ Hsp]".
+ iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
iAssert (▷ Ψ i ★ ▷ [★ set] j ∈ I ∖ {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
@@ -171,12 +171,12 @@ Lemma recv_split E l P1 P2 :
nclose N ⊆ E → recv l (P1 ★ P2) ={E}=> recv l P1 ★ recv l P2.
Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
- iIntros {?}. iDestruct 1 as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+ iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iApply pvs_trans'.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
- iPvs (saved_prop_alloc_strong _ (R1: ∙%CF iProp) I) as {i1} "[% #Hi1]".
+ iPvs (saved_prop_alloc_strong _ (R1: ∙%CF iProp) I) as (i1) "[% #Hi1]".
iPvs (saved_prop_alloc_strong _ (R2: ∙%CF iProp) (I ∪ {[i1]}))
- as {i2} "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2; iPvsIntro.
+ as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2; iPvsIntro.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iExists (State p ({[i1; i2]} ∪ I ∖ {[i]})).
iExists ({[Change i1; Change i2 ]}).
@@ -199,7 +199,7 @@ Qed.
Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ recv l P1 -★ recv l P2.
Proof.
rewrite /recv.
- iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)".
+ iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
iIntros "> HQ". by iApply "HP"; iApply "HP1".
Qed.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index c56f4d8a8..a3bd8275f 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -22,9 +22,9 @@ Proof.
intros HN.
exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
split_and?; simpl.
- - iIntros {P} "#? ! _". iApply (newbarrier_spec _ _ P); eauto.
- - iIntros {l P} "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
- - iIntros {l P} "! Hl". iApply wait_spec; iFrame "Hl"; eauto.
+ - iIntros (P) "#? ! _". iApply (newbarrier_spec _ _ P); eauto.
+ - iIntros (l P) "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
+ - iIntros (l P) "! Hl". iApply wait_spec; iFrame "Hl"; eauto.
- intros; by apply recv_split.
- apply recv_weaken.
Qed.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 62e3abe0a..05d110fbd 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -38,9 +38,9 @@ Lemma newcounter_spec N (R : iProp) Φ :
heapN ⊥ N →
heap_ctx heapN ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
Proof.
- iIntros {?} "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+ iIntros (?) "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
- as {γ} "[#? Hγ]"; try by auto.
+ as (γ) "[#? Hγ]"; try by auto.
iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
Qed.
@@ -48,13 +48,13 @@ Lemma inc_spec l j (Φ : val → iProp) :
counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
- iDestruct "Hl" as {N γ} "(% & #? & #Hγ & Hγf)".
+ iDestruct "Hl" as (N γ) "(% & #? & #Hγ & Hγf)".
wp_focus (! _)%E; iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
- iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /="; rewrite {2}/counter_inv.
+ iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /="; rewrite {2}/counter_inv.
wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
wp_let; wp_op.
wp_focus (CAS _ _ _); iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
- iIntros "{$Hγ $Hγf}"; iIntros {j''} "[% Hl] /="; rewrite {2}/counter_inv.
+ iIntros "{$Hγ $Hγf}"; iIntros (j'') "[% Hl] /="; rewrite {2}/counter_inv.
destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
- wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
iExists (1 + j `max` j')%nat; iSplit.
@@ -73,9 +73,9 @@ Lemma read_spec l j (Φ : val → iProp) :
counter l j ★ (∀ i, ■(j ≤ i)%nat → counter l i -★ Φ #i)
⊢ WP read #l {{ Φ }}.
Proof.
- iIntros "[Hc HΦ]". iDestruct "Hc" as {N γ} "(% & #? & #Hγ & Hγf)".
+ iIntros "[Hc HΦ]". iDestruct "Hc" as (N γ) "(% & #? & #Hγ & Hγf)".
rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
- iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /=".
+ iIntros "{$Hγ $Hγf}"; iIntros (j') "[% Hl] /=".
wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
{ iPureIntro; apply mnat_local_update; abstract lia. }
rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent; iIntros "{$Hl} Hγf".
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 3edac7433..a5495285c 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -44,15 +44,15 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed.
Lemma locked_is_lock l R : locked l R ⊢ is_lock l R.
-Proof. rewrite /is_lock. iDestruct 1 as {N γ} "(?&?&?&_)"; eauto. Qed.
+Proof. rewrite /is_lock. iDestruct 1 as (N γ) "(?&?&?&_)"; eauto. Qed.
Lemma newlock_spec N (R : iProp) Φ :
heapN ⊥ N →
heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
Proof.
- iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
+ iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl".
- iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
+ iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
{ iIntros ">". iExists false. by iFrame. }
iPvsIntro. iApply "HΦ". iExists N, γ; eauto.
@@ -61,9 +61,9 @@ Qed.
Lemma acquire_spec l R (Φ : val → iProp) :
is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}.
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.
- iInv N as { [] } "[Hl HR]".
+ iInv N as ([]) "[Hl HR]".
- wp_cas_fail. iPvsIntro; iSplitL "Hl".
+ iNext. iExists true; eauto.
+ wp_if. by iApply "IH".
@@ -75,8 +75,8 @@ Qed.
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 {b} "[Hl _]".
+ iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (N γ) "(% & #? & #? & Hγ)".
+ rewrite /release. wp_let. iInv N as (b) "[Hl _]".
wp_store. iPvsIntro. iFrame "HΦ". iNext. iExists false. by iFrame.
Qed.
End proof.
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 05e0f1cfe..d1612a5aa 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -27,12 +27,12 @@ Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
⊢ WP par e {{ Φ }}.
Proof.
- iIntros {??} "(#Hh&Hf1&Hf2&HΦ)".
+ iIntros (??) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iPvsIntro. wp_let. wp_proj.
wp_apply spawn_spec; try wp_done. iFrame "Hf1 Hh".
- iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _).
- iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let.
- wp_apply join_spec; iFrame "Hl". iIntros {w} "H1".
+ iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _).
+ iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
+ wp_apply join_spec; iFrame "Hl". iIntros (w) "H1".
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Qed.
@@ -42,7 +42,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
⊢ WP e1 || e2 {{ Φ }}.
Proof.
- iIntros {?} "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto.
+ iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); auto.
iFrame "Hh H". iSplitL "H1"; by wp_let.
Qed.
End proof.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 5bfb576cd..a912a548e 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -56,15 +56,15 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
heap_ctx heapN ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l)
⊢ WP spawn e {{ Φ }}.
Proof.
- iIntros {<-%of_to_val ?} "(#Hh & Hf & HΦ)". rewrite /spawn.
+ iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
wp_let. wp_alloc l as "Hl". wp_let.
- iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
+ iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
{ iNext. iExists (InjLV #0). iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf".
- iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros {v} "Hv".
- iInv N as {v'} "[Hl _]"; first wp_done.
+ - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
+ iInv N as (v') "[Hl _]"; first wp_done.
wp_store. iPvsIntro. iSplit; [iNext|done].
iExists (InjRV v). iFrame. eauto.
Qed.
@@ -72,12 +72,12 @@ Qed.
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 {v} "[Hl Hinv]".
+ rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
+ iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
wp_match. iApply ("IH" with "Hγ Hv").
- - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; simplify_eq/=.
+ - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
+ iPvsIntro; iSplitL "Hl Hγ".
{ iNext. iExists _; iFrame; eauto. }
wp_match. by iApply "Hv".
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 7b71e277d..c418dc4f4 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -28,9 +28,9 @@ Lemma wp_alloc_pst E σ e v Φ :
▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) ={E}=★ Φ (LitV (LitLoc l)))
⊢ WP Alloc e @ E {{ Φ }}.
Proof.
- iIntros {?} "[HP HΦ]".
+ iIntros (?) "[HP HΦ]".
iApply (wp_lift_atomic_head_step (Alloc e) σ); try (by simpl; eauto).
- iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]". inv_head_step.
+ iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 9fd82aa07..841d143d9 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -70,8 +70,8 @@ Section auth.
✓ a → nclose N ⊆ E →
▷ φ a ={E}=> ∃ γ, ■(γ ∉ G) ∧ auth_ctx γ N φ ∧ auth_own γ a.
Proof.
- iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
- iPvs (own_alloc_strong (Auth (Excl' a) a) _ G) as {γ} "[% Hγ]"; first done.
+ iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
+ iPvs (own_alloc_strong (Auth (Excl' a) a) _ G) as (γ) "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
{ iNext. iExists a. by iFrame. }
@@ -82,8 +82,8 @@ Section auth.
✓ a → nclose N ⊆ E →
▷ φ a ={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a.
Proof.
- iIntros {??} "Hφ".
- iPvs (auth_alloc_strong N E a ∅ with "Hφ") as {γ} "[_ ?]"; [done..|].
+ iIntros (??) "Hφ".
+ iPvs (auth_alloc_strong N E a ∅ with "Hφ") as (γ) "[_ ?]"; [done..|].
by iExists γ.
Qed.
@@ -100,16 +100,16 @@ Section auth.
■(a ~l~> b @ Some af) ★ ▷ φ (b ⋅ af) ★ (auth_own γ b -★ Ψ x)))
⊢ fsa E Ψ.
Proof.
- iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
- iInv N as {a'} "[Hγ Hφ]".
+ iIntros (??) "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
+ iInv N as (a') "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (own_valid _ with "#Hγ") as "Hvalid".
iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
- iDestruct "Ha'" as {af} "Ha'"; iDestruct "Ha'" as %Ha'.
+ iDestruct "Ha'" as (af) "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. }
- iIntros {v}; iDestruct 1 as {b} "(% & Hφ & HΨ)".
+ iIntros (v); iDestruct 1 as (b) "(% & Hφ & HΨ)".
iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto.
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext. iExists (b â‹… af). by iFrame.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index d46352a15..fd1037149 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -94,10 +94,10 @@ Lemma box_insert f P Q :
▷ box N f P ={N}=> ∃ γ, f !! γ = None ★
slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P).
Proof.
- iDestruct 1 as {Φ} "[#HeqP Hf]".
+ iDestruct 1 as (Φ) "[#HeqP Hf]".
iPvs (own_alloc_strong (â— Excl' false â‹… â—¯ Excl' false,
Some (to_agree (Next (iProp_unfold Q)))) _ (dom _ f))
- as {γ} "[Hdom Hγ]"; first done.
+ as (γ) "[Hdom Hγ]"; first done.
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
iDestruct "Hdom" as % ?%not_elem_of_dom.
iPvs (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
@@ -114,9 +114,9 @@ Lemma box_delete f P Q γ :
slice N γ Q ★ ▷ box N f P ={N}=> ∃ P',
▷ ▷ (P ≡ (Q ★ P')) ★ ▷ box N (delete γ f) P'.
Proof.
- iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
+ iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists ([★ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
- iInv N as {b} "(Hγ & #HγQ &_)"; iPvsIntro; iNext.
+ iInv N as (b) "(Hγ & #HγQ &_)"; iPvsIntro; iNext.
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[Hγ' #[HγΦ ?]] ?]"; first done.
iDestruct (box_own_agree γ Q (Φ γ) with "[#]") as "HeqQ"; first by eauto.
@@ -132,8 +132,8 @@ Lemma box_fill f γ P Q :
f !! γ = Some false →
slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=> ▷ box N (<[γ:=true]> f) P.
Proof.
- iIntros {?} "(#Hinv & HQ & H)"; iDestruct "H" as {Φ} "[#HeqP Hf]".
- iInv N as {b'} "(Hγ & #HγQ & _)"; iTimeless "Hγ".
+ iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]".
+ iInv N as (b') "(Hγ & #HγQ & _)"; iTimeless "Hγ".
iDestruct (big_sepM_later _ f with "Hf") as "Hf".
iDestruct (big_sepM_delete _ f _ false with "Hf")
as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
@@ -150,8 +150,8 @@ Lemma box_empty f P Q γ :
f !! γ = Some true →
slice N γ Q ★ ▷ box N f P ={N}=> ▷ Q ★ ▷ box N (<[γ:=false]> f) P.
Proof.
- iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
- iInv N as {b} "(Hγ & #HγQ & HQ)"; iTimeless "Hγ".
+ iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
+ iInv N as (b) "(Hγ & #HγQ & HQ)"; iTimeless "Hγ".
iDestruct (big_sepM_later _ f with "Hf") as "Hf".
iDestruct (big_sepM_delete _ f with "Hf")
as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
@@ -169,14 +169,14 @@ Qed.
Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=> box N (const true <$> f) P.
Proof.
- iIntros "[H HP]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
+ iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
rewrite eq_iff later_iff big_sepM_later; iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
rewrite big_sepM_fmap; iApply (pvs_big_sepM _ _ f).
iApply (big_sepM_impl _ _ f); iFrame "Hf".
- iAlways; iIntros {γ b' ?} "[(Hγ' & #$ & #$) HΦ]".
- iInv N as {b} "[Hγ _]"; iTimeless "Hγ".
+ iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
+ iInv N as (b) "[Hγ _]"; iTimeless "Hγ".
iPvs (box_own_auth_update _ γ with "[Hγ Hγ']")
as "[Hγ $]"; first by iFrame.
iPvsIntro; iNext; iExists true. by iFrame.
@@ -186,13 +186,13 @@ Lemma box_empty_all f P Q :
map_Forall (λ _, (true =)) f →
box N f P ={N}=> ▷ P ★ box N (const false <$> f) P.
Proof.
- iDestruct 1 as {Φ} "[#HeqP Hf]".
+ iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★
box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "|==>[Hf]" as "[HΦ ?]".
{ iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
- iAlways; iIntros {γ b ?} "(Hγ' & #$ & #$)".
+ iAlways; iIntros (γ b ?) "(Hγ' & #$ & #$)".
assert (true = b) as <- by eauto.
- iInv N as {b} "(Hγ & _ & HΦ)"; iTimeless "Hγ".
+ iInv N as (b) "(Hγ & _ & HΦ)"; iTimeless "Hγ".
iDestruct (box_own_auth_agree γ b true with "[#]")
as "%"; subst; first by iFrame.
iPvs (box_own_auth_update _ γ true true false with "[Hγ Hγ']")
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 1324aff0c..48a49739d 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -25,9 +25,9 @@ Lemma wp_lift_head_step E1 E2 Φ e1 :
={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef)
⊢ WP e1 @ E1 {{ Φ }}.
Proof.
- iIntros {??} "H". iApply (wp_lift_step E1 E2); try done.
- iPvs "H" as {σ1} "(%&Hσ1&Hwp)". set_solver. iPvsIntro. iExists σ1.
- iSplit; first by eauto. iFrame. iNext. iIntros {e2 σ2 ef} "[% ?]".
+ iIntros (??) "H". iApply (wp_lift_step E1 E2); try done.
+ iPvs "H" as (σ1) "(%&Hσ1&Hwp)". set_solver. iPvsIntro. iExists σ1.
+ iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 ef) "[% ?]".
iApply "Hwp". by eauto.
Qed.
@@ -38,8 +38,8 @@ Lemma wp_lift_pure_head_step E Φ e1 :
(▷ ∀ e2 ef σ, ■head_step e1 σ e2 σ ef → WP e2 @ E {{ Φ }} ★ wp_fork ef)
⊢ WP e1 @ E {{ Φ }}.
Proof.
- iIntros {???} "H". iApply wp_lift_pure_step; eauto. iNext.
- iIntros {????}. iApply "H". eauto.
+ iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
+ iIntros (????). iApply "H". eauto.
Qed.
Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
@@ -49,8 +49,8 @@ Lemma wp_lift_atomic_head_step {E Φ} e1 σ1 :
■head_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
⊢ WP e1 @ E {{ Φ }}.
Proof.
- iIntros {??} "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
- iIntros {???} "[% ?]". iApply "H". eauto.
+ iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
+ iIntros (???) "[% ?]". iApply "H". eauto.
Qed.
Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index ef46d9880..942394275 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -53,7 +53,7 @@ Global Instance ht_mono' E :
Proof. solve_proper. Qed.
Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
-Proof. iIntros {Hwp} "! HP". by iApply Hwp. Qed.
+Proof. iIntros (Hwp) "! HP". by iApply Hwp. Qed.
Lemma ht_val E v : {{ True : iProp Λ Σ }} of_val v @ E {{ v', v = v' }}.
Proof. iIntros "! _". by iApply wp_value'. Qed.
@@ -64,7 +64,7 @@ Lemma ht_vs E P P' Φ Φ' e :
Proof.
iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs ("Hvs" with "HP") as "HP".
iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
- iIntros {v} "Hv". by iApply "HΦ".
+ iIntros (v) "Hv". by iApply "HΦ".
Qed.
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
@@ -72,10 +72,10 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e :
(P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
⊢ {{ P }} e @ E1 {{ Φ }}.
Proof.
- iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
+ iIntros (??) "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
iPvs ("Hvs" with "HP") as "HP"; first set_solver. iPvsIntro.
iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
- iIntros {v} "Hv". by iApply "HΦ".
+ iIntros (v) "Hv". by iApply "HΦ".
Qed.
Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
@@ -84,13 +84,13 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
Proof.
iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
- iIntros {v} "Hv". by iApply "HwpK".
+ iIntros (v) "Hv". by iApply "HwpK".
Qed.
Lemma ht_mask_weaken E1 E2 P Φ e :
E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊢ {{ P }} e @ E2 {{ Φ }}.
Proof.
- iIntros {?} "#Hwp ! HP". iApply (wp_mask_frame_mono E1 E2); try done.
+ iIntros (?) "#Hwp ! HP". iApply (wp_mask_frame_mono E1 E2); try done.
by iApply "Hwp".
Qed.
@@ -107,7 +107,7 @@ Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
(R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }}
⊢ {{ R1 ★ P }} e @ E ∪ E1 {{ λ v, R3 ★ Φ v }}.
Proof.
- iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
+ iIntros (???) "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
iApply (wp_frame_step_l E E1 E2); try done.
iSplitL "HR"; [|by iApply "Hwp"].
iPvs ("Hvs1" with "HR"); first by set_solver.
@@ -119,7 +119,7 @@ Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
(R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }}
⊢ {{ P ★ R1 }} e @ (E ∪ E1) {{ λ v, Φ v ★ R3 }}.
Proof.
- iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
+ iIntros (???) "[#Hvs1 [#Hvs2 #Hwp]]".
setoid_rewrite (comm _ _ R3); rewrite (comm _ _ R1).
iApply (ht_frame_step_l _ _ E2); by repeat iSplit.
Qed.
@@ -128,7 +128,7 @@ Lemma ht_frame_step_l' E P R e Φ :
to_val e = None →
{{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ v, R ★ Φ v }}.
Proof.
- iIntros {?} "#Hwp ! [HR HP]".
+ iIntros (?) "#Hwp ! [HR HP]".
iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Qed.
@@ -136,7 +136,7 @@ Lemma ht_frame_step_r' E P Φ R e :
to_val e = None →
{{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ v, Φ v ★ R }}.
Proof.
- iIntros {?} "#Hwp ! [HP HR]".
+ iIntros (?) "#Hwp ! [HP HR]".
iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Qed.
@@ -145,6 +145,6 @@ 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 {??} "[#? #Hwp] ! HP". iInv N as "HR". iApply "Hwp". by iSplitL "HR".
+ iIntros (??) "[#? #Hwp] ! HP". iInv N as "HR". iApply "Hwp". by iSplitL "HR".
Qed.
End hoare.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 5148d1726..25623bb11 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -27,11 +27,11 @@ Lemma ht_lift_step E1 E2 P Pσ1 Φ1 Φ2 Ψ e1 :
(∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }})
⊢ {{ P }} e1 @ E1 {{ Ψ }}.
Proof.
- iIntros {??} "#(#Hvs&HΦ&He2&Hef) ! HP".
+ iIntros (??) "#(#Hvs&HΦ&He2&Hef) ! HP".
iApply (wp_lift_step E1 E2 _ e1); auto.
- iPvs ("Hvs" with "HP") as {σ1} "(%&Hσ&HP)"; first set_solver.
+ iPvs ("Hvs" with "HP") as (σ1) "(%&Hσ&HP)"; first set_solver.
iPvsIntro. iExists σ1. repeat iSplit. by eauto. iFrame.
- iNext. iIntros {e2 σ2 ef} "[#Hstep Hown]".
+ iNext. iIntros (e2 σ2 ef) "[#Hstep Hown]".
iSpecialize ("HΦ" $! σ1 e2 σ2 ef with "[-]"). by iFrame "Hstep HP Hown".
iPvs "HΦ" as "[H1 H2]"; first by set_solver. iPvsIntro. iSplitL "H1".
- by iApply "He2".
@@ -45,7 +45,7 @@ Lemma ht_lift_atomic_step E P e1 σ1 :
{{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2
★ ■prim_step e1 σ1 (of_val v) σ2 ef }}.
Proof.
- iIntros {? Hsafe} "#Hef".
+ iIntros (? Hsafe) "#Hef".
iApply (ht_lift_step E E _ (λ σ1', P ∧ σ1 = σ1')%I
(λ e2 σ2 ef, ownP σ2 ★ ■(is_Some (to_val e2) ∧ prim_step e1 σ1 e2 σ2 ef))%I
(λ e2 σ2 ef, ■prim_step e1 σ1 e2 σ2 ef ★ P)%I);
@@ -53,9 +53,9 @@ Proof.
repeat iSplit.
- iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro.
iSplit. by eauto using atomic_step. iFrame. by auto.
- - iIntros {? e2 σ2 ef} "! (%&Hown&HP&%)". iPvsIntro. subst.
+ - iIntros (? e2 σ2 ef) "! (%&Hown&HP&%)". iPvsIntro. subst.
iFrame. iSplit; iPureIntro; auto. split; eauto using atomic_step.
- - iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
+ - iIntros (e2 σ2 ef) "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
iApply wp_value'. iExists σ2, ef. by iSplit.
- done.
Qed.
@@ -68,8 +68,8 @@ Lemma ht_lift_pure_step E P P' Ψ e1 :
(∀ e2 ef σ, {{ ■prim_step e1 σ e2 σ ef ★ P' }} ef ?@ ⊤ {{ _, True }})
⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
- iIntros {? Hsafe Hpure} "[#He2 #Hef] ! HP". iApply wp_lift_pure_step; auto.
- iNext; iIntros {e2 ef σ Hstep}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
+ iIntros (? Hsafe Hpure) "[#He2 #Hef] ! HP". iApply wp_lift_pure_step; auto.
+ iNext; iIntros (e2 ef σ Hstep). iDestruct "HP" as "[HP HP']"; iSplitL "HP".
- iApply "He2"; by iSplit.
- destruct ef as [e|]; last done. iApply ("Hef" $! _ (Some e)); by iSplit.
Qed.
@@ -81,9 +81,9 @@ Lemma ht_lift_pure_det_step E P P' Ψ e1 e2 ef :
{{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ _, True }}
⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
- iIntros {? Hsafe Hpuredet} "[#He2 #Hef]".
+ iIntros (? Hsafe Hpuredet) "[#He2 #Hef]".
iApply ht_lift_pure_step; eauto. by intros; eapply Hpuredet.
- iSplit; iIntros {e2' ef' σ}.
+ iSplit; iIntros (e2' ef' σ).
- iIntros "! [% ?]". edestruct Hpuredet as (_&->&->). done. by iApply "He2".
- destruct ef' as [e'|]; last done.
iIntros "! [% ?]". edestruct Hpuredet as (_&->&->). done. by iApply "Hef".
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 3037ced25..0c48db809 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -42,7 +42,7 @@ Lemma inv_open E N P :
inv N P ⊢ ∃ E', ■(E ∖ nclose N ⊆ E' ⊆ E) ★
|={E,E'}=> ▷ P ★ (▷ P ={E',E}=★ True).
Proof.
- rewrite inv_eq /inv. iDestruct 1 as {i} "[% #Hi]".
+ rewrite inv_eq /inv. iDestruct 1 as (i) "[% #Hi]".
iExists (E ∖ {[ i ]}). iSplit. { iPureIntro. set_solver. }
iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|].
iPvsIntro. iSplitL "HP"; first done. iIntros "HP".
@@ -56,13 +56,13 @@ Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ
fsaV → nclose N ⊆ E →
inv N P ★ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) ⊢ fsa E Ψ.
Proof.
- iIntros {??} "[Hinv HΨ]".
- iDestruct (inv_open E N P with "Hinv") as {E'} "[% Hvs]"; first done.
+ iIntros (??) "[Hinv HΨ]".
+ iDestruct (inv_open E N P with "Hinv") as (E') "[% Hvs]"; first done.
iApply (fsa_open_close E E'); auto; first set_solver.
iPvs "Hvs" as "[HP Hvs]"; first set_solver.
(* TODO: How do I do sth. like [iSpecialize "HΨ HP"]? *)
iPvsIntro. iApply (fsa_mask_weaken _ (E ∖ N)); first set_solver.
iApply fsa_wand_r. iSplitR "Hvs"; first by iApply "HΨ"; simpl.
- iIntros {v} "[HP HΨ]". by iPvs ("Hvs" with "HP"); first set_solver.
+ iIntros (v) "[HP HΨ]". by iPvs ("Hvs" with "HP"); first set_solver.
Qed.
End inv.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index afc1be2dc..0de2b8be7 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -67,9 +67,9 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
■prim_step e1 σ1 (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef)
⊢ WP e1 @ E {{ Φ }}.
Proof.
- iIntros {??} "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val.
+ iIntros (??) "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val.
iPvsIntro. iExists σ1. repeat iSplit; eauto 10 using atomic_step.
- iFrame. iNext. iIntros {e2 σ2 ef} "[% Hσ2]".
+ iFrame. iNext. iIntros (e2 σ2 ef) "[% Hσ2]".
edestruct @atomic_step as [v2 Hv%of_to_val]; eauto. subst e2.
iDestruct ("Hwp" $! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto.
iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val.
@@ -82,8 +82,8 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
▷ ownP σ1 ★ ▷ (ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
Proof.
- iIntros {?? Hdet} "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
- iFrame. iNext. iIntros {v2' σ2' ef'} "[% Hσ2']".
+ iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
+ iFrame. iNext. iIntros (v2' σ2' ef') "[% Hσ2']".
edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
Qed.
@@ -93,7 +93,7 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
▷ (WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
Proof.
- iIntros {?? Hpuredet} "?". iApply (wp_lift_pure_step E); try done.
- by intros; eapply Hpuredet. iNext. by iIntros {e' ef' σ (_&->&->)%Hpuredet}.
+ iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
+ by intros; eapply Hpuredet. iNext. by iIntros (e' ef' σ (_&->&->)%Hpuredet).
Qed.
End lifting.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index e6ebf515c..a8180d0e9 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -82,8 +82,8 @@ Section sts.
nclose N ⊆ E →
▷ φ s ={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
Proof.
- iIntros {?} "Hφ". rewrite /sts_ctx /sts_own.
- iPvs (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as {γ} "Hγ".
+ iIntros (?) "Hφ". rewrite /sts_ctx /sts_own.
+ iPvs (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
{ apply sts_auth_valid; set_solver. }
iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
iPvs (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
@@ -100,15 +100,15 @@ Section sts.
■sts.steps (s, T) (s', T') ★ ▷ φ s' ★ (sts_own γ s' T' -★ Ψ x)))
⊢ fsa E Ψ.
Proof.
- iIntros {??} "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
- iInv N as {s} "[Hγ Hφ]"; iTimeless "Hγ".
+ iIntros (??) "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
+ iInv N as (s) "[Hγ Hφ]"; iTimeless "Hγ".
iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid.
assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. }
- iIntros {a}; iDestruct 1 as {s' T'} "(% & Hφ & HΨ)".
+ iIntros (a); iDestruct 1 as (s' T') "(% & Hφ & HΨ)".
iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index c8a39cf0d..b131eed65 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -42,7 +42,7 @@ Proof. by apply pvs_timeless. Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
E2 ⊆ E1 ∪ E3 → (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
Proof.
- iIntros {?} "#[HvsP HvsQ] ! HP".
+ iIntros (?) "#[HvsP HvsQ] ! HP".
iPvs ("HvsP" with "HP") as "HQ"; first done. by iApply "HvsQ".
Qed.
@@ -63,7 +63,7 @@ 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.
Proof.
- iIntros {?} "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply "Hvs".
+ iIntros (?) "#Hvs ! HP". iApply pvs_mask_frame; auto. by iApply "Hvs".
Qed.
Lemma vs_mask_frame' E Ef P Q : Ef ⊥ E → (P ={E}=> Q) ⊢ P ={E ∪ Ef}=> Q.
@@ -72,7 +72,7 @@ Proof. intros; apply vs_mask_frame; set_solver. Qed.
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 {?} "#[? Hvs] ! HP". iInv N as "HR". iApply "Hvs". by iSplitL "HR".
+ iIntros (?) "#[? Hvs] ! HP". iInv N as "HR". iApply "Hvs". by iSplitL "HR".
Qed.
Lemma vs_alloc N P : â–· P ={N}=> inv N P.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index bb080ac1b..9d563ad01 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -46,19 +46,19 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
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) "}"
+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) "}"
+ 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.
+ 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 _ _;
@@ -74,16 +74,16 @@ Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
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) "}"
+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) "}"
+ 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.
+ let H := iFresh in iInvCore> N as H; last iDestruct H as (x1 x2 x3 x4) pat.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 20de4de2e..e919ea13e 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -124,42 +124,42 @@ Tactic Notation "iPvs" open_constr(H) :=
iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1) "}"
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 } pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) "}" constr(pat) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 } pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as { x1 x2 x3 } pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+ iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 ) pat).
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" constr(pat) :=
+ iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+ iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iDestructHelp H as (fun H =>
- iPvsCore H; last iDestruct H as { x1 x2 x3 x4 } pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+ iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) "}" constr(pat) :=
+ simple_intropattern(x5) ")" constr(pat) :=
iDestructHelp H as (fun H =>
- iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 } pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+ iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
+ simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
iDestructHelp H as (fun H =>
- iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 } pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+ iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
+ simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
iDestructHelp H as (fun H =>
- iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 } pat).
-Tactic Notation "iPvs" open_constr(H) "as" "{" simple_intropattern(x1)
+ iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
- simple_intropattern(x8) "}" constr(pat) :=
+ simple_intropattern(x8) ")" constr(pat) :=
iDestructHelp H as (fun H =>
- iPvsCore H; last iDestruct H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+ iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Tactic Notation "iTimeless" constr(H) :=
match goal with
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 7e21c1739..8e6a504da 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -274,48 +274,48 @@ Tactic Notation "iRevert" constr(Hs) :=
end in
let Hs := words Hs in go Hs.
-Tactic Notation "iRevert" "{" ident(x1) "}" :=
+Tactic Notation "iRevert" "(" ident(x1) ")" :=
iForallRevert x1.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) "}" :=
- iForallRevert x2; iRevert { x1 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) "}" :=
- iForallRevert x3; iRevert { x1 x2 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" :=
- iForallRevert x4; iRevert { x1 x2 x3 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) "}" :=
- iForallRevert x5; iRevert { x1 x2 x3 x4 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) "}" :=
- iForallRevert x6; iRevert { x1 x2 x3 x4 x5 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) ident(x7) "}" :=
- iForallRevert x7; iRevert { x1 x2 x3 x4 x5 x6 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) ident(x7) ident(x8) "}" :=
- iForallRevert x8; iRevert { x1 x2 x3 x4 x5 x6 x7 }.
-
-Tactic Notation "iRevert" "{" ident(x1) "}" constr(Hs) :=
- iRevert Hs; iRevert { x1 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) "}" constr(Hs) :=
- iRevert Hs; iRevert { x1 x2 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) "}" constr(Hs) :=
- iRevert Hs; iRevert { x1 x2 x3 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}"
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ")" :=
+ iForallRevert x2; iRevert ( x1 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ")" :=
+ iForallRevert x3; iRevert ( x1 x2 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" :=
+ iForallRevert x4; iRevert ( x1 x2 x3 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ")" :=
+ iForallRevert x5; iRevert ( x1 x2 x3 x4 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ")" :=
+ iForallRevert x6; iRevert ( x1 x2 x3 x4 x5 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ident(x7) ")" :=
+ iForallRevert x7; iRevert ( x1 x2 x3 x4 x5 x6 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ident(x7) ident(x8) ")" :=
+ iForallRevert x8; iRevert ( x1 x2 x3 x4 x5 x6 x7 ).
+
+Tactic Notation "iRevert" "(" ident(x1) ")" constr(Hs) :=
+ iRevert Hs; iRevert ( x1 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ")" constr(Hs) :=
+ iRevert Hs; iRevert ( x1 x2 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs) :=
+ iRevert Hs; iRevert ( x1 x2 x3 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")"
constr(Hs) :=
- iRevert Hs; iRevert { x1 x2 x3 x4 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) "}" constr(Hs) :=
- iRevert Hs; iRevert { x1 x2 x3 x4 x5 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) "}" constr(Hs) :=
- iRevert Hs; iRevert { x1 x2 x3 x4 x5 x6 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) ident(x7) "}" constr(Hs) :=
- iRevert Hs; iRevert { x1 x2 x3 x4 x5 x6 x7 }.
-Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) ident(x7) ident(x8) "}" constr(Hs) :=
- iRevert Hs; iRevert { x1 x2 x3 x4 x5 x6 x7 x8 }.
+ iRevert Hs; iRevert ( x1 x2 x3 x4 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ")" constr(Hs) :=
+ iRevert Hs; iRevert ( x1 x2 x3 x4 x5 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ")" constr(Hs) :=
+ iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ident(x7) ")" constr(Hs) :=
+ iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 ).
+Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
+ iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 ).
(** * Disjunction *)
Tactic Notation "iLeft" :=
@@ -457,37 +457,37 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
end
in let pat := intro_pat.parse_one pat in go H pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) "}"
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
iExistDestruct H as x1 H; iDestructHyp H as @ pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) "}" constr(pat) :=
- iExistDestruct H as x1 H; iDestructHyp H as { x2 } pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
- iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 } pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" constr(pat) :=
+ iExistDestruct H as x1 H; iDestructHyp H as ( x2 ) pat.
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+ iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 ) pat.
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
- iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 } pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+ iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 ) pat.
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) "}" constr(pat) :=
- iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 } pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+ simple_intropattern(x5) ")" constr(pat) :=
+ iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 ) pat.
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
- iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 } pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+ simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+ iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 ) pat.
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
+ simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
- iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 } pat.
-Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
+ iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 ) pat.
+Local Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
- simple_intropattern(x8) "}" constr(pat) :=
- iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 x8 } pat.
+ simple_intropattern(x8) ")" constr(pat) :=
+ iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat.
(** * Always *)
Tactic Notation "iAlways":=
@@ -502,7 +502,7 @@ Tactic Notation "iNext":=
apply _ || fail "iNext:" P "does not contain laters"|].
(** * Introduction tactic *)
-Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
+Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
[ (* (∀ _, _) *) apply tac_forall_intro; intros x
| (* (?P → _) *) eapply tac_impl_intro_pure;
[let P := match goal with |- IntoPure ?P _ => P end in
@@ -542,13 +542,13 @@ Local Tactic Notation "iIntroForall" :=
lazymatch goal with
| |- ∀ _, ?P => fail
| |- ∀ _, _ => intro
- | |- _ ⊢ (∀ x : _, _) => iIntro {x}
+ | |- _ ⊢ (∀ x : _, _) => iIntro (x)
end.
Local Tactic Notation "iIntro" :=
lazymatch goal with
| |- _ → ?P => intro
- | |- _ ⊢ (_ -★ _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
- | |- _ ⊢ (_ → _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
+ | |- _ ⊢ (_ -★ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+ | |- _ ⊢ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
end.
Tactic Notation "iIntros" constr(pat) :=
@@ -571,7 +571,7 @@ Tactic Notation "iIntros" constr(pat) :=
| IName ?H :: ?pats => iIntro H; go pats
| IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
| IAnom :: ?pats => let H := iFresh in iIntro H; go pats
- | IAnomPure :: ?pats => iIntro {?}; go pats
+ | IAnomPure :: ?pats => iIntro (?); go pats
| IPersistent ?pat :: ?pats =>
let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
| ?pat :: ?pats =>
@@ -581,61 +581,61 @@ Tactic Notation "iIntros" constr(pat) :=
in let pats := intro_pat.parse pat in try iProof; go pats.
Tactic Notation "iIntros" := iIntros "**".
-Tactic Notation "iIntros" "{" simple_intropattern(x1) "}" :=
- try iProof; iIntro { x1 }.
-Tactic Notation "iIntros" "{" simple_intropattern(x1)
- simple_intropattern(x2) "}" :=
- iIntros { x1 }; iIntro { x2 }.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
- simple_intropattern(x3) "}" :=
- iIntros { x1 x2 }; iIntro { x3 }.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
- simple_intropattern(x3) simple_intropattern(x4) "}" :=
- iIntros { x1 x2 x3 }; iIntro { x4 }.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
- simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5) "}" :=
- iIntros { x1 x2 x3 x4 }; iIntro { x5 }.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
+ try iProof; iIntro ( x1 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" :=
+ iIntros ( x1 ); iIntro ( x2 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x3) ")" :=
+ iIntros ( x1 x2 ); iIntro ( x3 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x3) simple_intropattern(x4) ")" :=
+ iIntros ( x1 x2 x3 ); iIntro ( x4 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5) ")" :=
+ iIntros ( x1 x2 x3 x4 ); iIntro ( x5 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
- simple_intropattern(x6) "}" :=
- iIntros { x1 x2 x3 x4 x5 }; iIntro { x6 }.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x6) ")" :=
+ iIntros ( x1 x2 x3 x4 x5 ); iIntro ( x6 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
- simple_intropattern(x6) simple_intropattern(x7) "}" :=
- iIntros { x1 x2 x3 x4 x5 x6 }; iIntro { x7 }.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x6) simple_intropattern(x7) ")" :=
+ iIntros ( x1 x2 x3 x4 x5 x6 ); iIntro ( x7 ).
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
- simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8) "}" :=
- iIntros { x1 x2 x3 x4 x5 x6 x7 }; iIntro { x8 }.
-
-Tactic Notation "iIntros" "{" simple_intropattern(x1) "}" constr(p) :=
- iIntros { x1 }; iIntros p.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
- "}" constr(p) :=
- iIntros { x1 x2 }; iIntros p.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
- simple_intropattern(x3) "}" constr(p) :=
- iIntros { x1 x2 x3 }; iIntros p.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
- simple_intropattern(x3) simple_intropattern(x4) "}" constr(p) :=
- iIntros { x1 x2 x3 x4 }; iIntros p.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8) ")" :=
+ iIntros ( x1 x2 x3 x4 x5 x6 x7 ); iIntro ( x8 ).
+
+Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" constr(p) :=
+ iIntros ( x1 ); iIntros p.
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+ ")" constr(p) :=
+ iIntros ( x1 x2 ); iIntros p.
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x3) ")" constr(p) :=
+ iIntros ( x1 x2 x3 ); iIntros p.
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x3) simple_intropattern(x4) ")" constr(p) :=
+ iIntros ( x1 x2 x3 x4 ); iIntros p.
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
- "}" constr(p) :=
- iIntros { x1 x2 x3 x4 x5 }; iIntros p.
-Tactic Notation "iIntros" "{"simple_intropattern(x1) simple_intropattern(x2)
+ ")" constr(p) :=
+ iIntros ( x1 x2 x3 x4 x5 ); iIntros p.
+Tactic Notation "iIntros" "("simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
- simple_intropattern(x6) "}" constr(p) :=
- iIntros { x1 x2 x3 x4 x5 x6 }; iIntros p.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x6) ")" constr(p) :=
+ iIntros ( x1 x2 x3 x4 x5 x6 ); iIntros p.
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
- simple_intropattern(x6) simple_intropattern(x7) "}" constr(p) :=
- iIntros { x1 x2 x3 x4 x5 x6 x7 }; iIntros p.
-Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
+ simple_intropattern(x6) simple_intropattern(x7) ")" constr(p) :=
+ iIntros ( x1 x2 x3 x4 x5 x6 x7 ); iIntros p.
+Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
simple_intropattern(x6) simple_intropattern(x7) simple_intropattern(x8)
- "}" constr(p) :=
- iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }; iIntros p.
+ ")" constr(p) :=
+ iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p.
(** * Destruct tactic *)
Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
@@ -663,37 +663,37 @@ Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
iDestructHelp H as (fun H => iDestructHyp H as pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}"
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) "}" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}"
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 ) pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" constr(pat) :=
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 ) pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) "}" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+ simple_intropattern(x5) ")" constr(pat) :=
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+ simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}"
+ simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1)
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
- simple_intropattern(x8) "}" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat).
+ simple_intropattern(x8) ")" constr(pat) :=
+ iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
@@ -712,31 +712,31 @@ Local Ltac iLöbHelp IH tac_before tac_after :=
end.
Tactic Notation "iLöb" "as" constr (IH) := iLöbHelp IH idtac idtac.
-Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (IH) :=
- iLöbHelp IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (IH) :=
- iLöbHelp IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (IH) :=
- iLöbHelp IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" "as"
+Tactic Notation "iLöb" "(" ident(x1) ")" "as" constr (IH) :=
+ iLöbHelp IH ltac:(iRevert ( x1 )) ltac:(iIntros ( x1 )).
+Tactic Notation "iLöb" "(" ident(x1) ident(x2) ")" "as" constr (IH) :=
+ iLöbHelp IH ltac:(iRevert ( x1 x2 )) ltac:(iIntros ( x1 x2 )).
+Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ")" "as" constr (IH) :=
+ iLöbHelp IH ltac:(iRevert ( x1 x2 x3 )) ltac:(iIntros ( x1 x2 x3 )).
+Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" "as"
constr (IH):=
- iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) "}" "as" constr (IH) :=
- iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 })
- ltac:(iIntros { x1 x2 x3 x4 x5 }).
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) "}" "as" constr (IH) :=
- iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
- ltac:(iIntros { x1 x2 x3 x4 x5 x6 }).
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) ident(x7) "}" "as" constr (IH) :=
- iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
- ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 }).
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
- ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (IH) :=
- iLöbHelp IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
- ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
+ iLöbHelp IH ltac:(iRevert ( x1 x2 x3 x4 )) ltac:(iIntros ( x1 x2 x3 x4 )).
+Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ")" "as" constr (IH) :=
+ iLöbHelp IH ltac:(iRevert ( x1 x2 x3 x4 x5 ))
+ ltac:(iIntros ( x1 x2 x3 x4 x5 )).
+Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ")" "as" constr (IH) :=
+ iLöbHelp IH ltac:(iRevert ( x1 x2 x3 x4 x5 x6 ))
+ ltac:(iIntros ( x1 x2 x3 x4 x5 x6 )).
+Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ident(x7) ")" "as" constr (IH) :=
+ iLöbHelp IH ltac:(iRevert ( x1 x2 x3 x4 x5 x6 x7 ))
+ ltac:(iIntros ( x1 x2 x3 x4 x5 x6 x7 )).
+Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4)
+ ident(x5) ident(x6) ident(x7) ident(x8) ")" "as" constr (IH) :=
+ iLöbHelp IH ltac:(iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 ))
+ ltac:(iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 )).
(** * Assert *)
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 4d17d5a92..268d4a5fa 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -22,7 +22,7 @@ Section client.
Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ★ y_inv (q/2) l).
Proof.
- iDestruct 1 as {f} "[[Hl1 Hl2] #Hf]".
+ iDestruct 1 as (f) "[[Hl1 Hl2] #Hf]".
iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
Qed.
@@ -32,28 +32,28 @@ Section client.
Proof.
iIntros "[#Hh Hrecv]". wp_lam. wp_let.
wp_apply wait_spec; iFrame "Hrecv".
- iDestruct 1 as {f} "[Hy #Hf]".
+ iDestruct 1 as (f) "[Hy #Hf]".
wp_seq. wp_load.
- iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros {v} "_"].
+ iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros (v) "_"].
Qed.
Lemma client_safe : heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ _, True }}.
Proof.
- iIntros {?} "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
+ iIntros (?) "#Hh"; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec heapN N (y_inv 1 y)); first done.
- iFrame "Hh". iIntros {l} "[Hr Hs]". wp_let.
+ iFrame "Hh". iIntros (l) "[Hr Hs]". wp_let.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done.
iFrame "Hh". iSplitL "Hy Hs".
- (* The original thread, the sender. *)
wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
- iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
+ iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
- (* The two spawned threads, the waiters. *)
- iSplitL; [|by iIntros {_ _} "_ >"].
+ iSplitL; [|by iIntros (_ _) "_ >"].
iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). }
iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto.
- iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros {_ _} "_ >"]];
+ iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros (_ _) "_ >"]];
iApply worker_safe; by iSplit.
Qed.
End client.
@@ -65,7 +65,7 @@ Section ClosedProofs.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ v, True }}.
Proof.
iIntros "! Hσ".
- iPvs (heap_alloc (nroot .@ "Barrier") with "Hσ") as {h} "[#Hh _]"; first done.
+ iPvs (heap_alloc (nroot .@ "Barrier") with "Hσ") as (h) "[#Hh _]"; first done.
iApply (client_safe (nroot .@ "Barrier") (nroot .@ "Heap")); auto with ndisj.
Qed.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 61f357958..e3dce20dc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -26,7 +26,7 @@ Section LiftingTests.
Lemma heap_e_spec E N :
nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}.
Proof.
- iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
+ iIntros (HN) "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
Qed.
@@ -37,7 +37,7 @@ Section LiftingTests.
Lemma heap_e2_spec E N :
nclose N ⊆ E → heap_ctx N ⊢ WP heap_e2 @ E {{ v, v = #2 }}.
Proof.
- iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
+ iIntros (HN) "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
wp_alloc l. wp_let. wp_alloc l'. wp_let.
wp_load. wp_op. wp_store. wp_load. done.
Qed.
@@ -55,7 +55,7 @@ Section LiftingTests.
n1 < n2 →
Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
Proof.
- iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
+ iIntros (Hn) "HΦ". iLöb (n1 Hn) as "IH".
wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
- iApply ("IH" with "[%] HΦ"). omega.
- iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
@@ -82,7 +82,7 @@ Section ClosedProofs.
Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ v, v = #2 }}.
Proof.
iProof. iIntros "! Hσ".
- iPvs (heap_alloc nroot with "Hσ") as {h} "[? _]"; first by rewrite nclose_nroot.
+ iPvs (heap_alloc nroot with "Hσ") as (h) "[? _]"; first by rewrite nclose_nroot.
iApply heap_e_spec; last done; by rewrite nclose_nroot.
Qed.
End ClosedProofs.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 9373ad731..5ee371809 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -34,9 +34,9 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
Proof.
iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
- iDestruct 1 as {x} "[#Hγ Hx]".
+ iDestruct 1 as (x) "[#Hγ Hx]".
wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
- iIntros {v} "?"; iExists x; by iSplit.
+ iIntros (v) "?"; iExists x; by iSplit.
Qed.
Context (P : iProp) (Φ Φ1 Φ2 Ψ Ψ1 Ψ2 : X -n> iProp).
@@ -45,14 +45,14 @@ Context {Ψ_join : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}.
Lemma P_res_split γ : barrier_res γ Φ ⊢ barrier_res γ Φ1 ★ barrier_res γ Φ2.
Proof.
- iDestruct 1 as {x} "[#Hγ Hx]".
+ iDestruct 1 as (x) "[#Hγ Hx]".
iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit.
Qed.
Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_res γ Ψ.
Proof.
iIntros "[Hγ Hγ']";
- iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
+ iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']".
iAssert (▷ (x ≡ x'))%I as "Hxx" .
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI later_equivI /=.
@@ -72,16 +72,16 @@ Lemma client_spec_new (eM eW1 eW2 : expr []) (eM' eW1' eW2' : expr ("b" :b: []))
★ (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }})
⊢ WP client eM' eW1' eW2' {{ _, ∃ γ, barrier_res γ Ψ }}.
Proof.
- iIntros {HN -> -> ->} "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
- iPvs (own_alloc (Cinl (Excl ()))) as {γ} "Hγ". done.
+ iIntros (HN -> -> ->) "/= (#Hh&HP&#He&#He1&#He2)"; rewrite /client.
+ iPvs (own_alloc (Cinl (Excl ()))) as (γ) "Hγ". done.
wp_apply (newbarrier_spec heapN N (barrier_res γ Φ)); auto.
- iFrame "Hh". iIntros {l} "[Hr Hs]".
+ iFrame "Hh". iIntros (l) "[Hr Hs]".
set (workers_post (v : val) := (barrier_res γ Ψ1 ★ barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par _ _ (λ _, True)%I workers_post);
try iFrame "Hh"; first done.
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
- iIntros {v} "HP"; iDestruct "HP" as {x} "HP". wp_let.
+ iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iPvs (own_update _ _ (Cinr (to_agree _)) with "Hγ") as "Hx".
by apply cmra_update_exclusive.
iApply signal_spec; iFrame "Hs"; iSplit; last done.
@@ -94,6 +94,6 @@ Proof.
+ iApply worker_spec; auto.
+ iApply worker_spec; auto.
+ auto.
- - iIntros {_ v} "[_ H]"; iPoseProof (Q_res_join with "H"). auto.
+ - iIntros (_ v) "[_ H]"; iPoseProof (Q_res_join with "H"). auto.
Qed.
End proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 6cd421733..c77e38b03 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -46,12 +46,12 @@ Lemma wp_one_shot (Φ : val → iProp) :
Proof.
iIntros "[#? Hf] /=".
rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let.
- iPvs (own_alloc Pending) as {γ} "Hγ"; first done.
+ iPvs (own_alloc Pending) as (γ) "Hγ"; first done.
iPvs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN"; first done.
{ iNext. iLeft. by iSplitL "Hl". }
iPvsIntro. iApply "Hf"; iSplit.
- - iIntros {n} "!". wp_let.
- iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
+ - iIntros (n) "!". wp_let.
+ iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as (m) "[Hl Hγ]".
+ wp_cas_suc. iSplitL; [|by iLeft].
iPvs (own_update with "Hγ") as "Hγ".
{ by apply cmra_update_exclusive with (y:=Cinr (DecAgree n)). }
@@ -60,20 +60,20 @@ Proof.
- iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
iAssert (∃ v, l ↦ v ★ ((v = InjLV #0 ★ own γ Pending) ∨
∃ n : Z, v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv".
- { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
+ { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
+ iExists (InjLV #0). iFrame. eauto.
+ iExists (InjRV #m). iFrame. eauto. }
- iDestruct "Hv" as {v} "[Hl Hv]". wp_load; iPvsIntro.
+ iDestruct "Hv" as (v) "[Hl Hv]". wp_load; iPvsIntro.
iAssert (one_shot_inv γ l ★ (v = InjLV #0 ∨ ∃ n : Z,
v = InjRV #n ★ own γ (Cinr (DecAgree n))))%I with "[-]" as "[$ #Hv]".
- { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
+ { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
wp_let. iPvsIntro. iIntros "!". wp_seq.
- iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
+ iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_focus (! _)%E.
- iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
+ iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as (m') "[Hl Hγ]".
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
wp_load; iPvsIntro.
iCombine "Hγ" "Hγ'" as "Hγ".
@@ -90,9 +90,9 @@ Lemma hoare_one_shot (Φ : val → iProp) :
}}.
Proof.
iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.
- iIntros {f1 f2} "[#Hf1 #Hf2]"; iSplit.
- - iIntros {n} "! _". wp_proj. iApply "Hf1".
+ iIntros (f1 f2) "[#Hf1 #Hf2]"; iSplit.
+ - iIntros (n) "! _". wp_proj. iApply "Hf1".
- iIntros "! _". wp_proj.
- iApply wp_wand_l; iFrame "Hf2". by iIntros {v} "#? ! _".
+ iApply wp_wand_l; iFrame "Hf2". by iIntros (v) "#? ! _".
Qed.
End proof.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e0694d4b2..7ac9b8956 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -20,12 +20,12 @@ Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat → uPred M) :
▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (n = n ↔ P3 n))) -★
▷ (x = 0) ∨ ∃ x z, ▷ P3 (x + z) ★ uPred_ownM b ★ uPred_ownM (core b)).
Proof.
- iIntros {i [|j] a b ?} "! [Ha Hb] H1 #H2 H3"; setoid_subst.
+ iIntros (i [|j] a b ?) "! [Ha Hb] H1 #H2 H3"; setoid_subst.
{ iLeft. by iNext. }
iRight.
- iDestruct "H1" as {z1 z2 c} "(H1&_&#Hc)".
+ iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
iPoseProof "Hc" as "foo".
- iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha".
+ iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
iAssert (uPred_ownM (a â‹… core a)) with "[Ha]" as "[Ha #Hac]".
{ by rewrite cmra_core_r. }
iIntros "{$Hac $Ha}".
@@ -61,7 +61,7 @@ Definition foo {M} (P : uPred M) := (P → P)%I.
Definition bar {M} : uPred M := (∀ P, foo P)%I.
Lemma demo_4 (M : ucmraT) : True ⊢ @bar M.
-Proof. iIntros. iIntros {P} "HP". done. Qed.
+Proof. iIntros. iIntros (P) "HP". done. Qed.
Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
(∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
@@ -76,7 +76,7 @@ Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
True ⊢ ∀ x y z : nat,
x = plus 0 x → y = 0 → z = 0 → P → □ Q → foo (x ≡ x).
Proof.
- iIntros {a} "*".
+ iIntros (a) "*".
iIntros "#Hfoo **".
by iIntros "# _".
Qed.
@@ -90,7 +90,7 @@ Section iris.
E1 ⊆ E2 → E ⊆ E1 →
(|={E1,E}=> ▷ P) ={E2,E ∪ E2 ∖ E1}=> ▷ P.
Proof.
- iIntros {? ?} "Hpvs".
+ iIntros (? ?) "Hpvs".
iPvs "Hpvs"; first set_solver.
done.
Qed.
@@ -99,7 +99,7 @@ Section iris.
nclose N ⊆ E →
(True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q ={E}=★ R.
Proof.
- iIntros {?} "H HP HQ".
+ iIntros (?) "H HP HQ".
iApply ("H" with "[#] HP |==>[HQ] |==>").
- done.
- by iApply inv_alloc.
--
GitLab