Commit 437b700f authored by Robbert Krebbers's avatar Robbert Krebbers

Support `iIntros "ipat" (x1 .. xn) "ipat".

This makes it easier to frame or introduce some modalities before introducing
universal quantifiers.
parent b0e11cff
...@@ -214,7 +214,7 @@ Proof. ...@@ -214,7 +214,7 @@ Proof.
iCombine "Hf" "HP" as "Hf". iCombine "Hf" "HP" as "Hf".
rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f). rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
iApply (@big_sepM_impl with "[$Hf]"). iApply (@big_sepM_impl with "[$Hf]").
iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]". iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
iInv N as (b) "[>Hγ _]" "Hclose". iInv N as (b) "[>Hγ _]" "Hclose".
iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame. iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iApply "Hclose". iNext; iExists true. by iFrame. iApply "Hclose". iNext; iExists true. by iFrame.
...@@ -230,7 +230,7 @@ Proof. ...@@ -230,7 +230,7 @@ Proof.
[ map] γ↦b f, box_own_auth γ ( Excl' false) box_own_prop γ (Φ γ) [ map] γ↦b f, box_own_auth γ ( Excl' false) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]". inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]"). { rewrite -big_opM_opM -fupd_big_sepM. iApply (@big_sepM_impl with "[$Hf]").
iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)". iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto. assert (true = b) as <- by eauto.
iInv N as (b) "[>Hγ HΦ]" "Hclose". iInv N as (b) "[>Hγ HΦ]" "Hclose".
iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame. iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
...@@ -252,11 +252,11 @@ Proof. ...@@ -252,11 +252,11 @@ Proof.
- iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done. - iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
iDestruct ("HQQ'" with "HQ") as "HQ'". iDestruct ("HQQ'" with "HQ") as "HQ'".
iMod (slice_insert_full with "HQ' Hb") as (γ') "(% & #Hs' & Hb)"; try done. iMod (slice_insert_full with "HQ' Hb") as (γ') "(% & #Hs' & Hb)"; try done.
iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iRewrite "Heq". iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'". iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done. - iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
iMod (slice_insert_empty with "Hb") as (γ') "(% & #Hs' & Hb)"; try done. iMod (slice_insert_empty with "Hb") as (γ') "(% & #Hs' & Hb)"; try done.
iExists γ', _. iFrame "∗#%". iIntros "!>". do 2 iNext. iRewrite "Heq". iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'". iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed. Qed.
...@@ -270,7 +270,7 @@ Proof. ...@@ -270,7 +270,7 @@ Proof.
- iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done. - iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
iMod (slice_insert_full with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)"; first done. iMod (slice_insert_full with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)"; first done.
iMod (slice_insert_full with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)"; first done. iMod (slice_insert_full with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)"; first done.
iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 true). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
...@@ -278,7 +278,7 @@ Proof. ...@@ -278,7 +278,7 @@ Proof.
- iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done. - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
iMod (slice_insert_empty with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)".
iMod (slice_insert_empty with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)".
iExists γ1, γ2. iFrame "%#". iModIntro. iSplit; last iSplit; try iPureIntro. iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. } { by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 false). } { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
...@@ -297,14 +297,14 @@ Proof. ...@@ -297,14 +297,14 @@ Proof.
{ by simplify_map_eq. } { by simplify_map_eq. }
iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox") iMod (slice_insert_full _ _ _ _ (Q1 Q2)%I with "[$HQ1 $HQ2] Hbox")
as (γ) "(% & #Hslice & Hbox)"; first done. as (γ) "(% & #Hslice & Hbox)"; first done.
iExists γ. iFrame "%#". iModIntro. iNext. iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
- iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done. - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done. iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
{ by simplify_map_eq. } { by simplify_map_eq. }
iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)". iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
iExists γ. iFrame "%#". iModIntro. iNext. iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto]. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc. iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
Qed. Qed.
......
...@@ -207,7 +207,7 @@ Qed. ...@@ -207,7 +207,7 @@ Qed.
Lemma wp_mono E e Φ Ψ : ( v, Φ v Ψ v) WP e @ E {{ Φ }} WP e @ E {{ Ψ }}. Lemma wp_mono E e Φ Ψ : ( v, Φ v Ψ v) WP e @ E {{ Φ }} WP e @ E {{ Ψ }}.
Proof. Proof.
iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto. iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto.
iFrame. iIntros (v) "?". by iApply HΦ. iIntros "{$H}" (v) "?". by iApply HΦ.
Qed. Qed.
Lemma wp_mask_mono E1 E2 e Φ : E1 E2 WP e @ E1 {{ Φ }} WP e @ E2 {{ Φ }}. Lemma wp_mask_mono E1 E2 e Φ : E1 E2 WP e @ E1 {{ Φ }} WP e @ E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono E1 E2); auto. iFrame; eauto. Qed. Proof. iIntros (?) "H"; iApply (wp_strong_mono E1 E2); auto. iFrame; eauto. Qed.
...@@ -253,7 +253,7 @@ Lemma wp_wand E e Φ Ψ : ...@@ -253,7 +253,7 @@ Lemma wp_wand E e Φ Ψ :
WP e @ E {{ Φ }} - ( v, Φ v - Ψ v) - WP e @ E {{ Ψ }}. WP e @ E {{ Φ }} - ( v, Φ v - Ψ v) - WP e @ E {{ Ψ }}.
Proof. Proof.
iIntros "Hwp H". iApply (wp_strong_mono E); auto. iIntros "Hwp H". iApply (wp_strong_mono E); auto.
iFrame "Hwp". iIntros (?) "?". by iApply "H". iIntros "{$Hwp}" (?) "?". by iApply "H".
Qed. Qed.
Lemma wp_wand_l E e Φ Ψ : Lemma wp_wand_l E e Φ Ψ :
( v, Φ v - Ψ v) WP e @ E {{ Φ }} WP e @ E {{ Ψ }}. ( v, Φ v - Ψ v) WP e @ E {{ Φ }} WP e @ E {{ Ψ }}.
......
...@@ -976,7 +976,7 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2) ...@@ -976,7 +976,7 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
")" constr(p) := ")" constr(p) :=
iIntros ( x1 x2 x3 x4 x5 ); iIntros p. iIntros ( x1 x2 x3 x4 x5 ); iIntros p.
Tactic Notation "iIntros" "("simple_intropattern(x1) simple_intropattern(x2) Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x3) simple_intropattern(x4) simple_intropattern(x5)
simple_intropattern(x6) ")" constr(p) := simple_intropattern(x6) ")" constr(p) :=
iIntros ( x1 x2 x3 x4 x5 x6 ); iIntros p. iIntros ( x1 x2 x3 x4 x5 x6 ); iIntros p.
...@@ -1012,6 +1012,112 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2) ...@@ -1012,6 +1012,112 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x12) ")" constr(p) := simple_intropattern(x12) ")" constr(p) :=
iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ); iIntros p. iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ); iIntros p.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1) ")" :=
iIntros p; iIntros ( x1 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) ")" :=
iIntros p; iIntros ( x1 x2 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" :=
iIntros p; iIntros ( x1 x2 x3 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 ).
Tactic Notation "iIntros" constr(p) "(" 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 p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10)
simple_intropattern(x11) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10)
simple_intropattern(x11) simple_intropattern(x12) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1) ")" constr(p2) :=
iIntros p; iIntros ( x1 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" 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(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10)
")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10)
simple_intropattern(x11) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10)
simple_intropattern(x11) simple_intropattern(x12) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ); iIntros p2.
(* Used for generalization in iInduction and iLöb *) (* Used for generalization in iInduction and iLöb *)
Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) := Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
let rec go Hs := let rec go Hs :=
......
...@@ -46,7 +46,7 @@ Section client. ...@@ -46,7 +46,7 @@ Section client.
- (* The original thread, the sender. *) - (* The original thread, the sender. *)
wp_store. iApply (signal_spec with "[-]"); last by iNext; auto. wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
iSplitR "Hy"; first by eauto. iSplitR "Hy"; first by eauto.
iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op. iExists _; iSplitL; [done|]. iIntros "!#" (n). wp_let. by wp_op.
- (* The two spawned threads, the waiters. *) - (* The two spawned threads, the waiters. *)
iDestruct (recv_weaken with "[] Hr") as "Hr". iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "Hy". by iApply (y_inv_split with "Hy"). } { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
......
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