Commit 99fd8e5b authored by Robbert Krebbers's avatar Robbert Krebbers

Make iPure and iPersistent internal to reduce the number of tactics.

These tactics are superfluous:
- iPure H as pat => iDestruct H as pat
- iPersistent H => iSpecialize H "!"
parent 0d68d6b6
Pipeline #572 passed with stage
......@@ -176,7 +176,7 @@ Proof.
iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
iPvs (saved_prop_alloc_strong _ (R1: %CF iProp) I) as {i1} "[% #Hi1]".
iPvs (saved_prop_alloc_strong _ (R2: %CF iProp) (I {[i1]}))
as {i2} "[Hi2' #Hi2]"; iPure "Hi2'" as Hi2; iPvsIntro.
as {i2} "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2; iPvsIntro.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iExists (State p ({[i1]} ({[i2]} (I {[i]})))).
iExists ({[Change i1 ]} {[ Change i2 ]}).
......
......@@ -57,8 +57,8 @@ Proof.
repeat iSplit.
- by iApply vs_reflexive.
- iIntros {e2 σ2 ef} "! (#Hφ&Hown&HP)"; iPvsIntro.
iSplitL "Hown". by iSplit. iSplit. by iPure "Hφ" as [_ ?]. done.
- iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iPure "Hφ" as [[v2 <-%of_to_val] ?].
iSplitL "Hown". by iSplit. iSplit. by iDestruct "Hφ" as %[_ ?]. done.
- iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?].
iApply wp_value'. iExists σ2, ef. by iSplit.
- done.
Qed.
......@@ -89,8 +89,8 @@ Proof.
iIntros {? Hsafe Hdet} "[#He2 #Hef]".
iApply (ht_lift_pure_step _ (λ e2' ef', e2 = e2' ef = ef')); eauto.
iSplit; iIntros {e2' ef'}.
- iIntros "! [#He ?]"; iPure "He" as [-> ->]. by iApply "He2".
- iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "He2".
- destruct ef' as [e'|]; last done.
iIntros "! [#He ?]"; iPure "He" as [-> ->]. by iApply "Hef" "!".
iIntros "! [#He ?]"; iDestruct "He" as %[-> ->]. by iApply "Hef" "!".
Qed.
End lifting.
......@@ -138,7 +138,7 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
end.
(** * Making hypotheses persistent or pure *)
Tactic Notation "iPersistent" constr(H) :=
Local Tactic Notation "iPersistent" constr(H) :=
eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
[env_cbv; reflexivity || fail "iPersistent:" H "not found"
|let Q := match goal with |- ToPersistentP ?Q _ => Q end in
......@@ -153,13 +153,12 @@ Tactic Notation "iDuplicate" constr(H1) "as" constr(H2) :=
Tactic Notation "iDuplicate" "#" constr(H1) "as" constr(H2) :=
iPersistent H1; iDuplicate H1 as H2.
Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
[env_cbv; reflexivity || fail "iPure:" H "not found"
|let P := match goal with |- ToPure ?P _ => P end in
apply _ || fail "iPure:" H ":" P "not pure"
|intros pat].
Tactic Notation "iPure" constr(H) := iPure H as ?.
Tactic Notation "iPureIntro" := apply uPred.const_intro.
......@@ -544,7 +543,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
let rec go Hz pat :=
lazymatch pat with
| IAnom => idtac
| IAnomPure => iPure Hz
| IAnomPure => iPure Hz as ?
| IDrop => iClear Hz
| IFrame => iFrame Hz
| IName ?y => iRename Hz into y
......
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