From stdpp Require Export coPset. From fri.algebra Require Export upred updates. From fri.program_logic Require Export model. From fri.program_logic Require Import ownership wsat. From iris.proofmode Require Import tactics classes. Local Hint Extern 10 (_ ≤ _) => lia. 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 lia end; solve_validN. Import uPred. 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. - exists (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. Global Instance pvs_FUpd {Λ Σ} : FUpd _ := @pvs Λ Σ. Global Instance pvs_BUpd {Λ Σ} : BUpd _ := @pvs Λ Σ ⊤ ⊤. (* 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) : stdpp_scope. Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q) (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope. (* Infix "-∗" := bi_wand. 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") : bi_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. lia. 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; exists 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_FUpd pvs_eq. split=> n r ? HP k Ef σ rf ???; exists 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_FUpd pvs_eq. intros HPQ; split=> n r rl ? ? HP k Ef σ rf rfl ???. destruct (HP k Ef σ rf rfl) as (r2&?&?); eauto. exists r2; eauto using uPred_in_entails. Qed. Lemma pvs_trans E1 E2 E3 P : E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P. Proof. rewrite /pvs_FUpd 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_FUpd 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 exists r'; rewrite -(assoc_L _). Qed. Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) ∗ Q)%I ={E1,E2}=> P ∗ Q. Proof. rewrite /pvs_FUpd 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. } exists (r' ⋅ r2); split. - exists 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_FUpd 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. } exists (rP ⋅ r); split; last by rewrite (left_id_L _ _) -assoc. eapply uPred_mono with rP rl; eauto using cmra_includedN_l. unseal; split; auto; rewrite (dist_le _ _ _ _ Hrl); last lia; auto; split; auto. Qed. Lemma pvs_closeI i P : (ownI i P ∧ ▷P) ⊢ (|={∅,{[i]}}=> emp). Proof. rewrite /pvs_FUpd 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). exists ∅; 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_FUpd 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). exists ∅; split. - move: HP. unseal. intros [HAff HP]. 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. move: HP. unseal. intros [HAff HP]. 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_FUpd 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. } exists (update_gst m' r); split; [exists 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_FUpd pvs_eq. intros ?; rewrite /ownI; unseal. unseal. split=> -[|n] r rl ? ? [Hrl HP] [|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. } exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅). split; [|done]. exists i; split_and!; rewrite /uPred_holds /= /uPred_holds /= ; auto. split; eauto. eapply dist_le with (S n); eauto. Qed. Lemma pvs_affine E1 E2 P : (⧆(|={E1, E2}=> P) ⊣⊢ ⧆(|={E1, E2}=> ⧆P))%I. Proof. apply (anti_symm (⊢)). - rewrite !/pvs_FUpd pvs_eq //=. unfold_bi. unseal. split=> -[|n] r rl ?? [Hrl HP]; split; auto; intros [|k] Ef σ rf rfl ???; try lia. destruct (HP (S k) Ef σ rf rfl) as (r'&?&?); eauto; try lia. exists r'; split; auto. split; eauto. apply dist_le with (S n); eauto. - rewrite -pvs_mono; eauto. Qed. (** * Derived rules *) 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_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_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 pure_elim_l=> ->. Qed. Lemma except_0_pvs E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P. Proof. rewrite /pvs_FUpd pvs_eq /sbi_except_0; unseal. split=> n r rl ? ? HP k Ef σ rf rfl ???. destruct n; first by lia. destruct HP as [Hfalse|HP]. - rewrite /uPred_holds//= in Hfalse. - rewrite //= in HP. edestruct HP; eauto. Qed. (** Proofmode class instances *) Section proofmode_classes. Global Instance from_pure_pvs b E P φ : FromPure b P φ → FromPure b (|={E,E}=> P)%I φ. Proof. rewrite /FromPure. intros <-. apply pvs_intro. Qed. (* Global Instance from_assumption_pvs E p P Q : FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I. Proof. rewrite /FromAssumption=>->. apply bupd_pvs. Qed. *) Global Instance into_wand_pvs E p q R P Q : IntoWand false false R P Q → IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q). Proof. rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR. apply wand_intro_l. by rewrite pvs_sep wand_elim_r. Qed. Global Instance into_wand_pvs_persistent E1 E2 p q R P Q : IntoWand false q R P Q → IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q). Proof. rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR. apply wand_intro_l. by rewrite pvs_frame_l wand_elim_r. Qed. Global Instance into_wand_pvs_args E1 E2 p q R P Q : IntoWand p false R P Q → IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q). Proof. rewrite /IntoWand' /IntoWand /= => ->. apply wand_intro_l. by rewrite intuitionistically_if_elim pvs_wand_r. 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 from_or_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 from_exist_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 p E1 E2 R P Q : Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q). Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed. Global Instance is_except_0_pvs E1 E2 P : IsExcept0 (|={E1,E2}=> P). Proof. rewrite /IsExcept0. apply except_0_pvs. Qed. Lemma modality_pvs_mixin E: modality_mixin (@pvs Λ Σ E E) MIEnvId MIEnvId. Proof. split. - intros P. apply pvs_intro. - intros P. apply pvs_intro. - apply pvs_intro. - intros P Q ?. by apply pvs_mono. - intros P Q. by apply pvs_sep. Qed. Definition modality_pvs E := Modality _ (modality_pvs_mixin E). Global Instance from_modal_pvs E P : FromModal (modality_pvs E) (True : iProp Λ Σ)%I (|={E}=> P)%I P. Proof. rewrite /FromModal => //=. Qed. Global Instance elim_modal_pvs_pvs E1 E2 E3 P Q : ElimModal (E2 ⊆ E1 ∪ E3) p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q). Proof. intros. rewrite /ElimModal bi.intuitionistically_if_elim => ?. rewrite pvs_frame_r wand_elim_r pvs_trans //=. Qed. End proofmode_classes. Hint Extern 2 (environments.of_envs _ ⊢ |={_}=> _) => iModIntro. End pvs. (** * Frame Shift Assertions. *) (* Yes, the name is horrible... Frame Shift Assertions take a mask and a predicate over some type (that's their "postcondition"). They support weakening the mask, framing resources into the postcondition, and composition witn mask-changing view shifts. *) 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) }. (** 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 Φ `{Affine _ P} : (fsa E Φ ∗ P) ⊢ fsa E (λ a, Φ a ∗ P) }. (* Used to solve side-conditions related to [fsaV] *) 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. Global Instance is_except_0_fsa E Ψ: IsExcept0 (fsa E Ψ). Proof. rewrite /IsExcept0. iIntros "HP". iApply fsa_pvs_fsa. iMod "HP". by iModIntro. 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 Λ Σ) Φ `{Affine _ 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) affinely_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. Global Instance is_except_0_afsa E Ψ: IsExcept0 (afsa E Ψ). Proof. rewrite /IsExcept0. iIntros "HP". iApply afsa_pvs_afsa. iMod "HP". by iModIntro. 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. intros. rewrite pvs_frame_r. done. Qed. Instance pvs_afsa_prf {Λ Σ} : AffineFrameShiftAssertion True (@pvs_fsa Λ Σ). Proof. rewrite /pvs_fsa. split; auto using pvs_mask_frame_mono, pvs_trans3. intros. rewrite pvs_frame_r. done. Qed. Global Instance elim_modal_fsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ: FrameShiftAssertion fsaV fsa → ElimModal True false false (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ). Proof. rewrite /ElimModal /= => FSA H. iIntros "(H1&H2)". iApply fsa_pvs_fsa. iMod "H1"; first by set_solver. iModIntro. by iApply "H2". Qed. Global Instance elim_modal_afsa {Λ Σ} {V: Type} (fsa : FSA Λ Σ V) fsaV E1 P Ψ p: AffineFrameShiftAssertion fsaV fsa → ElimModal True p false (|={E1}=> P) P (fsa E1 Ψ) (fsa E1 Ψ). Proof. rewrite /ElimModal intuitionistically_if_elim /= => FSA H. iIntros "(H1&H2)". iApply afsa_pvs_afsa. iMod "H1"; first by set_solver. iModIntro. by iApply "H2". Qed.