Commit 97bd63aa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More sane/consistent syntax for modal specialization patterns.

parent 87a8a19c
...@@ -242,12 +242,10 @@ _specification patterns_ to express splitting of hypotheses: ...@@ -242,12 +242,10 @@ _specification patterns_ to express splitting of hypotheses:
consumed. Hypotheses may be prefixed with a `$`, which results in them being consumed. Hypotheses may be prefixed with a `$`, which results in them being
framed in the generated goal for the premise. framed in the generated goal for the premise.
- `[-H1 ... Hn]` : negated form of the above pattern. - `[-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
Please register or sign in to reply
is a modality, in which case the modality will be kept in the generated goal is a modality, in which case the modality will be kept in the generated goal
for the premise will be wrapped into the modality. for the premise will be wrapped into the modality.
- `>[-H1 ... Hn]` : negated form of the above pattern. - `[> -H1 ... Hn]` : negated form of the above pattern.
- `>` : shorthand for `>[-]` (typically used for the last premise of an applied
lemma).
- `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P` being - `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P` being
persistent. Using this pattern, all hypotheses are available in the goal for persistent. Using this pattern, all hypotheses are available in the goal for
`P`, as well the remaining goal. The pattern can optionally contain `P`, as well the remaining goal. The pattern can optionally contain
......
...@@ -225,7 +225,7 @@ Lemma box_empty E f P : ...@@ -225,7 +225,7 @@ Lemma box_empty E f P :
Proof. Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]". iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert ([ map] γ↦b f, Φ γ box_own_auth γ ( Excl' false) 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 (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf". { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)". iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
assert (true = b) as <- by eauto. assert (true = b) as <- by eauto.
......
...@@ -93,7 +93,7 @@ Lemma newbarrier_spec (P : iProp Σ) : ...@@ -93,7 +93,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
Proof. Proof.
iIntros (Φ) "HΦ". iIntros (Φ) "HΦ".
rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl". rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
iApply ("HΦ" with ">[-]"). iApply ("HΦ" with "[> -]").
iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?". iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]") iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto. as (γ') "[#? Hγ']"; eauto.
...@@ -102,7 +102,7 @@ Proof. ...@@ -102,7 +102,7 @@ Proof.
iAssert (barrier_ctx γ' l P)%I as "#?". iAssert (barrier_ctx γ' l P)%I as "#?".
{ done. } { done. }
iAssert (sts_ownS γ' (i_states γ) {[Change γ]} 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. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- set_solver. - set_solver.
- iApply (sts_own_weaken with "Hγ'"); - iApply (sts_own_weaken with "Hγ'");
...@@ -140,7 +140,7 @@ Proof. ...@@ -140,7 +140,7 @@ Proof.
wp_load. destruct p. wp_load. destruct p.
- iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ". - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
{ iSplit; first done. rewrite /barrier_inv /=. by iFrame. } { iSplit; first done. rewrite /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. } { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
iModIntro. wp_if. iModIntro. wp_if.
iApply ("IH" with "Hγ [HQR] [HΦ]"); auto. iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
...@@ -175,7 +175,7 @@ Proof. ...@@ -175,7 +175,7 @@ Proof.
rewrite /barrier_inv /=. iNext. iFrame "Hl". rewrite /barrier_inv /=. iNext. iFrame "Hl".
by iApply (ress_split with "HQ Hi1 Hi2 HQR"). } by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
iAssert (sts_ownS γ (i_states i1) {[Change i1]} 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. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
- abstract set_solver. - abstract set_solver.
- iApply (sts_own_weaken with "Hγ"); - iApply (sts_own_weaken with "Hγ");
......
...@@ -129,7 +129,7 @@ Lemma wp_strong_mono E1 E2 e Φ Ψ : ...@@ -129,7 +129,7 @@ Lemma wp_strong_mono E1 E2 e Φ Ψ :
Proof. Proof.
iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre. iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
destruct (to_val e) as [v|] eqn:?. destruct (to_val e) as [v|] eqn:?.
{ iApply ("HΦ" with ">[-]"). by iApply (fupd_mask_mono E1 _). } { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done. iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
iMod ("H" with "[$]") as "[$ H]". iMod ("H" with "[$]") as "[$ H]".
iModIntro. iNext. iIntros (e2 σ2 efs Hstep). iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
......
...@@ -41,14 +41,13 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) ...@@ -41,14 +41,13 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
parse_go ts (SAutoFrame GPersistent :: k) parse_go ts (SAutoFrame GPersistent :: k)
| TBracketL :: TFrame :: TBracketR :: ts => | TBracketL :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GSpatial :: k) parse_go ts (SAutoFrame GSpatial :: k)
| TModal :: TBracketL :: TFrame :: TBracketR :: ts => | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GModal :: k) parse_go ts (SAutoFrame GModal :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k) | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k)
| TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k) | TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k)
| TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k | TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k
| TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
| TBracketL :: ts => parse_goal ts GSpatial false [] [] k | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
| TModal :: TBracketL :: ts => parse_goal ts GModal false [] [] k
| TModal :: ts => parse_go ts (SGoal (SpecGoal GModal true [] [] false) :: k)
| TForall :: ts => parse_go ts (SForall :: k) | TForall :: ts => parse_go ts (SForall :: k)
| _ => None | _ => None
end end
......
...@@ -96,7 +96,7 @@ Section iris. ...@@ -96,7 +96,7 @@ Section iris.
(True - P - inv N Q - True - R) - P - Q ={E}= R. (True - P - inv N Q - True - R) - P - Q ={E}= R.
Proof. Proof.
iIntros (?) "H HP HQ". iIntros (?) "H HP HQ".
iApply ("H" with "[% //] HP >[HQ] >[//]"). iApply ("H" with "[% //] [$] [> HQ] [> //]").
by iApply inv_alloc. by iApply inv_alloc.
Qed. Qed.
End iris. End iris.
...@@ -124,7 +124,7 @@ Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x. ...@@ -124,7 +124,7 @@ Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed. Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) - |==> P. Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) - |==> P.
Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed. Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
Lemma demo_14 (M : ucmraT) (P : uPred M) : False - P. Lemma demo_14 (M : ucmraT) (P : uPred M) : False - P.
Proof. iIntros "H". done. Qed. Proof. iIntros "H". done. Qed.
......
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