Library iris.proofmode.pviewshifts
From iris.proofmode Require Import coq_tactics spec_patterns.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export pviewshifts.
Import uPred.
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
Global Instance from_assumption_pvs E p P Q :
FromAssumption p P Q → FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
Global Instance from_sep_pvs E P Q1 Q2 :
FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof.
rewrite /FromExist=><-. apply exist_elim⇒ a. by rewrite -(exist_intro a).
Qed.
Global Instance frame_pvs E1 E2 R P Q :
Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance into_wand_pvs E1 E2 R P Q :
IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
Proof.
intros P ?. rewrite (pvs_timeless E1 P) pvs_frame_r.
by rewrite wand_elim_r pvs_trans; last set_solver.
Qed.
Global Instance atimeless_elim_pvs E1 E2 Q : ATimelessElim (|={E1,E2}=> Q).
Proof.
intros P ?. rewrite (pvs_timeless_affine E1 P) pvs_frame_r.
by rewrite wand_elim_r pvs_trans; last set_solver.
Qed.
Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
(fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
is_fsa : P ⊣⊢ fsa E Φ;
is_fsa_is_fsa :> FrameShiftAssertion fsaV fsa;
}.
Global Arguments is_fsa {_} _ _ _ _ _ {_}.
Global Instance is_fsa_pvs E P :
IsFSA (|={E}=> P)%I E pvs_fsa True (λ _, P).
Proof. split. done. apply _. Qed.
Global Instance is_fsa_fsa {A} (fsa : FSA Λ Σ A) E Φ :
FrameShiftAssertion fsaV fsa → IsFSA (fsa E Φ) E fsa fsaV Φ.
Proof. done. Qed.
Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ → IntoAssert P Q (|={E}=> P).
Proof.
intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
Qed.
Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ → TimelessElim Q.
Proof.
intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
Global Instance atimeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ → ATimelessElim Q.
Proof.
intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
by rewrite (pvs_timeless_affine _ P) pvs_frame_r wand_elim_r.
Qed.
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → (Δ ⊢ Q) → Δ ⊢ |={E1,E2}=> Q.
Proof. intros → →. apply pvs_intro. Qed.
Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P' E1' E2' P Q :
envs_lookup i Δ = Some (p, P') → P' = (|={E1',E2'}=> P)%I →
(E1' = E1 ∧ E2' = E2 ∧ E2 ⊆ E1 ∪ E3
∨ E2 = E2' ∪ E1 ∖ E1' ∧ E2' ⊥ E1 ∖ E1' ∧ E1' ⊆ E1 ∧ E2' ⊆ E1' ∪ E3) →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ={E2,E3}=> Q) → Δ ={E1,E3}=> Q.
Proof.
intros ? → HE ? HQ. rewrite envs_replace_sound //; simpl. destruct p.
- rewrite relevant_elim right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
- rewrite right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
Qed.
Lemma tac_pvs_elim' Δ Δ' E1 E2 E3 i p P' E1' E2' P Q :
envs_lookup i Δ = Some (p, P') → (P' ⊢ (|={E1',E2'}=> P)%I) →
(E1' = E1 ∧ E2' = E2 ∧ E2 ⊆ E1 ∪ E3
∨ E2 = E2' ∪ E1 ∖ E1' ∧ E2' ⊥ E1 ∖ E1' ∧ E1' ⊆ E1 ∧ E2' ⊆ E1' ∪ E3) →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ={E2,E3}=> Q) → Δ ={E1,E3}=> Q.
Proof.
intros ? HP' HE ? HQ. rewrite envs_replace_sound //; simpl. destruct p; rewrite HP'.
- rewrite relevant_elim right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
- rewrite right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
Qed.
Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P' P Q Φ :
envs_lookup i Δ = Some (p, P') → P' = (|={E}=> P)%I →
IsFSA Q E fsa fsaV Φ →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ? → ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
eapply tac_pvs_elim; set_solver.
Qed.
Class IsAFSA {A} (P : iProp Λ Σ) (E : coPset)
(fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
is_afsa : P ⊣⊢ fsa E Φ;
is_afsa_is_afsa :> AffineFrameShiftAssertion fsaV fsa;
}.
Global Arguments is_afsa {_} _ _ _ _ _ {_}.
Global Instance is_afsa_pvs E P :
IsAFSA (|={E}=> P)%I E pvs_fsa True (λ _, P).
Proof. split. done. apply fsa_afsa, _. Qed.
Global Instance is_afsa_afsa {A} (fsa : FSA Λ Σ A) E Φ :
AffineFrameShiftAssertion fsaV fsa → IsAFSA (fsa E Φ) E fsa fsaV Φ.
Proof. done. Qed.
Class IntoPvs R E P := into_pvs : R ⊢ (|={E}=> P).
Global Arguments into_pvs : clear implicits.
Global Instance into_pvs_pvs E P: IntoPvs (|={E}=> P)%I E P.
Proof. rewrite /IntoPvs. reflexivity. Qed.
Global Instance into_pvs_relevant R E P: IntoPvs R E P → IntoPvs (□ R) E P.
Proof. rewrite /IntoPvs⇒ →. apply relevant_elim. Qed.
Global Instance into_pvs_affine R E P : IntoPvs R E P → IntoPvs (⧆ R) E P.
Proof. rewrite /IntoPvs⇒ →. apply affine_elim. Qed.
Lemma tac_pvs_elim_afsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P0 P Q Φ :
envs_lookup i Δ = Some (p, P0)%I → IntoPvs P0 E P → IsAFSA Q E fsa fsaV Φ →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ???. rewrite (is_afsa Q) -afsa_pvs_afsa.
eapply tac_pvs_elim'; eauto; set_solver.
Qed.
Global Instance timeless_elim_afsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsAFSA Q E fsa fsaV Φ → TimelessElim Q.
Proof.
intros ? P ?. rewrite (is_afsa Q) -{2}afsa_pvs_afsa.
by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
Global Instance atimeless_elim_afsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsAFSA Q E fsa fsaV Φ → ATimelessElim Q.
Proof.
intros ? P ?. rewrite (is_afsa Q) -{2}afsa_pvs_afsa.
by rewrite (pvs_timeless_affine _ P) pvs_frame_r wand_elim_r.
Qed.
Lemma tac_pvs_timeless Δ Δ' E1 E2 i P Q :
envs_lookup i Δ = Some (false, ▷ P)%I → TimelessP P →
envs_simple_replace i false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ |={E1,E2}=> Q) → Δ ⊢ (|={E1,E2}=> Q).
Proof.
intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite (pvs_timeless E1 P) pvs_frame_r right_id wand_elim_r HQ.
by rewrite pvs_trans; last set_solver.
Qed.
Lemma tac_pvs_timeless_affine Δ Δ' E1 E2 i P Q :
envs_lookup i Δ = Some (false, ⧆▷ P)%I → ATimelessP P →
envs_simple_replace i false (Esnoc Enil i (⧆P)) Δ = Some Δ' →
(Δ' ⊢ |={E1,E2}=> Q) → Δ ⊢ (|={E1,E2}=> Q).
Proof.
intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite (pvs_timeless_affine E1 P) pvs_frame_r right_id wand_elim_r HQ.
by rewrite pvs_trans; last set_solver.
Qed.
Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i P Q Φ :
IsAFSA Q E fsa fsaV Φ →
envs_lookup i Δ = Some (false, ▷ P)%I → TimelessP P →
envs_simple_replace i false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ????. rewrite (is_afsa Q) -afsa_pvs_afsa.
eauto using tac_pvs_timeless.
Qed.
Lemma tac_pvs_timeless_fsa_affine {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i P Q Φ :
IsAFSA Q E fsa fsaV Φ →
envs_lookup i Δ = Some (false, ⧆▷ P)%I → ATimelessP P →
envs_simple_replace i false (Esnoc Enil i (⧆P)) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ????. rewrite (is_afsa Q) -afsa_pvs_afsa.
eauto using tac_pvs_timeless_affine.
Qed.
Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
IsAFSA 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 (is_afsa Q) -afsa_pvs_afsa -HQ envs_split_sound //.
rewrite HP envs_app_sound //; simpl.
by rewrite right_id pvs_frame_r wand_elim_r.
Qed.
End pvs.
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
Tactic Notation "iPvsCore" constr(H) :=
match goal with
| |- _ ⊢ |={_,_}=> _ ⇒
eapply tac_pvs_elim with _ _ H _ _ _ _ _;
[env_cbv; reflexivity || fail "iPvs:" H "not found"
|let P := match goal with |- ?P = _ ⇒ P end in
reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
|first
[left; split_and!;
[reflexivity|reflexivity|try (rewrite (idemp_L (∪)); reflexivity)]
|right; split; first reflexivity]
|env_cbv; reflexivity|]
| |- ?Δ ⊢ _ ⇒
let Δ' := fresh "Δ" in
match type of Δ with
| uPred ?T ⇒
evar (Δ': coq_tactics.envs T);
eapply tac_pvs_elim_afsa with _ _ Δ' _ H _ _ _ _;
[env_cbv; reflexivity || fail "iPvs:" H "not found"
|let P := match goal with |- IntoPvs ?P _ _ ⇒ P end in
apply _ || fail "iPvs:" P "not a pvs"
|let P := match goal with |- IsAFSA ?P _ _ _ _ ⇒ P end in
apply _ || fail "iPvs:" P "not a pvs"
|env_cbv; rewrite /Δ'; eauto | simpl; rewrite /Δ'; clear Δ']
end
end.
Tactic Notation "iPvs" open_constr(lem) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as "?").
Tactic Notation "iPvs" open_constr(lem) "as" constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as ( x1 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Hint Extern 2 (of_envs _ ⊢ _) ⇒
match goal with |- _ ⊢ (|={_}=> _)%I ⇒ iPvsIntro end.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export pviewshifts.
Import uPred.
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Global Instance from_pure_pvs E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
Proof. intros ??. by rewrite -pvs_intro (from_pure P). Qed.
Global Instance from_assumption_pvs E p P Q :
FromAssumption p P Q → FromAssumption p P (|={E}=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
Global Instance from_sep_pvs E P Q1 Q2 :
FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
Global Instance or_split_pvs E1 E2 P Q1 Q2 :
FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof.
rewrite /FromExist=><-. apply exist_elim⇒ a. by rewrite -(exist_intro a).
Qed.
Global Instance frame_pvs E1 E2 R P Q :
Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
Global Instance into_wand_pvs E1 E2 R P Q :
IntoWand R P Q → IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
Proof.
intros P ?. rewrite (pvs_timeless E1 P) pvs_frame_r.
by rewrite wand_elim_r pvs_trans; last set_solver.
Qed.
Global Instance atimeless_elim_pvs E1 E2 Q : ATimelessElim (|={E1,E2}=> Q).
Proof.
intros P ?. rewrite (pvs_timeless_affine E1 P) pvs_frame_r.
by rewrite wand_elim_r pvs_trans; last set_solver.
Qed.
Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
(fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
is_fsa : P ⊣⊢ fsa E Φ;
is_fsa_is_fsa :> FrameShiftAssertion fsaV fsa;
}.
Global Arguments is_fsa {_} _ _ _ _ _ {_}.
Global Instance is_fsa_pvs E P :
IsFSA (|={E}=> P)%I E pvs_fsa True (λ _, P).
Proof. split. done. apply _. Qed.
Global Instance is_fsa_fsa {A} (fsa : FSA Λ Σ A) E Φ :
FrameShiftAssertion fsaV fsa → IsFSA (fsa E Φ) E fsa fsaV Φ.
Proof. done. Qed.
Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ → IntoAssert P Q (|={E}=> P).
Proof.
intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
Qed.
Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ → TimelessElim Q.
Proof.
intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
Global Instance atimeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ → ATimelessElim Q.
Proof.
intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
by rewrite (pvs_timeless_affine _ P) pvs_frame_r wand_elim_r.
Qed.
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 → (Δ ⊢ Q) → Δ ⊢ |={E1,E2}=> Q.
Proof. intros → →. apply pvs_intro. Qed.
Lemma tac_pvs_elim Δ Δ' E1 E2 E3 i p P' E1' E2' P Q :
envs_lookup i Δ = Some (p, P') → P' = (|={E1',E2'}=> P)%I →
(E1' = E1 ∧ E2' = E2 ∧ E2 ⊆ E1 ∪ E3
∨ E2 = E2' ∪ E1 ∖ E1' ∧ E2' ⊥ E1 ∖ E1' ∧ E1' ⊆ E1 ∧ E2' ⊆ E1' ∪ E3) →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ={E2,E3}=> Q) → Δ ={E1,E3}=> Q.
Proof.
intros ? → HE ? HQ. rewrite envs_replace_sound //; simpl. destruct p.
- rewrite relevant_elim right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
- rewrite right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
Qed.
Lemma tac_pvs_elim' Δ Δ' E1 E2 E3 i p P' E1' E2' P Q :
envs_lookup i Δ = Some (p, P') → (P' ⊢ (|={E1',E2'}=> P)%I) →
(E1' = E1 ∧ E2' = E2 ∧ E2 ⊆ E1 ∪ E3
∨ E2 = E2' ∪ E1 ∖ E1' ∧ E2' ⊥ E1 ∖ E1' ∧ E1' ⊆ E1 ∧ E2' ⊆ E1' ∪ E3) →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ={E2,E3}=> Q) → Δ ={E1,E3}=> Q.
Proof.
intros ? HP' HE ? HQ. rewrite envs_replace_sound //; simpl. destruct p; rewrite HP'.
- rewrite relevant_elim right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
- rewrite right_id pvs_frame_r wand_elim_r HQ.
destruct HE as [(?&?&?)|(?&?&?&?)]; subst; first (by apply pvs_trans).
etrans; [eapply pvs_mask_frame'|apply pvs_trans]; auto; set_solver.
Qed.
Lemma tac_pvs_elim_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P' P Q Φ :
envs_lookup i Δ = Some (p, P') → P' = (|={E}=> P)%I →
IsFSA Q E fsa fsaV Φ →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ? → ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
eapply tac_pvs_elim; set_solver.
Qed.
Class IsAFSA {A} (P : iProp Λ Σ) (E : coPset)
(fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A → iProp Λ Σ) := {
is_afsa : P ⊣⊢ fsa E Φ;
is_afsa_is_afsa :> AffineFrameShiftAssertion fsaV fsa;
}.
Global Arguments is_afsa {_} _ _ _ _ _ {_}.
Global Instance is_afsa_pvs E P :
IsAFSA (|={E}=> P)%I E pvs_fsa True (λ _, P).
Proof. split. done. apply fsa_afsa, _. Qed.
Global Instance is_afsa_afsa {A} (fsa : FSA Λ Σ A) E Φ :
AffineFrameShiftAssertion fsaV fsa → IsAFSA (fsa E Φ) E fsa fsaV Φ.
Proof. done. Qed.
Class IntoPvs R E P := into_pvs : R ⊢ (|={E}=> P).
Global Arguments into_pvs : clear implicits.
Global Instance into_pvs_pvs E P: IntoPvs (|={E}=> P)%I E P.
Proof. rewrite /IntoPvs. reflexivity. Qed.
Global Instance into_pvs_relevant R E P: IntoPvs R E P → IntoPvs (□ R) E P.
Proof. rewrite /IntoPvs⇒ →. apply relevant_elim. Qed.
Global Instance into_pvs_affine R E P : IntoPvs R E P → IntoPvs (⧆ R) E P.
Proof. rewrite /IntoPvs⇒ →. apply affine_elim. Qed.
Lemma tac_pvs_elim_afsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P0 P Q Φ :
envs_lookup i Δ = Some (p, P0)%I → IntoPvs P0 E P → IsAFSA Q E fsa fsaV Φ →
envs_replace i p false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ???. rewrite (is_afsa Q) -afsa_pvs_afsa.
eapply tac_pvs_elim'; eauto; set_solver.
Qed.
Global Instance timeless_elim_afsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsAFSA Q E fsa fsaV Φ → TimelessElim Q.
Proof.
intros ? P ?. rewrite (is_afsa Q) -{2}afsa_pvs_afsa.
by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
Global Instance atimeless_elim_afsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsAFSA Q E fsa fsaV Φ → ATimelessElim Q.
Proof.
intros ? P ?. rewrite (is_afsa Q) -{2}afsa_pvs_afsa.
by rewrite (pvs_timeless_affine _ P) pvs_frame_r wand_elim_r.
Qed.
Lemma tac_pvs_timeless Δ Δ' E1 E2 i P Q :
envs_lookup i Δ = Some (false, ▷ P)%I → TimelessP P →
envs_simple_replace i false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ |={E1,E2}=> Q) → Δ ⊢ (|={E1,E2}=> Q).
Proof.
intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite (pvs_timeless E1 P) pvs_frame_r right_id wand_elim_r HQ.
by rewrite pvs_trans; last set_solver.
Qed.
Lemma tac_pvs_timeless_affine Δ Δ' E1 E2 i P Q :
envs_lookup i Δ = Some (false, ⧆▷ P)%I → ATimelessP P →
envs_simple_replace i false (Esnoc Enil i (⧆P)) Δ = Some Δ' →
(Δ' ⊢ |={E1,E2}=> Q) → Δ ⊢ (|={E1,E2}=> Q).
Proof.
intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite (pvs_timeless_affine E1 P) pvs_frame_r right_id wand_elim_r HQ.
by rewrite pvs_trans; last set_solver.
Qed.
Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i P Q Φ :
IsAFSA Q E fsa fsaV Φ →
envs_lookup i Δ = Some (false, ▷ P)%I → TimelessP P →
envs_simple_replace i false (Esnoc Enil i P) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ????. rewrite (is_afsa Q) -afsa_pvs_afsa.
eauto using tac_pvs_timeless.
Qed.
Lemma tac_pvs_timeless_fsa_affine {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i P Q Φ :
IsAFSA Q E fsa fsaV Φ →
envs_lookup i Δ = Some (false, ⧆▷ P)%I → ATimelessP P →
envs_simple_replace i false (Esnoc Enil i (⧆P)) Δ = Some Δ' →
(Δ' ⊢ fsa E Φ) → Δ ⊢ Q.
Proof.
intros ????. rewrite (is_afsa Q) -afsa_pvs_afsa.
eauto using tac_pvs_timeless_affine.
Qed.
Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
IsAFSA 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 (is_afsa Q) -afsa_pvs_afsa -HQ envs_split_sound //.
rewrite HP envs_app_sound //; simpl.
by rewrite right_id pvs_frame_r wand_elim_r.
Qed.
End pvs.
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
Tactic Notation "iPvsCore" constr(H) :=
match goal with
| |- _ ⊢ |={_,_}=> _ ⇒
eapply tac_pvs_elim with _ _ H _ _ _ _ _;
[env_cbv; reflexivity || fail "iPvs:" H "not found"
|let P := match goal with |- ?P = _ ⇒ P end in
reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
|first
[left; split_and!;
[reflexivity|reflexivity|try (rewrite (idemp_L (∪)); reflexivity)]
|right; split; first reflexivity]
|env_cbv; reflexivity|]
| |- ?Δ ⊢ _ ⇒
let Δ' := fresh "Δ" in
match type of Δ with
| uPred ?T ⇒
evar (Δ': coq_tactics.envs T);
eapply tac_pvs_elim_afsa with _ _ Δ' _ H _ _ _ _;
[env_cbv; reflexivity || fail "iPvs:" H "not found"
|let P := match goal with |- IntoPvs ?P _ _ ⇒ P end in
apply _ || fail "iPvs:" P "not a pvs"
|let P := match goal with |- IsAFSA ?P _ _ _ _ ⇒ P end in
apply _ || fail "iPvs:" P "not a pvs"
|env_cbv; rewrite /Δ'; eauto | simpl; rewrite /Δ'; clear Δ']
end
end.
Tactic Notation "iPvs" open_constr(lem) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as "?").
Tactic Notation "iPvs" open_constr(lem) "as" constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as ( x1 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒ iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iDestructCore lem as (fun H ⇒
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Hint Extern 2 (of_envs _ ⊢ _) ⇒
match goal with |- _ ⊢ (|={_}=> _)%I ⇒ iPvsIntro end.