Commit 4d8c4ac8 authored by Robbert Krebbers's avatar Robbert Krebbers

More introduction patterns.

Also make those for introduction and elimination more symmetric:

  !%   pure introduction         %        pure elimination
  !#   always introduction       #        always elimination
  !>   later introduction        > pat    timeless later elimination
  !==> view shift introduction   ==> pat  view shift elimination
parent 1f589858
......@@ -93,14 +93,14 @@ Rewriting
Iris
----
- `iPvsIntro` : introduction of a primitive view shift. Generates a goal if
the masks are not syntactically equal.
- `iPvs pm_trm as (x1 ... xn) "ipat"` : runs a primitive view shift `pm_trm`.
- `iVsIntro` : introduction of a raw or primitive view shift.
- `iVs pm_trm as (x1 ... xn) "ipat"` : run a raw or primitive view shift
`pm_trm` (if the goal permits, i.e. it is a raw or primitive view shift, or
a weakest precondition).
- `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
- `iInv> N as (x1 ... xn) "ipat"` : open the invariant `N` and establish that
it is timeless so no laters have to be added.
- `iTimeless "H"` : strip a later of a timeless hypotheses `H` in case the
conclusion is a primitive view shifts or weakest precondition.
- `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal
permits, i.e. it is a later, True now, raw or primitive view shift, or a
weakest precondition).
Miscellaneous
-------------
......@@ -123,20 +123,24 @@ introduction patterns:
- `?` : create an anonymous hypothesis.
- `_` : remove the hypothesis.
- `$` : frame the hypothesis in the goal.
- `# ipat` : move the hypothesis to the persistent context.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `[ipat ipat]` : (separating) conjunction elimination.
- `[ipat|ipat]` : disjunction elimination.
- `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `# ipat` : move the hypothesis to the persistent context.
- `> ipat` : remove a later of a timeless hypothesis (if the goal permits).
- `==> ipat` : run a view shift (if the goal permits).
Apart from this, there are the following introduction patterns that can only
appear at the top level:
- `!` : introduce a box (provided that the spatial context is empty).
- `>` : introduce a later (which strips laters from all hypotheses).
- `{H1 ... Hn}` : clear `H1 ... Hn`.
- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
previous pattern, e.g., `{$H1 H2 $H3}`).
- `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an always modality (given that the spatial context is empty).
- `!>` : introduce a later (which strips laters from all hypotheses).
- `!==>` : introduce a view shift.
- `/=` : perform `simpl`.
- `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands.
......@@ -147,7 +151,7 @@ For example, given:
You can write
iIntros (x) "% ! $ [[] | #[HQ HR]] /= >".
iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
which results in:
......@@ -173,7 +177,7 @@ so called specification patterns to express this splitting:
- `[H1 ... Hn]` : generate a goal with the spatial hypotheses `H1 ... Hn` and
all persistent hypotheses. The hypotheses `H1 ... Hn` will be consumed.
- `[-H1 ... Hn]` : negated form of the above pattern
- `=>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is a primitive view shift, in which case the view shift will be kept in the
goal of the premise too.
- `[#]` : This pattern can be used when eliminating `P -★ Q` when either `P` or
......
......@@ -164,7 +164,7 @@ Section heap.
iVs (auth_open with "[Hh]") as (h) "[Hv [Hh Hclose]]"; eauto.
rewrite left_id /heap_inv. iDestruct "Hv" as %?.
iApply wp_alloc_pst. iFrame "Hh". iNext.
iIntros (l) "[% Hh]"; iVsIntro.
iIntros (l) "[% Hh] !==>".
iVs ("Hclose" $! {[ l := (1%Qp, DecAgree v) ]} with "[Hh]").
{ rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
iFrame "Hh". iPureIntro.
......@@ -183,7 +183,7 @@ Section heap.
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". iVsIntro. iVs ("Hclose" with "* [Hown]").
iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]").
{ iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
by iApply "HΦ".
Qed.
......@@ -199,7 +199,7 @@ Section heap.
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 "> Hl". iVsIntro.
iIntros "!> Hl !==>".
iVs ("Hclose" $! {[l := (1%Qp, DecAgree v)]} with "[Hl]").
{ iSplit.
- iPureIntro; by apply singleton_local_update, exclusive_local_update.
......@@ -218,7 +218,7 @@ Section heap.
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". iVsIntro. iVs ("Hclose" with "* [Hown]").
iIntros "!> Hown !==>". iVs ("Hclose" with "* [Hown]").
{ iSplit; first done. rewrite of_heap_singleton_op //. by iFrame. }
by iApply "HΦ".
Qed.
......@@ -234,7 +234,7 @@ Section heap.
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 "> Hl". iVsIntro.
iIntros "!> Hl !==>".
iVs ("Hclose" $! {[l := (1%Qp, DecAgree v2)]} with "[Hl]").
{ iSplit.
- iPureIntro; by apply singleton_local_update, exclusive_local_update.
......
......@@ -96,7 +96,7 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
Proof.
iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with "|==>[-]").
iApply ("HΦ" with "==>[-]").
iVs (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iVs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto.
......@@ -105,7 +105,7 @@ Proof.
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
sts_ownS γ' low_states {[Send]})%I with "|==>[-]" as "[Hr Hs]".
sts_ownS γ' low_states {[Send]})%I with "==>[-]" as "[Hr Hs]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- set_solver.
- iApply (sts_own_weaken with "Hγ'");
......@@ -128,7 +128,7 @@ Proof.
iSplit; [iPureIntro; by eauto using signal_step|].
iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
iIntros "> _"; by iApply "Hr".
iIntros "!> _"; by iApply "Hr".
Qed.
Lemma wait_spec l P (Φ : val iProp Σ) :
......@@ -142,7 +142,7 @@ Proof.
wp_load. destruct p.
- iVs ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
{ iSplit; first done. iNext. rewrite {2}/barrier_inv /=. by iFrame. }
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "|==>[Hγ]" as "Hγ".
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "==>[Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
iVsIntro. wp_op=> ?; simplify_eq; wp_if.
iApply ("IH" with "Hγ [HQR] HΦ"). auto.
......@@ -177,7 +177,7 @@ Proof.
iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto. }
iAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I with "|==>[-]" as "[Hγ1 Hγ2]".
sts_ownS γ (i_states i2) {[Change i2]})%I with "==>[-]" as "[Hγ1 Hγ2]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- abstract set_solver.
- iApply (sts_own_weaken with "Hγ");
......@@ -193,7 +193,7 @@ Proof.
rewrite /recv.
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".
iIntros "!> HQ". by iApply "HP"; iApply "HP1".
Qed.
Lemma recv_mono l P1 P2 : (P1 P2) recv l P1 recv l P2.
......
......@@ -20,9 +20,9 @@ Proof.
intros HN.
exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send 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.
......
......@@ -52,7 +52,7 @@ Proof.
wp_seq. wp_alloc l as "Hl".
iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros ">". iExists false. by iFrame. }
{ iIntros "!>". iExists false. by iFrame. }
iVsIntro. iApply "HΦ". iExists γ; eauto.
Qed.
......
......@@ -97,9 +97,8 @@ Section auth.
(a af) φ (a af) b,
(a ~l~> b @ Some af) φ (b af) ={EN,E}= auth_own γ b.
Proof.
iIntros (?) "(#? & Hγf)". rewrite /auth_ctx /auth_own.
iInv N as (a') "[Hγ Hφ]" "Hclose".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
iIntros (?) "(#? & >Hγf)". rewrite /auth_ctx /auth_own.
iInv N as (a') "[>Hγ Hφ]" "Hclose". iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (own_valid with "#Hγ") as % [[af Ha'] ?]%auth_valid_discrete.
simpl in Ha'; rewrite ->(left_id _ _) in Ha'; setoid_subst.
iVsIntro. iExists af; iFrame "Hφ"; iSplit; first done.
......
......@@ -76,7 +76,7 @@ Lemma box_own_agree γ Q1 Q2 :
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
iIntros "#HQ >". rewrite -{2}(iProp_fold_unfold Q1).
iIntros "#HQ !>". rewrite -{2}(iProp_fold_unfold Q1).
iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed.
......@@ -131,10 +131,10 @@ Lemma box_fill f γ P Q :
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 & _)" "Hclose". iTimeless "Hγ".
iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose".
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γ'".
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iVs (box_own_auth_update γ b' false true with "[Hγ Hγ']")
as "[Hγ Hγ']"; first by iFrame.
iVs ("Hclose" with "[Hγ HQ]"); first (iNext; iExists true; by iFrame).
......@@ -149,12 +149,12 @@ Lemma box_empty f P Q γ :
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)" "Hclose"; iTimeless "Hγ".
iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose".
iDestruct (big_sepM_later _ f with "Hf") as "Hf".
iDestruct (big_sepM_delete _ f with "Hf")
as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
iDestruct (box_own_auth_agree γ b true with "[#]")
as "%"; subst; first by iFrame.
as %?; subst; first by iFrame.
iFrame "HQ".
iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ Hγ']"; first by iFrame.
iVs ("Hclose" with "[Hγ]"); first (iNext; iExists false; by repeat iSplit).
......@@ -173,7 +173,7 @@ Proof.
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γ _]" "Hclose"; iTimeless "Hγ".
iInv N as (b) "[>Hγ _]" "Hclose".
iVs (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
iApply "Hclose". iNext; iExists true. by iFrame.
Qed.
......@@ -184,11 +184,11 @@ Lemma box_empty_all f P Q :
Proof.
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Φ ?]".
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γ' & #$ & #$)".
assert (true = b) as <- by eauto.
iInv N as (b) "(Hγ & _ & HΦ)" "Hclose"; iTimeless "Hγ".
iInv N as (b) "(>Hγ & _ & HΦ)" "Hclose".
iDestruct (box_own_auth_agree γ b true with "[#]")
as "%"; subst; first by iFrame.
iVs (box_own_auth_update γ true true false with "[Hγ Hγ']")
......
......@@ -21,7 +21,7 @@ Section savedprop.
Proof.
iIntros "#[H1 H2]".
iAssert P as "#HP".
{ iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). }
{ iApply "H2". iIntros "!# #HP". by iApply ("H1" with "[#]"). }
by iApply ("H1" with "[#]").
Qed.
......@@ -29,7 +29,7 @@ Section savedprop.
Definition A (i : sprop) : iProp := P, saved i P P.
Lemma saved_is_A i P `{!PersistentP P} : saved i P (A i P).
Proof.
iIntros "#HS !". iSplit.
iIntros "#HS !#". iSplit.
- iDestruct 1 as (Q) "[#HSQ HQ]".
iApply (sprop_agree i P Q with "[]"); eauto.
- iIntros "#HP". iExists P. by iSplit.
......@@ -39,7 +39,7 @@ Section savedprop.
implies that assertion with name [i] is equivalent to its own negation. *)
Definition Q i := saved i (¬ A i).
Lemma Q_self_contradiction i : Q i (A i ¬ A i).
Proof. iIntros "#HQ !". by iApply (saved_is_A i (¬A i)). Qed.
Proof. iIntros "#HQ !#". by iApply (saved_is_A i (¬A i)). Qed.
(* We can obtain such a [Q i]. *)
Lemma make_Q : True =r=> i, Q i.
......
......@@ -53,16 +53,16 @@ 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 }} of_val v @ E {{ v', v = v' }}.
Proof. iIntros "! _". by iApply wp_value'. Qed.
Proof. iIntros "!# _". by iApply wp_value'. Qed.
Lemma ht_vs E P P' Φ Φ' e :
(P ={E}= P') {{ P' }} e @ E {{ Φ' }} ( v, Φ' v ={E}= Φ v)
{{ P }} e @ E {{ Φ }}.
Proof.
iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iVs ("Hvs" with "HP") as "HP".
iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iVs ("Hvs" with "HP") as "HP".
iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
iIntros (v) "Hv". by iApply "HΦ".
Qed.
......@@ -72,7 +72,7 @@ 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.
iVs ("Hvs" with "HP") as "HP". iVsIntro.
iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
iIntros (v) "Hv". by iApply "HΦ".
......@@ -82,7 +82,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
{{ P }} e @ E {{ Φ }} ( v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
{{ P }} K e @ E {{ Φ' }}.
Proof.
iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
iIntros (v) "Hv". by iApply "HwpK".
Qed.
......@@ -90,24 +90,24 @@ Qed.
Lemma ht_mask_weaken E1 E2 P Φ e :
E1 E2 {{ P }} e @ E1 {{ Φ }} {{ P }} e @ E2 {{ Φ }}.
Proof.
iIntros (?) "#Hwp ! HP". iApply (wp_mask_mono E1 E2); try done.
iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono E1 E2); try done.
by iApply "Hwp".
Qed.
Lemma ht_frame_l E P Φ R e :
{{ P }} e @ E {{ Φ }} {{ R P }} e @ E {{ v, R Φ v }}.
Proof. iIntros "#Hwp ! [$ HP]". by iApply "Hwp". Qed.
Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
Lemma ht_frame_r E P Φ R e :
{{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ v, Φ v R }}.
Proof. iIntros "#Hwp ! [HP $]". by iApply "Hwp". Qed.
Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
Lemma ht_frame_step_l E1 E2 P R1 R2 e Φ :
to_val e = None E2 E1
(R1 ={E1,E2}= |={E2,E1}=> R2) {{ P }} e @ E2 {{ Φ }}
{{ R1 P }} e @ E1 {{ λ v, R2 Φ v }}.
Proof.
iIntros (??) "[#Hvs #Hwp] ! [HR HP]".
iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
iApply (wp_frame_step_l E1 E2); try done.
iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
Qed.
......@@ -117,7 +117,7 @@ Lemma ht_frame_step_r E1 E2 P R1 R2 e Φ :
(R1 ={E1,E2}= |={E2,E1}=> R2) {{ P }} e @ E2 {{ Φ }}
{{ P R1 }} e @ E1 {{ λ v, Φ v R2 }}.
Proof.
iIntros (??) "[#Hvs #Hwp] ! [HP HR]".
iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
iApply (wp_frame_step_r E1 E2); try done.
iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
Qed.
......@@ -126,7 +126,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.
......@@ -134,7 +134,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.
End hoare.
......@@ -51,13 +51,13 @@ Proof.
rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
iIntros "(Hw & [HE $] & $)"; iVsIntro; iRight.
iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
iIntros "HP [Hw $]"; iVsIntro; iRight. iApply ownI_close; by iFrame.
iIntros "HP [Hw $] !==>"; iRight. iApply ownI_close; by iFrame.
Qed.
Lemma inv_open_timeless E N P `{!TimelessP P} :
nclose N E inv N P ={E,EN}=> P (P ={EN,E}= True).
Proof.
iIntros (?) "Hinv". iVs (inv_open with "Hinv") as "[HP Hclose]"; auto.
iTimeless "HP"; iVsIntro; iIntros "{$HP} HP". iApply "Hclose"; auto.
iIntros (?) "Hinv". iVs (inv_open with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
Qed.
End inv.
......@@ -18,7 +18,7 @@ Lemma wp_lift_step E Φ e1 :
WP e1 @ E {{ Φ }}.
Proof.
iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & Hσf & H)". iTimeless "Hσf".
iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
iDestruct (ownP_agree σ1 σ1' with "[#]") as %<-; first by iFrame.
iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 ef Hstep).
iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
......
......@@ -43,9 +43,8 @@ Proof. apply ne_proper, _. Qed.
Lemma pvs_intro' E1 E2 P : E2 E1 ((|={E2,E1}=> True) - P) ={E1,E2}=> P.
Proof.
intros (E1''&->&?)%subseteq_disjoint_union_L.
rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE)".
iVsIntro. iApply now_True_intro. iApply "H".
iIntros "[$ $]". iVsIntro; iRight; eauto.
rewrite pvs_eq /pvs_def ownE_op //; iIntros "H ($ & $ & HE) !==>".
iApply now_True_intro. iApply "H". iIntros "[$ $] !==>". iRight; eauto.
Qed.
Lemma now_True_pvs E1 E2 P : (|={E1,E2}=> P) ={E1,E2}=> P.
Proof.
......
......@@ -97,7 +97,7 @@ Section sts.
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
iInv N as (s) "[Hγ Hφ]" "Hclose". iTimeless "Hγ".
iInv N as (s) "[>Hγ Hφ]" "Hclose".
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.
......
......@@ -124,7 +124,7 @@ Proof.
iVsIntro. iNext. iIntros (e2 σ2 ef Hstep).
destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
iVs ("H" $! _ σ2 ef with "[#]") as "($ & H & $)"; auto.
iVs (wp_value_inv with "H") as "H". iVs "H". by iApply wp_value'.
iVs (wp_value_inv with "H") as "==> H". by iApply wp_value'.
Qed.
Lemma wp_strong_mono E1 E2 e Φ Ψ :
......@@ -133,7 +133,7 @@ Proof.
iIntros (?) "[HΦ H]". iLöb (e) as "IH". rewrite !wp_unfold /wp_pre.
iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight].
{ iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
iApply (pvs_mask_mono E1 _); first done. by iApply ("HΦ" with "|==>[-]"). }
iApply (pvs_mask_mono E1 _); first done. by iApply ("HΦ" with "==>[-]"). }
iSplit; [done|]; iIntros (σ1) "Hσ".
iApply (pvs_trans _ E1); iApply pvs_intro'; auto. iIntros "Hclose".
iVs ("H" $! σ1 with "Hσ") as "[$ H]".
......
......@@ -3,14 +3,18 @@ From iris.prelude Require Export strings.
Inductive intro_pat :=
| IName : string intro_pat
| IAnom : intro_pat
| IAnomPure : intro_pat
| IDrop : intro_pat
| IFrame : intro_pat
| IPersistent : intro_pat intro_pat
| IList : list (list intro_pat) intro_pat
| IPureElim : intro_pat
| IAlwaysElim : intro_pat intro_pat
| ILaterElim : intro_pat intro_pat
| IVsElim : intro_pat intro_pat
| IPureIntro : intro_pat
| IAlwaysIntro : intro_pat
| ILaterIntro : intro_pat
| IVsIntro : intro_pat
| ISimpl : intro_pat
| IAlways : intro_pat
| INext : intro_pat
| IForall : intro_pat
| IAll : intro_pat
| IClear : list (bool * string) intro_pat. (* true = frame, false = clear *)
......@@ -19,23 +23,27 @@ Module intro_pat.
Inductive token :=
| TName : string token
| TAnom : token
| TAnomPure : token
| TDrop : token
| TFrame : token
| TPersistent : token
| TBar : token
| TBracketL : token
| TBracketR : token
| TAmp : token
| TParenL : token
| TParenR : token
| TPureElim : token
| TAlwaysElim : token
| TLaterElim : token
| TVsElim : token
| TPureIntro : token
| TAlwaysIntro : token
| TLaterIntro : token
| TVsIntro : token
| TSimpl : token
| TAlways : token
| TNext : token
| TClearL : token
| TClearR : token
| TForall : token
| TAll : token.
| TAll : token
| TClearL : token
| TClearR : token.
Fixpoint cons_name (kn : string) (k : list token) : list token :=
match kn with "" => k | _ => TName (string_rev kn) :: k end.
......@@ -44,18 +52,24 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| "" => rev (cons_name kn k)
| String " " s => tokenize_go s (cons_name kn k) ""
| String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
| String "%" s => tokenize_go s (TAnomPure :: cons_name kn k) ""
| String "_" s => tokenize_go s (TDrop :: cons_name kn k) ""
| String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
| String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
| String "|" s => tokenize_go s (TBar :: cons_name kn k) ""
| String "(" s => tokenize_go s (TParenL :: cons_name kn k) ""
| String ")" s => tokenize_go s (TParenR :: cons_name kn k) ""
| String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
| String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
| String ">" s => tokenize_go s (TNext :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPureElim :: cons_name kn k) ""
| String "#" s => tokenize_go s (TAlwaysElim :: cons_name kn k) ""
| String ">" s => tokenize_go s (TLaterElim :: cons_name kn k) ""
| String "=" (String "=" (String ">" s)) =>
tokenize_go s (TVsElim :: cons_name kn k) ""
| String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
| String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
| String "!" (String ">" s) => tokenize_go s (TLaterIntro :: cons_name kn k) ""
| String "!" (String "=" (String "=" (String ">" s))) =>
tokenize_go s (TVsIntro :: cons_name kn k) ""
| String "{" s => tokenize_go s (TClearL :: cons_name kn k) ""
| String "}" s => tokenize_go s (TClearR :: cons_name kn k) ""
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
......@@ -67,11 +81,13 @@ Definition tokenize (s : string) : list token := tokenize_go s [] "".
Inductive stack_item :=
| SPat : intro_pat stack_item
| SPersistent : stack_item
| SList : stack_item
| SConjList : stack_item
| SBar : stack_item
| SAmp : stack_item.
| SAmp : stack_item
| SAlwaysElim : stack_item
| SLaterElim : stack_item
| SVsElim : stack_item.
Notation stack := (list stack_item).
Fixpoint close_list (k : stack)
......@@ -79,8 +95,11 @@ Fixpoint close_list (k : stack)
match k with
| SList :: k => Some (SPat (IList (ps :: pss)) :: k)
| SPat pat :: k => close_list k (pat :: ps) pss
| SPersistent :: k =>
'(p,ps) maybe2 (::) ps; close_list k (IPersistent p :: ps) pss
| SAlwaysElim :: k =>
'(p,ps) maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
| SLaterElim :: k =>
'(p,ps) maybe2 (::) ps; close_list k (ILaterElim p :: ps) pss
| SVsElim :: k => '(p,ps) maybe2 (::) ps; close_list k (IVsElim p :: ps) pss
| SBar :: k => close_list k [] (ps :: pss)
| _ => None
end.
......@@ -102,7 +121,9 @@ Fixpoint close_conj_list (k : stack)
end;
Some (SPat (big_conj ps) :: k)
| SPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
| SPersistent :: k => p cur; close_conj_list k (Some (IPersistent p)) ps
| SAlwaysElim :: k => p cur; close_conj_list k (Some (IAlwaysElim p)) ps
| SLaterElim :: k => p cur; close_conj_list k (Some (ILaterElim p)) ps
| SVsElim :: k => p cur; close_conj_list k (Some (IVsElim p)) ps
| SAmp :: k => p cur; close_conj_list k None (p :: ps)
| _ => None
end.
......@@ -112,19 +133,23 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| [] => Some k
| TName s :: ts => parse_go ts (SPat (IName s) :: k)
| TAnom :: ts => parse_go ts (SPat IAnom :: k)
| TAnomPure :: ts => parse_go ts (SPat IAnomPure :: k)
| TDrop :: ts => parse_go ts (SPat IDrop :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k)
| TPersistent :: ts => parse_go ts (SPersistent :: k)
| TBracketL :: ts => parse_go ts (SList :: k)
| TBar :: ts => parse_go ts (SBar :: k)
| TBracketR :: ts => close_list k [] [] = parse_go ts
| TParenL :: ts => parse_go ts (SConjList :: k)
| TAmp :: ts => parse_go ts (SAmp :: k)
| TParenR :: ts => close_conj_list k None [] = parse_go ts
| TPureElim :: ts => parse_go ts (SPat IPureElim :: k)
| TAlwaysElim :: ts => parse_go ts (SAlwaysElim :: k)
| TLaterElim :: ts => parse_go ts (SLaterElim :: k)
| TVsElim :: ts => parse_go ts (SVsElim :: k)
| TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
| TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
| TLaterIntro :: ts => parse_go ts (SPat ILaterIntro :: k)
| TVsIntro :: ts => parse_go ts (SPat IVsIntro :: k)
| TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
| TAlways :: ts => parse_go ts (SPat IAlways :: k)
| TNext :: ts => parse_go ts (SPat INext :: k)
| TAll :: ts => parse_go ts (SPat IAll :: k)
| TForall :: ts => parse_go ts (SPat IForall :: k)
| TClearL :: ts => parse_clear ts [] k
......
......@@ -32,8 +32,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
| String "|" (String "=" (String "=" (String ">" s))) =>
tokenize_go s (TVs :: cons_name kn k) ""
| String "=" (String "=" (String ">" s)) => tokenize_go s (TVs :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn)
end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".
......
......@@ -483,20 +483,57 @@ Local Tactic Notation "iExistDestruct" constr(H)
[env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
|revert y; intros x].
(** * Always *)
Tactic Notation "iAlways":=
apply tac_always_intro;
[reflexivity || fail "iAlways: spatial context non-empty"|].
(** * Later *)
Tactic Notation "iNext":=
eapply tac_next;
[apply _
|let P := match goal with |- FromLater ?P _ => P end in
apply _ || fail "iNext:" P "does not contain laters"|].