Library iris.program_logic.pviewshifts
From iris.prelude Require Export coPset.
From iris.algebra Require Export upred_big_op updates.
From iris.program_logic Require Export model.
From iris.program_logic Require Import ownership wsat.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 100 (_ ∉ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
{| uPred_holds n r1 rl := ∀ k Ef σ rf rfl ,
0 < k ≤ n → E1 ∪ E2 ⊥ Ef →
wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) (rl ⋅ rfl) →
∃ r2, P k r2 rl ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) (rl ⋅ rfl) |}.
Next Obligation.
intros Λ Σ E1 E2 P n r1 rl1 r2 rl2 HP [r3 Hr2] Hrl k Ef σ rf rfl ?? Hwsat; simpl in ×.
edestruct (HP k Ef σ (r3 ⋅ rf) rfl) as (r'&?&?); rewrite ?(assoc op); eauto.
- rewrite ?(assoc op) -(dist_le _ _ _ _ Hr2); last lia.
by rewrite (dist_le _ _ _ _ Hrl); last lia.
- ∃ (r' ⋅ r3); rewrite -assoc -(dist_le _ _ _ _ Hrl) //; last lia.
split; last done.
apply uPred_mono with r' rl1; eauto using cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
Definition pvs := proj1_sig pvs_aux.
Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
Arguments pvs {_ _} _ _ _%I.
Instance: Params (@pvs) 4.
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : uPred_scope.
Notation "|={ E }=> Q" := (pvs E E Q%I)
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : uPred_scope.
Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
(at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=★ Q") : uPred_scope.
Notation "P ={ E }=★ Q" := (P ={E,E}=★ Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=★ Q") : uPred_scope.
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Lemma pvs_zero E1 E2 P r rl: pvs_def E1 E2 P 0 r rl.
Proof. intros ??????. exfalso. omega. Qed.
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Proof.
rewrite pvs_eq.
intros P Q HPQ; split⇒ n' r1 ??; simpl; split; intros HP k Ef σ rf rfl ???;
destruct (HP k Ef σ rf rfl) as (r2&?&?); auto;
∃ r2; split_and?; auto; apply HPQ; eauto.
Qed.
Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P ={E}=> P.
Proof.
rewrite pvs_eq. split⇒ n r ? HP k Ef σ rf ???; ∃ r; split; last done.
apply uPred_closed with n; eauto.
Qed.
Lemma pvs_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof.
rewrite pvs_eq. intros HPQ; split⇒ n r rl ? ? HP k Ef σ rf rfl ???.
destruct (HP k Ef σ rf rfl) as (r2&?&?); eauto.
∃ r2; eauto using uPred_in_entails.
Qed.
Lemma pvs_timeless E P : TimelessP P → ▷ P ={E}=> P.
Proof.
rewrite pvs_eq uPred.timelessP_spec⇒ HP.
uPred.unseal; split=>-[|n] r ? HP' k Ef σ rf ???; first lia.
∃ r; split; last done.
apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.
Lemma pvs_timeless_affine E P : ATimelessP P → ⧆▷ P ={E}=> ⧆P.
Proof.
rewrite pvs_eq uPred.atimelessP_spec⇒ HP.
uPred.unseal; split=>-[|n] r rl ?? [HP' Haff] rf ? k Ef σ ???; first lia.
∃ r; split; last done.
split.
- rewrite (dist_le _ _ _ _ Haff); auto. apply HP, uPred_closed with n; eauto using cmra_validN_le.
rewrite -(dist_le _ _ _ _ Haff); auto.
- eapply dist_le; eauto.
Qed.
Lemma pvs_trans E1 E2 E3 P :
E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
Proof.
rewrite pvs_eq. intros ?; split⇒ n r1 rl ? ? HP1 rf rfl k Ef σ ???.
destruct (HP1 rf rfl k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
Ef ⊥ E1 ∪ E2 → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
Proof.
rewrite pvs_eq. intros ?; split⇒ n r rl ? ? HP k Ef' σ rf rfl ???.
destruct (HP k (Ef∪Ef') σ rf rfl) as (r'&?&?); rewrite ?(assoc_L _); eauto.
by ∃ r'; rewrite -(assoc_L _).
Qed.
Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
Proof.
rewrite pvs_eq.
uPred.unseal; split; intros n r rl ? ? (r1&r2&rl1&rl2&Hr&Hrl&HP&HQ) k Ef σ rf rfl ???.
destruct (HP k Ef σ (r2 ⋅ rf) (rl2 ⋅ rfl)) as (r'&?&?); eauto.
{
rewrite ?assoc -(dist_le _ _ _ _ Hr); last lia.
rewrite -(dist_le _ _ _ _ Hrl); last lia; auto.
}
∃ (r' ⋅ r2); split.
- ∃ r', r2, rl1, rl2. split_and?; eauto using dist_le.
eauto using dist_le.
apply uPred_closed with n; auto.
- rewrite (dist_le _ _ _ _ Hrl); last lia.
by rewrite ?right_id -?assoc.
Qed.
Lemma pvs_openI i P : ownI i P ⊢ (|={{[i]},∅}=> ⧆▷ P).
Proof.
rewrite pvs_eq. uPred.unseal; split⇒ -[|n] r rl ? ? Hinv [|k] Ef σ rf rfl ???; try lia.
apply ownI_spec in Hinv as [Hinv Hrl]; auto.
destruct (wsat_open k Ef σ (r ⋅ rf) (rl ⋅ rfl) i P) as (rP&?&?); auto.
{ rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
∃ (rP ⋅ r); split; last by rewrite (left_id_L _ _) -assoc.
eapply uPred_mono with rP rl; eauto using cmra_includedN_l.
split; auto; rewrite (dist_le _ _ _ _ Hrl); last lia; auto.
Qed.
Lemma pvs_closeI i P : (ownI i P ∧ ▷P) ⊢ (|={∅,{[i]}}=> Emp).
Proof.
rewrite pvs_eq. uPred.unseal; split⇒ -[|n] r rl ? ? [HI HP] [|k] Ef σ rf rfl ? HE ?; try lia.
rewrite ownI_spec in HI *; auto; intros (Heq&Hrl).
∃ ∅; split.
- rewrite (dist_le _ _ _ _ Hrl); last lia.
split; auto.
- rewrite left_id; apply wsat_close with P r.
+ eauto using dist_le.
+ set_solver +HE.
+ by rewrite -(left_id_L ∅ (∪) Ef).
+ apply uPred_closed with n; auto.
rewrite -(dist_le _ _ _ _ Hrl); auto.
Qed.
Lemma pvs_closeI_sep i P : (ownI i P ★ ⧆▷P) ⊢ (|={∅,{[i]}}=> Emp).
Proof.
rewrite pvs_eq. uPred.unseal; split⇒ -[|n] r rl Hv Hvl;
intros (x1&y1&x2&y2&Heq&Heql&HI&HP) [|k] Ef σ rf rfl ? HE ?; try lia.
rewrite Heq in Hv *=>Hv.
rewrite {1}Heql in Hvl *=>Hvl.
rewrite ownI_spec in HI *; eauto using cmra_validN_op_r, cmra_validN_op_l.
intros (Heq2&Hrl2).
∃ ∅; split.
- destruct HP as [HP HAff]. rewrite HAff in Heql ×.
rewrite Hrl2 ?left_id. intros Heq1l'.
rewrite (dist_le _ _ _ _ Heq1l'); last lia.
split; auto.
- rewrite left_id; apply wsat_close with P r.
+ rewrite (dist_le _ _ _ _ Heq); eauto using dist_le.
rewrite lookup_wld_op_l; eauto.
apply dist_le with (S n); eauto.
+ set_solver +HE.
+ by rewrite -(left_id_L ∅ (∪) Ef).
+ apply uPred_closed with n; auto.
destruct HP as [HP HAff].
rewrite (dist_le _ _ _ _ Heq); last lia.
rewrite -(dist_le _ _ _ _ HAff); last lia.
apply uPred_mono with y1 y2; eauto using cmra_includedN_r.
Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m ~~>: P → ownG m ={E}=> ∃ m', ■ P m' ∧ ownG m'.
Proof.
rewrite pvs_eq. intros Hup.
uPred.unseal; split⇒ -[|n] r rl ? ? /ownG_spec [Hinv ?] [|k] Ef σ rf rfl ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf (rl ⋅ rfl) m P) as (m'&?&?); eauto.
{ apply cmra_includedN_le with (S n); auto. }
∃ (update_gst m' r); split; [∃ m'; split; [|apply ownG_spec; split; auto]|]; auto.
eapply dist_le; eauto.
Qed.
Lemma pvs_allocI E P : ¬set_finite E → ⧆▷ P ⊢ (|={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P).
Proof.
rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
split⇒ -[|n] r rl ? ? [HP Hrl] [|k] Ef σ rf rfl ???; try lia.
destruct (wsat_alloc k E Ef σ rf (rl ⋅ rfl) P r) as (i&?&?&?); auto.
{ apply uPred_closed with n; eauto. rewrite -(dist_le _ _ _ _ Hrl); eauto. }
∃ (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
split; [|done]. ∃ i; split_and!; rewrite /uPred_holds /= /uPred_holds /= ; auto.
split; eauto using dist_le.
Qed.
Lemma pvs_affine E1 E2 P : (⧆(|={E1, E2}=> P) ⊣⊢ ⧆(|={E1, E2}=> ⧆P))%I.
Proof.
apply (anti_symm (⊢)).
- rewrite pvs_eq. uPred.unseal.
split⇒ -[|n] r rl ?? [HP Hrl]; split; auto;
intros [|k] Ef σ rf rfl ???; try lia.
destruct (HP (S k) Ef σ rf rfl) as (r'&?&?); eauto; try lia.
∃ r'; split; auto. split; eauto using dist_le.
- by rewrite pvs_mono; last apply uPred.affine_elim.
Qed.
From iris.algebra Require Export upred_big_op updates.
From iris.program_logic Require Export model.
From iris.program_logic Require Import ownership wsat.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 100 (_ ∉ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
{| uPred_holds n r1 rl := ∀ k Ef σ rf rfl ,
0 < k ≤ n → E1 ∪ E2 ⊥ Ef →
wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) (rl ⋅ rfl) →
∃ r2, P k r2 rl ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) (rl ⋅ rfl) |}.
Next Obligation.
intros Λ Σ E1 E2 P n r1 rl1 r2 rl2 HP [r3 Hr2] Hrl k Ef σ rf rfl ?? Hwsat; simpl in ×.
edestruct (HP k Ef σ (r3 ⋅ rf) rfl) as (r'&?&?); rewrite ?(assoc op); eauto.
- rewrite ?(assoc op) -(dist_le _ _ _ _ Hr2); last lia.
by rewrite (dist_le _ _ _ _ Hrl); last lia.
- ∃ (r' ⋅ r3); rewrite -assoc -(dist_le _ _ _ _ Hrl) //; last lia.
split; last done.
apply uPred_mono with r' rl1; eauto using cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
Definition pvs_aux : { x | x = @pvs_def }. by eexists. Qed.
Definition pvs := proj1_sig pvs_aux.
Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
Arguments pvs {_ _} _ _ _%I.
Instance: Params (@pvs) 4.
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : uPred_scope.
Notation "|={ E }=> Q" := (pvs E E Q%I)
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : uPred_scope.
Notation "|==> Q" := (pvs ⊤ ⊤ Q%I)
(at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=★ Q") : uPred_scope.
Notation "P ={ E }=★ Q" := (P ={E,E}=★ Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=★ Q") : uPred_scope.
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
Lemma pvs_zero E1 E2 P r rl: pvs_def E1 E2 P 0 r rl.
Proof. intros ??????. exfalso. omega. Qed.
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Proof.
rewrite pvs_eq.
intros P Q HPQ; split⇒ n' r1 ??; simpl; split; intros HP k Ef σ rf rfl ???;
destruct (HP k Ef σ rf rfl) as (r2&?&?); auto;
∃ r2; split_and?; auto; apply HPQ; eauto.
Qed.
Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P ={E}=> P.
Proof.
rewrite pvs_eq. split⇒ n r ? HP k Ef σ rf ???; ∃ r; split; last done.
apply uPred_closed with n; eauto.
Qed.
Lemma pvs_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof.
rewrite pvs_eq. intros HPQ; split⇒ n r rl ? ? HP k Ef σ rf rfl ???.
destruct (HP k Ef σ rf rfl) as (r2&?&?); eauto.
∃ r2; eauto using uPred_in_entails.
Qed.
Lemma pvs_timeless E P : TimelessP P → ▷ P ={E}=> P.
Proof.
rewrite pvs_eq uPred.timelessP_spec⇒ HP.
uPred.unseal; split=>-[|n] r ? HP' k Ef σ rf ???; first lia.
∃ r; split; last done.
apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.
Lemma pvs_timeless_affine E P : ATimelessP P → ⧆▷ P ={E}=> ⧆P.
Proof.
rewrite pvs_eq uPred.atimelessP_spec⇒ HP.
uPred.unseal; split=>-[|n] r rl ?? [HP' Haff] rf ? k Ef σ ???; first lia.
∃ r; split; last done.
split.
- rewrite (dist_le _ _ _ _ Haff); auto. apply HP, uPred_closed with n; eauto using cmra_validN_le.
rewrite -(dist_le _ _ _ _ Haff); auto.
- eapply dist_le; eauto.
Qed.
Lemma pvs_trans E1 E2 E3 P :
E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
Proof.
rewrite pvs_eq. intros ?; split⇒ n r1 rl ? ? HP1 rf rfl k Ef σ ???.
destruct (HP1 rf rfl k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
Ef ⊥ E1 ∪ E2 → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
Proof.
rewrite pvs_eq. intros ?; split⇒ n r rl ? ? HP k Ef' σ rf rfl ???.
destruct (HP k (Ef∪Ef') σ rf rfl) as (r'&?&?); rewrite ?(assoc_L _); eauto.
by ∃ r'; rewrite -(assoc_L _).
Qed.
Lemma pvs_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
Proof.
rewrite pvs_eq.
uPred.unseal; split; intros n r rl ? ? (r1&r2&rl1&rl2&Hr&Hrl&HP&HQ) k Ef σ rf rfl ???.
destruct (HP k Ef σ (r2 ⋅ rf) (rl2 ⋅ rfl)) as (r'&?&?); eauto.
{
rewrite ?assoc -(dist_le _ _ _ _ Hr); last lia.
rewrite -(dist_le _ _ _ _ Hrl); last lia; auto.
}
∃ (r' ⋅ r2); split.
- ∃ r', r2, rl1, rl2. split_and?; eauto using dist_le.
eauto using dist_le.
apply uPred_closed with n; auto.
- rewrite (dist_le _ _ _ _ Hrl); last lia.
by rewrite ?right_id -?assoc.
Qed.
Lemma pvs_openI i P : ownI i P ⊢ (|={{[i]},∅}=> ⧆▷ P).
Proof.
rewrite pvs_eq. uPred.unseal; split⇒ -[|n] r rl ? ? Hinv [|k] Ef σ rf rfl ???; try lia.
apply ownI_spec in Hinv as [Hinv Hrl]; auto.
destruct (wsat_open k Ef σ (r ⋅ rf) (rl ⋅ rfl) i P) as (rP&?&?); auto.
{ rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
∃ (rP ⋅ r); split; last by rewrite (left_id_L _ _) -assoc.
eapply uPred_mono with rP rl; eauto using cmra_includedN_l.
split; auto; rewrite (dist_le _ _ _ _ Hrl); last lia; auto.
Qed.
Lemma pvs_closeI i P : (ownI i P ∧ ▷P) ⊢ (|={∅,{[i]}}=> Emp).
Proof.
rewrite pvs_eq. uPred.unseal; split⇒ -[|n] r rl ? ? [HI HP] [|k] Ef σ rf rfl ? HE ?; try lia.
rewrite ownI_spec in HI *; auto; intros (Heq&Hrl).
∃ ∅; split.
- rewrite (dist_le _ _ _ _ Hrl); last lia.
split; auto.
- rewrite left_id; apply wsat_close with P r.
+ eauto using dist_le.
+ set_solver +HE.
+ by rewrite -(left_id_L ∅ (∪) Ef).
+ apply uPred_closed with n; auto.
rewrite -(dist_le _ _ _ _ Hrl); auto.
Qed.
Lemma pvs_closeI_sep i P : (ownI i P ★ ⧆▷P) ⊢ (|={∅,{[i]}}=> Emp).
Proof.
rewrite pvs_eq. uPred.unseal; split⇒ -[|n] r rl Hv Hvl;
intros (x1&y1&x2&y2&Heq&Heql&HI&HP) [|k] Ef σ rf rfl ? HE ?; try lia.
rewrite Heq in Hv *=>Hv.
rewrite {1}Heql in Hvl *=>Hvl.
rewrite ownI_spec in HI *; eauto using cmra_validN_op_r, cmra_validN_op_l.
intros (Heq2&Hrl2).
∃ ∅; split.
- destruct HP as [HP HAff]. rewrite HAff in Heql ×.
rewrite Hrl2 ?left_id. intros Heq1l'.
rewrite (dist_le _ _ _ _ Heq1l'); last lia.
split; auto.
- rewrite left_id; apply wsat_close with P r.
+ rewrite (dist_le _ _ _ _ Heq); eauto using dist_le.
rewrite lookup_wld_op_l; eauto.
apply dist_le with (S n); eauto.
+ set_solver +HE.
+ by rewrite -(left_id_L ∅ (∪) Ef).
+ apply uPred_closed with n; auto.
destruct HP as [HP HAff].
rewrite (dist_le _ _ _ _ Heq); last lia.
rewrite -(dist_le _ _ _ _ HAff); last lia.
apply uPred_mono with y1 y2; eauto using cmra_includedN_r.
Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m ~~>: P → ownG m ={E}=> ∃ m', ■ P m' ∧ ownG m'.
Proof.
rewrite pvs_eq. intros Hup.
uPred.unseal; split⇒ -[|n] r rl ? ? /ownG_spec [Hinv ?] [|k] Ef σ rf rfl ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf (rl ⋅ rfl) m P) as (m'&?&?); eauto.
{ apply cmra_includedN_le with (S n); auto. }
∃ (update_gst m' r); split; [∃ m'; split; [|apply ownG_spec; split; auto]|]; auto.
eapply dist_le; eauto.
Qed.
Lemma pvs_allocI E P : ¬set_finite E → ⧆▷ P ⊢ (|={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P).
Proof.
rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
split⇒ -[|n] r rl ? ? [HP Hrl] [|k] Ef σ rf rfl ???; try lia.
destruct (wsat_alloc k E Ef σ rf (rl ⋅ rfl) P r) as (i&?&?&?); auto.
{ apply uPred_closed with n; eauto. rewrite -(dist_le _ _ _ _ Hrl); eauto. }
∃ (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
split; [|done]. ∃ i; split_and!; rewrite /uPred_holds /= /uPred_holds /= ; auto.
split; eauto using dist_le.
Qed.
Lemma pvs_affine E1 E2 P : (⧆(|={E1, E2}=> P) ⊣⊢ ⧆(|={E1, E2}=> ⧆P))%I.
Proof.
apply (anti_symm (⊢)).
- rewrite pvs_eq. uPred.unseal.
split⇒ -[|n] r rl ?? [HP Hrl]; split; auto;
intros [|k] Ef σ rf rfl ???; try lia.
destruct (HP (S k) Ef σ rf rfl) as (r'&?&?); eauto; try lia.
∃ r'; split; auto. split; eauto using dist_le.
- by rewrite pvs_mono; last apply uPred.affine_elim.
Qed.
Import uPred.
Global Instance pvs_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
Global Instance pvs_flip_mono' E1 E2 :
Proper (flip (⊢) ==> flip (⊢)) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ={E}=> P.
Proof. apply pvs_trans; set_solver. Qed.
Lemma pvs_strip_pvs E P Q : (P ={E}=> Q) → (|={E}=> P) ={E}=> Q.
Proof. move=>->. by rewrite pvs_trans'. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ⊢ |={E1,E2}=> P ★ Q.
Proof. rewrite !(comm _ P%I); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!RelevantP P} :
P ∧ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ★ Q.
Proof. rewrite -{1}(relevant_relevant' P).
rewrite !relevant_and_sep_l_1 pvs_frame_l relevant_elim //=.
Qed.
Lemma pvs_always_r E1 E2 P Q `{!RelevantP Q} :
(|={E1,E2}=> P) ∧ Q ⊢ |={E1,E2}=> P ★ Q.
Proof. rewrite -(comm _ Q) -(comm _ Q). eapply pvs_always_l; auto. Qed.
Lemma pvs_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
Lemma pvs_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=> P ★ Q.
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Λ Σ) (m : gmap K A) :
([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [★ map] k↦x ∈ m, Φ k x.
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; auto using pvs_intro.
by rewrite IH pvs_sep.
Qed.
Lemma pvs_big_sepS `{Countable A} E (Φ : A → iProp Λ Σ) X :
([★ set] x ∈ X, |={E}=> Φ x) ={E}=> [★ set] x ∈ X, Φ x.
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; csimpl; auto using pvs_intro.
by rewrite IH pvs_sep.
Qed.
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → (|={E1',E2'}=> P) ={E1,E2}=> P.
Proof.
intros HE1 HE2 HEE.
rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
by rewrite {2}HEE -!union_difference_L.
Qed.
Lemma pvs_openI' E i P : i ∈ E → ownI i P ⊢ |={E, E ∖ {[i]}}=> ⧆▷ P.
Proof. intros. etrans. apply pvs_openI. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_closeI' E i P : i ∈ E → (ownI i P ∧ ▷ P) ⊢ |={E ∖ {[i]}, E}=> Emp.
Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_closeI_sep' E i P : i ∈ E → (ownI i P ★ ⧆▷ P) ⊢ |={E ∖ {[i]}, E}=> Emp.
Proof. intros. etrans. apply pvs_closeI_sep. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
(P ⊢ Q) → (|={E1',E2'}=> P) ={E1,E2}=> Q.
Proof. intros HE1 HE2 HEE →. by apply pvs_mask_frame'. Qed.
Global Instance pvs_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
Global Instance pvs_flip_mono' E1 E2 :
Proper (flip (⊢) ==> flip (⊢)) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ={E}=> P.
Proof. apply pvs_trans; set_solver. Qed.
Lemma pvs_strip_pvs E P Q : (P ={E}=> Q) → (|={E}=> P) ={E}=> Q.
Proof. move=>->. by rewrite pvs_trans'. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ⊢ |={E1,E2}=> P ★ Q.
Proof. rewrite !(comm _ P%I); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!RelevantP P} :
P ∧ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ★ Q.
Proof. rewrite -{1}(relevant_relevant' P).
rewrite !relevant_and_sep_l_1 pvs_frame_l relevant_elim //=.
Qed.
Lemma pvs_always_r E1 E2 P Q `{!RelevantP Q} :
(|={E1,E2}=> P) ∧ Q ⊢ |={E1,E2}=> P ★ Q.
Proof. rewrite -(comm _ Q) -(comm _ Q). eapply pvs_always_l; auto. Qed.
Lemma pvs_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.
Lemma pvs_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=> P ★ Q.
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
Lemma pvs_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Λ Σ) (m : gmap K A) :
([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [★ map] k↦x ∈ m, Φ k x.
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; auto using pvs_intro.
by rewrite IH pvs_sep.
Qed.
Lemma pvs_big_sepS `{Countable A} E (Φ : A → iProp Λ Σ) X :
([★ set] x ∈ X, |={E}=> Φ x) ={E}=> [★ set] x ∈ X, Φ x.
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; csimpl; auto using pvs_intro.
by rewrite IH pvs_sep.
Qed.
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → (|={E1',E2'}=> P) ={E1,E2}=> P.
Proof.
intros HE1 HE2 HEE.
rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
by rewrite {2}HEE -!union_difference_L.
Qed.
Lemma pvs_openI' E i P : i ∈ E → ownI i P ⊢ |={E, E ∖ {[i]}}=> ⧆▷ P.
Proof. intros. etrans. apply pvs_openI. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_closeI' E i P : i ∈ E → (ownI i P ∧ ▷ P) ⊢ |={E ∖ {[i]}, E}=> Emp.
Proof. intros. etrans. apply pvs_closeI. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_closeI_sep' E i P : i ∈ E → (ownI i P ★ ⧆▷ P) ⊢ |={E ∖ {[i]}, E}=> Emp.
Proof. intros. etrans. apply pvs_closeI_sep. apply pvs_mask_frame'; set_solver. Qed.
Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
(P ⊢ Q) → (|={E1',E2'}=> P) ={E1,E2}=> Q.
Proof. intros HE1 HE2 HEE →. by apply pvs_mask_frame'. Qed.
It should be possible to give a stronger version of this rule
that does not force the conclusion view shift to have twice the
same mask. However, even expressing the side-conditions on the
mask becomes really ugly then, and we have not found an instance
where that would be useful.
Lemma pvs_trans3 E1 E2 Q :
E2 ⊆ E1 → (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ={E1}=> Q.
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=> P.
Proof. auto using pvs_mask_frame'. Qed.
Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ={E}=> ownG m'.
Proof.
intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim⇒ m''; apply uPred.pure_elim_l⇒ →.
Qed.
End pvs.
E2 ⊆ E1 → (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ={E1}=> Q.
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=> P.
Proof. auto using pvs_mask_frame'. Qed.
Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ={E}=> ownG m'.
Proof.
intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim⇒ m''; apply uPred.pure_elim_l⇒ →.
Qed.
End pvs.
Notation FSA Λ Σ A := (coPset → (A → iProp Λ Σ) → iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
fsa_mask_frame_mono E1 E2 Φ Ψ :
E1 ⊆ E2 → (∀ a, Φ a ⊢ Ψ a) → fsa E1 Φ ⊢ fsa E2 Ψ;
fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊢ fsa E Φ;
fsa_open_close E1 E2 Φ :
fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊢ fsa E1 Φ;
fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊢ fsa E (λ a, Φ a ★ P)
}.
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
fsa_mask_frame_mono E1 E2 Φ Ψ :
E1 ⊆ E2 → (∀ a, Φ a ⊢ Ψ a) → fsa E1 Φ ⊢ fsa E2 Ψ;
fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊢ fsa E Φ;
fsa_open_close E1 E2 Φ :
fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊢ fsa E1 Φ;
fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊢ fsa E (λ a, Φ a ★ P)
}.
Affine Frame Shift Assertion -- (an even more horrible name)
only allows framing affine resources.
Class AffineFrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
afsa_mask_frame_mono E1 E2 Φ Ψ :
E1 ⊆ E2 → (∀ a, Φ a ⊢ Ψ a) → fsa E1 Φ ⊢ fsa E2 Ψ;
afsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊢ fsa E Φ;
afsa_open_close E1 E2 Φ :
fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊢ fsa E1 Φ;
afsa_frame_r E P Φ `{AffineP _ P} : (fsa E Φ ★ P) ⊢ fsa E (λ a, Φ a ★ P)
}.
Create HintDb fsaV.
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
Implicit Types Φ Ψ : A → iProp Λ Σ.
Import uPred.
Lemma fsa_mono E Φ Ψ : (∀ a, Φ a ⊢ Ψ a) → fsa E Φ ⊢ fsa E Ψ.
Proof. apply fsa_mask_frame_mono; auto. Qed.
Lemma fsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → fsa E1 Φ ⊢ fsa E2 Φ.
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
Lemma fsa_frame_l E P Φ : P ★ fsa E Φ ⊢ fsa E (λ a, P ★ Φ a).
Proof. rewrite comm fsa_frame_r. apply fsa_mono⇒a. by rewrite comm. Qed.
Lemma fsa_strip_pvs E P Φ : (P ⊢ fsa E Φ) → (|={E}=> P) ⊢ fsa E Φ.
Proof.
move=>->. rewrite -{2}fsa_trans3.
apply pvs_mono, fsa_mono⇒a; apply pvs_intro.
Qed.
Lemma fsa_pvs_fsa E Φ : (|={E}=> fsa E Φ) ⊣⊢ fsa E Φ.
Proof. apply (anti_symm (⊢)); [by apply fsa_strip_pvs|apply pvs_intro]. Qed.
Lemma pvs_fsa_fsa E Φ : fsa E (λ a, |={E}=> Φ a) ⊣⊢ fsa E Φ.
Proof.
apply (anti_symm (⊢)); [|apply fsa_mono⇒ a; apply pvs_intro].
by rewrite (pvs_intro E (fsa E _)) fsa_trans3.
Qed.
Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ={E}=> Ψ a) → fsa E Φ ⊢ fsa E Ψ.
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
Lemma fsa_wand_l E Φ Ψ : (∀ a, Φ a -★ Ψ a) ★ fsa E Φ ⊢ fsa E Ψ.
Proof.
rewrite fsa_frame_l. apply fsa_mono⇒ a.
by rewrite (forall_elim a) wand_elim_l.
Qed.
Lemma fsa_wand_r E Φ Ψ : fsa E Φ ★ (∀ a, Φ a -★ Ψ a) ⊢ fsa E Ψ.
Proof. by rewrite (comm _ (fsa _ _)) fsa_wand_l. Qed.
Instance fsa_afsa : AffineFrameShiftAssertion fsaV fsa.
Proof.
split; eauto using fsa_mask_frame_mono, fsa_trans3, fsa_open_close, fsa_frame_r.
Qed.
End fsa.
Section afsa.
Context {Λ Σ A} (afsa : FSA Λ Σ A) `{!AffineFrameShiftAssertion fsaV afsa}.
Implicit Types Φ Ψ : A → iProp Λ Σ.
Import uPred.
Lemma afsa_mono E Φ Ψ : (∀ a, Φ a ⊢ Ψ a) → afsa E Φ ⊢ afsa E Ψ.
Proof. apply afsa_mask_frame_mono; auto. Qed.
Lemma afsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → afsa E1 Φ ⊢ afsa E2 Φ.
Proof. intros. apply afsa_mask_frame_mono; auto. Qed.
Lemma afsa_frame_l E (P: iProp Λ Σ) Φ `{AffineP _ P} : (P ★ afsa E Φ) ⊢ afsa E (λ a, P ★ Φ a).
Proof. rewrite comm afsa_frame_r. apply afsa_mono⇒a. by rewrite comm. Qed.
Lemma afsa_strip_pvs E P Φ : (P ⊢ afsa E Φ) → (|={E}=> P) ⊢ afsa E Φ.
Proof.
move=>->. rewrite -{2}afsa_trans3.
apply pvs_mono, afsa_mono⇒a; apply pvs_intro.
Qed.
Lemma afsa_pvs_afsa E Φ : (|={E}=> afsa E Φ) ⊣⊢ afsa E Φ.
Proof. apply (anti_symm (⊢)); [by apply afsa_strip_pvs|apply pvs_intro]. Qed.
Lemma pvs_afsa_afsa E Φ : afsa E (λ a, |={E}=> Φ a) ⊣⊢ afsa E Φ.
Proof.
apply (anti_symm (⊢)); [|apply afsa_mono⇒ a; apply pvs_intro].
by rewrite (pvs_intro E (afsa E _)) afsa_trans3.
Qed.
Lemma afsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊢ (|={E}=> Ψ a)) → afsa E Φ ⊢ afsa E Ψ.
Proof. intros. rewrite -[afsa E Ψ]afsa_trans3 -pvs_intro. by apply afsa_mono. Qed.
Lemma afsa_wand_l E Φ Ψ : (⧆(∀ a, Φ a -★ Ψ a) ★ afsa E Φ) ⊢ (afsa E Ψ).
Proof.
rewrite afsa_frame_l. apply afsa_mono⇒ a.
by rewrite (forall_elim a) affine_elim wand_elim_l.
Qed.
Lemma afsa_wand_r E Φ Ψ : (afsa E Φ ★ ⧆(∀ a, Φ a -★ Ψ a)) ⊢ (afsa E Ψ).
Proof. by rewrite (comm _ (afsa _ _)) afsa_wand_l. Qed.
End afsa.
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
Arguments pvs_fsa _ _ _ _/.
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
Proof.
rewrite /pvs_fsa.
split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
Qed.
Instance pvs_afsa_prf {Λ Σ} : AffineFrameShiftAssertion True (@pvs_fsa Λ Σ).
Proof.
rewrite /pvs_fsa.
split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
Qed.
afsa_mask_frame_mono E1 E2 Φ Ψ :
E1 ⊆ E2 → (∀ a, Φ a ⊢ Ψ a) → fsa E1 Φ ⊢ fsa E2 Ψ;
afsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊢ fsa E Φ;
afsa_open_close E1 E2 Φ :
fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊢ fsa E1 Φ;
afsa_frame_r E P Φ `{AffineP _ P} : (fsa E Φ ★ P) ⊢ fsa E (λ a, Φ a ★ P)
}.
Create HintDb fsaV.
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
Implicit Types Φ Ψ : A → iProp Λ Σ.
Import uPred.
Lemma fsa_mono E Φ Ψ : (∀ a, Φ a ⊢ Ψ a) → fsa E Φ ⊢ fsa E Ψ.
Proof. apply fsa_mask_frame_mono; auto. Qed.
Lemma fsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → fsa E1 Φ ⊢ fsa E2 Φ.
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
Lemma fsa_frame_l E P Φ : P ★ fsa E Φ ⊢ fsa E (λ a, P ★ Φ a).
Proof. rewrite comm fsa_frame_r. apply fsa_mono⇒a. by rewrite comm. Qed.
Lemma fsa_strip_pvs E P Φ : (P ⊢ fsa E Φ) → (|={E}=> P) ⊢ fsa E Φ.
Proof.
move=>->. rewrite -{2}fsa_trans3.
apply pvs_mono, fsa_mono⇒a; apply pvs_intro.
Qed.
Lemma fsa_pvs_fsa E Φ : (|={E}=> fsa E Φ) ⊣⊢ fsa E Φ.
Proof. apply (anti_symm (⊢)); [by apply fsa_strip_pvs|apply pvs_intro]. Qed.
Lemma pvs_fsa_fsa E Φ : fsa E (λ a, |={E}=> Φ a) ⊣⊢ fsa E Φ.
Proof.
apply (anti_symm (⊢)); [|apply fsa_mono⇒ a; apply pvs_intro].
by rewrite (pvs_intro E (fsa E _)) fsa_trans3.
Qed.
Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ={E}=> Ψ a) → fsa E Φ ⊢ fsa E Ψ.
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
Lemma fsa_wand_l E Φ Ψ : (∀ a, Φ a -★ Ψ a) ★ fsa E Φ ⊢ fsa E Ψ.
Proof.
rewrite fsa_frame_l. apply fsa_mono⇒ a.
by rewrite (forall_elim a) wand_elim_l.
Qed.
Lemma fsa_wand_r E Φ Ψ : fsa E Φ ★ (∀ a, Φ a -★ Ψ a) ⊢ fsa E Ψ.
Proof. by rewrite (comm _ (fsa _ _)) fsa_wand_l. Qed.
Instance fsa_afsa : AffineFrameShiftAssertion fsaV fsa.
Proof.
split; eauto using fsa_mask_frame_mono, fsa_trans3, fsa_open_close, fsa_frame_r.
Qed.
End fsa.
Section afsa.
Context {Λ Σ A} (afsa : FSA Λ Σ A) `{!AffineFrameShiftAssertion fsaV afsa}.
Implicit Types Φ Ψ : A → iProp Λ Σ.
Import uPred.
Lemma afsa_mono E Φ Ψ : (∀ a, Φ a ⊢ Ψ a) → afsa E Φ ⊢ afsa E Ψ.
Proof. apply afsa_mask_frame_mono; auto. Qed.
Lemma afsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → afsa E1 Φ ⊢ afsa E2 Φ.
Proof. intros. apply afsa_mask_frame_mono; auto. Qed.
Lemma afsa_frame_l E (P: iProp Λ Σ) Φ `{AffineP _ P} : (P ★ afsa E Φ) ⊢ afsa E (λ a, P ★ Φ a).
Proof. rewrite comm afsa_frame_r. apply afsa_mono⇒a. by rewrite comm. Qed.
Lemma afsa_strip_pvs E P Φ : (P ⊢ afsa E Φ) → (|={E}=> P) ⊢ afsa E Φ.
Proof.
move=>->. rewrite -{2}afsa_trans3.
apply pvs_mono, afsa_mono⇒a; apply pvs_intro.
Qed.
Lemma afsa_pvs_afsa E Φ : (|={E}=> afsa E Φ) ⊣⊢ afsa E Φ.
Proof. apply (anti_symm (⊢)); [by apply afsa_strip_pvs|apply pvs_intro]. Qed.
Lemma pvs_afsa_afsa E Φ : afsa E (λ a, |={E}=> Φ a) ⊣⊢ afsa E Φ.
Proof.
apply (anti_symm (⊢)); [|apply afsa_mono⇒ a; apply pvs_intro].
by rewrite (pvs_intro E (afsa E _)) afsa_trans3.
Qed.
Lemma afsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊢ (|={E}=> Ψ a)) → afsa E Φ ⊢ afsa E Ψ.
Proof. intros. rewrite -[afsa E Ψ]afsa_trans3 -pvs_intro. by apply afsa_mono. Qed.
Lemma afsa_wand_l E Φ Ψ : (⧆(∀ a, Φ a -★ Ψ a) ★ afsa E Φ) ⊢ (afsa E Ψ).
Proof.
rewrite afsa_frame_l. apply afsa_mono⇒ a.
by rewrite (forall_elim a) affine_elim wand_elim_l.
Qed.
Lemma afsa_wand_r E Φ Ψ : (afsa E Φ ★ ⧆(∀ a, Φ a -★ Ψ a)) ⊢ (afsa E Ψ).
Proof. by rewrite (comm _ (afsa _ _)) afsa_wand_l. Qed.
End afsa.
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Φ, (|={E}=> Φ ())%I.
Arguments pvs_fsa _ _ _ _/.
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
Proof.
rewrite /pvs_fsa.
split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
Qed.
Instance pvs_afsa_prf {Λ Σ} : AffineFrameShiftAssertion True (@pvs_fsa Λ Σ).
Proof.
rewrite /pvs_fsa.
split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
Qed.