Commit 65bfa071 authored by Robbert Krebbers's avatar Robbert Krebbers

Make specialization patterns for persistent premises more uniform.

Changes:
- We no longer have a different syntax for specializing a term H : P -★ Q whose
  range P or domain Q is persistent. There is just one syntax, and the system
  automatically determines whether either P or Q is persistent.
- While specializing a term, always modalities are automatically stripped. This
  gets rid of the specialization pattern !.
- Make the syntax of specialization patterns more consistent. The syntax for
  generating a goal is [goal_spec] where goal_spec is one of the following:

    H1 .. Hn : generate a goal using hypotheses H1 .. Hn
   -H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn
           # : generate a goal for the premise in which all hypotheses can be
               used. This is only allowed when specializing H : P -★ Q where
               either P or Q is persistent.
           % : generate a goal for a pure premise.
parent 81c377c9
Pipeline #1126 passed with stage
......@@ -84,7 +84,7 @@ Proof.
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.
- iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
......@@ -102,7 +102,7 @@ Proof.
rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
iApply "HΦ".
iPvs (saved_prop_alloc (F:=idCF) _ P) as {γ} "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "-")
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as {γ'} "[#? Hγ']"; eauto.
{ iNext. rewrite /barrier_inv /=. iFrame "Hl".
iExists (const P). rewrite !big_sepS_singleton /=.
......@@ -110,7 +110,7 @@ Proof.
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "-".
sts_ownS γ' low_states {[Send]})%I as "[Hr Hs]" with "[-]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ iApply (sts_own_weaken with "Hγ'");
......@@ -162,7 +162,7 @@ Proof.
iSplitL "HΨ' Hl Hsp"; [iNext|].
+ rewrite {2}/barrier_inv /=; iFrame "Hl".
iExists Ψ; iFrame "Hsp". by iIntros "> _".
+ iPoseProof (saved_prop_agree i Q (Ψ i) with "#") as "Heq"; first by iSplit.
+ iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
Qed.
......@@ -185,7 +185,7 @@ Proof.
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
- iIntros "Hγ".
iPvsAssert (sts_ownS γ (i_states i1) {[Change i1]}
sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "-".
sts_ownS γ (i_states i2) {[Change i2]})%I as "[Hγ1 Hγ2]" with "[-]".
{ iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+ set_solver.
+ iApply (sts_own_weaken with "Hγ");
......
......@@ -57,7 +57,7 @@ Proof.
iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "-[HΦ]") as "#?"; first done.
iPvs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?"; first done.
{ iIntros ">". iExists false. by iFrame "Hl HR". }
iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
Qed.
......@@ -73,7 +73,7 @@ Proof.
+ wp_if. by iApply "IH".
- wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl".
+ iNext. iExists true. by iSplit.
+ wp_if. iApply ("HΦ" with "-[HR] HR"). iExists N, γ. by repeat iSplit.
+ wp_if. iApply ("HΦ" with "[-HR] HR"). iExists N, γ. by repeat iSplit.
Qed.
Lemma release_spec R l (Φ : val iProp) :
......
......@@ -32,7 +32,7 @@ Proof.
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.
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
Qed.
Lemma wp_par (Ψ1 Ψ2 : val iProp) (e1 e2 : expr []) (Φ : val iProp) :
......
......@@ -34,9 +34,8 @@ Proof.
ef = None e' = Lit (LitLoc l) σ' = <[l:=v]>σ σ !! l = None).
iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
[by intros; subst φ; inv_head_step; eauto 8|].
iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
(* FIXME: I should not have to refer to "H0". *)
destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
iFrame "HP". iNext. iIntros {v2 σ2 ef} "[Hφ HP]".
iDestruct "Hφ" as %(l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
iSplit; last done. iApply "HΦ"; by iSplit.
Qed.
......
......@@ -61,7 +61,7 @@ Section auth.
iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
iPvs (inv_alloc N _ (auth_inv γ φ) with "[-Hγ']"); first done.
{ iNext. iExists a. by iFrame "Hφ". }
iPvsIntro; iExists γ; by iFrame "Hγ'".
Qed.
......@@ -83,7 +83,7 @@ Section auth.
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 (own_valid _ with "#Hγ") as "Hvalid".
iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
......
......@@ -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Φ" with "!").
iIntros {v} "Hv". by iApply "HΦ".
Qed.
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
......@@ -75,7 +75,7 @@ Proof.
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Φ" with "!").
iIntros {v} "Hv". by iApply "HΦ".
Qed.
Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
......@@ -84,7 +84,7 @@ 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" with "!").
iIntros {v} "Hv". by iApply "HwpK".
Qed.
Lemma ht_mask_weaken E1 E2 P Φ e :
......
......@@ -33,11 +33,11 @@ Proof.
iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto.
iPvs ("Hvs" with "HP") as "[Hσ HP]"; first set_solver.
iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"].
iSpecialize ("HΦ" $! e2 σ2 ef with "! -"). by iFrame "Hφ HP Hown".
iSpecialize ("HΦ" $! e2 σ2 ef with "[-]"). by iFrame "Hφ HP Hown".
iPvs "HΦ" as "[H1 H2]"; first by set_solver.
iPvsIntro. iSplitL "H1".
- by iApply ("He2" with "!").
- destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e) with "!").
- by iApply "He2".
- destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e)).
Qed.
Lemma ht_lift_atomic_step
......@@ -74,9 +74,9 @@ Proof.
iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP".
iApply (wp_lift_pure_step E φ _ e1); auto.
iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP".
- iApply ("He2" with "!"); by iSplit.
- iApply "He2"; by iSplit.
- destruct ef as [e|]; last done.
iApply ("Hef" $! _ (Some e) with "!"); by iSplit.
iApply ("Hef" $! _ (Some e)); by iSplit.
Qed.
Lemma ht_lift_pure_det_step
......@@ -92,6 +92,6 @@ Proof.
iSplit; iIntros {e2' ef'}.
- iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2".
- destruct ef' as [e'|]; last done.
iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply ("Hef" with "!").
iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "Hef".
Qed.
End lifting.
......@@ -101,7 +101,7 @@ Section sts.
Proof.
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.
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γ".
......
......@@ -65,7 +65,7 @@ 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".
iPvs ("HvsP" with "! HP") as "HQ"; first done. by iApply ("HvsQ" with "!").
iPvs ("HvsP" with "HP") as "HQ"; first done. by iApply "HvsQ".
Qed.
Lemma vs_transitive' E P Q R : ((P ={E}=> Q) (Q ={E}=> R)) (P ={E}=> R).
......@@ -94,8 +94,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" with "!"). 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.
......
......@@ -294,9 +294,13 @@ Qed.
(** * Basic rules *)
Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : ?p P Q.
Arguments to_assumption _ _ _ {_}.
Global Instance to_assumption_exact p P : ToAssumption p P P.
Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
Global Instance to_assumption_always P Q :
Global Instance to_assumption_always_l p P Q :
ToAssumption p P Q ToAssumption p ( P) Q.
Proof. rewrite /ToAssumption=><-. by rewrite always_elim. Qed.
Global Instance to_assumption_always_r P Q :
ToAssumption true P Q ToAssumption true P ( Q).
Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.
......@@ -465,6 +469,8 @@ Global Instance to_wand_iff_l P Q : ToWand (P ↔ Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance to_wand_iff_r P Q : ToWand (P Q) Q P.
Proof. apply and_elim_r', impl_wand. Qed.
Global Instance to_wand_always R P Q : ToWand R P Q ToWand ( R) P Q.
+Proof. rewrite /ToWand=> ->. apply always_elim. Qed.
(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
but it is doing some work to keep the order of hypotheses preserved. *)
......@@ -508,32 +514,34 @@ Proof.
by rewrite always_if_elim assoc HP1 wand_elim_l wand_elim_r.
Qed.
Lemma tac_specialize_range_persistent Δ Δ' Δ'' j q P1 P2 R Q :
envs_lookup_delete j Δ = Some (q, R, Δ')%I
ToWand R P1 P2 PersistentP P1
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ''
Δ' P1 Δ'' Q Δ Q.
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R)
ToWand R P1 P2 ToPure P1 φ
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'
φ Δ' Q Δ Q.
Proof.
intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
rewrite envs_lookup_sound //.
rewrite -(idemp uPred_and (envs_delete _ _ _)).
rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
rewrite envs_simple_replace_sound' //; simpl.
rewrite right_id (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
by rewrite wand_elim_r.
intros. rewrite envs_simple_replace_sound //; simpl.
by rewrite right_id (to_wand R) (to_pure P1) const_equiv // wand_True wand_elim_r.
Qed.
Lemma tac_specialize_domain_persistent Δ Δ' Δ'' j q P1 P2 P2' R Q :
envs_lookup_delete j Δ = Some (q, R, Δ')%I
ToWand R P1 P2 ToPersistentP P2 P2'
envs_replace j q true (Esnoc Enil j P2') Δ = Some Δ''
Δ' P1 Δ'' Q Δ Q.
Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
envs_lookup_delete j Δ = Some (q, R, Δ')
ToWand R P1 P2
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ''
Δ' P1 (PersistentP P1 PersistentP P2)
Δ'' Q Δ Q.
Proof.
intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
rewrite envs_replace_sound //; simpl.
rewrite (sep_elim_r _ (_ - _)) right_id (to_wand R) always_if_elim.
by rewrite wand_elim_l (to_persistentP P2) always_and_sep_l' wand_elim_r.
intros [? ->]%envs_lookup_delete_Some ?? HP1 [?|?] <-.
- rewrite envs_lookup_sound //.
rewrite -(idemp uPred_and (envs_delete _ _ _)).
rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
rewrite envs_simple_replace_sound' //; simpl.
rewrite right_id (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
by rewrite wand_elim_r.
- rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
rewrite envs_simple_replace_sound //; simpl.
rewrite (sep_elim_r _ (_ - _)) right_id (to_wand R) always_if_elim.
by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
Qed.
Lemma tac_revert Δ Δ' i p P Q :
......@@ -553,22 +561,19 @@ Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q :
envs_split lr js Δ = Some (Δ1,Δ2)
envs_app (envs_persistent Δ1) (Esnoc Enil j P) Δ2 = Some Δ2'
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
Δ1 P Δ2' Q Δ Q.
Proof.
intros ?? HP ?. rewrite envs_split_sound //.
destruct (envs_persistent Δ1) eqn:?.
- rewrite (persistentP Δ1) HP envs_app_sound //; simpl.
by rewrite right_id wand_elim_r.
- rewrite HP envs_app_sound //; simpl. by rewrite right_id wand_elim_r.
intros ?? HP HQ. rewrite envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
by rewrite right_id HP HQ wand_elim_r.
Qed.
Lemma tac_assert_persistent Δ Δ' j P Q :
PersistentP P
envs_app true (Esnoc Enil j P) Δ = Some Δ'
Δ P Δ' Q Δ Q.
Δ P PersistentP P Δ' Q Δ Q.
Proof.
intros ?? HP ?.
intros ? HP ??.
rewrite -(idemp uPred_and Δ) {1}HP envs_app_sound //; simpl.
by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
Qed.
......
......@@ -26,7 +26,7 @@ Global Instance frame_pvs E1 E2 R P mQ :
Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> if mQ is Some Q then Q else True))%I.
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance to_wand_pvs E1 E2 R P Q :
ToWand R P Q ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q).
ToWand R P Q ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
......@@ -190,7 +190,7 @@ Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
let H := iFresh in
let Hs := spec_pat.parse_one Hs in
lazymatch Hs with
| SAssert ?lr ?Hs =>
| SGoal ?lr ?Hs =>
eapply tac_pvs_assert with _ _ _ _ _ _ lr Hs H Q _;
[let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
apply _ || fail "iPvsAssert: " P "not a pvs"
......
From iris.prelude Require Export strings.
Inductive spec_pat :=
| SAssert : bool list string spec_pat
| SPersistent : spec_pat
| SPure : spec_pat
| SAlways : spec_pat
| SName : string spec_pat
| SGoal : bool list string spec_pat
| SGoalPersistent : spec_pat
| SGoalPure : spec_pat
| SName : bool string spec_pat (* first arg = persistent *)
| SForall : spec_pat.
Module spec_pat.
......@@ -16,7 +15,6 @@ Inductive token :=
| TBracketR : token
| TPersistent : token
| TPure : token
| TAlways : token
| TForall : token.
Fixpoint cons_name (kn : string) (k : list token) : list token :=
......@@ -30,37 +28,39 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
| 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 (TAlways :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn)
end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".
Fixpoint parse_go (ts : list token) (g : option (bool * list string))
Inductive state :=
| StTop : state
| StAssert : bool list string state.
Fixpoint parse_go (ts : list token) (s : state)
(k : list spec_pat) : option (list spec_pat) :=
match g with
| None =>
match s with
| StTop =>
match ts with
| [] => Some (rev k)
| TName s :: ts => parse_go ts None (SName s :: k)
| TMinus :: TBracketL :: ts => parse_go ts (Some (true,[])) k
| TMinus :: ts => parse_go ts None (SAssert true [] :: k)
| TBracketL :: ts => parse_go ts (Some (false,[])) k
| TAlways :: ts => parse_go ts None (SAlways :: k)
| TPersistent :: ts => parse_go ts None (SPersistent :: k)
| TPure :: ts => parse_go ts None (SPure :: k)
| TForall :: ts => parse_go ts None (SForall :: k)
| TName s :: ts => parse_go ts StTop (SName false s :: k)
| TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
| TBracketL :: ts => parse_go ts (StAssert false []) k
| TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
| TForall :: ts => parse_go ts StTop (SForall :: k)
| _ => None
end
| Some (b, ss) =>
| StAssert neg ss =>
match ts with
| TName s :: ts => parse_go ts (Some (b,s :: ss)) k
| TBracketR :: ts => parse_go ts None (SAssert b (rev ss) :: k)
| TMinus :: ts => guard (¬neg ss = []); parse_go ts (StAssert true ss) k
| TName s :: ts => parse_go ts (StAssert neg (s :: ss)) k
| TBracketR :: ts => parse_go ts StTop (SGoal neg (rev ss) :: k)
| _ => None
end
end.
Definition parse (s : string) : option (list spec_pat) :=
parse_go (tokenize s) None [].
parse_go (tokenize s) StTop [].
Ltac parse s :=
lazymatch type of s with
......@@ -76,4 +76,4 @@ Ltac parse_one s :=
| Some [?pat] => pat | _ => fail "invalid spec_pat" s
end
end.
End spec_pat.
\ No newline at end of file
End spec_pat.
......@@ -129,7 +129,7 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
(ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 0).
Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
match xs with
| hnil => idtac
| _ =>
......@@ -139,7 +139,7 @@ Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
|env_cbv; reflexivity|]
end.
Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let solve_to_wand H1 :=
let P := match goal with |- ToWand ?P _ _ => P end in
apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
......@@ -147,25 +147,7 @@ Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
lazymatch pats with
| [] => idtac
| SForall :: ?pats => try (iSpecializeArgs H1 (hcons _ _)); go H1 pats
| SAlways :: ?pats => iPersistent H1; go H1 pats
| SAssert true [] :: SAlways :: ?pats =>
eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|let Q := match goal with |- ToPersistentP ?Q _ => Q end in
apply _ || fail "iSpecialize:" Q "not persistent"
|env_cbv; reflexivity
| |go H1 pats]
| SName ?H2 :: SAlways :: ?pats =>
eapply tac_specialize_domain_persistent with _ _ H1 _ _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|let Q := match goal with |- ToPersistentP ?Q _ => Q end in
apply _ || fail "iSpecialize:" Q "not persistent"
|env_cbv; reflexivity
|iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
|go H1 pats]
| SName ?H2 :: ?pats =>
| SName false ?H2 :: ?pats =>
eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
[env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
|env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
......@@ -173,26 +155,43 @@ Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let Q := match goal with |- ToWand ?P ?Q _ => Q end in
apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q
|env_cbv; reflexivity|go H1 pats]
| SPersistent :: ?pats =>
eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
| SName true ?H2 :: ?pats =>
eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|let Q := match goal with |- PersistentP ?Q => Q end in
apply _ || fail "iSpecialize:" Q "not persistent"
|env_cbv; reflexivity| |go H1 pats]
| SPure :: ?pats =>
eapply tac_specialize_range_persistent with _ _ H1 _ _ _ _;
(* make custom tac_ lemma *)
|env_cbv; reflexivity
|iExact H2 || fail "iSpecialize:" H2 "not found or wrong type"
|let Q1 := match goal with |- PersistentP ?Q1 _ => Q1 end in
let Q2 := match goal with |- _ PersistentP ?Q2 => Q2 end in
first [left; apply _ | right; apply _]
|| fail "iSpecialize:" Q1 "nor" Q2 "persistent"
|go H1 pats]
| SGoalPersistent :: ?pats =>
eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|env_cbv; reflexivity
|(*goal*)
|let Q1 := match goal with |- PersistentP ?Q1 _ => Q1 end in
let Q2 := match goal with |- _ PersistentP ?Q2 => Q2 end in
first [left; apply _ | right; apply _]
|| fail "iSpecialize:" Q1 "nor" Q2 "persistent"
|go H1 pats]
| SGoalPure :: ?pats =>
eapply tac_specialize_pure with _ H1 _ _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|let Q := match goal with |- PersistentP ?Q => Q end in
apply _ || fail "iSpecialize:" Q "not persistent"
|env_cbv; reflexivity|iPureIntro|go H1 pats]
| SAssert ?lr ?Hs :: ?pats =>
|let Q := match goal with |- ToPure ?Q _ => Q end in
apply _ || fail "iSpecialize:" Q "not pure"
|env_cbv; reflexivity
|(*goal*)
|go H1 pats]
| SGoal ?lr ?Hs :: ?pats =>
eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"|
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
|(*goal*)
|go H1 pats]
end in let pats := spec_pat.parse pat in go H pats.
......@@ -202,7 +201,7 @@ Tactic Notation "iSpecialize" open_constr(t) :=
end.
(** * Pose proof *)
Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
lazymatch type of H1 with
| string =>
eapply tac_pose_proof_hyp with _ _ H1 _ H2 _;
......@@ -704,12 +703,12 @@ Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=
let H := iFresh in
let Hs := spec_pat.parse Hs in
lazymatch Hs with
| [SAssert ?lr ?Hs] =>
| [SGoal ?lr ?Hs] =>
eapply tac_assert with _ _ _ lr Hs H Q; (* (js:=Hs) (j:=H) (P:=Q) *)
[env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity|
|iDestructHyp H as pat]
| [SAssert true [] :: SAlways] =>
| [SGoalPersistent] =>
eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
[apply _ || fail "iAssert:" Q "not persistent"
|env_cbv; reflexivity|
......
......@@ -45,7 +45,7 @@ Section LiftingTests.
Proof.
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 ("IH" with "[%] HΦ"). omega.
- iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
Qed.
......
......@@ -25,7 +25,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
Proof.
iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
wp_seq. iApply wp_wand_l. iSplitR; [|by iApply ("He" with "!")].
wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"].
iIntros {v} "?"; iExists x; by iSplit.
Qed.
......@@ -43,7 +43,7 @@ Lemma Q_res_join γ : (barrier_res γ Ψ1 ★ barrier_res γ Ψ2) ⊢ ▷ barrie
Proof.
iIntros "[Hγ Hγ']";
iDestruct "Hγ" as {x} "[#Hγ Hx]"; iDestruct "Hγ'" as {x'} "[#Hγ' Hx']".
iDestruct (one_shot_agree γ x x' with "- !") as "Hxx"; first (by iSplit).
iDestruct (one_shot_agree γ x x' with "[#]") as "Hxx"; first (by iSplit).
iNext. iRewrite -"Hxx" in "Hx'".
iExists x; iFrame "Hγ". iApply Ψ_join; by iSplitL "Hx".
Qed.
......@@ -68,8 +68,7 @@ Proof.
iPvs (one_shot_init _ _ x with "Hγ") as "Hx".
iApply signal_spec; iFrame "Hs"; iSplit; last done.
iExists x; by iSplitL "Hx".
- iDestruct (recv_weaken with "[] Hr") as "Hr".
{ iIntros "?". by iApply (P_res_split with "-"). }
- iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
iPvs (recv_split with "Hr") as "[H1 H2]"; first done.
wp_apply (wp_par _ _ (λ _, barrier_res γ Ψ1)%I
(λ _, barrier_res γ Ψ2)%I); first done.
......
......@@ -58,13 +58,13 @@ Proof.
+ wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
- iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
iAssert ( v, l v ((v = InjLV #0 own γ OneShotPending)
n : Z, v = InjRV #n own γ (Shot (DecAgree n))))%I as "Hv" with "-".
n : Z, v = InjRV #n own γ (Shot (DecAgree n))))%I as "Hv" with "[-]".
{ iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
+ iExists (InjLV #0). iFrame "Hl". iLeft; by iSplit.
+ iExists (InjRV #m). iFrame "Hl". iRight; iExists m; by iSplit. }
iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
iAssert (one_shot_inv γ l (v = InjLV #0 n : Z,
v = InjRV #n own γ (Shot (DecAgree n))))%I as "[$ #Hv]" with "-".
v = InjRV #n own γ (Shot (DecAgree n))))%I as "[$ #Hv]" with "[-]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". by iLeft.
+ iSplit. iRight; iExists m; by iSplitL "Hl". iRight; iExists m; by iSplit. }
......@@ -76,7 +76,7 @@ Proof.
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
wp_load.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "Hγ !") as % [=->]%dec_agree_op_inv.
iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
iSplitL "Hl"; [iRight; iExists m; by iSplit|].
wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=.
iSplit. done. by iNext.
......@@ -91,7 +91,7 @@ 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" with "!").
- iIntros {n} "! _". wp_proj. iApply "Hf1".
- iIntros "! _". wp_proj.
iApply wp_wand_l; iFrame "Hf2". by iIntros {v} "#? ! _".
Qed.
......
......@@ -31,7 +31,7 @@ Proof.
iFrame "Ha Hac".
iExists (S j + z1), z2.
iNext.
iApply ("H3" $! _ 0 with "H1 ! [] !").
iApply ("H3" $! _ 0 with "H1 []").
- iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
- done.
Qed.
......@@ -67,8 +67,8 @@ Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) :
( z, P z y) (P - (x,x) (y,</