Commit e965b669 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge iAssert and iPvsAssert.

To do so, we have introduced the specialization patterns:

  =>[H1 .. Hn] and =>[-H1 .. Hn]

That generate a goal in which the view shift is preserved. These specialization
patterns can also be used for e.g. iApply.

Note that this machinery is not tied to primitive view shifts, and works for
various kinds of goal (as captured by the ToAssert type class, which describes
how to transform the asserted goal based on the main goal).

TODO: change the name of these specialization patterns to reflect this
generality.
parent 555e1dad
...@@ -109,8 +109,8 @@ Proof. ...@@ -109,8 +109,8 @@ Proof.
iSplit; [|done]. by iIntros "> ?". } iSplit; [|done]. by iIntros "> ?". }
iAssert (barrier_ctx γ' l P)%I as "#?". iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. } { rewrite /barrier_ctx. by repeat iSplit. }
iPvsAssert (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γ'");
...@@ -148,7 +148,7 @@ Proof. ...@@ -148,7 +148,7 @@ Proof.
iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"]. iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
{ 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 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. }
wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "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
...@@ -184,8 +184,8 @@ Proof. ...@@ -184,8 +184,8 @@ Proof.
- iNext. rewrite {2}/barrier_inv /=. iFrame "Hl". - iNext. rewrite {2}/barrier_inv /=. iFrame "Hl".
iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit. iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame "Hr HQR". by repeat iSplit.
- iIntros "Hγ". - iIntros "Hγ".
iPvsAssert (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.
+ set_solver. + set_solver.
+ iApply (sts_own_weaken with "Hγ"); + iApply (sts_own_weaken with "Hγ");
......
...@@ -494,24 +494,28 @@ Proof. ...@@ -494,24 +494,28 @@ Proof.
by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r. by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
Qed. Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js P1 P2 R Q : Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
to_assert : (R (P - Q)) Q.
Global Arguments to_assert _ _ _ {_}.
Lemma to_assert_fallthrough P Q : ToAssert P Q P.
Proof. by rewrite /ToAssert wand_elim_r. Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ') envs_lookup_delete j Δ = Some (q, R, Δ')
ToWand R P1 P2 ToWand R P1 P2 ToAssert P1 Q P1'
('(Δ1,Δ2) envs_split lr js Δ'; ('(Δ1,Δ2) envs_split lr js Δ';
Δ2' envs_app (envs_persistent Δ1 && q) (Esnoc Enil j P2) Δ2; Δ2' envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *) Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *)
Δ1 P1 Δ2' Q Δ Q. Δ1 P1' Δ2' Q Δ Q.
Proof. Proof.
intros [? ->]%envs_lookup_delete_Some ?? HP1 <-. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=; destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
destruct (envs_app _ _ _) eqn:?; simplify_eq/=. destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
rewrite envs_lookup_sound // envs_split_sound //. rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl. rewrite (envs_app_sound Δ2) //; simpl.
destruct (envs_persistent Δ1) eqn:?; simplify_eq/=. rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
- rewrite right_id (to_wand R) (persistentP Δ1) HP1. rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
by rewrite assoc (always_elim_if q) -always_if_sep wand_elim_l wand_elim_r. by rewrite always_if_elim assoc !wand_elim_r.
- rewrite right_id (to_wand R).
by rewrite always_if_elim assoc HP1 wand_elim_l wand_elim_r.
Qed. Qed.
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q : Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
...@@ -559,14 +563,15 @@ Proof. ...@@ -559,14 +563,15 @@ Proof.
intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l. intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
Qed. Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q : Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
ToAssert P Q R
envs_split lr js Δ = Some (Δ1,Δ2) envs_split lr js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
Δ1 P Δ2' Q Δ Q. Δ1 R Δ2' Q Δ Q.
Proof. Proof.
intros ?? HP HQ. rewrite envs_split_sound //. intros ??? HP HQ. rewrite envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl. rewrite (envs_app_sound Δ2) //; simpl.
by rewrite right_id HP HQ wand_elim_r. by rewrite right_id HP HQ.
Qed. Qed.
Lemma tac_assert_persistent Δ Δ' j P Q : Lemma tac_assert_persistent Δ Δ' j P Q :
......
...@@ -31,7 +31,7 @@ Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed. ...@@ -31,7 +31,7 @@ Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Class FSASplit {A} (P : iProp Λ Σ) (E : coPset) Class FSASplit {A} (P : iProp Λ Σ) (E : coPset)
(fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A iProp Λ Σ) := { (fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A iProp Λ Σ) := {
fsa_split : fsa E Φ P; fsa_split : fsa E Φ P;
fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa; fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
}. }.
Global Arguments fsa_split {_} _ _ _ _ _ {_}. Global Arguments fsa_split {_} _ _ _ _ _ {_}.
...@@ -42,6 +42,13 @@ Global Instance fsa_split_fsa {A} (fsa : FSA Λ Σ A) E Φ : ...@@ -42,6 +42,13 @@ Global Instance fsa_split_fsa {A} (fsa : FSA Λ Σ A) E Φ :
FrameShiftAssertion fsaV fsa FSASplit (fsa E Φ) E fsa fsaV Φ. FrameShiftAssertion fsaV fsa FSASplit (fsa E Φ) E fsa fsaV Φ.
Proof. done. Qed. Proof. done. Qed.
Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
FSASplit Q E fsa fsaV Φ ToAssert P Q (|={E}=> P).
Proof.
intros.
by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
Qed.
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 Δ Q Δ |={E1,E2}=> Q. Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 Δ Q Δ |={E1,E2}=> Q.
Proof. intros -> ->. apply pvs_intro. Qed. Proof. intros -> ->. apply pvs_intro. Qed.
...@@ -87,17 +94,6 @@ Proof. ...@@ -87,17 +94,6 @@ Proof.
intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa. intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
eauto using tac_pvs_timeless. eauto using tac_pvs_timeless.
Qed. Qed.
Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
FSASplit Q E fsa fsaV Φ
envs_split lr js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
Δ1 (|={E}=> P) Δ2' fsa E Φ Δ Q.
Proof.
intros ??? HP HQ. rewrite -(fsa_split Q) -fsa_pvs_fsa -HQ envs_split_sound //.
rewrite HP envs_app_sound //; simpl.
by rewrite right_id pvs_frame_r wand_elim_r.
Qed.
End pvs. End pvs.
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done. Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
...@@ -185,19 +181,3 @@ Tactic Notation "iTimeless" constr(H) := ...@@ -185,19 +181,3 @@ Tactic Notation "iTimeless" constr(H) :=
Tactic Notation "iTimeless" constr(H) "as" constr(Hs) := Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
iTimeless H; iDestruct H as Hs. iTimeless H; iDestruct H as Hs.
Tactic Notation "iPvsAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
let H := iFresh in
let Hs := spec_pat.parse_one Hs in
lazymatch Hs with
| 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"
|env_cbv; reflexivity || fail "iPvsAssert:" Hs "not found"
|env_cbv; reflexivity|
|simpl; iDestruct H as pat]
| ?pat => fail "iPvsAssert: invalid pattern" pat
end.
Tactic Notation "iPvsAssert" constr(Q) "as" constr(pat) :=
iPvsAssert Q with "[]" as pat.
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
Inductive spec_goal_kind := GoalStd | GoalPvs.
Inductive spec_pat := Inductive spec_pat :=
| SGoal : bool list string spec_pat | SGoal : spec_goal_kind bool list string spec_pat
| SGoalPersistent : spec_pat | SGoalPersistent : spec_pat
| SGoalPure : spec_pat | SGoalPure : spec_pat
| SName : bool string spec_pat (* first arg = persistent *) | SName : bool string spec_pat (* first arg = persistent *)
...@@ -15,7 +17,8 @@ Inductive token := ...@@ -15,7 +17,8 @@ Inductive token :=
| TBracketR : token | TBracketR : token
| TPersistent : token | TPersistent : token
| TPure : token | TPure : token
| TForall : token. | TForall : token
| TPvs : token.
Fixpoint cons_name (kn : string) (k : list token) : list token := Fixpoint cons_name (kn : string) (k : list token) : list token :=
match kn with "" => k | _ => TName (string_rev kn) :: k end. match kn with "" => k | _ => TName (string_rev kn) :: k end.
...@@ -29,13 +32,14 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token := ...@@ -29,13 +32,14 @@ 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 (TPersistent :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPure :: 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 "*" s => tokenize_go s (TForall :: cons_name kn k) ""
| String "=" (String ">" s) => tokenize_go s (TPvs :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn) | String a s => tokenize_go s k (String a kn)
end. end.
Definition tokenize (s : string) : list token := tokenize_go s [] "". Definition tokenize (s : string) : list token := tokenize_go s [] "".
Inductive state := Inductive state :=
| StTop : state | StTop : state
| StAssert : bool list string state. | StAssert : spec_goal_kind bool list string state.
Fixpoint parse_go (ts : list token) (s : state) Fixpoint parse_go (ts : list token) (s : state)
(k : list spec_pat) : option (list spec_pat) := (k : list spec_pat) : option (list spec_pat) :=
...@@ -46,16 +50,18 @@ Fixpoint parse_go (ts : list token) (s : state) ...@@ -46,16 +50,18 @@ Fixpoint parse_go (ts : list token) (s : state)
| TName s :: ts => parse_go ts StTop (SName false s :: k) | TName s :: ts => parse_go ts StTop (SName false s :: k)
| TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k) | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k) | TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
| TBracketL :: ts => parse_go ts (StAssert false []) k | TBracketL :: ts => parse_go ts (StAssert GoalStd false []) k
| TPvs :: TBracketL :: ts => parse_go ts (StAssert GoalPvs false []) k
| TPvs :: ts => parse_go ts StTop (SGoal GoalPvs true [] :: k)
| TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k) | TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
| TForall :: ts => parse_go ts StTop (SForall :: k) | TForall :: ts => parse_go ts StTop (SForall :: k)
| _ => None | _ => None
end end
| StAssert neg ss => | StAssert kind neg ss =>
match ts with match ts with
| TMinus :: ts => guard (¬neg ss = []); parse_go ts (StAssert true ss) k | TMinus :: ts => guard (¬neg ss = []); parse_go ts (StAssert kind true ss) k
| TName s :: ts => parse_go ts (StAssert neg (s :: ss)) k | TName s :: ts => parse_go ts (StAssert kind neg (s :: ss)) k
| TBracketR :: ts => parse_go ts StTop (SGoal neg (rev ss) :: k) | TBracketR :: ts => parse_go ts StTop (SGoal kind neg (rev ss) :: k)
| _ => None | _ => None
end end
end. end.
......
...@@ -186,10 +186,11 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) := ...@@ -186,10 +186,11 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
|env_cbv; reflexivity |env_cbv; reflexivity
|(*goal*) |(*goal*)
|go H1 pats] |go H1 pats]
| SGoal ?lr ?Hs :: ?pats => | SGoal ?k ?lr ?Hs :: ?pats =>
eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _; eapply tac_specialize_assert with _ _ _ H1 _ lr Hs _ _ _ _;
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found" [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1 |solve_to_wand H1
|match k with GoalStd => apply to_assert_fallthrough | GoalPvs => apply _ end
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found" |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
|(*goal*) |(*goal*)
|go H1 pats] |go H1 pats]
...@@ -225,24 +226,25 @@ Tactic Notation "iPoseProof" open_constr(t) := ...@@ -225,24 +226,25 @@ Tactic Notation "iPoseProof" open_constr(t) :=
let H := iFresh in iPoseProof t as H. let H := iFresh in iPoseProof t as H.
(** * Apply *) (** * Apply *)
Tactic Notation "iApplyCore" constr(H) := first
[iExact H
|eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity || fail 1 "iApply:" H "not found"
|apply _ || fail 1 "iApply: cannot apply" H|]].
Tactic Notation "iApply" open_constr(t) := Tactic Notation "iApply" open_constr(t) :=
let finish H := first
[iExact H
|eapply tac_apply with _ H _ _ _;
[env_cbv; reflexivity || fail 1 "iApply:" H "not found"
|let P := match goal with |- ToWand ?P _ _ => P end in
apply _ || fail 1 "iApply: cannot apply" H ":" P
|lazy beta (* reduce betas created by instantiation *)]] in
let Htmp := iFresh in let Htmp := iFresh in
lazymatch t with lazymatch t with
| ITrm ?H ?xs ?pat => | ITrm ?H ?xs ?pat =>
iPoseProofCore H as Htmp; last ( iPoseProofCore H as Htmp; last (
iSpecializeArgs Htmp xs; iSpecializeArgs Htmp xs;
try (iSpecializeArgs Htmp (hcons _ _)); try (iSpecializeArgs Htmp (hcons _ _));
iSpecializePat Htmp pat; last iApplyCore Htmp) iSpecializePat Htmp pat; last finish Htmp)
| _ => | _ =>
iPoseProofCore t as Htmp; last ( iPoseProofCore t as Htmp; last (
try (iSpecializeArgs Htmp (hcons _ _)); try (iSpecializeArgs Htmp (hcons _ _));
iApplyCore Htmp) finish Htmp)
end; try apply _. end; try apply _.
(** * Revert *) (** * Revert *)
...@@ -703,18 +705,21 @@ Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) := ...@@ -703,18 +705,21 @@ Tactic Notation "iAssert" constr(Q) "with" constr(Hs) "as" constr(pat) :=
let H := iFresh in let H := iFresh in
let Hs := spec_pat.parse Hs in let Hs := spec_pat.parse Hs in
lazymatch Hs with lazymatch Hs with
| [SGoal ?lr ?Hs] => | [SGoalPersistent] =>
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]
| [SGoalPersistent] =>
eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *) eapply tac_assert_persistent with _ H Q; (* (j:=H) (P:=Q) *)
[apply _ || fail "iAssert:" Q "not persistent" [env_cbv; reflexivity
|(*goal*)
|apply _ || fail "iAssert:" Q "not persistent"
|iDestructHyp H as pat]
| [SGoal ?k ?lr ?Hs] =>
eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
[match k with GoalStd => apply to_assert_fallthrough | GoalPvs => apply _ end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity| |env_cbv; reflexivity|
|iDestructHyp H as pat] |iDestructHyp H as pat]
| ?pat => fail "iAssert: invalid pattern" pat | ?pat => fail "iAssert: invalid pattern" pat
end. end.
Tactic Notation "iAssert" constr(Q) "as" constr(pat) := Tactic Notation "iAssert" constr(Q) "as" constr(pat) :=
iAssert Q with "[]" as pat. iAssert Q with "[]" as pat.
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.proofmode Require Import pviewshifts. From iris.proofmode Require Import pviewshifts invariants.
Lemma demo_0 {M : cmraT} (P Q : uPred M) : Lemma demo_0 {M : cmraT} (P Q : uPred M) :
(P Q) (( x, x = 0 x = 1) (Q P)). (P Q) (( x, x = 0 x = 1) (Q P)).
...@@ -83,13 +83,26 @@ Qed. ...@@ -83,13 +83,26 @@ Qed.
Section iris. Section iris.
Context {Λ : language} {Σ : iFunctor}. Context {Λ : language} {Σ : iFunctor}.
Implicit Types E : coPset.
Implicit Types P Q : iProp Λ Σ.
Lemma demo_7 (E1 E2 E : coPset) (P : iProp Λ Σ) : Lemma demo_7 E1 E2 E P :
E1 E2 E E1 E1 E2 E E1
(|={E1,E}=> P) (|={E2,E E2 E1}=> P). (|={E1,E}=> P) (|={E2,E E2 E1}=> P).
Proof. Proof.
iIntros {? ?} "Hpvs". iIntros {? ?} "Hpvs".
iPvs "Hpvs"; first (split_and?; set_solver). iPvs "Hpvs"; first set_solver.
done. done.
Qed. Qed.
Lemma demo_8 N E P Q R :
nclose N E
(True - P - inv N Q - True - R) (P - Q - |={E}=> R).
Proof.
iIntros {?} "H HP HQ".
iApply ("H" with "[#] HP =>[HQ] =>").
- done.
- by iApply inv_alloc.
- by iPvsIntro.
Qed.
End iris. End iris.
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