Commit 5b224d9c by Robbert Krebbers

### More uniform treatment of arguments of iApply, iPoseProof,

iSpecialize and iDestruct.

These tactics now all take an iTrm, which is a tuple consisting of
a.) a lemma or name of a hypotheses b.) arguments to instantiate
c.) a specialization pattern.
parent 5c1f62d7
 ... @@ -82,12 +82,12 @@ Lemma ress_split i i1 i2 Q R1 R2 P I : ... @@ -82,12 +82,12 @@ Lemma ress_split i i1 i2 Q R1 R2 P I : ⊢ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))). ⊢ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))). Proof. 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) "HΨ" as "[#HΨi HΨ]"; first done. iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done. iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ". iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ". - iPoseProof (saved_prop_agree i Q (Ψ i)) "#" 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Ψ" "HP". iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP"). iDestruct (big_sepS_delete _ _ i) "HPΨ" as "[HΨ HPΨ]"; first done. iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done. iDestruct "HQR" "HΨ" as "[HR1 HR2]". iDestruct ("HQR" with "HΨ") as "[HR1 HR2]". rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2". rewrite !big_sepS_insert''; [|set_solver ..]. by iFrame "HR1 HR2". - rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit. - rewrite !big_sepS_insert'; [|set_solver ..]. by repeat iSplit. Qed. Qed. ... @@ -102,8 +102,8 @@ Proof. ... @@ -102,8 +102,8 @@ Proof. rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl". rewrite /newbarrier. wp_seq. iApply wp_pvs. wp_alloc l as "Hl". iApply "HΦ". 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 {[ γ ]})) iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "-") "-" as {γ'} "[#? Hγ']"; eauto. as {γ'} "[#? Hγ']"; eauto. { iNext. rewrite /barrier_inv /=. iFrame "Hl". { iNext. rewrite /barrier_inv /=. iFrame "Hl". iExists (const P). rewrite !big_sepS_singleton /=. iExists (const P). rewrite !big_sepS_singleton /=. iSplit; [|done]. by iIntros "> ?". } iSplit; [|done]. by iIntros "> ?". } ... @@ -113,7 +113,7 @@ Proof. ... @@ -113,7 +113,7 @@ Proof. ★ 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. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. + set_solver. + set_solver. + iApply sts_own_weaken "Hγ'"; + iApply (sts_own_weaken with "Hγ'"); auto using sts.closed_op, i_states_closed, low_states_closed; auto using sts.closed_op, i_states_closed, low_states_closed; set_solver. } set_solver. } iPvsIntro. rewrite /recv /send. iSplitL "Hr". iPvsIntro. rewrite /recv /send. iSplitL "Hr". ... @@ -132,7 +132,7 @@ Proof. ... @@ -132,7 +132,7 @@ Proof. iSplit; [iPureIntro; by eauto using signal_step|]. iSplit; [iPureIntro; by eauto using signal_step|]. iSplitR "HΦ"; [iNext|by iIntros "?"]. iSplitR "HΦ"; [iNext|by iIntros "?"]. rewrite {2}/barrier_inv /ress /=; iFrame "Hl". rewrite {2}/barrier_inv /ress /=; iFrame "Hl". iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp". iDestruct "Hr" as {Ψ} "[Hr Hsp]"; iExists Ψ; iFrame "Hsp". iIntros "> _"; by iApply "Hr". iIntros "> _"; by iApply "Hr". Qed. Qed. ... @@ -149,20 +149,20 @@ Proof. ... @@ -149,20 +149,20 @@ Proof. { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". } { iNext. rewrite {2}/barrier_inv /=. by iFrame "Hl". } iIntros "Hγ". iIntros "Hγ". iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]". iPvsAssert (sts_ownS γ (i_states i) {[Change i]})%I as "Hγ" with "[Hγ]". { iApply sts_own_weaken "Hγ"; eauto using i_states_closed. } { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. } wp_op=> ?; simplify_eq; wp_if. iApply "IH" "Hγ [HQR] HΦ". by iNext. wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). by iNext. - (* a High state: the comparison succeeds, and we perform a transition and - (* a High state: the comparison succeeds, and we perform a transition and return to the client *) return to the client *) iExists (State High (I ∖ {[ i ]})), (∅ : set token). iExists (State High (I ∖ {[ i ]})), (∅ : set token). iSplit; [iPureIntro; by eauto using wait_step|]. iSplit; [iPureIntro; by eauto using wait_step|]. iDestruct "Hr" as {Ψ} "[HΨ Hsp]". iDestruct "Hr" as {Ψ} "[HΨ Hsp]". iDestruct (big_sepS_delete _ _ i) "Hsp" as "[#HΨi Hsp]"; first done. iDestruct (big_sepS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done. iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]". iAssert (▷ Ψ i ★ ▷ Π★{set (I ∖ {[i]})} Ψ)%I as "[HΨ HΨ']" with "[HΨ]". { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". } { iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". } iSplitL "HΨ' Hl Hsp"; [iNext|]. iSplitL "HΨ' Hl Hsp"; [iNext|]. + rewrite {2}/barrier_inv /=; iFrame "Hl". + rewrite {2}/barrier_inv /=; iFrame "Hl". iExists Ψ; iFrame "Hsp". by iIntros "> _". iExists Ψ; iFrame "Hsp". by iIntros "> _". + iPoseProof (saved_prop_agree i Q (Ψ i)) "#" 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. iIntros "_". wp_op=> ?; simplify_eq/=; wp_if. iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq". iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq". Qed. Qed. ... @@ -188,7 +188,8 @@ Proof. ... @@ -188,7 +188,8 @@ Proof. ★ 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. { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed. + set_solver. + set_solver. + iApply sts_own_weaken "Hγ"; eauto using sts.closed_op, i_states_closed. + iApply (sts_own_weaken with "Hγ"); eauto using sts.closed_op, i_states_closed. set_solver. } set_solver. } iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx. iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx. + iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto. + iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto. ... @@ -205,8 +206,7 @@ Proof. ... @@ -205,8 +206,7 @@ Proof. iIntros "> HQ". by iApply "HP"; iApply "HP1". iIntros "> HQ". by iApply "HP"; iApply "HP1". Qed. Qed. Lemma recv_mono l P1 P2 : Lemma recv_mono l P1 P2 : P1 ⊢ P2 → recv l P1 ⊢ recv l P2. P1 ⊢ P2 → recv l P1 ⊢ recv l P2. Proof. Proof. intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken. intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken. Qed. Qed. ... ...
 ... @@ -56,7 +56,7 @@ Proof. ... @@ -56,7 +56,7 @@ Proof. iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock. iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock. wp_seq. iApply wp_pvs. wp_alloc l as "Hl". wp_seq. iApply wp_pvs. 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)) "-[HΦ]" as "#?"; first done. iPvs (inv_alloc N _ (lock_inv γ l R) with "-[HΦ]") as "#?"; first done. { iNext. iExists false. by iFrame "Hl HR". } { iNext. iExists false. by iFrame "Hl HR". } iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit. iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit. Qed. Qed. ... @@ -72,7 +72,7 @@ Proof. ... @@ -72,7 +72,7 @@ Proof. + wp_if. by iApply "IH". + wp_if. by iApply "IH". - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl". - wp_cas_suc. iDestruct "HR" as "[Hγ HR]". iSplitL "Hl". + iNext. iExists true. by iSplit. + iNext. iExists true. by iSplit. + wp_if. iPvsIntro. iApply "HΦ" "-[HR] HR". iExists N, γ. by repeat iSplit. + wp_if. iApply ("HΦ" with "-[HR] HR"). iExists N, γ. by repeat iSplit. Qed. Qed. Lemma release_spec R l (Φ : val → iProp) : Lemma release_spec R l (Φ : val → iProp) : ... @@ -83,6 +83,6 @@ Proof. ... @@ -83,6 +83,6 @@ Proof. iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b. iInv N as "Hinv". iDestruct "Hinv" as {b} "[Hl Hγ']"; destruct b. - wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ". - wp_store. iFrame "HΦ". iNext. iExists false. by iFrame "Hl HR Hγ". - wp_store. iDestruct "Hγ'" as "[Hγ' _]". - wp_store. iDestruct "Hγ'" as "[Hγ' _]". iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%". iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". Qed. Qed. End proof. End proof.
 ... @@ -32,7 +32,7 @@ Proof. ... @@ -32,7 +32,7 @@ Proof. iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _). iIntros {l} "Hl". wp_let. wp_proj. wp_focus (f2 _). iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let. iApply wp_wand_l; iFrame "Hf2"; iIntros {v} "H2". wp_let. wp_apply join_spec; iFrame "Hl". iIntros {w} "H1". wp_apply join_spec; iFrame "Hl". iIntros {w} "H1". iSpecialize "HΦ" "-"; first by iSplitL "H1". by wp_let. iSpecialize ("HΦ" with "* -"); first by iSplitL "H1". by wp_let. Qed. Qed. Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) : Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) : ... ...
 ... @@ -59,11 +59,11 @@ Proof. ... @@ -59,11 +59,11 @@ 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. 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 Ψ)) "[Hl]" as "#?"; first done. iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done. { iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. } { iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. } wp_apply wp_fork. iSplitR "Hf". wp_apply wp_fork. iSplitR "Hf". - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. iSplit; first done. - wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. iExists γ. iFrame "Hγ"; by iSplit. iSplit; first done. iExists γ. iFrame "Hγ"; by iSplit. - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv". - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv". iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]". iInv N as "Hinv"; first wp_done; iDestruct "Hinv" as {v'} "[Hl _]". wp_store. iSplit; [iNext|done]. wp_store. iSplit; [iNext|done]. ... @@ -78,13 +78,13 @@ Proof. ... @@ -78,13 +78,13 @@ Proof. iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]". iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]". wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst. - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|]. - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|]. wp_case. wp_seq. iApply "IH" "Hγ Hv". wp_case. wp_seq. iApply ("IH" with "Hγ Hv"). - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst. - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst. + iSplitL "Hl Hγ". + iSplitL "Hl Hγ". { iNext. iExists _; iFrame "Hl"; iRight. { iNext. iExists _; iFrame "Hl"; iRight. iExists _; iSplit; [done|by iRight]. } iExists _; iSplit; [done|by iRight]. } wp_case. wp_let. iPvsIntro. by iApply "Hv". wp_case. wp_let. iPvsIntro. by iApply "Hv". + iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%". + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[]. Qed. Qed. End proof. End proof. ... ...
 ... @@ -90,12 +90,6 @@ Tactic Notation "wp_apply" open_constr(lem) := ... @@ -90,12 +90,6 @@ Tactic Notation "wp_apply" open_constr(lem) := wp_bind K; iApply lem; try iNext) wp_bind K; iApply lem; try iNext) end. end. Tactic Notation "wp_apply" open_constr(lem) constr(Hs) := match goal with | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; iApply lem Hs; try iNext) end. Tactic Notation "wp_alloc" ident(l) "as" constr(H) := Tactic Notation "wp_alloc" ident(l) "as" constr(H) := match goal with match goal with | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => ... ...
 ... @@ -62,9 +62,9 @@ Lemma ht_vs E P P' Φ Φ' e : ... @@ -62,9 +62,9 @@ Lemma ht_vs E P P' Φ Φ' e : ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v) ((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v) ⊢ {{ P }} e @ E {{ Φ }}. ⊢ {{ P }} e @ E {{ Φ }}. Proof. Proof. iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs "Hvs" "HP" as "HP". iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs ("Hvs" with "HP") as "HP". iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|]. iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|]. iIntros {v} "Hv". by iApply "HΦ" "!". iIntros {v} "Hv". by iApply ("HΦ" with "!"). Qed. Qed. Lemma ht_atomic E1 E2 P P' Φ Φ' e : Lemma ht_atomic E1 E2 P P' Φ Φ' e : ... @@ -73,9 +73,9 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e : ... @@ -73,9 +73,9 @@ Lemma ht_atomic E1 E2 P P' Φ Φ' e : ⊢ {{ P }} e @ E1 {{ Φ }}. ⊢ {{ P }} e @ E1 {{ Φ }}. Proof. Proof. iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto. iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto. iPvs "Hvs" "HP" as "HP"; first set_solver. iPvsIntro. iPvs ("Hvs" with "HP") as "HP"; first set_solver. iPvsIntro. iApply wp_wand_r; iSplitL; [by iApply "Hwp"|]. iApply wp_wand_r; iSplitL; [by iApply "Hwp"|]. iIntros {v} "Hv". by iApply "HΦ" "!". iIntros {v} "Hv". by iApply ("HΦ" with "!"). Qed. Qed. Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e : Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e : ... @@ -84,7 +84,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e : ... @@ -84,7 +84,7 @@ Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e : Proof. Proof. iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind. iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind. iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|]. iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|]. iIntros {v} "Hv". by iApply "HwpK" "!". iIntros {v} "Hv". by iApply ("HwpK" with "!"). Qed. Qed. Lemma ht_mask_weaken E1 E2 P Φ e : Lemma ht_mask_weaken E1 E2 P Φ e : ... @@ -110,9 +110,8 @@ Proof. ... @@ -110,9 +110,8 @@ Proof. iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]". iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]". iApply (wp_frame_step_l E E1 E2); try done. iApply (wp_frame_step_l E E1 E2); try done. iSplitL "HR"; [|by iApply "Hwp"]. iSplitL "HR"; [|by iApply "Hwp"]. iPvs "Hvs1" "HR"; first by set_solver. iPvs ("Hvs1" with "HR"); first by set_solver. iPvsIntro. iNext. iPvsIntro. iNext. by iApply "Hvs2". by iPvs "Hvs2" "Hvs1"; first by set_solver. Qed. Qed. Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ : Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ : ... ...
 ... @@ -31,13 +31,13 @@ Lemma ht_lift_step E1 E2 ... @@ -31,13 +31,13 @@ Lemma ht_lift_step E1 E2 Proof. Proof. iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP". iIntros {?? Hsafe Hstep} "#(#Hvs&HΦ&He2&Hef) ! HP". iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto. iApply (wp_lift_step E1 E2 φ _ e1 σ1); auto. iPvs "Hvs" "HP" as "[Hσ HP]"; first set_solver. iPvs ("Hvs" with "HP") as "[Hσ HP]"; first set_solver. iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"]. iPvsIntro. iNext. iSplitL "Hσ"; [done|iIntros {e2 σ2 ef} "[#Hφ Hown]"]. iSpecialize "HΦ" {e2 σ2 ef} "! -". 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. iPvs "HΦ" as "[H1 H2]"; first by set_solver. iPvsIntro. iSplitL "H1". iPvsIntro. iSplitL "H1". - by iApply "He2" "!". - by iApply ("He2" with "!"). - destruct ef as [e|]; last done. by iApply "Hef" {_ _ (Some e)} "!". - destruct ef as [e|]; last done. by iApply ("Hef" \$! _ _ (Some e) with "!"). Qed. Qed. Lemma ht_lift_atomic_step Lemma ht_lift_atomic_step ... @@ -74,8 +74,9 @@ Proof. ... @@ -74,8 +74,9 @@ Proof. iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP". iIntros {? Hsafe Hstep} "[#He2 #Hef] ! HP". iApply (wp_lift_pure_step E φ _ e1); auto. iApply (wp_lift_pure_step E φ _ e1); auto. iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP". iNext; iIntros {e2 ef Hφ}. iDestruct "HP" as "[HP HP']"; iSplitL "HP". - iApply "He2" "!"; by iSplit. - iApply ("He2" with "!"); by iSplit. - destruct ef as [e|]; last done. iApply "Hef" {_ (Some e)} "!"; by iSplit. - destruct ef as [e|]; last done. iApply ("Hef" \$! _ (Some e) with "!"); by iSplit. Qed. Qed. Lemma ht_lift_pure_det_step Lemma ht_lift_pure_det_step ... @@ -91,6 +92,6 @@ Proof. ... @@ -91,6 +92,6 @@ Proof. iSplit; iIntros {e2' ef'}. iSplit; iIntros {e2' ef'}. - iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2". - iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2". - destruct ef' as [e'|]; last done. - destruct ef' as [e'|]; last done. iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "Hef" "!". iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply ("Hef" with "!"). Qed. Qed. End lifting. End lifting.
 ... @@ -65,7 +65,7 @@ Lemma vs_transitive E1 E2 E3 P Q R : ... @@ -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). E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R). Proof. Proof. iIntros {?} "#[HvsP HvsQ] ! HP". iIntros {?} "#[HvsP HvsQ] ! HP". iPvs "HvsP" "! HP" as "HQ"; first done. by iApply "HvsQ" "!". iPvs ("HvsP" with "! HP") as "HQ"; first done. by iApply ("HvsQ" with "!"). Qed. Qed. Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R). Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R). ... @@ -95,7 +95,7 @@ Lemma vs_inv N E P Q R : ... @@ -95,7 +95,7 @@ Lemma vs_inv N E P Q R : nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q). nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q). Proof. Proof. iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto. iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto. iIntros "HR". iApply "Hvs" "!". by iSplitL "HR". iIntros "HR". iApply ("Hvs" with "!"). by iSplitL "HR". Qed. Qed. Lemma vs_alloc N P : ▷ P ={N}=> inv N P. Lemma vs_alloc N P : ▷ P ={N}=> inv N P. ... ...
 From iris.algebra Require Export upred. From iris.algebra Require Export upred. From iris.algebra Require Import upred_big_op upred_tactics. From iris.algebra Require Import upred_big_op upred_tactics. From iris.proofmode Require Export environments. From iris.proofmode Require Export environments. From iris.prelude Require Import stringmap. From iris.prelude Require Import stringmap hlist. Import uPred. Import uPred. Local Notation "Γ !! j" := (env_lookup j Γ). Local Notation "Γ !! j" := (env_lookup j Γ). ... @@ -287,16 +287,6 @@ Lemma tac_clear_spatial Δ Δ' Q : ... @@ -287,16 +287,6 @@ Lemma tac_clear_spatial Δ Δ' Q : envs_clear_spatial Δ = Δ' → Δ' ⊢ Q → Δ ⊢ Q. envs_clear_spatial Δ = Δ' → Δ' ⊢ Q → Δ ⊢ Q. Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed. Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed. Lemma tac_duplicate Δ Δ' i p j P Q : envs_lookup i Δ = Some (p, P) → p = true → envs_simple_replace i true (Esnoc (Esnoc Enil i P) j P) Δ = Some Δ' → Δ' ⊢ Q → Δ ⊢ Q. Proof. intros ? -> ??. rewrite envs_simple_replace_sound //; simpl. by rewrite right_id idemp wand_elim_r. Qed. (** * False *) (** * False *) Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q. Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q. Proof. by rewrite -(False_elim Q). Qed. Proof. by rewrite -(False_elim Q). Qed. ... @@ -560,7 +550,7 @@ Proof. ... @@ -560,7 +550,7 @@ Proof. by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r. by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r. Qed. Qed. (** Whenever posing [lem : True ⊢ Q] as [H} we want it to appear as [H : Q] and (** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the [True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to [True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *) make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *) ... @@ -579,6 +569,18 @@ Proof. ... @@ -579,6 +569,18 @@ Proof. by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True. by rewrite right_id -(to_pose_proof P1 P2 R) // always_const wand_True. Qed. Qed. Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q : envs_lookup_delete i Δ = Some (p, P, Δ') → envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' → Δ'' ⊢ Q → Δ ⊢ Q. Proof. intros [? ->]%envs_lookup_delete_Some ? <-. destruct p. - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl. by rewrite right_id wand_elim_r. - rewrite envs_lookup_sound // envs_app_sound //; simpl. by rewrite right_id wand_elim_r. Qed. Lemma tac_apply Δ Δ' i p R P1 P2 : Lemma tac_apply Δ Δ' i p R P1 P2 : envs_lookup_delete i Δ = Some (p, R, Δ')%I → ToWand R P1 P2 → envs_lookup_delete i Δ = Some (p, R, Δ')%I → ToWand R P1 P2 → Δ' ⊢ P1 → Δ ⊢ P2. Δ' ⊢ P1 → Δ ⊢ P2. ... @@ -826,13 +828,26 @@ Qed. ... @@ -826,13 +828,26 @@ Qed. Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ (∀ a, Φ a). Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ (∀ a, Φ a). Proof. apply forall_intro. Qed. Proof. apply forall_intro. Qed. Lemma tac_forall_specialize {A} Δ Δ' i p (Φ : A → uPred M) Q a : Class ForallSpecialize {As} (xs : hlist As) envs_lookup i Δ = Some (p, ∀ a, Φ a)%I → (P : uPred M) (Φ : himpl As (uPred M)) := envs_simple_replace i p (Esnoc Enil i (Φ a)) Δ = Some Δ' → forall_specialize : P ⊢ happly Φ xs. Arguments forall_specialize {_} _ _ _ {_}. Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100. Proof. done. Qed. Global Instance forall_specialize_cons A As x xs Φ (Ψ : A → himpl As (uPred M)) : (∀ x, ForallSpecialize xs (Φ x) (Ψ x)) → ForallSpecialize (hcons x xs) (∀ x : A, Φ x) Ψ. Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed. Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs : envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ → envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' → Δ' ⊢ Q → Δ ⊢ Q. Δ' ⊢ Q → Δ ⊢ Q. Proof. Proof. intros. rewrite envs_simple_replace_sound //; simpl. intros. rewrite envs_simple_replace_sound //; simpl. destruct p. destruct p; by rewrite /= right_id (forall_elim a) wand_elim_r. - by rewrite right_id (forall_specialize _ P) wand_elim_r. - by rewrite right_id (forall_specialize _ P) wand_elim_r. Qed. Qed. Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) : Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) : ... ...
 ... @@ -118,89 +118,44 @@ Tactic Notation "iPvsCore" constr(H) := ... @@ -118,89 +118,44 @@ Tactic Notation "iPvsCore" constr(H) := end. end. Tactic Notation "iPvs" open_constr(H) := Tactic Notation "iPvs" open_constr(H) := iPoseProof H as (fun H => iPvsCore H; last iDestruct H as "?"). iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?"). Tactic Notation "iPvs" open_constr(H) "as" constr(pat) := Tactic Notation "iPvs" open_constr(H) "as" constr(pat) := iPoseProof H as (fun H => iPvsCore H; last iDestruct H as 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) := constr(pat) := iPoseProof H as (fun H => iPvsCore H; last iDestruct H