diff --git a/_CoqProject b/_CoqProject index 623fce6cc6d71ffdc1b58419dff44ec34dd083dc..4ddfcad2828c5bac0ccd3d904367d4bc1cd0b650 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,7 @@ theories/algebra/proofmode_classes.v theories/bi/interface.v theories/bi/derived_connectives.v theories/bi/derived_laws.v +theories/bi/plainly.v theories/bi/big_op.v theories/bi/updates.v theories/bi/bi.v diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v index 0972828f21cd098bb28f9c521b88b4f5955de0b5..c126c39334338cf2e5834754ecaeb6bbb9851d17 100644 --- a/theories/base_logic/derived.v +++ b/theories/base_logic/derived.v @@ -30,11 +30,8 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M). Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed. Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True. Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed. -Lemma affinely_plainly_cmra_valid {A : cmraT} (a : A) : ■✓ a ⊣⊢ ✓ a. -Proof. - rewrite affine_affinely. - apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. -Qed. +Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■✓ a ⊣⊢ ✓ a. +Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed. Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : â–¡ ✓ a ⊣⊢ ✓ a. Proof. rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim. diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v index 10f0a3b448d1cee136cd7316daaa3d7444bbb9bf..5861c57d92af8c66e13c17ecb848f083dbc49375 100644 --- a/theories/base_logic/lib/fancy_updates.v +++ b/theories/base_logic/lib/fancy_updates.v @@ -1,8 +1,7 @@ From iris.base_logic.lib Require Export own. From stdpp Require Export coPset. From iris.base_logic.lib Require Import wsat. -From iris.algebra Require Import gmap. -From iris.proofmode Require Import tactics classes. +From iris.proofmode Require Import tactics. Set Default Proof Using "Type". Export invG. Import uPred. @@ -10,18 +9,17 @@ Import uPred. Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ := (wsat ∗ ownE E1 ==∗ â—‡ (wsat ∗ ownE E2 ∗ P))%I. Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed. -Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux. -Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux. +Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux. +Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def := + seal_eq uPred_fupd_aux. -Instance fupd_facts `{invG Σ} : FUpdFacts (uPredSI (iResUR Σ)). +Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd. Proof. split. - - apply _. - rewrite uPred_fupd_eq. solve_proper. - intros E1 E2 P (E1''&->&?)%subseteq_disjoint_union_L. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. - by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" . - - rewrite uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". + by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" . - rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame. - rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP". - rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE". @@ -32,6 +30,16 @@ Proof. iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame. iIntros "!> !>". by iApply "HP". - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]". +Qed. +Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) := + {| bi_fupd_mixin := uPred_fupd_mixin |}. + +Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)). +Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed. + +Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)). +Proof. + split. - iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ". rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H". iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro. @@ -41,4 +49,4 @@ Proof. - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]". iAssert (â–· â—‡ P)%I with "[-]" as "#$"; last by iFrame. iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)". -Qed. +Qed. \ No newline at end of file diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v index b7a6e372142ab0c2457de7b47a8fe8c31eeac952..4284299a89ec8ed6fa7d35fbd43edf706e338f1e 100644 --- a/theories/base_logic/upred.v +++ b/theories/base_logic/upred.v @@ -1,5 +1,5 @@ From iris.algebra Require Export cmra updates. -From iris.bi Require Export derived_connectives updates. +From iris.bi Require Export derived_connectives updates plainly. From stdpp Require Import finite. Set Default Proof Using "Type". Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|]. @@ -278,13 +278,13 @@ Definition uPred_wand_eq : (* Equivalently, this could be `∀ y, P n y`. That's closer to the intuition of "embedding the step-indexed logic in Iris", but the two are equivalent because Iris is afine. The following is easier to work with. *) -Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M := +Program Definition uPred_plainly_def {M} : Plainly (uPred M) := λ P, {| uPred_holds n x := P n ε |}. Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN. -Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed. -Definition uPred_plainly {M} := unseal uPred_plainly_aux M. -Definition uPred_plainly_eq : - @uPred_plainly = @uPred_plainly_def := seal_eq uPred_plainly_aux. +Definition uPred_plainly_aux {M} : seal (@uPred_plainly_def M). by eexists. Qed. +Definition uPred_plainly {M} := unseal (@uPred_plainly_aux M). +Definition uPred_plainly_eq M : + @plainly _ uPred_plainly = @uPred_plainly_def M := seal_eq uPred_plainly_aux. Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M := {| uPred_holds n x := P n (core x) |}. @@ -336,7 +336,7 @@ Next Obligation. eauto using uPred_mono, cmra_includedN_l. Qed. Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed. -Instance uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux. +Definition uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux. Definition uPred_bupd_eq {M} : @bupd _ uPred_bupd = @uPred_bupd_def M := seal_eq uPred_bupd_aux. @@ -347,11 +347,11 @@ Definition unseal_eqs := uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, @uPred_bupd_eq). Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *) - unfold bi_emp; simpl; + unfold bi_emp; simpl; unfold sbi_emp; simpl; unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist, - bi_sep, bi_wand, bi_plainly, bi_persistently, sbi_internal_eq, sbi_later; simpl; + bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl; unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist, - sbi_internal_eq, sbi_sep, sbi_wand, sbi_plainly, sbi_persistently; simpl; + sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl; rewrite !unseal_eqs /=. End uPred_unseal. Import uPred_unseal. @@ -361,7 +361,7 @@ Local Arguments uPred_holds {_} !_ _ _ /. Lemma uPred_bi_mixin (M : ucmraT) : BiMixin uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl - (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand uPred_plainly + (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand uPred_persistently. Proof. split. @@ -398,9 +398,6 @@ Proof. intros n P P' HP Q Q' HQ; split=> n' x ??. unseal; split; intros HPQ x' n'' ???; apply HQ, HPQ, HP; eauto using cmra_validN_op_r. - - (* NonExpansive uPred_plainly *) - intros n P1 P2 HP. - unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN. - (* NonExpansive uPred_persistently *) intros n P1 P2 HP. unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN. @@ -460,32 +457,12 @@ Proof. - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *) intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst. eapply HPQR; eauto using cmra_validN_op_l. - - (* (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q *) - intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN. - - (* bi_plainly P ⊢ bi_persistently P *) - unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. - - (* bi_plainly P ⊢ bi_plainly (bi_plainly P) *) - unseal; split=> n x ?? //. - - (* (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a) *) - by unseal. - - (* (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q) *) - unseal; split=> /= n x ? HPQ n' x' ????. - eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN]. - apply (HPQ n' x); eauto using cmra_validN_le. - - (* (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q) *) - unseal; split=> /= n x ? HPQ n' x' ????. - eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN]. - apply (HPQ n' x); eauto using cmra_validN_le. - - (* P ⊢ bi_plainly emp (ADMISSIBLE) *) - by unseal. - - (* bi_plainly P ∗ Q ⊢ bi_plainly P *) - intros P Q. move: (uPred_persistently P)=> P'. - unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst; - eauto using uPred_mono, cmra_includedN_l. - (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *) intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN. - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *) intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. + - (* P ⊢ bi_persistently emp (ADMISSIBLE) *) + by unseal. - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *) by unseal. - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *) @@ -499,10 +476,10 @@ Proof. exists (core x), x; rewrite ?cmra_core_l; auto. Qed. -Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin uPred_ofe_mixin - uPred_entails uPred_pure uPred_and uPred_or uPred_impl - (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand - uPred_plainly uPred_persistently (@uPred_internal_eq M) uPred_later. +Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin + uPred_entails uPred_pure uPred_or uPred_impl + (@uPred_forall M) (@uPred_exist M) uPred_sep + uPred_persistently (@uPred_internal_eq M) uPred_later. Proof. split. - (* Contractive sbi_later *) @@ -523,10 +500,6 @@ Proof. by unseal. - (* Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌠*) intros A a b ?. unseal; split=> n x ?; by apply (discrete_iff n). - - (* bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *) - unseal; split=> n x ? /= HPQ. split=> n' x' ??. - move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?. - move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver. - (* Next x ≡ Next y ⊢ â–· (x ≡ y) *) by unseal. - (* â–· (x ≡ y) ⊢ Next x ≡ Next y *) @@ -550,10 +523,6 @@ Proof. - (* â–· P ∗ â–· Q ⊢ â–· (P ∗ Q) *) intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)]. exists x1, x2; eauto using dist_S. - - (* â–· bi_plainly P ⊢ bi_plainly (â–· P) *) - by unseal. - - (* bi_plainly (â–· P) ⊢ â–· bi_plainly P *) - by unseal. - (* â–· bi_persistently P ⊢ bi_persistently (â–· P) *) by unseal. - (* bi_persistently (â–· P) ⊢ â–· bi_persistently P *) @@ -575,6 +544,74 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid. (* Latest notation *) Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope. +Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly. +Proof. + split. + - (* NonExpansive uPred_plainly *) + intros n P1 P2 HP. + unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN. + - (* (P ⊢ Q) → â– P ⊢ â– Q *) + intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN. + - (* â– P ⊢ bi_persistently P *) + unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN. + - (* â– P ⊢ â– â– P *) + unseal; split=> n x ?? //. + - (* (∀ a, â– (Ψ a)) ⊢ â– (∀ a, Ψ a) *) + by unseal. + - (* (â– P → bi_persistently Q) ⊢ bi_persistently (â– P → Q) *) + unseal; split=> /= n x ? HPQ n' x' ????. + eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN]. + apply (HPQ n' x); eauto using cmra_validN_le. + - (* (â– P → â– Q) ⊢ â– (â– P → Q) *) + unseal; split=> /= n x ? HPQ n' x' ????. + eapply uPred_mono with n' ε=>//; [|by apply cmra_included_includedN]. + apply (HPQ n' x); eauto using cmra_validN_le. + - (* P ⊢ â– emp (ADMISSIBLE) *) + by unseal. + - (* â– P ∗ Q ⊢ â– P *) + intros P Q. move: (uPred_persistently P)=> P'. + unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst; + eauto using uPred_mono, cmra_includedN_l. + - (* â– ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q *) + unseal; split=> n x ? /= HPQ. split=> n' x' ??. + move: HPQ=> [] /(_ n' x'); rewrite !left_id=> ?. + move=> /(_ n' x'); rewrite !left_id=> ?. naive_solver. + - (* â–· â– P ⊢ â– â–· P *) + by unseal. + - (* â– â–· P ⊢ â–· â– P *) + by unseal. +Qed. +Instance uPred_plainlyC M : BiPlainly (uPredSI M) := + {| bi_plainly_mixin := uPred_plainly_mixin M |}. + +Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd. +Proof. + split. + - intros n P Q HPQ. + unseal; split=> n' x; split; intros HP k yf ??; + destruct (HP k yf) as (x'&?&?); auto; + exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l. + - unseal. split=> n x ? HP k yf ?; exists x; split; first done. + apply uPred_mono with n x; eauto using cmra_validN_op_l. + - unseal. intros HPQ; split=> n x ? HP k yf ??. + destruct (HP k yf) as (x'&?&?); eauto. + exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l. + - unseal; split; naive_solver. + - unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??. + destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto. + { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. } + exists (x' â‹… x2); split; first by rewrite -assoc. + exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r. +Qed. +Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}. + +Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M). +Proof. + rewrite /BiBUpdPlainly. unseal; split => n x Hnx /= Hng. + destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto. + eapply uPred_mono; eauto using ucmra_unit_leastN. +Qed. + Module uPred. Include uPred_unseal. Section uPred. @@ -606,7 +643,7 @@ Global Instance cmra_valid_proper {A : cmraT} : Global Instance uPred_affine : BiAffine (uPredI M) | 0. Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed. -Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredI M). +Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M). Proof. unfold BiPlainlyExist. by unseal. Qed. (** Limits *) @@ -660,7 +697,7 @@ Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ (False : u Proof. intros Ha. unseal. split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed. -Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ bi_plainly (✓ a : uPred M). +Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ â– (✓ a : uPred M). Proof. by unseal. Qed. Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a â‹… b) ⊢ (✓ a : uPred M). Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed. @@ -675,30 +712,6 @@ Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : (✓ g : uPred M) ⊣⊢ ∀ i, ✓ g i. Proof. by uPred.unseal. Qed. -(* Basic update modality *) -Global Instance bupd_facts : BUpdFacts (uPredSI M). -Proof. - split. - - intros n P Q HPQ. - unseal; split=> n' x; split; intros HP k yf ??; - destruct (HP k yf) as (x'&?&?); auto; - exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l. - - unseal. split=> n x ? HP k yf ?; exists x; split; first done. - apply uPred_mono with n x; eauto using cmra_validN_op_l. - - unseal. intros HPQ; split=> n x ? HP k yf ??. - destruct (HP k yf) as (x'&?&?); eauto. - exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l. - - unseal; split; naive_solver. - - unseal. split; intros n x ? (x1&x2&Hx&HP&?) k yf ??. - destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto. - { by rewrite assoc -(dist_le _ _ _ _ Hx); last lia. } - exists (x' â‹… x2); split; first by rewrite -assoc. - exists x', x2. eauto using uPred_mono, cmra_validN_op_l, cmra_validN_op_r. - - unseal; split => n x Hnx /= Hng. - destruct (Hng n ε) as [? [_ Hng']]; try rewrite right_id; auto. - eapply uPred_mono; eauto using ucmra_unit_leastN. -Qed. - Lemma bupd_ownM_updateP x (Φ : M → Prop) : x ~~>: Φ → uPred_ownM x ==∗ ∃ y, ⌜Φ y⌠∧ uPred_ownM y. Proof. diff --git a/theories/bi/bi.v b/theories/bi/bi.v index 4cef163c554776a75c9fd03b053716d240e90d0d..d00050dc4309fbd0a9f0b4f3fbfd6b50001e244c 100644 --- a/theories/bi/bi.v +++ b/theories/bi/bi.v @@ -1,4 +1,4 @@ -From iris.bi Require Export derived_laws big_op updates embedding. +From iris.bi Require Export derived_laws big_op updates plainly embedding. Set Default Proof Using "Type". Module Import bi. @@ -16,4 +16,4 @@ Hint Resolve sep_elim_l sep_elim_r sep_mono : BI. Hint Immediate True_intro False_elim : BI. (* Hint Immediate iff_refl internal_eq_refl' : BI. -*) \ No newline at end of file +*) diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v index 3472d004e2a2af15305b93e0d33de27ba92dbedb..d7648e9287febcd3da580f7b3a9af2a9703d6aa8 100644 --- a/theories/bi/big_op.v +++ b/theories/bi/big_op.v @@ -1,5 +1,6 @@ From iris.algebra Require Export big_op. From iris.bi Require Export derived_laws. +From iris.bi Require Import plainly. From stdpp Require Import countable fin_collections functions. Set Default Proof Using "Type". @@ -125,10 +126,6 @@ Section sep_list. ⊢ ([∗ list] k↦x ∈ l, Φ k x) ∧ ([∗ list] k↦x ∈ l, Ψ k x). Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed. - Lemma big_sepL_plainly `{BiAffine PROP} Φ l : - bi_plainly ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, bi_plainly (Φ k x). - Proof. apply (big_opL_commute _). Qed. - Lemma big_sepL_persistently `{BiAffine PROP} Φ l : bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, bi_persistently (Φ k x). @@ -163,16 +160,6 @@ Section sep_list. apply forall_intro=> k. by rewrite (forall_elim (S k)). Qed. - Global Instance big_sepL_nil_plain Φ : - Plain ([∗ list] k↦x ∈ [], Φ k x). - Proof. simpl; apply _. Qed. - Global Instance big_sepL_plain Φ l : - (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x). - Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. - Global Instance big_sepL_plain_id Ps : - TCForall Plain Ps → Plain ([∗] Ps). - Proof. induction 1; simpl; apply _. Qed. - Global Instance big_sepL_nil_persistent Φ : Persistent ([∗ list] k↦x ∈ [], Φ k x). Proof. simpl; apply _. Qed. @@ -278,10 +265,6 @@ Section and_list. ⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x). Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed. - Lemma big_andL_plainly Φ l : - bi_plainly ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, bi_plainly (Φ k x). - Proof. apply (big_opL_commute _). Qed. - Lemma big_andL_persistently Φ l : bi_persistently ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, bi_persistently (Φ k x). @@ -299,19 +282,13 @@ Section and_list. - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)). Qed. - Global Instance big_andL_nil_plain Φ : - Plain ([∧ list] k↦x ∈ [], Φ k x). - Proof. simpl; apply _. Qed. - Global Instance big_andL_plain Φ l : - (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x). - Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. - Global Instance big_andL_nil_persistent Φ : Persistent ([∧ list] k↦x ∈ [], Φ k x). Proof. simpl; apply _. Qed. Global Instance big_andL_persistent Φ l : (∀ k x, Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x). Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. + End and_list. (** ** Big ops over finite maps *) @@ -420,10 +397,6 @@ Section gmap. ⊢ ([∗ map] k↦x ∈ m, Φ k x) ∧ ([∗ map] k↦x ∈ m, Ψ k x). Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed. - Lemma big_sepM_plainly `{BiAffine PROP} Φ m : - bi_plainly ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, bi_plainly (Φ k x). - Proof. apply (big_opM_commute _). Qed. - Lemma big_sepM_persistently `{BiAffine PROP} Φ m : (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)). @@ -464,12 +437,6 @@ Section gmap. by rewrite pure_True // True_impl. Qed. - Global Instance big_sepM_empty_plain Φ : Plain ([∗ map] k↦x ∈ ∅, Φ k x). - Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. - Global Instance big_sepM_plain Φ m : - (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x). - Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed. - Global Instance big_sepM_empty_persistent Φ : Persistent ([∗ map] k↦x ∈ ∅, Φ k x). Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. @@ -596,10 +563,6 @@ Section gset. ([∗ set] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ set] y ∈ X, Φ y) ∧ ([∗ set] y ∈ X, Ψ y). Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed. - Lemma big_sepS_plainly `{BiAffine PROP} Φ X : - bi_plainly ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_plainly (Φ y). - Proof. apply (big_opS_commute _). Qed. - Lemma big_sepS_persistently `{BiAffine PROP} Φ X : bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y). Proof. apply (big_opS_commute _). Qed. @@ -633,12 +596,6 @@ Section gset. by rewrite pure_True ?True_impl; last set_solver. Qed. - Global Instance big_sepS_empty_plain Φ : Plain ([∗ set] x ∈ ∅, Φ x). - Proof. rewrite /big_opS elements_empty. apply _. Qed. - Global Instance big_sepS_plain Φ X : - (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x). - Proof. rewrite /big_opS. apply _. Qed. - Global Instance big_sepS_empty_persistent Φ : Persistent ([∗ set] x ∈ ∅, Φ x). Proof. rewrite /big_opS elements_empty. apply _. Qed. @@ -714,21 +671,11 @@ Section gmultiset. ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y). Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed. - Lemma big_sepMS_plainly `{BiAffine PROP} Φ X : - bi_plainly ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, bi_plainly (Φ y). - Proof. apply (big_opMS_commute _). Qed. - Lemma big_sepMS_persistently `{BiAffine PROP} Φ X : bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, bi_persistently (Φ y). Proof. apply (big_opMS_commute _). Qed. - Global Instance big_sepMS_empty_plain Φ : Plain ([∗ mset] x ∈ ∅, Φ x). - Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed. - Global Instance big_sepMS_plain Φ X : - (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x). - Proof. rewrite /big_opMS. apply _. Qed. - Global Instance big_sepMS_empty_persistent Φ : Persistent ([∗ mset] x ∈ ∅, Φ x). Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed. @@ -773,6 +720,34 @@ Section list. Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps : TCForall Timeless Ps → Timeless ([∗] Ps). Proof. induction 1; simpl; apply _. Qed. + + Section plainly. + Context `{!BiPlainly PROP}. + + Lemma big_sepL_plainly `{!BiAffine PROP} Φ l : + â– ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, â– (Φ k x). + Proof. apply (big_opL_commute _). Qed. + + Global Instance big_sepL_nil_plain `{!BiAffine PROP} Φ : + Plain ([∗ list] k↦x ∈ [], Φ k x). + Proof. simpl; apply _. Qed. + + Global Instance big_sepL_plain `{!BiAffine PROP} Φ l : + (∀ k x, Plain (Φ k x)) → Plain ([∗ list] k↦x ∈ l, Φ k x). + Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. + + Lemma big_andL_plainly Φ l : + â– ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, â– (Φ k x). + Proof. apply (big_opL_commute _). Qed. + + Global Instance big_andL_nil_plain Φ : + Plain ([∧ list] k↦x ∈ [], Φ k x). + Proof. simpl; apply _. Qed. + + Global Instance big_andL_plain Φ l : + (∀ k x, Plain (Φ k x)) → Plain ([∧ list] k↦x ∈ l, Φ k x). + Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed. + End plainly. End list. (** ** Big ops over finite maps *) @@ -795,6 +770,21 @@ Section gmap. Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m : (∀ k x, Timeless (Φ k x)) → Timeless ([∗ map] k↦x ∈ m, Φ k x). Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed. + + Section plainly. + Context `{!BiPlainly PROP}. + + Lemma big_sepM_plainly `{BiAffine PROP} Φ m : + â– ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ [∗ map] k↦x ∈ m, â– (Φ k x). + Proof. apply (big_opM_commute _). Qed. + + Global Instance big_sepM_empty_plain `{BiAffine PROP} Φ : + Plain ([∗ map] k↦x ∈ ∅, Φ k x). + Proof. rewrite /big_opM map_to_list_empty. apply _. Qed. + Global Instance big_sepM_plain `{BiAffine PROP} Φ m : + (∀ k x, Plain (Φ k x)) → Plain ([∗ map] k↦x ∈ m, Φ k x). + Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed. + End plainly. End gmap. (** ** Big ops over finite sets *) @@ -817,6 +807,20 @@ Section gset. Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X : (∀ x, Timeless (Φ x)) → Timeless ([∗ set] x ∈ X, Φ x). Proof. rewrite /big_opS. apply _. Qed. + + Section plainly. + Context `{!BiPlainly PROP}. + + Lemma big_sepS_plainly `{BiAffine PROP} Φ X : + â– ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, â– (Φ y). + Proof. apply (big_opS_commute _). Qed. + + Global Instance big_sepS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ set] x ∈ ∅, Φ x). + Proof. rewrite /big_opS elements_empty. apply _. Qed. + Global Instance big_sepS_plain `{BiAffine PROP} Φ X : + (∀ x, Plain (Φ x)) → Plain ([∗ set] x ∈ X, Φ x). + Proof. rewrite /big_opS. apply _. Qed. + End plainly. End gset. (** ** Big ops over finite multisets *) @@ -839,6 +843,20 @@ Section gmultiset. Global Instance big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X : (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x). Proof. rewrite /big_opMS. apply _. Qed. + + Section plainly. + Context `{!BiPlainly PROP}. + + Lemma big_sepMS_plainly `{BiAffine PROP} Φ X : + â– ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, â– (Φ y). + Proof. apply (big_opMS_commute _). Qed. + + Global Instance big_sepMS_empty_plain `{BiAffine PROP} Φ : Plain ([∗ mset] x ∈ ∅, Φ x). + Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed. + Global Instance big_sepMS_plain `{BiAffine PROP} Φ X : + (∀ x, Plain (Φ x)) → Plain ([∗ mset] x ∈ X, Φ x). + Proof. rewrite /big_opMS. apply _. Qed. + End plainly. End gmultiset. End sbi_big_op. End bi. diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v index 1ad05c3aaab07f29ac29662081209db05559bb61..fbd3213ec5da0785ce67333a1f60fa5836f0bbc4 100644 --- a/theories/bi/derived_connectives.v +++ b/theories/bi/derived_connectives.v @@ -13,12 +13,6 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never. Instance: Params (@bi_wand_iff) 1. Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope. -Class Plain {PROP : bi} (P : PROP) := plain : P ⊢ bi_plainly P. -Arguments Plain {_} _%I : simpl never. -Arguments plain {_} _%I {_}. -Hint Mode Plain + ! : typeclass_instances. -Instance: Params (@Plain) 1. - Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P. Arguments Persistent {_} _%I : simpl never. Arguments persistent {_} _%I {_}. @@ -31,8 +25,6 @@ Instance: Params (@bi_affinely) 1. Typeclasses Opaque bi_affinely. Notation "â–¡ P" := (bi_affinely (bi_persistently P))%I (at level 20, right associativity) : bi_scope. -Notation "â– P" := (bi_affinely (bi_plainly P))%I - (at level 20, right associativity) : bi_scope. Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp. Arguments Affine {_} _%I : simpl never. @@ -45,11 +37,6 @@ Existing Instance absorbing_bi | 0. Class BiPositive (PROP : bi) := bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q. -Class BiPlainlyExist (PROP : bi) := - plainly_exist_1 A (Ψ : A → PROP) : - bi_plainly (∃ a, Ψ a) ⊢ ∃ a, bi_plainly (Ψ a). -Arguments plainly_exist_1 _ {_ _} _. - Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I. Arguments bi_absorbingly {_} _%I : simpl never. Instance: Params (@bi_absorbingly) 1. @@ -59,12 +46,6 @@ Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P. Arguments Absorbing {_} _%I : simpl never. Arguments absorbing {_} _%I. -Definition bi_plainly_if {PROP : bi} (p : bool) (P : PROP) : PROP := - (if p then bi_plainly P else P)%I. -Arguments bi_plainly_if {_} !_ _%I /. -Instance: Params (@bi_plainly_if) 2. -Typeclasses Opaque bi_plainly_if. - Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP := (if p then bi_persistently P else P)%I. Arguments bi_persistently_if {_} !_ _%I /. @@ -79,9 +60,6 @@ Typeclasses Opaque bi_affinely_if. Notation "â–¡? p P" := (bi_affinely_if p (bi_persistently_if p P))%I (at level 20, p at level 9, P at level 20, right associativity, format "â–¡? p P") : bi_scope. -Notation "â– ? p P" := (bi_affinely_if p (bi_plainly_if p P))%I - (at level 20, p at level 9, P at level 20, - right associativity, format "â– ? p P") : bi_scope. Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP := match As return himpl As PROP → PROP with diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v index 8e99ebd7dbf99dc4f9aed534e10445fd9e3c1762..474bf1bb7c390a79eb113b99730bcf59f5746860 100644 --- a/theories/bi/derived_laws.v +++ b/theories/bi/derived_laws.v @@ -68,8 +68,6 @@ Proof. intros Φ1 Φ2 HΦ. apply equiv_dist=> n. apply exist_ne=> x. apply equiv_dist, HΦ. Qed. -Global Instance plainly_proper : - Proper ((⊣⊢) ==> (⊣⊢)) (@bi_plainly PROP) := ne_proper _. Global Instance persistently_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_persistently PROP) := ne_proper _. @@ -755,9 +753,6 @@ Proof. apply persistently_mono, impl_elim with P; auto. Qed. -Lemma persistently_emp_intro P : P ⊢ bi_persistently emp. -Proof. by rewrite -plainly_elim_persistently -plainly_emp_intro. Qed. - Lemma persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp. Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed. @@ -941,182 +936,6 @@ Section persistently_affinely_bi. Qed. End persistently_affinely_bi. -(* Properties of the plainness modality *) -Hint Resolve plainly_mono. -Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@bi_plainly PROP). -Proof. intros P Q; apply plainly_mono. Qed. -Global Instance plainly_flip_mono' : - Proper (flip (⊢) ==> flip (⊢)) (@bi_plainly PROP). -Proof. intros P Q; apply plainly_mono. Qed. - -Lemma persistently_plainly P : bi_persistently (bi_plainly P) ⊣⊢ bi_plainly P. -Proof. - apply (anti_symm _). - - by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorbing. - - by rewrite {1}plainly_idemp_2 plainly_elim_persistently. -Qed. -Lemma plainly_persistently P : bi_plainly (bi_persistently P) ⊣⊢ bi_plainly P. -Proof. - apply (anti_symm _). - - rewrite -{1}(left_id True%I bi_and (bi_plainly _)) (plainly_emp_intro True%I). - rewrite -{2}(persistently_and_emp_elim P). - rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[]. - - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P). -Qed. - -Lemma absorbingly_plainly P : bi_absorbingly (bi_plainly P) ⊣⊢ bi_plainly P. -Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed. - -Lemma plainly_and_sep_elim P Q : bi_plainly P ∧ Q -∗ (emp ∧ P) ∗ Q. -Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed. -Lemma plainly_and_sep_assoc P Q R : - bi_plainly P ∧ (Q ∗ R) ⊣⊢ (bi_plainly P ∧ Q) ∗ R. -Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed. -Lemma plainly_and_emp_elim P : emp ∧ bi_plainly P ⊢ P. -Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed. -Lemma plainly_elim_absorbingly P : bi_plainly P ⊢ bi_absorbingly P. -Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed. -Lemma plainly_elim P `{!Absorbing P} : bi_plainly P ⊢ P. -Proof. by rewrite plainly_elim_persistently persistently_elim. Qed. - -Lemma plainly_idemp_1 P : bi_plainly (bi_plainly P) ⊢ bi_plainly P. -Proof. by rewrite plainly_elim_absorbingly absorbingly_plainly. Qed. -Lemma plainly_idemp P : bi_plainly (bi_plainly P) ⊣⊢ bi_plainly P. -Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed. - -Lemma plainly_intro' P Q : (bi_plainly P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q. -Proof. intros <-. apply plainly_idemp_2. Qed. - -Lemma plainly_pure φ : bi_plainly ⌜φ⌠⊣⊢ ⌜φâŒ. -Proof. - apply (anti_symm _); auto. - - by rewrite plainly_elim_persistently persistently_pure. - - apply pure_elim'=> Hφ. - trans (∀ x : False, bi_plainly True : PROP)%I; [by apply forall_intro|]. - rewrite plainly_forall_2. by rewrite -(pure_intro _ φ). -Qed. -Lemma plainly_forall {A} (Ψ : A → PROP) : - bi_plainly (∀ a, Ψ a) ⊣⊢ ∀ a, bi_plainly (Ψ a). -Proof. - apply (anti_symm _); auto using plainly_forall_2. - apply forall_intro=> x. by rewrite (forall_elim x). -Qed. -Lemma plainly_exist_2 {A} (Ψ : A → PROP) : - (∃ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∃ a, Ψ a). -Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed. -Lemma plainly_exist `{BiPlainlyExist PROP} {A} (Ψ : A → PROP) : - bi_plainly (∃ a, Ψ a) ⊣⊢ ∃ a, bi_plainly (Ψ a). -Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed. -Lemma plainly_and P Q : bi_plainly (P ∧ Q) ⊣⊢ bi_plainly P ∧ bi_plainly Q. -Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed. -Lemma plainly_or_2 P Q : bi_plainly P ∨ bi_plainly Q ⊢ bi_plainly (P ∨ Q). -Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed. -Lemma plainly_or `{BiPlainlyExist PROP} P Q : - bi_plainly (P ∨ Q) ⊣⊢ bi_plainly P ∨ bi_plainly Q. -Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed. -Lemma plainly_impl P Q : bi_plainly (P → Q) ⊢ bi_plainly P → bi_plainly Q. -Proof. - apply impl_intro_l; rewrite -plainly_and. - apply plainly_mono, impl_elim with P; auto. -Qed. - -Lemma plainly_sep_dup P : bi_plainly P ⊣⊢ bi_plainly P ∗ bi_plainly P. -Proof. - apply (anti_symm _). - - rewrite -{1}(idemp bi_and (bi_plainly _)). - by rewrite -{2}(left_id emp%I _ (bi_plainly _)) plainly_and_sep_assoc and_elim_l. - - by rewrite plainly_absorbing. -Qed. - -Lemma plainly_and_sep_l_1 P Q : bi_plainly P ∧ Q ⊢ bi_plainly P ∗ Q. -Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qed. -Lemma plainly_and_sep_r_1 P Q : P ∧ bi_plainly Q ⊢ P ∗ bi_plainly Q. -Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed. - -Lemma plainly_True_emp : bi_plainly True ⊣⊢ bi_plainly emp. -Proof. apply (anti_symm _); auto using plainly_emp_intro. Qed. -Lemma plainly_and_sep P Q : bi_plainly (P ∧ Q) ⊢ bi_plainly (P ∗ Q). -Proof. - rewrite plainly_and. - rewrite -{1}plainly_idemp -plainly_and -{1}(left_id emp%I _ Q%I). - by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim. -Qed. - -Lemma plainly_affinely P : bi_plainly (bi_affinely P) ⊣⊢ bi_plainly P. -Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed. - -Lemma and_sep_plainly P Q : - bi_plainly P ∧ bi_plainly Q ⊣⊢ bi_plainly P ∗ bi_plainly Q. -Proof. - apply (anti_symm _); auto using plainly_and_sep_l_1. - apply and_intro. - - by rewrite plainly_absorbing. - - by rewrite comm plainly_absorbing. -Qed. -Lemma plainly_sep_2 P Q : - bi_plainly P ∗ bi_plainly Q ⊢ bi_plainly (P ∗ Q). -Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed. -Lemma plainly_sep `{BiPositive PROP} P Q : - bi_plainly (P ∗ Q) ⊣⊢ bi_plainly P ∗ bi_plainly Q. -Proof. - apply (anti_symm _); auto using plainly_sep_2. - rewrite -plainly_affinely affinely_sep -and_sep_plainly. apply and_intro. - - by rewrite (affinely_elim_emp Q) right_id affinely_elim. - - by rewrite (affinely_elim_emp P) left_id affinely_elim. -Qed. - -Lemma plainly_wand P Q : bi_plainly (P -∗ Q) ⊢ bi_plainly P -∗ bi_plainly Q. -Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed. - -Lemma plainly_entails_l P Q : (P ⊢ bi_plainly Q) → P ⊢ bi_plainly Q ∗ P. -Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed. -Lemma plainly_entails_r P Q : (P ⊢ bi_plainly Q) → P ⊢ P ∗ bi_plainly Q. -Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed. - -Lemma plainly_impl_wand_2 P Q : bi_plainly (P -∗ Q) ⊢ bi_plainly (P → Q). -Proof. - apply plainly_intro', impl_intro_r. - rewrite -{2}(left_id emp%I _ P%I) plainly_and_sep_assoc. - by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l. -Qed. - -Lemma impl_wand_plainly_2 P Q : (bi_plainly P -∗ Q) ⊢ (bi_plainly P → Q). -Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed. - -Lemma valid_plainly P : bi_valid (bi_plainly P) ↔ bi_valid P. -Proof. - rewrite /bi_valid. split; intros HP. - - by rewrite -(idemp bi_and emp%I) {2}HP plainly_and_emp_elim. - - by rewrite (plainly_emp_intro emp%I) HP. -Qed. - -Section plainly_affinely_bi. - Context `{BiAffine PROP}. - - Lemma plainly_emp : bi_plainly emp ⊣⊢ emp. - Proof. by rewrite -!True_emp plainly_pure. Qed. - - Lemma plainly_and_sep_l P Q : bi_plainly P ∧ Q ⊣⊢ bi_plainly P ∗ Q. - Proof. - apply (anti_symm (⊢)); - eauto using plainly_and_sep_l_1, sep_and with typeclass_instances. - Qed. - Lemma plainly_and_sep_r P Q : P ∧ bi_plainly Q ⊣⊢ P ∗ bi_plainly Q. - Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed. - - Lemma plainly_impl_wand P Q : bi_plainly (P → Q) ⊣⊢ bi_plainly (P -∗ Q). - Proof. - apply (anti_symm (⊢)); auto using plainly_impl_wand_2. - apply plainly_intro', wand_intro_l. - by rewrite -plainly_and_sep_r plainly_elim impl_elim_r. - Qed. - - Lemma impl_wand_plainly P Q : (bi_plainly P → Q) ⊣⊢ (bi_plainly P -∗ Q). - Proof. - apply (anti_symm (⊢)). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2. - Qed. -End plainly_affinely_bi. - (* The combined affinely persistently modality *) Lemma affinely_persistently_elim P : â–¡ P ⊢ P. Proof. apply persistently_and_emp_elim. Qed. @@ -1170,52 +989,6 @@ Proof. - apply impl_intro_l. by rewrite persistently_and_affinely_sep_l wand_elim_r. Qed. -(* The combined affinely plainly modality *) -Lemma affinely_plainly_elim P : â– P ⊢ P. -Proof. apply plainly_and_emp_elim. Qed. -Lemma affinely_plainly_intro' P Q : (â– P ⊢ Q) → â– P ⊢ â– Q. -Proof. intros <-. by rewrite plainly_affinely plainly_idemp. Qed. - -Lemma affinely_plainly_emp : â– emp ⊣⊢ emp. -Proof. - by rewrite -plainly_True_emp plainly_pure affinely_True_emp affinely_emp. -Qed. -Lemma affinely_plainly_and P Q : â– (P ∧ Q) ⊣⊢ â– P ∧ â– Q. -Proof. by rewrite plainly_and affinely_and. Qed. -Lemma affinely_plainly_or_2 P Q : â– P ∨ â– Q ⊢ â– (P ∨ Q). -Proof. by rewrite -plainly_or_2 affinely_or. Qed. -Lemma affinely_plainly_or `{BiPlainlyExist PROP} P Q : â– (P ∨ Q) ⊣⊢ â– P ∨ â– Q. -Proof. by rewrite plainly_or affinely_or. Qed. -Lemma affinely_plainly_exist_2 {A} (Φ : A → PROP) : (∃ x, ■Φ x) ⊢ â– (∃ x, Φ x). -Proof. by rewrite -plainly_exist_2 affinely_exist. Qed. -Lemma affinely_plainly_exist `{BiPlainlyExist PROP} {A} (Φ : A → PROP) : - â– (∃ x, Φ x) ⊣⊢ ∃ x, ■Φ x. -Proof. by rewrite plainly_exist affinely_exist. Qed. -Lemma affinely_plainly_sep_2 P Q : â– P ∗ â– Q ⊢ â– (P ∗ Q). -Proof. by rewrite affinely_sep_2 plainly_sep_2. Qed. -Lemma affinely_plainly_sep `{BiPositive PROP} P Q : â– (P ∗ Q) ⊣⊢ â– P ∗ â– Q. -Proof. by rewrite -affinely_sep -plainly_sep. Qed. - -Lemma affinely_plainly_idemp P : â– â– P ⊣⊢ â– P. -Proof. by rewrite plainly_affinely plainly_idemp. Qed. - -Lemma plainly_and_affinely_sep_l P Q : bi_plainly P ∧ Q ⊣⊢ â– P ∗ Q. -Proof. by rewrite -(persistently_plainly P) persistently_and_affinely_sep_l. Qed. -Lemma plainly_and_affinely_sep_r P Q : P ∧ bi_plainly Q ⊣⊢ P ∗ â– Q. -Proof. by rewrite !(comm _ P) plainly_and_affinely_sep_l. Qed. -Lemma and_sep_affinely_plainly P Q : â– P ∧ â– Q ⊣⊢ â– P ∗ â– Q. -Proof. - by rewrite -plainly_and_affinely_sep_l -affinely_and affinely_and_r. -Qed. - -Lemma affinely_plainly_sep_dup P : â– P ⊣⊢ â– P ∗ â– P. -Proof. - by rewrite -plainly_and_affinely_sep_l affinely_and_r affinely_and idemp. -Qed. - -Lemma impl_wand_affinely_plainly P Q : (bi_plainly P → Q) ⊣⊢ (â– P -∗ Q). -Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed. - (* Conditional affinely modality *) Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p). Proof. solve_proper. Qed. @@ -1334,81 +1107,6 @@ Proof. destruct p; simpl; auto using affinely_persistently_sep. Qed. Lemma affinely_persistently_if_idemp p P : â–¡?p â–¡?p P ⊣⊢ â–¡?p P. Proof. destruct p; simpl; auto using affinely_persistently_idemp. Qed. -(* Conditional plainly *) -Global Instance plainly_if_ne p : NonExpansive (@bi_plainly_if PROP p). -Proof. solve_proper. Qed. -Global Instance plainly_if_proper p : - Proper ((⊣⊢) ==> (⊣⊢)) (@bi_plainly_if PROP p). -Proof. solve_proper. Qed. -Global Instance plainly_if_mono' p : - Proper ((⊢) ==> (⊢)) (@bi_plainly_if PROP p). -Proof. solve_proper. Qed. -Global Instance plainly_if_flip_mono' p : - Proper (flip (⊢) ==> flip (⊢)) (@bi_plainly_if PROP p). -Proof. solve_proper. Qed. - -Lemma plainly_if_mono p P Q : (P ⊢ Q) → bi_plainly_if p P ⊢ bi_plainly_if p Q. -Proof. by intros ->. Qed. - -Lemma plainly_if_pure p φ : bi_plainly_if p ⌜φ⌠⊣⊢ ⌜φâŒ. -Proof. destruct p; simpl; auto using plainly_pure. Qed. -Lemma plainly_if_and p P Q : bi_plainly_if p (P ∧ Q) ⊣⊢ bi_plainly_if p P ∧ bi_plainly_if p Q. -Proof. destruct p; simpl; auto using plainly_and. Qed. -Lemma plainly_if_or_2 p P Q : - bi_plainly_if p P ∨ bi_plainly_if p Q ⊢ bi_plainly_if p (P ∨ Q). -Proof. destruct p; simpl; auto using plainly_or_2. Qed. -Lemma plainly_if_or `{BiPlainlyExist PROP} p P Q : - bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P ∨ bi_plainly_if p Q. -Proof. destruct p; simpl; auto using plainly_or. Qed. -Lemma plainly_if_exist_2 {A} p (Ψ : A → PROP) : - (∃ a, bi_plainly_if p (Ψ a)) ⊢ bi_plainly_if p (∃ a, Ψ a). -Proof. destruct p; simpl; auto using plainly_exist_2. Qed. -Lemma plainly_if_exist `{BiPlainlyExist PROP} {A} p (Ψ : A → PROP) : - bi_plainly_if p (∃ a, Ψ a) ⊣⊢ ∃ a, bi_plainly_if p (Ψ a). -Proof. destruct p; simpl; auto using plainly_exist. Qed. -Lemma plainly_if_sep `{BiPositive PROP} p P Q : - bi_plainly_if p (P ∗ Q) ⊣⊢ bi_plainly_if p P ∗ bi_plainly_if p Q. -Proof. destruct p; simpl; auto using plainly_sep. Qed. - -Lemma plainly_if_idemp p P : - bi_plainly_if p (bi_plainly_if p P) ⊣⊢ bi_plainly_if p P. -Proof. destruct p; simpl; auto using plainly_idemp. Qed. - -(* Conditional affinely plainly *) -Lemma affinely_plainly_if_mono p P Q : (P ⊢ Q) → â– ?p P ⊢ â– ?p Q. -Proof. by intros ->. Qed. - -Lemma affinely_plainly_if_elim p P : â– ?p P ⊢ P. -Proof. destruct p; simpl; auto using affinely_plainly_elim. Qed. -Lemma affinely_plainly_affinely_plainly_if p P : â– P ⊢ â– ?p P. -Proof. destruct p; simpl; auto using affinely_plainly_elim. Qed. -Lemma affinely_plainly_if_intro' p P Q : (â– ?p P ⊢ Q) → â– ?p P ⊢ â– ?p Q. -Proof. destruct p; simpl; auto using affinely_plainly_intro'. Qed. - -Lemma affinely_plainly_if_emp p : â– ?p emp ⊣⊢ emp. -Proof. destruct p; simpl; auto using affinely_plainly_emp. Qed. -Lemma affinely_plainly_if_and p P Q : â– ?p (P ∧ Q) ⊣⊢ â– ?p P ∧ â– ?p Q. -Proof. destruct p; simpl; auto using affinely_plainly_and. Qed. -Lemma affinely_plainly_if_or_2 p P Q : â– ?p P ∨ â– ?p Q ⊢ â– ?p (P ∨ Q). -Proof. destruct p; simpl; auto using affinely_plainly_or_2. Qed. -Lemma affinely_plainly_if_or `{BiPlainlyExist PROP} p P Q : - â– ?p (P ∨ Q) ⊣⊢ â– ?p P ∨ â– ?p Q. -Proof. destruct p; simpl; auto using affinely_plainly_or. Qed. -Lemma affinely_plainly_if_exist_2 {A} p (Ψ : A → PROP) : - (∃ a, â– ?p Ψ a) ⊢ â– ?p ∃ a, Ψ a . -Proof. destruct p; simpl; auto using affinely_plainly_exist_2. Qed. -Lemma affinely_plainly_if_exist `{BiPlainlyExist PROP} {A} p (Ψ : A → PROP) : - (â– ?p ∃ a, Ψ a) ⊣⊢ ∃ a, â– ?p Ψ a. -Proof. destruct p; simpl; auto using affinely_plainly_exist. Qed. -Lemma affinely_plainly_if_sep_2 p P Q : â– ?p P ∗ â– ?p Q ⊢ â– ?p (P ∗ Q). -Proof. destruct p; simpl; auto using affinely_plainly_sep_2. Qed. -Lemma affinely_plainly_if_sep `{BiPositive PROP} p P Q : - â– ?p (P ∗ Q) ⊣⊢ â– ?p P ∗ â– ?p Q. -Proof. destruct p; simpl; auto using affinely_plainly_sep. Qed. - -Lemma affinely_plainly_if_idemp p P : â– ?p â– ?p P ⊣⊢ â– ?p P. -Proof. destruct p; simpl; auto using affinely_plainly_idemp. Qed. - (* Properties of persistent propositions *) Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP). Proof. solve_proper. Qed. @@ -1485,17 +1183,6 @@ Section persistent_bi_absorbing. Proof. apply (anti_symm _); auto using impl_wand_1, impl_wand_2. Qed. End persistent_bi_absorbing. -(* Properties of plain propositions *) -Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain PROP). -Proof. solve_proper. Qed. - -Lemma plain_plainly_2 P `{!Plain P} : P ⊢ bi_plainly P. -Proof. done. Qed. -Lemma plain_plainly P `{!Plain P, !Absorbing P} : bi_plainly P ⊣⊢ P. -Proof. apply (anti_symm _), plain_plainly_2, _. apply plainly_elim, _. Qed. -Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ bi_plainly Q. -Proof. by intros <-. Qed. - (* Affine instances *) Global Instance emp_affine_l : Affine (emp%I : PROP). Proof. by rewrite /Affine. Qed. @@ -1555,16 +1242,13 @@ Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_in Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P). Proof. rewrite /bi_absorbingly. apply _. Qed. -Global Instance plainly_absorbing P : Absorbing (bi_plainly P). -Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorbing. Qed. Global Instance persistently_absorbing P : Absorbing (bi_persistently P). Proof. by rewrite /Absorbing absorbingly_persistently. Qed. +Global Instance persistently_if_absorbing P p : + Absorbing P → Absorbing (bi_persistently_if p P). +Proof. intros; destruct p; simpl; apply _. Qed. (* Persistence instances *) -(* Not an instance, see the bottom of this file *) -Lemma plain_persistent P : Plain P → Persistent P. -Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed. - Global Instance pure_persistent φ : Persistent (⌜φâŒ%I : PROP). Proof. by rewrite /Persistent persistently_pure. Qed. Global Instance emp_persistent : Persistent (emp%I : PROP). @@ -1588,19 +1272,10 @@ Proof. apply exist_mono=> x. by rewrite -!persistent. Qed. -Global Instance impl_persistent P Q : - Absorbing P → Plain P → Persistent Q → Persistent (P → Q). -Proof. - intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly - -(persistent Q) (plainly_elim_absorbingly P) absorbing. -Qed. - Global Instance sep_persistent P Q : Persistent P → Persistent Q → Persistent (P ∗ Q). Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed. -Global Instance plainly_persistent P : Persistent (bi_plainly P). -Proof. by rewrite /Persistent persistently_plainly. Qed. Global Instance persistently_persistent P : Persistent (bi_persistently P). Proof. by rewrite /Persistent persistently_idemp. Qed. Global Instance affinely_persistent P : Persistent P → Persistent (bi_affinely P). @@ -1611,66 +1286,6 @@ Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) : (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx). Proof. destruct mx; apply _. Qed. -Global Instance wand_persistent P Q : - Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q). -Proof. - intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (bi_plainly P → Q)). - - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q). - by rewrite affinely_plainly_elim. - - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r. -Qed. - -(* Plainness instances *) -Global Instance pure_plain φ : Plain (⌜φâŒ%I : PROP). -Proof. by rewrite /Plain plainly_pure. Qed. -Global Instance emp_plain : Plain (emp%I : PROP). -Proof. apply plainly_emp_intro. Qed. -Global Instance and_plain P Q : Plain P → Plain Q → Plain (P ∧ Q). -Proof. intros. by rewrite /Plain plainly_and -!plain. Qed. -Global Instance or_plain P Q : Plain P → Plain Q → Plain (P ∨ Q). -Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed. -Global Instance forall_plain {A} (Ψ : A → PROP) : - (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x). -Proof. - intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain. -Qed. -Global Instance exist_plain {A} (Ψ : A → PROP) : - (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x). -Proof. - intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain. -Qed. - -Global Instance impl_plain P Q : - Absorbing P → Plain P → Plain Q → Plain (P → Q). -Proof. - intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q) - (plainly_elim_absorbingly P) absorbing. -Qed. -Global Instance wand_plain P Q : - Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q). -Proof. - intros. rewrite /Plain {2}(plain P). trans (bi_plainly (bi_plainly P → Q)). - - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q). - by rewrite affinely_plainly_elim. - - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r. -Qed. -Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q). -Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed. - -Global Instance plainly_plain P : Plain (bi_plainly P). -Proof. by rewrite /Plain plainly_idemp. Qed. -Global Instance persistently_plain P : Plain P → Plain (bi_persistently P). -Proof. - rewrite /Plain=> HP. by rewrite {1}HP plainly_persistently persistently_plainly. -Qed. -Global Instance affinely_plain P : Plain P → Plain (bi_affinely P). -Proof. rewrite /bi_affinely. apply _. Qed. -Global Instance absorbingly_plain P : Plain P → Plain (bi_absorbingly P). -Proof. rewrite /bi_absorbingly. apply _. Qed. -Global Instance from_option_palin {A} P (Ψ : A → PROP) (mx : option A) : - (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx). -Proof. destruct mx; apply _. Qed. - (* For big ops *) Global Instance bi_and_monoid : Monoid (@bi_and PROP) := {| monoid_unit := True%I |}. @@ -1679,34 +1294,6 @@ Global Instance bi_or_monoid : Monoid (@bi_or PROP) := Global Instance bi_sep_monoid : Monoid (@bi_sep PROP) := {| monoid_unit := emp%I |}. -Global Instance bi_plainly_and_homomorphism : - MonoidHomomorphism bi_and bi_and (≡) (@bi_plainly PROP). -Proof. - split; [split|]; try apply _. apply plainly_and. apply plainly_pure. -Qed. - -Global Instance bi_plainly_or_homomorphism `{BiPlainlyExist PROP} : - MonoidHomomorphism bi_or bi_or (≡) (@bi_plainly PROP). -Proof. - split; [split|]; try apply _. apply plainly_or. apply plainly_pure. -Qed. - -Global Instance bi_plainly_sep_weak_homomorphism `{BiPositive PROP} : - WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP). -Proof. split; try apply _. apply plainly_sep. Qed. - -Global Instance bi_plainly_sep_homomorphism `{BiAffine PROP} : - MonoidHomomorphism bi_sep bi_sep (≡) (@bi_plainly PROP). -Proof. split. apply _. apply plainly_emp. Qed. - -Global Instance bi_plainly_sep_entails_weak_homomorphism : - WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_plainly PROP). -Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed. - -Global Instance bi_plainly_sep_entails_homomorphism : - MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@bi_plainly PROP). -Proof. split. apply _. simpl. apply plainly_emp_intro. Qed. - Global Instance bi_persistently_and_homomorphism : MonoidHomomorphism bi_and bi_and (≡) (@bi_persistently PROP). Proof. @@ -1779,9 +1366,6 @@ Proof. { intros x. symmetry; apply equiv_spec. } apply limit_preserving_and; by apply limit_preserving_entails. Qed. -Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) : - NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)). -Proof. intros. apply limit_preserving_entails; solve_proper. Qed. Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → PROP) : NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)). Proof. intros. apply limit_preserving_entails; solve_proper. Qed. @@ -1908,48 +1492,10 @@ Proof. apply (internal_eq_rewrite' a b (λ b, bi_persistently (a ≡ b))%I); auto. rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro. Qed. -Lemma plainly_internal_eq {A:ofeT} (a b : A) : bi_plainly (a ≡ b) ⊣⊢ a ≡ b. -Proof. - apply (anti_symm (⊢)). - { by rewrite plainly_elim_absorbingly absorbingly_internal_eq. } - apply (internal_eq_rewrite' a b (λ b, bi_plainly (a ≡ b))%I); [solve_proper|done|]. - rewrite -(internal_eq_refl True%I a) plainly_pure; auto. -Qed. - -Lemma plainly_alt P : bi_plainly P ⊣⊢ bi_affinely P ≡ emp. -Proof. - rewrite -plainly_affinely. apply (anti_symm (⊢)). - - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l. - + by rewrite affinely_elim_emp left_id. - + by rewrite left_id. - - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly). - by rewrite -plainly_True_emp plainly_pure True_impl. -Qed. - -Lemma plainly_alt_absorbing P `{!Absorbing P} : bi_plainly P ⊣⊢ P ≡ True. -Proof. - apply (anti_symm (⊢)). - - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto. - - rewrite internal_eq_sym (internal_eq_rewrite _ _ bi_plainly). - by rewrite plainly_pure True_impl. -Qed. - -Lemma plainly_True_alt P : bi_plainly (True -∗ P) ⊣⊢ P ≡ True. -Proof. - apply (anti_symm (⊢)). - - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto. - by rewrite wand_elim_r. - - rewrite internal_eq_sym (internal_eq_rewrite _ _ - (λ Q, bi_plainly (True -∗ Q)) ltac:(solve_proper)). - by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl. -Qed. Global Instance internal_eq_absorbing {A : ofeT} (x y : A) : Absorbing (x ≡ y : PROP)%I. Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed. -Global Instance internal_eq_plain {A : ofeT} (a b : A) : - Plain (a ≡ b : PROP)%I. -Proof. by intros; rewrite /Plain plainly_internal_eq. Qed. Global Instance internal_eq_persistent {A : ofeT} (a b : A) : Persistent (a ≡ b : PROP)%I. Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed. @@ -2014,25 +1560,17 @@ Lemma later_wand P Q : â–· (P -∗ Q) ⊢ â–· P -∗ â–· Q. Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed. Lemma later_iff P Q : â–· (P ↔ Q) ⊢ â–· P ↔ â–· Q. Proof. by rewrite /bi_iff later_and !later_impl. Qed. -Lemma later_plainly P : â–· bi_plainly P ⊣⊢ bi_plainly (â–· P). -Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed. Lemma later_persistently P : â–· bi_persistently P ⊣⊢ bi_persistently (â–· P). Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed. Lemma later_affinely_2 P : bi_affinely (â–· P) ⊢ â–· bi_affinely P. Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed. -Lemma later_affinely_plainly_2 P : â– â–· P ⊢ â–· â– P. -Proof. by rewrite -later_plainly later_affinely_2. Qed. Lemma later_affinely_persistently_2 P : â–¡ â–· P ⊢ â–· â–¡ P. Proof. by rewrite -later_persistently later_affinely_2. Qed. -Lemma later_affinely_plainly_if_2 p P : â– ?p â–· P ⊢ â–· â– ?p P. -Proof. destruct p; simpl; auto using later_affinely_plainly_2. Qed. Lemma later_affinely_persistently_if_2 p P : â–¡?p â–· P ⊢ â–· â–¡?p P. Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed. Lemma later_absorbingly P : â–· bi_absorbingly P ⊣⊢ bi_absorbingly (â–· P). Proof. by rewrite /bi_absorbingly later_sep later_True. Qed. -Global Instance later_plain P : Plain P → Plain (â–· P). -Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed. Global Instance later_persistent P : Persistent P → Persistent (â–· P). Proof. intros. by rewrite /Persistent -later_persistently {1}(persistent P). Qed. Global Instance later_absorbing P : Absorbing P → Absorbing (â–· P). @@ -2089,25 +1627,17 @@ Lemma laterN_wand n P Q : â–·^n (P -∗ Q) ⊢ â–·^n P -∗ â–·^n Q. Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed. Lemma laterN_iff n P Q : â–·^n (P ↔ Q) ⊢ â–·^n P ↔ â–·^n Q. Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed. -Lemma laterN_plainly n P : â–·^n bi_plainly P ⊣⊢ bi_plainly (â–·^n P). -Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed. Lemma laterN_persistently n P : â–·^n bi_persistently P ⊣⊢ bi_persistently (â–·^n P). Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed. Lemma laterN_affinely_2 n P : bi_affinely (â–·^n P) ⊢ â–·^n bi_affinely P. Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed. -Lemma laterN_affinely_plainly_2 n P : â– â–·^n P ⊢ â–·^n â– P. -Proof. by rewrite -laterN_plainly laterN_affinely_2. Qed. Lemma laterN_affinely_persistently_2 n P : â–¡ â–·^n P ⊢ â–·^n â–¡ P. Proof. by rewrite -laterN_persistently laterN_affinely_2. Qed. -Lemma laterN_affinely_plainly_if_2 n p P : â– ?p â–·^n P ⊢ â–·^n â– ?p P. -Proof. destruct p; simpl; auto using laterN_affinely_plainly_2. Qed. Lemma laterN_affinely_persistently_if_2 n p P : â–¡?p â–·^n P ⊢ â–·^n â–¡?p P. Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed. Lemma laterN_absorbingly n P : â–·^n (bi_absorbingly P) ⊣⊢ bi_absorbingly (â–·^n P). Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed. -Global Instance laterN_plain n P : Plain P → Plain (â–·^n P). -Proof. induction n; apply _. Qed. Global Instance laterN_persistent n P : Persistent P → Persistent (â–·^n P). Proof. induction n; apply _. Qed. Global Instance laterN_absorbing n P : Absorbing P → Absorbing (â–·^n P). @@ -2170,24 +1700,14 @@ Proof. Qed. Lemma except_0_later P : â—‡ â–· P ⊢ â–· P. Proof. by rewrite /sbi_except_0 -later_or False_or. Qed. -Lemma except_0_plainly_1 P : â—‡ bi_plainly P ⊢ bi_plainly (â—‡ P). -Proof. by rewrite /sbi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed. -Lemma except_0_plainly `{BiPlainlyExist PROP} P : - â—‡ bi_plainly P ⊣⊢ bi_plainly (â—‡ P). -Proof. by rewrite /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed. Lemma except_0_persistently P : â—‡ bi_persistently P ⊣⊢ bi_persistently (â—‡ P). Proof. by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure. Qed. Lemma except_0_affinely_2 P : bi_affinely (â—‡ P) ⊢ â—‡ bi_affinely P. Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed. -Lemma except_0_affinely_plainly_2 `{BiPlainlyExist PROP} P : â– â—‡ P ⊢ â—‡ â– P. -Proof. by rewrite -except_0_plainly except_0_affinely_2. Qed. Lemma except_0_affinely_persistently_2 P : â–¡ â—‡ P ⊢ â—‡ â–¡ P. Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed. -Lemma except_0_affinely_plainly_if_2 `{BiPlainlyExist PROP} p P : - â– ?p â—‡ P ⊢ â—‡ â– ?p P. -Proof. destruct p; simpl; auto using except_0_affinely_plainly_2. Qed. Lemma except_0_affinely_persistently_if_2 p P : â–¡?p â—‡ P ⊢ â—‡ â–¡?p P. Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed. Lemma except_0_absorbingly P : â—‡ (bi_absorbingly P) ⊣⊢ bi_absorbingly (â—‡ P). @@ -2205,8 +1725,6 @@ Proof. by apply and_mono, except_0_intro. Qed. -Global Instance except_0_plain P : Plain P → Plain (â—‡ P). -Proof. rewrite /sbi_except_0; apply _. Qed. Global Instance except_0_persistent P : Persistent P → Persistent (â—‡ P). Proof. rewrite /sbi_except_0; apply _. Qed. Global Instance except_0_absorbing P : Absorbing P → Absorbing (â—‡ P). @@ -2263,12 +1781,6 @@ Proof. - rewrite /sbi_except_0; auto. - apply exist_elim=> x. rewrite -(exist_intro x); auto. Qed. -Global Instance plainly_timeless P `{BiPlainlyExist PROP} : - Timeless P → Timeless (bi_plainly P). -Proof. - intros. rewrite /Timeless /sbi_except_0 later_plainly_1. - by rewrite (timeless P) /sbi_except_0 plainly_or {1}plainly_elim. -Qed. Global Instance persistently_timeless P : Timeless P → Timeless (bi_persistently P). Proof. intros. rewrite /Timeless /sbi_except_0 later_persistently_1. @@ -2350,12 +1862,3 @@ Global Instance sbi_except_0_sep_entails_homomorphism : Proof. split; try apply _. apply except_0_intro. Qed. End sbi_derived. End bi. - -(* When declared as an actual instance, [plain_persistent] will cause -failing proof searches to take exponential time, as Coq will try to -apply it the instance at any node in the proof search tree. - -To avoid that, we declare it using a [Hint Immediate], so that it will -only be used at the leaves of the proof search tree, i.e. when the -premise of the hint can be derived from just the current context. *) -Hint Immediate bi.plain_persistent : typeclass_instances. diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v index 635d39dc309c2e987f6cc96275efc176bd1a2245..00ab11806f2e78e02ff0437a1ca394ae0b13d191 100644 --- a/theories/bi/embedding.v +++ b/theories/bi/embedding.v @@ -1,174 +1,222 @@ From iris.algebra Require Import monoid. -From iris.bi Require Import interface derived_laws big_op. +From iris.bi Require Import interface derived_laws big_op plainly. From stdpp Require Import hlist. -(* Embeddings are often used to *define* the connectives of the - domain BI. Hence we cannot ask it to verify the properties of - embeddings. *) -Class BiEmbed (A B : Type) := bi_embed : A → B. -Arguments bi_embed {_ _ _} _%I : simpl never. -Notation "⎡ P ⎤" := (bi_embed P) : bi_scope. -Instance: Params (@bi_embed) 3. -Typeclasses Opaque bi_embed. +Class Embed (A B : Type) := embed : A → B. +Arguments embed {_ _ _} _%I : simpl never. +Notation "⎡ P ⎤" := (embed P) : bi_scope. +Instance: Params (@embed) 3. +Typeclasses Opaque embed. +Hint Mode Embed ! - : typeclass_instances. +Hint Mode Embed - ! : typeclass_instances. + +(* Mixins allow us to create instances easily without having to use Program *) +Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := { + bi_embed_mixin_ne : NonExpansive embed; + bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) embed; + bi_embed_mixin_entails_inj :> Inj (⊢) (⊢) embed; + bi_embed_mixin_emp : ⎡emp⎤ ⊣⊢ emp; + bi_embed_mixin_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤; + bi_embed_mixin_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤; + bi_embed_mixin_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤; + bi_embed_mixin_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤; + bi_embed_mixin_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤; + bi_embed_mixin_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤ +}. + +Class BiEmbed (PROP1 PROP2 : bi) := { + bi_embed_embed :> Embed PROP1 PROP2; + bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed; +}. Hint Mode BiEmbed ! - : typeclass_instances. Hint Mode BiEmbed - ! : typeclass_instances. +Arguments bi_embed_embed : simpl never. -Class BiEmbedding (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := { - bi_embed_ne :> NonExpansive bi_embed; - bi_embed_mono :> Proper ((⊢) ==> (⊢)) bi_embed; - bi_embed_entails_inj :> Inj (⊢) (⊢) bi_embed; - bi_embed_emp : ⎡emp⎤ ⊣⊢ emp; - bi_embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤; - bi_embed_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤; - bi_embed_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤; - bi_embed_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤; - bi_embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤; - bi_embed_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤; - bi_embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤ +Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := { + embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y; + embed_later P : ⎡▷ P⎤ ⊣⊢ â–· ⎡P⎤; + embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢ (P ≡ Q : PROP'); }. -Class SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := { - sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2; - sbi_embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y; - sbi_embed_later P : ⎡▷ P⎤ ⊣⊢ â–· ⎡P⎤ -}. +Section embed_laws. + Context `{BiEmbed PROP1 PROP2}. + Local Notation embed := (embed (A:=PROP1) (B:=PROP2)). + Local Notation "⎡ P ⎤" := (embed P) : bi_scope. + Implicit Types P : PROP1. + + Global Instance embed_ne : NonExpansive embed. + Proof. eapply bi_embed_mixin_ne, bi_embed_mixin. Qed. + Global Instance embed_mono : Proper ((⊢) ==> (⊢)) embed. + Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed. + Global Instance embed_entails_inj : Inj (⊢) (⊢) embed. + Proof. eapply bi_embed_mixin_entails_inj, bi_embed_mixin. Qed. + Lemma embed_emp : ⎡emp⎤ ⊣⊢ emp. + Proof. eapply bi_embed_mixin_emp, bi_embed_mixin. Qed. + Lemma embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤. + Proof. eapply bi_embed_mixin_impl_2, bi_embed_mixin. Qed. + Lemma embed_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤. + Proof. eapply bi_embed_mixin_forall_2, bi_embed_mixin. Qed. + Lemma embed_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤. + Proof. eapply bi_embed_mixin_exist_1, bi_embed_mixin. Qed. + Lemma embed_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤. + Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed. + Lemma embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤. + Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed. + Lemma embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤. + Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed. +End embed_laws. -Section bi_embedding. - Context `{BiEmbedding PROP1 PROP2}. - Local Notation bi_embed := (bi_embed (A:=PROP1) (B:=PROP2)). - Local Notation "⎡ P ⎤" := (bi_embed P) : bi_scope. +Section embed. + Context `{BiEmbed PROP1 PROP2}. + Local Notation embed := (embed (A:=PROP1) (B:=PROP2)). + Local Notation "⎡ P ⎤" := (embed P) : bi_scope. Implicit Types P Q R : PROP1. - Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed. + Global Instance embed_proper : Proper ((≡) ==> (≡)) embed. Proof. apply (ne_proper _). Qed. - Global Instance bi_embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) bi_embed. + Global Instance embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) embed. Proof. solve_proper. Qed. - Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed. + Global Instance embed_inj : Inj (≡) (≡) embed. Proof. - intros P Q EQ. apply bi.equiv_spec, conj; apply (inj bi_embed); + intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed); rewrite EQ //. Qed. - Lemma bi_embed_valid (P : PROP1) : ⎡P⎤%I ↔ P. + Lemma embed_valid (P : PROP1) : ⎡P⎤%I ↔ P. Proof. - by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv]. + by rewrite /bi_valid -embed_emp; split=>?; [apply (inj embed)|f_equiv]. Qed. - Lemma bi_embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤. + Lemma embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤. Proof. - apply bi.equiv_spec; split; [|apply bi_embed_forall_2]. + apply bi.equiv_spec; split; [|apply embed_forall_2]. apply bi.forall_intro=>?. by rewrite bi.forall_elim. Qed. - Lemma bi_embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤. + Lemma embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤. Proof. - apply bi.equiv_spec; split; [apply bi_embed_exist_1|]. + apply bi.equiv_spec; split; [apply embed_exist_1|]. apply bi.exist_elim=>?. by rewrite -bi.exist_intro. Qed. - Lemma bi_embed_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤. - Proof. rewrite !bi.and_alt bi_embed_forall. by f_equiv=>-[]. Qed. - Lemma bi_embed_or P Q : ⎡P ∨ Q⎤ ⊣⊢ ⎡P⎤ ∨ ⎡Q⎤. - Proof. rewrite !bi.or_alt bi_embed_exist. by f_equiv=>-[]. Qed. - Lemma bi_embed_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤). + Lemma embed_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤. + Proof. rewrite !bi.and_alt embed_forall. by f_equiv=>-[]. Qed. + Lemma embed_or P Q : ⎡P ∨ Q⎤ ⊣⊢ ⎡P⎤ ∨ ⎡Q⎤. + Proof. rewrite !bi.or_alt embed_exist. by f_equiv=>-[]. Qed. + Lemma embed_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤). Proof. - apply bi.equiv_spec; split; [|apply bi_embed_impl_2]. - apply bi.impl_intro_l. by rewrite -bi_embed_and bi.impl_elim_r. + apply bi.equiv_spec; split; [|apply embed_impl_2]. + apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r. Qed. - Lemma bi_embed_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤). + Lemma embed_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤). Proof. - apply bi.equiv_spec; split; [|apply bi_embed_wand_2]. - apply bi.wand_intro_l. by rewrite -bi_embed_sep bi.wand_elim_r. + apply bi.equiv_spec; split; [|apply embed_wand_2]. + apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r. Qed. - Lemma bi_embed_pure φ : ⎡⌜φâŒâŽ¤ ⊣⊢ ⌜φâŒ. + Lemma embed_pure φ : ⎡⌜φâŒâŽ¤ ⊣⊢ ⌜φâŒ. Proof. - rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_embed_exist. + rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist. do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|]. - rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?bi_embed_impl; + rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?embed_impl; last apply bi.True_intro. apply bi.impl_intro_l. by rewrite right_id. Qed. - Lemma bi_embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤). - Proof. by rewrite bi_embed_and !bi_embed_impl. Qed. - Lemma bi_embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤). - Proof. by rewrite bi_embed_and !bi_embed_wand. Qed. - Lemma bi_embed_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤. - Proof. by rewrite bi_embed_and bi_embed_emp. Qed. - Lemma bi_embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤. - Proof. by rewrite bi_embed_sep bi_embed_pure. Qed. - Lemma bi_embed_plainly_if P b : ⎡bi_plainly_if b P⎤ ⊣⊢ bi_plainly_if b ⎡P⎤. - Proof. destruct b; simpl; auto using bi_embed_plainly. Qed. - Lemma bi_embed_persistently_if P b : + + Lemma embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤). + Proof. by rewrite embed_and !embed_impl. Qed. + Lemma embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤). + Proof. by rewrite embed_and !embed_wand. Qed. + Lemma embed_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤. + Proof. by rewrite embed_and embed_emp. Qed. + Lemma embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤. + Proof. by rewrite embed_sep embed_pure. Qed. + Lemma embed_persistently_if P b : ⎡bi_persistently_if b P⎤ ⊣⊢ bi_persistently_if b ⎡P⎤. - Proof. destruct b; simpl; auto using bi_embed_persistently. Qed. - Lemma bi_embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤. - Proof. destruct b; simpl; auto using bi_embed_affinely. Qed. - Lemma bi_embed_hforall {As} (Φ : himpl As PROP1): - ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose bi_embed Φ). - Proof. induction As=>//. rewrite /= bi_embed_forall. by do 2 f_equiv. Qed. - Lemma bi_embed_hexist {As} (Φ : himpl As PROP1): - ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose bi_embed Φ). - Proof. induction As=>//. rewrite /= bi_embed_exist. by do 2 f_equiv. Qed. - - Global Instance bi_embed_plain P : Plain P → Plain ⎡P⎤. - Proof. intros ?. by rewrite /Plain -bi_embed_plainly -plain. Qed. - Global Instance bi_embed_persistent P : Persistent P → Persistent ⎡P⎤. - Proof. intros ?. by rewrite /Persistent -bi_embed_persistently -persistent. Qed. - Global Instance bi_embed_affine P : Affine P → Affine ⎡P⎤. - Proof. intros ?. by rewrite /Affine (affine P) bi_embed_emp. Qed. - Global Instance bi_embed_absorbing P : Absorbing P → Absorbing ⎡P⎤. - Proof. intros ?. by rewrite /Absorbing -bi_embed_absorbingly absorbing. Qed. - - Global Instance bi_embed_and_homomorphism : - MonoidHomomorphism bi_and bi_and (≡) bi_embed. + Proof. destruct b; simpl; auto using embed_persistently. Qed. + Lemma embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤. + Proof. destruct b; simpl; auto using embed_affinely. Qed. + Lemma embed_hforall {As} (Φ : himpl As PROP1): + ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose embed Φ). + Proof. induction As=>//. rewrite /= embed_forall. by do 2 f_equiv. Qed. + Lemma embed_hexist {As} (Φ : himpl As PROP1): + ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose embed Φ). + Proof. induction As=>//. rewrite /= embed_exist. by do 2 f_equiv. Qed. + + Global Instance embed_persistent P : Persistent P → Persistent ⎡P⎤. + Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed. + Global Instance embed_affine P : Affine P → Affine ⎡P⎤. + Proof. intros ?. by rewrite /Affine (affine P) embed_emp. Qed. + Global Instance embed_absorbing P : Absorbing P → Absorbing ⎡P⎤. + Proof. intros ?. by rewrite /Absorbing -embed_absorbingly absorbing. Qed. + + Global Instance embed_and_homomorphism : + MonoidHomomorphism bi_and bi_and (≡) embed. Proof. by split; [split|]; try apply _; - [setoid_rewrite bi_embed_and|rewrite bi_embed_pure]. + [setoid_rewrite embed_and|rewrite embed_pure]. Qed. - Global Instance bi_embed_or_homomorphism : - MonoidHomomorphism bi_or bi_or (≡) bi_embed. + Global Instance embed_or_homomorphism : + MonoidHomomorphism bi_or bi_or (≡) embed. Proof. by split; [split|]; try apply _; - [setoid_rewrite bi_embed_or|rewrite bi_embed_pure]. + [setoid_rewrite embed_or|rewrite embed_pure]. Qed. - Global Instance bi_embed_sep_homomorphism : - MonoidHomomorphism bi_sep bi_sep (≡) bi_embed. + Global Instance embed_sep_homomorphism : + MonoidHomomorphism bi_sep bi_sep (≡) embed. Proof. by split; [split|]; try apply _; - [setoid_rewrite bi_embed_sep|rewrite bi_embed_emp]. + [setoid_rewrite embed_sep|rewrite embed_emp]. Qed. - Lemma bi_embed_big_sepL {A} (Φ : nat → A → PROP1) l : + Lemma embed_big_sepL {A} (Φ : nat → A → PROP1) l : ⎡[∗ list] k↦x ∈ l, Φ k x⎤ ⊣⊢ [∗ list] k↦x ∈ l, ⎡Φ k x⎤. Proof. apply (big_opL_commute _). Qed. - Lemma bi_embed_big_sepM `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) : + Lemma embed_big_sepM `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) : ⎡[∗ map] k↦x ∈ m, Φ k x⎤ ⊣⊢ [∗ map] k↦x ∈ m, ⎡Φ k x⎤. Proof. apply (big_opM_commute _). Qed. - Lemma bi_embed_big_sepS `{Countable A} (Φ : A → PROP1) (X : gset A) : + Lemma embed_big_sepS `{Countable A} (Φ : A → PROP1) (X : gset A) : ⎡[∗ set] y ∈ X, Φ y⎤ ⊣⊢ [∗ set] y ∈ X, ⎡Φ y⎤. Proof. apply (big_opS_commute _). Qed. - Lemma bi_embed_big_sepMS `{Countable A} (Φ : A → PROP1) (X : gmultiset A) : + Lemma embed_big_sepMS `{Countable A} (Φ : A → PROP1) (X : gmultiset A) : ⎡[∗ mset] y ∈ X, Φ y⎤ ⊣⊢ [∗ mset] y ∈ X, ⎡Φ y⎤. Proof. apply (big_opMS_commute _). Qed. -End bi_embedding. +End embed. -Section sbi_embedding. - Context `{SbiEmbedding PROP1 PROP2}. +Section sbi_embed. + Context `{SbiEmbed PROP1 PROP2}. Implicit Types P Q R : PROP1. - Lemma sbi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y. + Lemma embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y. Proof. - apply bi.equiv_spec; split; [apply sbi_embed_internal_eq_1|]. + apply bi.equiv_spec; split; [apply embed_internal_eq_1|]. etrans; [apply (bi.internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|]. - rewrite -(bi.internal_eq_refl True%I) bi_embed_pure. + rewrite -(bi.internal_eq_refl True%I) embed_pure. eapply bi.impl_elim; [done|]. apply bi.True_intro. Qed. - Lemma sbi_embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ â–·^n ⎡P⎤. - Proof. induction n=>//=. rewrite sbi_embed_later. by f_equiv. Qed. - Lemma sbi_embed_except_0 P : ⎡◇ P⎤ ⊣⊢ â—‡ ⎡P⎤. - Proof. by rewrite bi_embed_or sbi_embed_later bi_embed_pure. Qed. + Lemma embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ â–·^n ⎡P⎤. + Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed. + Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ â—‡ ⎡P⎤. + Proof. by rewrite embed_or embed_later embed_pure. Qed. - Global Instance sbi_embed_timeless P : Timeless P → Timeless ⎡P⎤. + Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■P⎤ ⊣⊢ ■⎡P⎤. Proof. - intros ?. by rewrite /Timeless -sbi_embed_except_0 -sbi_embed_later timeless. + rewrite !plainly_alt embed_internal_eq. apply (anti_symm _). + - rewrite -embed_affinely -embed_emp. apply bi.f_equiv, _. + - by rewrite -embed_affinely -embed_emp embed_interal_inj. Qed. -End sbi_embedding. + Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2} p P : ⎡■?p P⎤ ⊣⊢ â– ?p ⎡P⎤. + Proof. destruct p; simpl; auto using embed_plainly. Qed. + + Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} P : Plain P → Plain ⎡P⎤. + Proof. intros ?. by rewrite /Plain -embed_plainly -plain. Qed. + + Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤. + Proof. + intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless. + Qed. +End sbi_embed. + +(* Not defined using an ordinary [Instance] because the default +[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof +search for the other premises fail. See the proof of [monPred_absolutely_plain] +for an example where it would fail with a regular [Instance].*) +Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances. diff --git a/theories/bi/interface.v b/theories/bi/interface.v index 56ef28240860537cdbcf442ddaf8f89b986742b5..5fd4fa0e9276b76487da0cfcda71b188aac3e68b 100644 --- a/theories/bi/interface.v +++ b/theories/bi/interface.v @@ -9,7 +9,7 @@ Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity). Reserved Notation "â–· P" (at level 20, right associativity). Section bi_mixin. - Context {PROP : Type} `{Dist PROP, Equiv PROP} (prop_ofe_mixin : OfeMixin PROP). + Context {PROP : Type} `{Dist PROP, Equiv PROP}. Context (bi_entails : PROP → PROP → Prop). Context (bi_emp : PROP). Context (bi_pure : Prop → PROP). @@ -20,7 +20,6 @@ Section bi_mixin. Context (bi_exist : ∀ A, (A → PROP) → PROP). Context (bi_sep : PROP → PROP → PROP). Context (bi_wand : PROP → PROP → PROP). - Context (bi_plainly : PROP → PROP). Context (bi_persistently : PROP → PROP). Context (sbi_internal_eq : ∀ A : ofeT, A → A → PROP). Context (sbi_later : PROP → PROP). @@ -68,7 +67,6 @@ Section bi_mixin. Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A); bi_mixin_sep_ne : NonExpansive2 bi_sep; bi_mixin_wand_ne : NonExpansive2 bi_wand; - bi_mixin_plainly_ne : NonExpansive bi_plainly; bi_mixin_persistently_ne : NonExpansive bi_persistently; (* Higher-order logic *) @@ -102,26 +100,6 @@ Section bi_mixin. bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R; bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R; - (* Plainly *) - (* Note: plainly is about to be removed from this interface *) - bi_mixin_plainly_mono P Q : (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q; - bi_mixin_plainly_elim_persistently P : bi_plainly P ⊢ bi_persistently P; - bi_mixin_plainly_idemp_2 P : bi_plainly P ⊢ bi_plainly (bi_plainly P); - - bi_mixin_plainly_forall_2 {A} (Ψ : A → PROP) : - (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a); - - (* The following two laws are very similar, and indeed they hold not just - for persistently and plainly, but for any modality defined as `M P n x := - ∀ y, R x y → P n y`. *) - bi_mixin_persistently_impl_plainly P Q : - (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q); - bi_mixin_plainly_impl_plainly P Q : - (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q); - - bi_mixin_plainly_emp_intro P : P ⊢ bi_plainly emp; - bi_mixin_plainly_absorbing P Q : bi_plainly P ∗ Q ⊢ bi_plainly P; - (* Persistently *) (* In the ordered RA model: Holds without further assumptions. *) bi_mixin_persistently_mono P Q : @@ -130,8 +108,8 @@ Section bi_mixin. bi_mixin_persistently_idemp_2 P : bi_persistently P ⊢ bi_persistently (bi_persistently P); - (* In the ordered RA model [P ⊢ persisently emp] (which can currently still - be derived from the plainly axioms, which will be removed): `ε ≼ core x` *) + (* In the ordered RA model: `ε ≼ core x` *) + bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp; bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) : (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a); @@ -158,8 +136,6 @@ Section bi_mixin. sbi_mixin_fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g; sbi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y; sbi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ bâŒ; - sbi_mixin_prop_ext P Q : bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ - sbi_internal_eq (OfeT PROP prop_ofe_mixin) P Q; (* Later *) sbi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ â–· (x ≡ y); @@ -173,8 +149,6 @@ Section bi_mixin. (â–· ∃ a, Φ a) ⊢ â–· False ∨ (∃ a, â–· Φ a); sbi_mixin_later_sep_1 P Q : â–· (P ∗ Q) ⊢ â–· P ∗ â–· Q; sbi_mixin_later_sep_2 P Q : â–· P ∗ â–· Q ⊢ â–· (P ∗ Q); - sbi_mixin_later_plainly_1 P : â–· bi_plainly P ⊢ bi_plainly (â–· P); - sbi_mixin_later_plainly_2 P : bi_plainly (â–· P) ⊢ â–· bi_plainly P; sbi_mixin_later_persistently_1 P : â–· bi_persistently P ⊢ bi_persistently (â–· P); sbi_mixin_later_persistently_2 P : @@ -198,11 +172,10 @@ Structure bi := Bi { bi_exist : ∀ A, (A → bi_car) → bi_car; bi_sep : bi_car → bi_car → bi_car; bi_wand : bi_car → bi_car → bi_car; - bi_plainly : bi_car → bi_car; bi_persistently : bi_car → bi_car; bi_ofe_mixin : OfeMixin bi_car; bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall - bi_exist bi_sep bi_wand bi_plainly bi_persistently; + bi_exist bi_sep bi_wand bi_persistently; }. Coercion bi_ofeC (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP). @@ -218,7 +191,6 @@ Instance: Params (@bi_forall) 2. Instance: Params (@bi_exist) 2. Instance: Params (@bi_sep) 1. Instance: Params (@bi_wand) 1. -Instance: Params (@bi_plainly) 1. Instance: Params (@bi_persistently) 1. Delimit Scope bi_scope with I. @@ -235,7 +207,6 @@ Arguments bi_forall {PROP _} _%I : simpl never, rename. Arguments bi_exist {PROP _} _%I : simpl never, rename. Arguments bi_sep {PROP} _%I _%I : simpl never, rename. Arguments bi_wand {PROP} _%I _%I : simpl never, rename. -Arguments bi_plainly {PROP} _%I : simpl never, rename. Arguments bi_persistently {PROP} _%I : simpl never, rename. Structure sbi := Sbi { @@ -252,17 +223,15 @@ Structure sbi := Sbi { sbi_exist : ∀ A, (A → sbi_car) → sbi_car; sbi_sep : sbi_car → sbi_car → sbi_car; sbi_wand : sbi_car → sbi_car → sbi_car; - sbi_plainly : sbi_car → sbi_car; sbi_persistently : sbi_car → sbi_car; sbi_internal_eq : ∀ A : ofeT, A → A → sbi_car; sbi_later : sbi_car → sbi_car; sbi_ofe_mixin : OfeMixin sbi_car; sbi_bi_mixin : BiMixin sbi_entails sbi_emp sbi_pure sbi_and sbi_or sbi_impl - sbi_forall sbi_exist sbi_sep sbi_wand sbi_plainly - sbi_persistently; - sbi_sbi_mixin : SbiMixin sbi_ofe_mixin sbi_entails sbi_pure sbi_and sbi_or - sbi_impl sbi_forall sbi_exist sbi_sep sbi_wand - sbi_plainly sbi_persistently sbi_internal_eq sbi_later; + sbi_forall sbi_exist sbi_sep sbi_wand sbi_persistently; + sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl + sbi_forall sbi_exist sbi_sep + sbi_persistently sbi_internal_eq sbi_later; }. Instance: Params (@sbi_later) 1. @@ -290,7 +259,6 @@ Arguments sbi_forall {PROP _} _%I : simpl never, rename. Arguments sbi_exist {PROP _} _%I : simpl never, rename. Arguments sbi_sep {PROP} _%I _%I : simpl never, rename. Arguments sbi_wand {PROP} _%I _%I : simpl never, rename. -Arguments sbi_plainly {PROP} _%I : simpl never, rename. Arguments sbi_persistently {PROP} _%I : simpl never, rename. Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename. Arguments sbi_later {PROP} _%I : simpl never, rename. @@ -366,8 +334,6 @@ Global Instance sep_ne : NonExpansive2 (@bi_sep PROP). Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed. Global Instance wand_ne : NonExpansive2 (@bi_wand PROP). Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed. -Global Instance plainly_ne : NonExpansive (@bi_plainly PROP). -Proof. eapply bi_mixin_plainly_ne, bi_bi_mixin. Qed. Global Instance persistently_ne : NonExpansive (@bi_persistently PROP). Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed. @@ -424,27 +390,6 @@ Proof. eapply bi_mixin_wand_intro_r, bi_bi_mixin. Qed. Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R. Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed. -(* Plainly *) -Lemma plainly_mono P Q : (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q. -Proof. eapply bi_mixin_plainly_mono, bi_bi_mixin. Qed. -Lemma plainly_elim_persistently P : bi_plainly P ⊢ bi_persistently P. -Proof. eapply bi_mixin_plainly_elim_persistently, bi_bi_mixin. Qed. -Lemma plainly_idemp_2 P : bi_plainly P ⊢ bi_plainly (bi_plainly P). -Proof. eapply bi_mixin_plainly_idemp_2, bi_bi_mixin. Qed. -Lemma plainly_forall_2 {A} (Ψ : A → PROP) : - (∀ a, bi_plainly (Ψ a)) ⊢ bi_plainly (∀ a, Ψ a). -Proof. eapply bi_mixin_plainly_forall_2, bi_bi_mixin. Qed. -Lemma persistently_impl_plainly P Q : - (bi_plainly P → bi_persistently Q) ⊢ bi_persistently (bi_plainly P → Q). -Proof. eapply bi_mixin_persistently_impl_plainly, bi_bi_mixin. Qed. -Lemma plainly_impl_plainly P Q : - (bi_plainly P → bi_plainly Q) ⊢ bi_plainly (bi_plainly P → Q). -Proof. eapply bi_mixin_plainly_impl_plainly, bi_bi_mixin. Qed. -Lemma plainly_absorbing P Q : bi_plainly P ∗ Q ⊢ bi_plainly P. -Proof. eapply (bi_mixin_plainly_absorbing bi_entails), bi_bi_mixin. Qed. -Lemma plainly_emp_intro P : P ⊢ bi_plainly emp. -Proof. eapply bi_mixin_plainly_emp_intro, bi_bi_mixin. Qed. - (* Persistently *) Lemma persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q. Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed. @@ -452,6 +397,9 @@ Lemma persistently_idemp_2 P : bi_persistently P ⊢ bi_persistently (bi_persistently P). Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed. +Lemma persistently_emp_intro P : P ⊢ bi_persistently emp. +Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed. + Lemma persistently_forall_2 {A} (Ψ : A → PROP) : (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a). Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed. @@ -488,9 +436,6 @@ Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ (⌜a ≡ b⌠: PROP). Proof. eapply sbi_mixin_discrete_eq_1, sbi_sbi_mixin. Qed. -Lemma prop_ext P Q : bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q. -Proof. eapply (sbi_mixin_prop_ext _ bi_entails), sbi_sbi_mixin. Qed. - (* Later *) Global Instance later_contractive : Contractive (@sbi_later PROP). Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed. @@ -514,14 +459,10 @@ Lemma later_sep_1 P Q : â–· (P ∗ Q) ⊢ â–· P ∗ â–· Q. Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed. Lemma later_sep_2 P Q : â–· P ∗ â–· Q ⊢ â–· (P ∗ Q). Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed. -Lemma later_plainly_1 P : â–· bi_plainly P ⊢ bi_plainly (â–· P). -Proof. eapply (sbi_mixin_later_plainly_1 _ bi_entails), sbi_sbi_mixin. Qed. -Lemma later_plainly_2 P : bi_plainly (â–· P) ⊢ â–· bi_plainly P. -Proof. eapply (sbi_mixin_later_plainly_2 _ bi_entails), sbi_sbi_mixin. Qed. Lemma later_persistently_1 P : â–· bi_persistently P ⊢ bi_persistently (â–· P). -Proof. eapply (sbi_mixin_later_persistently_1 _ bi_entails), sbi_sbi_mixin. Qed. +Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed. Lemma later_persistently_2 P : bi_persistently (â–· P) ⊢ â–· bi_persistently P. -Proof. eapply (sbi_mixin_later_persistently_2 _ bi_entails), sbi_sbi_mixin. Qed. +Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed. Lemma later_false_em P : â–· P ⊢ â–· False ∨ (â–· False → P). Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed. diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v index 74eeec2015722fd87c0a1d60c970699ee52ef1f5..59792e0f078dd27789103ede34947e5b74b4471e 100644 --- a/theories/bi/lib/atomic.v +++ b/theories/bi/lib/atomic.v @@ -3,7 +3,7 @@ From stdpp Require Import coPset. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". -Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type} +Definition atomic_shift `{BiFUpd PROP} {A B : Type} (α : A → PROP) (* atomic pre-condition *) (β : A → B → PROP) (* atomic post-condition *) (Eo Em : coPset) (* outside/module masks *) @@ -14,7 +14,7 @@ Definition atomic_shift {PROP: sbi} `{!FUpd PROP} {A B : Type} ((α x ={E∖Em, E}=∗ P) ∧ (∀ y, β x y ={E∖Em, E}=∗ Q x y))) )%I. -Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type} +Definition atomic_update `{BiFUpd PROP} {A B : Type} (α : A → PROP) (* atomic pre-condition *) (β : A → B → PROP) (* atomic post-condition *) (Eo Em : coPset) (* outside/module masks *) @@ -25,7 +25,7 @@ Definition atomic_update {PROP: sbi} `{!FUpd PROP} {A B : Type} )%I. Section lemmas. - Context {PROP: sbi} `{FUpdFacts PROP} {A B : Type}. + Context `{BiFUpd PROP} {A B : Type}. Implicit Types (α : A → PROP) (β: A → B → PROP) (P : PROP) (Q : A → B → PROP). Lemma aupd_acc α β Eo Em Q E : diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v index 36dcb9f0e560aa7b1c40ad81a830887d44a49796..606cc00260d7004cc6f26adc5939a6635da23d38 100644 --- a/theories/bi/monpred.v +++ b/theories/bi/monpred.v @@ -2,7 +2,6 @@ From stdpp Require Import coPset. From iris.bi Require Import bi. (** Definitions. *) - Structure biIndex := BiIndex { bi_index_type :> Type; @@ -128,14 +127,28 @@ Next Obligation. solve_proper. Qed. Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _. Definition monPred_embed_aux : seal (@monPred_embed_def). by eexists. Qed. -Global Instance monPred_embed : BiEmbed PROP monPred := unseal monPred_embed_aux. -Definition monPred_embed_eq : bi_embed (A:=PROP) = _ := seal_eq _. +Definition monPred_embed : Embed PROP monPred := unseal monPred_embed_aux. +Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := seal_eq _. + +Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _. +Definition monPred_emp_aux : seal (@monPred_emp_def). by eexists. Qed. +Definition monPred_emp := unseal monPred_emp_aux. +Definition monPred_emp_eq : @monPred_emp = _ := seal_eq _. + +Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φâŒ)%I _. +Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed. +Definition monPred_pure := unseal monPred_pure_aux. +Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _. + +Definition monPred_absolutely_def P : monPred := MonPred (λ _, ∀ i, P i)%I _. +Definition monPred_absolutely_aux : seal (@monPred_absolutely_def). by eexists. Qed. +Definition monPred_absolutely := unseal monPred_absolutely_aux. +Definition monPred_absolutely_eq : @monPred_absolutely = _ := seal_eq _. -Definition monPred_pure (φ : Prop) : monPred := tc_opaque ⎡⌜φâŒâŽ¤%I. -Definition monPred_emp : monPred := tc_opaque ⎡emp⎤%I. -Definition monPred_plainly P : monPred := tc_opaque ⎡∀ i, bi_plainly (P i)⎤%I. -Definition monPred_absolutely (P : monPred) : monPred := tc_opaque ⎡∀ i, P i⎤%I. -Definition monPred_relatively (P : monPred) : monPred := tc_opaque ⎡∃ i, P i⎤%I. +Definition monPred_relatively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _. +Definition monPred_relatively_aux : seal (@monPred_relatively_def). by eexists. Qed. +Definition monPred_relatively := unseal monPred_relatively_aux. +Definition monPred_relatively_eq : @monPred_relatively = _ := seal_eq _. Program Definition monPred_and_def P Q : monPred := MonPred (λ i, P i ∧ Q i)%I _. @@ -205,8 +218,8 @@ Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred := terms in logical terms. *) monPred_upclosed (λ i, |==> P i)%I. Definition monPred_bupd_aux `{BUpd PROP} : seal monPred_bupd_def. by eexists. Qed. -Global Instance monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux. -Definition monPred_bupd_eq `{BUpd PROP} : @bupd monPred _ = _ := seal_eq _. +Definition monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux. +Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := seal_eq _. End Bi. Arguments monPred_absolutely {_ _} _%I. @@ -214,15 +227,21 @@ Arguments monPred_relatively {_ _} _%I. Notation "'∀ᵢ' P" := (monPred_absolutely P) (at level 20, right associativity) : bi_scope. Notation "'∃ᵢ' P" := (monPred_relatively P) (at level 20, right associativity) : bi_scope. -Typeclasses Opaque monPred_pure monPred_emp monPred_plainly. - Section Sbi. Context {I : biIndex} {PROP : sbi}. Implicit Types i : I. Notation monPred := (monPred I PROP). Implicit Types P Q : monPred. -Definition monPred_internal_eq (A : ofeT) (a b : A) : monPred := tc_opaque ⎡a ≡ b⎤%I. +Definition monPred_plainly_def `{BiPlainly PROP} P : monPred := MonPred (λ _, ∀ i, â– (P i))%I _. +Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. by eexists. Qed. +Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := unseal monPred_plainly_aux. +Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := seal_eq _. + +Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _. +Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed. +Definition monPred_internal_eq := unseal monPred_internal_eq_aux. +Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := seal_eq _. Program Definition monPred_later_def P : monPred := MonPred (λ i, â–· (P i))%I _. Next Obligation. solve_proper. Qed. @@ -237,8 +256,8 @@ Definition monPred_fupd_def `{FUpd PROP} (E1 E2 : coPset) (P : monPred) : monPre terms in logical terms. *) monPred_upclosed (λ i, |={E1,E2}=> P i)%I. Definition monPred_fupd_aux `{FUpd PROP} : seal monPred_fupd_def. by eexists. Qed. -Global Instance monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux. -Definition monPred_fupd_eq `{FUpd PROP} : @fupd monPred _ = _ := seal_eq _. +Definition monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux. +Definition monPred_fupd_eq `{FUpd PROP} : @fupd _ monPred_fupd = _ := seal_eq _. End Sbi. Module MonPred. @@ -246,18 +265,18 @@ Definition unseal_eqs := (@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq, @monPred_forall_eq, @monPred_exist_eq, @monPred_sep_eq, @monPred_wand_eq, - @monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq, - @monPred_embed_eq, @monPred_bupd_eq, @monPred_fupd_eq). + @monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq, + @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq, @monPred_plainly_eq, + @monPred_absolutely_eq, @monPred_relatively_eq, @monPred_bupd_eq, @monPred_fupd_eq). Ltac unseal := unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp, - monPred_absolutely, monPred_relatively, monPred_upclosed, bi_and, bi_or, + monPred_upclosed, bi_and, bi_or, bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand, - bi_persistently, bi_affinely, bi_plainly, sbi_later; + bi_persistently, bi_affinely, sbi_later; simpl; unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist, - sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly; + sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl; - unfold monPred_pure, monPred_emp, monPred_internal_eq, monPred_plainly; simpl; rewrite !unseal_eqs /=. End MonPred. Import MonPred. @@ -268,7 +287,7 @@ Context (I : biIndex) (PROP : bi). Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP) monPred_entails monPred_emp monPred_pure monPred_and monPred_or monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand - monPred_plainly monPred_persistently. + monPred_persistently. Proof. split; try unseal; try by (split=> ? /=; repeat f_equiv). - split. @@ -306,26 +325,9 @@ Proof. apply bi.wand_intro_r. by rewrite -HR /= !Hij. - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'. rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //. - - intros P Q [?]. split=> i /=. by do 3 f_equiv. - - intros P. split=> i /=. by rewrite bi.forall_elim bi.plainly_elim_persistently. - - intros P. split=> i /=. repeat setoid_rewrite <-bi.plainly_forall. - rewrite -bi.plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_. - - intros A Ψ. split=> i /=. apply bi.forall_intro=> j. - rewrite bi.plainly_forall. apply bi.forall_intro=> a. - by rewrite !bi.forall_elim. - - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall. - repeat setoid_rewrite <-bi.plainly_forall. - repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv. - apply bi.persistently_impl_plainly. - - intros P Q. split=> i /=. - repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //. - repeat setoid_rewrite <-bi.plainly_forall. - setoid_rewrite bi.plainly_impl_plainly. f_equiv. - do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //. - - intros P. split=> i. apply bi.forall_intro=>_. by apply bi.plainly_emp_intro. - - intros P Q. split=> i. apply bi.sep_elim_l, _. - intros P Q [?]. split=> i /=. by f_equiv. - intros P. split=> i. by apply bi.persistently_idemp_2. + - intros P. split=> i. by apply bi.persistently_emp_intro. - intros A Ψ. split=> i. by apply bi.persistently_forall_2. - intros A Ψ. split=> i. by apply bi.persistently_exist_1. - intros P Q. split=> i. apply bi.sep_elim_l, _. @@ -333,20 +335,16 @@ Proof. Qed. Canonical Structure monPredI : bi := - Bi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp - monPred_pure monPred_and monPred_or monPred_impl monPred_forall - monPred_exist monPred_sep monPred_wand monPred_plainly monPred_persistently - monPred_ofe_mixin monPred_bi_mixin. + {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin |}. End canonical_bi. Section canonical_sbi. Context (I : biIndex) (PROP : sbi). Lemma monPred_sbi_mixin : - SbiMixin (PROP:=monPred I PROP) monPred_ofe_mixin monPred_entails monPred_pure - monPred_and monPred_or monPred_impl monPred_forall monPred_exist - monPred_sep monPred_wand monPred_plainly monPred_persistently - monPred_internal_eq monPred_later. + SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure + monPred_or monPred_impl monPred_forall monPred_exist + monPred_sep monPred_persistently monPred_internal_eq monPred_later. Proof. split; unseal. - intros n P Q HPQ. split=> i /=. @@ -359,11 +357,6 @@ Proof. - intros A1 A2 f g. split=> i. by apply bi.fun_ext. - intros A P x y. split=> i. by apply bi.sig_eq. - intros A a b ?. split=> i. by apply bi.discrete_eq_1. - - intros P Q. split=> i /=. - rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _). - rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j. - rewrite -bi.prop_ext !(bi.forall_elim j) !bi.pure_impl_forall - !bi.forall_elim //. - intros A x y. split=> i. by apply bi.later_eq_1. - intros A x y. split=> i. by apply bi.later_eq_2. - intros P Q [?]. split=> i. by apply bi.later_mono. @@ -373,10 +366,6 @@ Proof. - intros A Ψ. split=> i. by apply bi.later_exist_false. - intros P Q. split=> i. by apply bi.later_sep_1. - intros P Q. split=> i. by apply bi.later_sep_2. - - intros P. split=> i /=. - rewrite bi.later_forall. f_equiv=> j. by rewrite -bi.later_plainly_1. - - intros P. split=> i /=. - rewrite bi.later_forall. f_equiv=> j. by rewrite -bi.later_plainly_2. - intros P. split=> i. by apply bi.later_persistently_1. - intros P. split=> i. by apply bi.later_persistently_2. - intros P. split=> i /=. rewrite -bi.forall_intro. apply bi.later_false_em. @@ -384,12 +373,50 @@ Proof. Qed. Canonical Structure monPredSI : sbi := - Sbi (monPred I PROP) monPred_dist monPred_equiv monPred_entails monPred_emp - monPred_pure monPred_and monPred_or monPred_impl monPred_forall - monPred_exist monPred_sep monPred_wand monPred_plainly - monPred_persistently monPred_internal_eq monPred_later monPred_ofe_mixin - (bi_bi_mixin _) monPred_sbi_mixin. + {| sbi_ofe_mixin := monPred_ofe_mixin; sbi_bi_mixin := monPred_bi_mixin I PROP; + sbi_sbi_mixin := monPred_sbi_mixin |}. + +Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredSI monPred_plainly. +Proof. + split; unseal. + - by (split=> ? /=; repeat f_equiv). + - intros P Q [?]. split=> i /=. by do 3 f_equiv. + - intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently. + - intros P. split=> i /=. repeat setoid_rewrite <-plainly_forall. + rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_. + - intros A Ψ. split=> i /=. apply bi.forall_intro=> j. + rewrite plainly_forall. apply bi.forall_intro=> a. + by rewrite !bi.forall_elim. + - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall. + repeat setoid_rewrite <-plainly_forall. + repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv. + apply persistently_impl_plainly. + - intros P Q. split=> i /=. + repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //. + repeat setoid_rewrite <-plainly_forall. + setoid_rewrite plainly_impl_plainly. f_equiv. + do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //. + - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro. + - intros P Q. split=> i. apply bi.sep_elim_l, _. + - intros P Q. split=> i /=. + rewrite <-(sig_monPred_sig P), <-(sig_monPred_sig Q), <-(bi.f_equiv _). + rewrite -bi.sig_equivI /= -bi.fun_ext. f_equiv=> j. + rewrite -prop_ext !(bi.forall_elim j) !bi.pure_impl_forall + !bi.forall_elim //. + - intros P. split=> i /=. + rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_1. + - intros P. split=> i /=. + rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2. +Qed. +Global Instance monPred_plainlyC `{BiPlainly PROP} : BiPlainly monPredSI := + {| bi_plainly_mixin := monPred_plainly_mixin |}. +Global Instance monPred_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} : + BiPlainlyExist PROP → BiPlainlyExist monPredSI. +Proof. + split=>?/=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv. + apply bi.forall_intro=>?. by do 2 f_equiv. +Qed. End canonical_sbi. Class Absolute {I : biIndex} {PROP : bi} (P : monPred I PROP) := @@ -411,7 +438,6 @@ Implicit Types i : I. Implicit Types P Q : monPred. (** Instances *) - Global Instance monPred_at_mono : Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at. Proof. by move=> ?? [?] ?? ->. Qed. @@ -433,17 +459,8 @@ Proof. split => ?. unseal. apply bi_positive. Qed. Global Instance monPred_affine : BiAffine PROP → BiAffine monPredI. Proof. split => ?. unseal. by apply affine. Qed. -Global Instance monPred_plainly_exist `{BiIndexBottom bot} : - BiPlainlyExist PROP → BiPlainlyExist monPredI. -Proof. - split=>?/=. unseal. rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv. - apply bi.forall_intro=>?. by do 2 f_equiv. -Qed. - Global Instance monPred_at_persistent P i : Persistent P → Persistent (P i). Proof. move => [] /(_ i). by unseal. Qed. -Global Instance monPred_at_plain P i : Plain P → Plain (P i). -Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed. Global Instance monPred_at_absorbing P i : Absorbing P → Absorbing (P i). Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed. Global Instance monPred_at_affine P i : Affine P → Affine (P i). @@ -458,8 +475,7 @@ Global Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i). Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed. - -Global Instance monPred_bi_embedding : BiEmbedding PROP monPredI. +Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed. Proof. split; try apply _; unseal; try done. - move =>?? /= [/(_ inhabitant) ?] //. @@ -467,64 +483,64 @@ Proof. by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim. - split=>? /=. by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim. - - intros ?. split => ? /=. apply bi.equiv_spec; split. - by apply bi.forall_intro. by rewrite bi.forall_elim. Qed. +Global Instance monPred_bi_embed : BiEmbed PROP monPredI := + {| bi_embed_mixin := monPred_embedding_mixin |}. + +Lemma monPred_emp_unfold : emp%I = ⎡emp : PROP⎤%I. +Proof. by unseal. Qed. +Lemma monPred_pure_unfold : bi_pure = λ φ, ⎡ ⌜ φ ⌠: PROP⎤%I. +Proof. by unseal. Qed. +Lemma monPred_absolutely_unfold : monPred_absolutely = λ P, ⎡∀ i, P i⎤%I. +Proof. by unseal. Qed. +Lemma monPred_relatively_unfold : monPred_relatively = λ P, ⎡∃ i, P i⎤%I. +Proof. by unseal. Qed. Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP). -Proof. rewrite /monPred_absolutely /=. solve_proper. Qed. +Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed. Global Instance monPred_absolutely_proper : Proper ((≡) ==> (≡)) (@monPred_absolutely I PROP). Proof. apply (ne_proper _). Qed. Lemma monPred_absolutely_mono P Q : (P ⊢ Q) → (∀ᵢ P ⊢ ∀ᵢ Q). -Proof. rewrite /monPred_absolutely /=. solve_proper. Qed. +Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed. Global Instance monPred_absolutely_mono' : Proper ((⊢) ==> (⊢)) (@monPred_absolutely I PROP). -Proof. rewrite /monPred_absolutely /=. solve_proper. Qed. +Proof. intros ???. by apply monPred_absolutely_mono. Qed. Global Instance monPred_absolutely_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@monPred_absolutely I PROP). -Proof. solve_proper. Qed. - -Local Notation "'∀ᵢ' P" := (@monPred_absolutely I PROP P) : bi_scope. -Local Notation "'∃ᵢ' P" := (@monPred_relatively I PROP P) : bi_scope. +Proof. intros ???. by apply monPred_absolutely_mono. Qed. -Global Instance monPred_absolutely_plain P : Plain P → Plain (∀ᵢ P). -Proof. rewrite /monPred_absolutely /=. apply _. Qed. Global Instance monPred_absolutely_persistent P : Persistent P → Persistent (∀ᵢ P). -Proof. rewrite /monPred_absolutely /=. apply _. Qed. +Proof. rewrite monPred_absolutely_unfold. apply _. Qed. Global Instance monPred_absolutely_absorbing P : Absorbing P → Absorbing (∀ᵢ P). -Proof. rewrite /monPred_absolutely /=. apply _. Qed. +Proof. rewrite monPred_absolutely_unfold. apply _. Qed. Global Instance monPred_absolutely_affine P : Affine P → Affine (∀ᵢ P). -Proof. rewrite /monPred_absolutely /=. apply _. Qed. +Proof. rewrite monPred_absolutely_unfold. apply _. Qed. Global Instance monPred_relatively_ne : NonExpansive (@monPred_relatively I PROP). -Proof. rewrite /monPred_relatively /=. solve_proper. Qed. +Proof. rewrite monPred_relatively_unfold. solve_proper. Qed. Global Instance monPred_relatively_proper : Proper ((≡) ==> (≡)) (@monPred_relatively I PROP). Proof. apply (ne_proper _). Qed. Lemma monPred_relatively_mono P Q : (P ⊢ Q) → (∃ᵢ P ⊢ ∃ᵢ Q). -Proof. rewrite /monPred_relatively /=. solve_proper. Qed. +Proof. rewrite monPred_relatively_unfold. solve_proper. Qed. Global Instance monPred_relatively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_relatively I PROP). -Proof. rewrite /monPred_relatively /=. solve_proper. Qed. +Proof. intros ???. by apply monPred_relatively_mono. Qed. Global Instance monPred_relatively_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@monPred_relatively I PROP). -Proof. solve_proper. Qed. +Proof. intros ???. by apply monPred_relatively_mono. Qed. -Global Instance monPred_relatively_plain P : Plain P → Plain (∃ᵢ P). -Proof. rewrite /monPred_relatively /=. apply _. Qed. Global Instance monPred_relatively_persistent P : Persistent P → Persistent (∃ᵢ P). -Proof. rewrite /monPred_relatively /=. apply _. Qed. +Proof. rewrite monPred_relatively_unfold. apply _. Qed. Global Instance monPred_relatively_absorbing P : Absorbing P → Absorbing (∃ᵢ P). -Proof. rewrite /monPred_relatively /=. apply _. Qed. +Proof. rewrite monPred_relatively_unfold. apply _. Qed. Global Instance monPred_relatively_affine P : Affine P → Affine (∃ᵢ P). -Proof. rewrite /monPred_relatively /=. apply _. Qed. +Proof. rewrite monPred_relatively_unfold. apply _. Qed. (** monPred_at unfolding laws *) Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P. Proof. by unseal. Qed. Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌠i ⊣⊢ ⌜φâŒ. -Proof. by apply monPred_at_embed. Qed. +Proof. by unseal. Qed. Lemma monPred_at_emp i : monPred_at emp i ⊣⊢ emp. -Proof. by apply monPred_at_embed. Qed. -Lemma monPred_at_plainly i P : bi_plainly P i ⊣⊢ ∀ j, bi_plainly (P j). -Proof. by apply monPred_at_embed. Qed. +Proof. by unseal. Qed. Lemma monPred_at_and i P Q : (P ∧ Q) i ⊣⊢ P i ∧ Q i. Proof. by unseal. Qed. Lemma monPred_at_or i P Q : (P ∨ Q) i ⊣⊢ P i ∨ Q i. @@ -545,7 +561,7 @@ Lemma monPred_at_in i j : monPred_at (monPred_in j) i ⊣⊢ ⌜j ⊑ iâŒ. Proof. by unseal. Qed. Lemma monPred_at_absolutely i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j. Proof. by unseal. Qed. -Lemma monPred_at_ex i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j. +Lemma monPred_at_relatively i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j. Proof. by unseal. Qed. Lemma monPred_at_persistently_if i p P : bi_persistently_if p P i ⊣⊢ bi_persistently_if p (P i). @@ -565,7 +581,7 @@ Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed (* Laws for monPred_absolutely and of Absolute. *) Lemma monPred_absolutely_elim P : ∀ᵢ P ⊢ P. -Proof. unseal. split=>?. apply bi.forall_elim. Qed. +Proof. rewrite monPred_absolutely_unfold. unseal. split=>?. apply bi.forall_elim. Qed. Lemma monPred_absolutely_idemp P : ∀ᵢ (∀ᵢ P) ⊣⊢ ∀ᵢ P. Proof. apply bi.equiv_spec; split; [by apply monPred_absolutely_elim|]. @@ -601,6 +617,10 @@ Proof. apply bi.equiv_spec; split; unseal; split=>i /=. by rewrite (bi.forall_elim inhabitant). by apply bi.forall_intro. Qed. +Lemma monPred_absolutely_emp : ∀ᵢ (emp : monPred) ⊣⊢ emp. +Proof. rewrite monPred_emp_unfold. apply monPred_absolutely_embed. Qed. +Lemma monPred_absolutely_pure φ : ∀ᵢ (⌜ φ ⌠: monPred) ⊣⊢ ⌜ φ âŒ. +Proof. rewrite monPred_pure_unfold. apply monPred_absolutely_embed. Qed. Lemma monPred_relatively_intro P : P ⊢ ∃ᵢ P. Proof. unseal. split=>?. apply bi.exist_intro. Qed. @@ -633,27 +653,25 @@ Qed. Lemma absolute_absolutely P `{!Absolute P} : P ⊢ ∀ᵢ P. Proof. - rewrite /monPred_absolutely /= bi_embed_forall. apply bi.forall_intro=>?. + rewrite monPred_absolutely_unfold /= embed_forall. apply bi.forall_intro=>?. split=>?. unseal. apply absolute_at, _. Qed. Lemma absolute_relatively P `{!Absolute P} : ∃ᵢ P ⊢ P. Proof. - rewrite /monPred_relatively /= bi_embed_exist. apply bi.exist_elim=>?. + rewrite monPred_relatively_unfold /= embed_exist. apply bi.exist_elim=>?. split=>?. unseal. apply absolute_at, _. Qed. -Global Instance emb_absolute (P : PROP) : @Absolute I PROP ⎡P⎤. +Global Instance embed_absolute (P : PROP) : @Absolute I PROP ⎡P⎤. Proof. intros ??. by unseal. Qed. Global Instance pure_absolute φ : @Absolute I PROP ⌜φâŒ. -Proof. apply emb_absolute. Qed. +Proof. intros ??. by unseal. Qed. Global Instance emp_absolute : @Absolute I PROP emp. -Proof. apply emb_absolute. Qed. -Global Instance plainly_absolute P : Absolute (bi_plainly P). -Proof. apply emb_absolute. Qed. +Proof. intros ??. by unseal. Qed. Global Instance absolutely_absolute P : Absolute (∀ᵢ P). -Proof. apply emb_absolute. Qed. +Proof. intros ??. by unseal. Qed. Global Instance relatively_absolute P : Absolute (∃ᵢ P). -Proof. apply emb_absolute. Qed. +Proof. intros ??. by unseal. Qed. Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∧ Q). Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed. @@ -691,9 +709,6 @@ Proof. rewrite /bi_affinely. apply _. Qed. Global Instance absorbingly_absolute P `{!Absolute P} : Absolute (bi_absorbingly P). Proof. rewrite /bi_absorbingly. apply _. Qed. -Global Instance plainly_if_absolute P p `{!Absolute P} : - Absolute (bi_plainly_if p P). -Proof. rewrite /bi_plainly_if. destruct p; apply _. Qed. Global Instance persistently_if_absolute P p `{!Absolute P} : Absolute (bi_persistently_if p P). Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed. @@ -741,19 +756,19 @@ Global Instance monPred_absolutely_monoid_and_homomorphism : MonoidHomomorphism bi_and bi_and (≡) (@monPred_absolutely I PROP). Proof. split; [split|]; try apply _. apply monPred_absolutely_and. - apply monPred_absolutely_embed. + apply monPred_absolutely_pure. Qed. Global Instance monPred_absolutely_monoid_sep_entails_homomorphism : MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_absolutely I PROP). Proof. split; [split|]; try apply _. apply monPred_absolutely_sep_2. - by rewrite monPred_absolutely_embed. + by rewrite monPred_absolutely_emp. Qed. Global Instance monPred_absolutely_monoid_sep_homomorphism `{BiIndexBottom bot} : MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_absolutely I PROP). Proof. split; [split|]; try apply _. apply monPred_absolutely_sep. - by rewrite monPred_absolutely_embed. + by rewrite monPred_absolutely_emp. Qed. Lemma monPred_absolutely_big_sepL_entails {A} (Φ : nat → A → monPred) l : @@ -802,17 +817,8 @@ Global Instance big_sepMS_absolute `{Countable A} (Φ : A → monPred) Absolute ([∗ mset] y ∈ X, Φ y)%I. Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply absolute_at. Qed. -End bi_facts. - -Section sbi_facts. -Context {I : biIndex} {PROP : sbi}. -Local Notation monPred := (monPred I PROP). -Local Notation monPredSI := (monPredSI I PROP). -Implicit Types i : I. -Implicit Types P Q : monPred. - (** bupd *) -Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI. +Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd. Proof. split; unseal; unfold monPred_bupd_def, monPred_upclosed. (* Note: Notation is somewhat broken here. *) @@ -825,27 +831,35 @@ Proof. - intros P Q. split=> /= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall. apply bi.forall_intro=><-. rewrite -bupd_frame_r bi.forall_elim bi.pure_impl_forall bi.forall_elim //. - - intros P. split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall - bi.forall_elim // -bi.plainly_forall bupd_plainly bi.forall_elim //. Qed. +Global Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI := + {| bi_bupd_mixin := monPred_bupd_mixin |}. -Lemma monPred_at_bupd `{BUpdFacts PROP} i P : (|==> P) i ⊣⊢ |==> P i. +Lemma monPred_at_bupd `{BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i. Proof. unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split. - rewrite !bi.forall_elim //. - do 2 apply bi.forall_intro=>?. by do 2 f_equiv. Qed. -Global Instance bupd_absolute `{BUpdFacts PROP} P `{!Absolute P} : +Global Instance bupd_absolute `{BiBUpd PROP} P `{!Absolute P} : Absolute (|==> P)%I. Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed. -Lemma monPred_bupd_embed `{BUpdFacts PROP} (P : PROP) : - ⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredSI) ⎡P⎤. +Lemma monPred_bupd_embed `{BiBUpd PROP} (P : PROP) : + ⎡|==> P⎤ ⊣⊢ bupd (PROP:=monPredI) ⎡P⎤. Proof. unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split. - by do 2 apply bi.forall_intro=>?. - rewrite !bi.forall_elim //. Qed. +End bi_facts. + +Section sbi_facts. +Context {I : biIndex} {PROP : sbi}. +Local Notation monPred := (monPred I PROP). +Local Notation monPredSI := (monPredSI I PROP). +Implicit Types i : I. +Implicit Types P Q : monPred. Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i). Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed. @@ -862,19 +876,26 @@ Proof. by apply timeless, bi.exist_timeless. Qed. -Global Instance monPred_sbi_embedding : SbiEmbedding PROP monPredSI. -Proof. split; try apply _; by unseal. Qed. +Global Instance monPred_sbi_embed : SbiEmbed PROP monPredSI. +Proof. + split; unseal=> //. intros ? P Q. + apply (@bi.f_equiv _ _ _ (λ P, monPred_at P inhabitant)); solve_proper. +Qed. -Global Instance monPred_fupd_facts `{FUpdFacts PROP} : FUpdFacts monPredSI. +Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, â– (P i) ⎤%I. +Proof. by unseal. Qed. +Lemma monPred_internal_eq_unfold : @sbi_internal_eq monPredSI = λ A x y, ⎡ x ≡ y ⎤%I. +Proof. by unseal. Qed. + +Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredSI monPred_fupd. Proof. - split; first apply _; unseal; unfold monPred_fupd_def, monPred_upclosed. + split; unseal; unfold monPred_fupd_def, monPred_upclosed. (* Note: Notation is somewhat broken here. *) - intros E1 E2 n P Q HPQ. split=>/= i. by repeat f_equiv. - intros E1 E2 P HE12. split=>/= i. do 2 setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro=>?. rewrite (fupd_intro_mask E1 E2 (P i)) //. f_equiv. do 2 apply bi.forall_intro=>?. do 2 f_equiv. by etrans. - - intros E P. split=>/= i. by setoid_rewrite bupd_fupd. - intros E1 E2 P. split=>/= i. etrans; [apply bi.equiv_entails, bi.except_0_forall|]. do 2 f_equiv. rewrite bi.pure_impl_forall bi.except_0_forall. do 2 f_equiv. by apply except_0_fupd. @@ -886,6 +907,28 @@ Proof. - intros E1 E2 P Q. split=>/= i. setoid_rewrite bi.pure_impl_forall. do 2 setoid_rewrite bi.sep_forall_r. setoid_rewrite fupd_frame_r. by repeat f_equiv. +Qed. +Global Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredSI := + {| bi_fupd_mixin := monPred_fupd_mixin |}. +Global Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredSI. +Proof. + rewrite /BiBUpdFUpd; unseal; unfold monPred_fupd_def, monPred_upclosed. + intros E P. split=>/= i. by setoid_rewrite bupd_fupd. +Qed. + +Global Instance monPred_bi_bupd_plainly `{BiBUpdPlainly PROP} : BiBUpdPlainly monPredSI. +Proof. + rewrite /BiBUpdPlainly=> P; unseal. + split=> /= i. rewrite bi.forall_elim bi.pure_impl_forall. + by rewrite bi.forall_elim // -plainly_forall bupd_plainly bi.forall_elim. +Qed. + +Global Instance monPred_at_plain `{BiPlainly PROP} P i : Plain P → Plain (P i). +Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed. + +Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI. +Proof. + split; unseal. - intros E1 E2 E2' P Q ? HE12. split=>/= i. repeat setoid_rewrite bi.pure_impl_forall. do 4 f_equiv. rewrite 4?bi.forall_elim // fupd_plain' //. apply bi.wand_intro_r. rewrite bi.wand_elim_l. do 2 apply bi.forall_intro=>?. @@ -895,13 +938,14 @@ Proof. Qed. (** Unfolding lemmas *) - +Lemma monPred_at_plainly `{BiPlainly PROP} i P : (â– P) i ⊣⊢ ∀ j, â– (P j). +Proof. by unseal. Qed. Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) : @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b. -Proof. by apply monPred_at_embed. Qed. +Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed. Lemma monPred_at_later i P : (â–· P) i ⊣⊢ â–· P i. Proof. by unseal. Qed. -Lemma monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P : +Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P : (|={E1,E2}=> P) i ⊣⊢ |={E1,E2}=> P i. Proof. unseal. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split. @@ -911,7 +955,7 @@ Qed. Lemma monPred_at_except_0 i P : (â—‡ P) i ⊣⊢ â—‡ P i. Proof. by unseal. Qed. -Lemma monPred_fupd_embed `{FUpdFacts PROP} E1 E2 (P : PROP) : +Lemma monPred_fupd_embed `{BiFUpd PROP} E1 E2 (P : PROP) : ⎡|={E1,E2}=> P⎤ ⊣⊢ fupd E1 E2 (PROP:=monPred) ⎡P⎤. Proof. unseal. split=>i /=. setoid_rewrite bi.pure_impl_forall. apply bi.equiv_spec; split. @@ -928,7 +972,17 @@ Proof. -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI. Qed. +Global Instance monPred_absolutely_plain `{BiPlainly PROP} P : Plain P → Plain (∀ᵢ P). +Proof. rewrite monPred_absolutely_unfold. apply _. Qed. +Global Instance monPred_relatively_plain `{BiPlainly PROP} P : Plain P → Plain (∃ᵢ P). +Proof. rewrite monPred_relatively_unfold. apply _. Qed. + (** Absolute *) +Global Instance plainly_absolute `{BiPlainly PROP} P : Absolute (â– P). +Proof. intros ??. by unseal. Qed. +Global Instance plainly_if_absolute `{BiPlainly PROP} P p `{!Absolute P} : + Absolute (â– ?p P). +Proof. rewrite /plainly_if. destruct p; apply _. Qed. Global Instance internal_eq_absolute {A : ofeT} (x y : A) : @Absolute I PROP (x ≡ y)%I. @@ -941,8 +995,7 @@ Proof. induction n; apply _. Qed. Global Instance except0_absolute P `{!Absolute P} : Absolute (â—‡ P)%I. Proof. rewrite /sbi_except_0. apply _. Qed. -Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{FUpdFacts PROP} : +Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{BiFUpd PROP} : Absolute (|={E1,E2}=> P)%I. Proof. intros ??. by rewrite !monPred_at_fupd absolute_at. Qed. - End sbi_facts. diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v new file mode 100644 index 0000000000000000000000000000000000000000..06fff510df79c80d1340fc7d52d23d2ebb68df29 --- /dev/null +++ b/theories/bi/plainly.v @@ -0,0 +1,528 @@ +From iris.bi Require Export derived_laws. +From iris.algebra Require Import monoid. +Import interface.bi derived_laws.bi. + +Class Plainly (A : Type) := plainly : A → A. +Hint Mode Plainly ! : typeclass_instances. +Instance: Params (@plainly) 2. +Notation "â– P" := (plainly P)%I + (at level 20, right associativity) : bi_scope. + +(* Mixins allow us to create instances easily without having to use Program *) +Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := { + bi_plainly_mixin_plainly_ne : NonExpansive plainly; + + bi_plainly_mixin_plainly_mono P Q : (P ⊢ Q) → â– P ⊢ â– Q; + bi_plainly_mixin_plainly_elim_persistently P : â– P ⊢ bi_persistently P; + bi_plainly_mixin_plainly_idemp_2 P : â– P ⊢ â– â– P; + + bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) : + (∀ a, â– (Ψ a)) ⊢ â– (∀ a, Ψ a); + + (* The following two laws are very similar, and indeed they hold not just + for persistently and plainly, but for any modality defined as `M P n x := + ∀ y, R x y → P n y`. *) + bi_plainly_mixin_persistently_impl_plainly P Q : + (â– P → bi_persistently Q) ⊢ bi_persistently (â– P → Q); + bi_plainly_mixin_plainly_impl_plainly P Q : (â– P → â– Q) ⊢ â– (â– P → Q); + + bi_plainly_mixin_plainly_emp_intro P : P ⊢ â– emp; + bi_plainly_mixin_plainly_absorb P Q : â– P ∗ Q ⊢ â– P; + + bi_plainly_mixin_prop_ext P Q : â– ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q; + + bi_plainly_mixin_later_plainly_1 P : â–· â– P ⊢ â– â–· P; + bi_plainly_mixin_later_plainly_2 P : â– â–· P ⊢ â–· â– P; +}. + +Class BiPlainly (PROP : sbi) := { + bi_plainly_plainly :> Plainly PROP; + bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly; +}. +Hint Mode BiPlainly ! : typeclass_instances. +Arguments bi_plainly_plainly : simpl never. + +Class BiPlainlyExist `{!BiPlainly PROP} := + plainly_exist_1 A (Ψ : A → PROP) : + â– (∃ a, Ψ a) ⊢ ∃ a, â– (Ψ a). +Arguments BiPlainlyExist : clear implicits. +Arguments BiPlainlyExist _ {_}. +Arguments plainly_exist_1 _ {_ _} _. +Hint Mode BiPlainlyExist + ! : typeclass_instances. + +Section plainly_laws. + Context `{BiPlainly PROP}. + Implicit Types P Q : PROP. + + Global Instance plainly_ne : NonExpansive (@plainly PROP _). + Proof. eapply bi_plainly_mixin_plainly_ne, bi_plainly_mixin. Qed. + + Lemma plainly_mono P Q : (P ⊢ Q) → â– P ⊢ â– Q. + Proof. eapply bi_plainly_mixin_plainly_mono, bi_plainly_mixin. Qed. + Lemma plainly_elim_persistently P : â– P ⊢ bi_persistently P. + Proof. eapply bi_plainly_mixin_plainly_elim_persistently, bi_plainly_mixin. Qed. + Lemma plainly_idemp_2 P : â– P ⊢ â– â– P. + Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed. + Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, â– (Ψ a)) ⊢ â– (∀ a, Ψ a). + Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed. + Lemma persistently_impl_plainly P Q : + (â– P → bi_persistently Q) ⊢ bi_persistently (â– P → Q). + Proof. eapply bi_plainly_mixin_persistently_impl_plainly, bi_plainly_mixin. Qed. + Lemma plainly_impl_plainly P Q : (â– P → â– Q) ⊢ â– (â– P → Q). + Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed. + Lemma plainly_absorb P Q : â– P ∗ Q ⊢ â– P. + Proof. eapply bi_plainly_mixin_plainly_absorb, bi_plainly_mixin. Qed. + Lemma plainly_emp_intro P : P ⊢ â– emp. + Proof. eapply bi_plainly_mixin_plainly_emp_intro, bi_plainly_mixin. Qed. + + Lemma prop_ext P Q : â– ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q. + Proof. eapply bi_plainly_mixin_prop_ext, bi_plainly_mixin. Qed. + + Lemma later_plainly_1 P : â–· â– P ⊢ â– (â–· P). + Proof. eapply bi_plainly_mixin_later_plainly_1, bi_plainly_mixin. Qed. + Lemma later_plainly_2 P : â– â–· P ⊢ â–· â– P. + Proof. eapply bi_plainly_mixin_later_plainly_2, bi_plainly_mixin. Qed. +End plainly_laws. + +(* Derived properties and connectives *) +Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ â– P. +Arguments Plain {_ _} _%I : simpl never. +Arguments plain {_ _} _%I {_}. +Hint Mode Plain + ! ! : typeclass_instances. +Instance: Params (@Plain) 1. + +Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP := + (if p then â– P else P)%I. +Arguments plainly_if {_ _} !_ _%I /. +Instance: Params (@plainly_if) 2. +Typeclasses Opaque plainly_if. + +Notation "â– ? p P" := (plainly_if p P)%I + (at level 20, p at level 9, P at level 20, + right associativity, format "â– ? p P") : bi_scope. + +(* Derived laws *) +Section plainly_derived. +Context `{BiPlainly PROP}. +Implicit Types P : PROP. + +Hint Resolve pure_intro forall_intro. +Hint Resolve or_elim or_intro_l' or_intro_r'. +Hint Resolve and_intro and_elim_l' and_elim_r'. + +Global Instance plainly_proper : + Proper ((⊣⊢) ==> (⊣⊢)) (@plainly PROP _) := ne_proper _. + +Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@plainly PROP _). +Proof. intros P Q; apply plainly_mono. Qed. +Global Instance plainly_flip_mono' : + Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _). +Proof. intros P Q; apply plainly_mono. Qed. + +Lemma affinely_plainly_elim P : bi_affinely (â– P) ⊢ P. +Proof. by rewrite plainly_elim_persistently affinely_persistently_elim. Qed. + +Lemma persistently_plainly P : bi_persistently (â– P) ⊣⊢ â– P. +Proof. + apply (anti_symm _). + - by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorb. + - by rewrite {1}plainly_idemp_2 plainly_elim_persistently. +Qed. +Lemma persistently_if_plainly P p : bi_persistently_if p (â– P) ⊣⊢ â– P. +Proof. destruct p; last done. exact: persistently_plainly. Qed. + +Lemma plainly_persistently P : â– (bi_persistently P) ⊣⊢ â– P. +Proof. + apply (anti_symm _). + - rewrite -{1}(left_id True%I bi_and (â– _)%I) (plainly_emp_intro True%I). + rewrite -{2}(persistently_and_emp_elim P). + rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[]. + - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P). +Qed. + +Lemma absorbingly_plainly P : bi_absorbingly (â– P) ⊣⊢ â– P. +Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed. + +Lemma plainly_and_sep_elim P Q : â– P ∧ Q -∗ (emp ∧ P) ∗ Q. +Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed. +Lemma plainly_and_sep_assoc P Q R : â– P ∧ (Q ∗ R) ⊣⊢ (â– P ∧ Q) ∗ R. +Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed. +Lemma plainly_and_emp_elim P : emp ∧ â– P ⊢ P. +Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed. +Lemma plainly_elim_absorbingly P : â– P ⊢ bi_absorbingly P. +Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed. +Lemma plainly_elim P `{!Absorbing P} : â– P ⊢ P. +Proof. by rewrite plainly_elim_persistently persistently_elim. Qed. + +Lemma plainly_idemp_1 P : â– â– P ⊢ â– P. +Proof. by rewrite plainly_elim_absorbingly absorbingly_plainly. Qed. +Lemma plainly_idemp P : â– â– P ⊣⊢ â– P. +Proof. apply (anti_symm _); auto using plainly_idemp_1, plainly_idemp_2. Qed. + +Lemma plainly_intro' P Q : (â– P ⊢ Q) → â– P ⊢ â– Q. +Proof. intros <-. apply plainly_idemp_2. Qed. + +Lemma plainly_pure φ : ■⌜φ⌠⊣⊢ bi_pure (PROP:=PROP) φ. +Proof. + apply (anti_symm _); auto. + - by rewrite plainly_elim_persistently persistently_pure. + - apply pure_elim'=> Hφ. + trans (∀ x : False, â– True : PROP)%I; [by apply forall_intro|]. + rewrite plainly_forall_2. by rewrite -(pure_intro _ φ). +Qed. +Lemma plainly_forall {A} (Ψ : A → PROP) : â– (∀ a, Ψ a) ⊣⊢ ∀ a, â– (Ψ a). +Proof. + apply (anti_symm _); auto using plainly_forall_2. + apply forall_intro=> x. by rewrite (forall_elim x). +Qed. +Lemma plainly_exist_2 {A} (Ψ : A → PROP) : (∃ a, â– (Ψ a)) ⊢ â– (∃ a, Ψ a). +Proof. apply exist_elim=> x. by rewrite (exist_intro x). Qed. +Lemma plainly_exist `{!BiPlainlyExist PROP} {A} (Ψ : A → PROP) : + â– (∃ a, Ψ a) ⊣⊢ ∃ a, â– (Ψ a). +Proof. apply (anti_symm _); auto using plainly_exist_1, plainly_exist_2. Qed. +Lemma plainly_and P Q : â– (P ∧ Q) ⊣⊢ â– P ∧ â– Q. +Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed. +Lemma plainly_or_2 P Q : â– P ∨ â– Q ⊢ â– (P ∨ Q). +Proof. rewrite !or_alt -plainly_exist_2. by apply exist_mono=> -[]. Qed. +Lemma plainly_or `{!BiPlainlyExist PROP} P Q : â– (P ∨ Q) ⊣⊢ â– P ∨ â– Q. +Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed. +Lemma plainly_impl P Q : â– (P → Q) ⊢ â– P → â– Q. +Proof. + apply impl_intro_l; rewrite -plainly_and. + apply plainly_mono, impl_elim with P; auto. +Qed. + +Lemma plainly_sep_dup P : â– P ⊣⊢ â– P ∗ â– P. +Proof. + apply (anti_symm _). + - rewrite -{1}(idemp bi_and (â– _)%I). + by rewrite -{2}(left_id emp%I _ (â– _)%I) plainly_and_sep_assoc and_elim_l. + - by rewrite plainly_absorb. +Qed. + +Lemma plainly_and_sep_l_1 P Q : â– P ∧ Q ⊢ â– P ∗ Q. +Proof. by rewrite -{1}(left_id emp%I _ Q%I) plainly_and_sep_assoc and_elim_l. Qed. +Lemma plainly_and_sep_r_1 P Q : P ∧ â– Q ⊢ P ∗ â– Q. +Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed. + +Lemma plainly_True_emp : â– True ⊣⊢ â– (@bi_emp PROP). +Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed. +Lemma plainly_and_sep P Q : â– (P ∧ Q) ⊢ â– (P ∗ Q). +Proof. + rewrite plainly_and. + rewrite -{1}plainly_idemp -plainly_and -{1}(left_id emp%I _ Q%I). + by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim. +Qed. + +Lemma plainly_affinely P : â– (bi_affinely P) ⊣⊢ â– P. +Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed. + +Lemma and_sep_plainly P Q : â– P ∧ â– Q ⊣⊢ â– P ∗ â– Q. +Proof. + apply (anti_symm _); auto using plainly_and_sep_l_1. + apply and_intro. + - by rewrite plainly_absorb. + - by rewrite comm plainly_absorb. +Qed. +Lemma plainly_sep_2 P Q : â– P ∗ â– Q ⊢ â– (P ∗ Q). +Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed. +Lemma plainly_sep `{BiPositive PROP} P Q : â– (P ∗ Q) ⊣⊢ â– P ∗ â– Q. +Proof. + apply (anti_symm _); auto using plainly_sep_2. + rewrite -(plainly_affinely (_ ∗ _)%I) affinely_sep -and_sep_plainly. apply and_intro. + - by rewrite (affinely_elim_emp Q) right_id affinely_elim. + - by rewrite (affinely_elim_emp P) left_id affinely_elim. +Qed. + +Lemma plainly_wand P Q : â– (P -∗ Q) ⊢ â– P -∗ â– Q. +Proof. apply wand_intro_r. by rewrite plainly_sep_2 wand_elim_l. Qed. + +Lemma plainly_entails_l P Q : (P ⊢ â– Q) → P ⊢ â– Q ∗ P. +Proof. intros; rewrite -plainly_and_sep_l_1; auto. Qed. +Lemma plainly_entails_r P Q : (P ⊢ â– Q) → P ⊢ P ∗ â– Q. +Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed. + +Lemma plainly_impl_wand_2 P Q : â– (P -∗ Q) ⊢ â– (P → Q). +Proof. + apply plainly_intro', impl_intro_r. + rewrite -{2}(left_id emp%I _ P%I) plainly_and_sep_assoc. + by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l. +Qed. + +Lemma impl_wand_plainly_2 P Q : (â– P -∗ Q) ⊢ (â– P → Q). +Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed. + +Lemma impl_wand_affinely_plainly P Q : (â– P → Q) ⊣⊢ (bi_affinely (â– P) -∗ Q). +Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed. + +Section plainly_affine_bi. + Context `{BiAffine PROP}. + + Lemma plainly_emp : â– emp ⊣⊢ bi_emp (PROP:=PROP). + Proof. by rewrite -!True_emp plainly_pure. Qed. + + Lemma plainly_and_sep_l P Q : â– P ∧ Q ⊣⊢ â– P ∗ Q. + Proof. + apply (anti_symm (⊢)); + eauto using plainly_and_sep_l_1, sep_and with typeclass_instances. + Qed. + Lemma plainly_and_sep_r P Q : P ∧ â– Q ⊣⊢ P ∗ â– Q. + Proof. by rewrite !(comm _ P) plainly_and_sep_l. Qed. + + Lemma plainly_impl_wand P Q : â– (P → Q) ⊣⊢ â– (P -∗ Q). + Proof. + apply (anti_symm (⊢)); auto using plainly_impl_wand_2. + apply plainly_intro', wand_intro_l. + by rewrite -plainly_and_sep_r plainly_elim impl_elim_r. + Qed. + + Lemma impl_wand_plainly P Q : (â– P → Q) ⊣⊢ (â– P -∗ Q). + Proof. + apply (anti_symm (⊢)). by rewrite -impl_wand_1. by rewrite impl_wand_plainly_2. + Qed. +End plainly_affine_bi. + +(* Conditional plainly *) +Global Instance plainly_if_ne p : NonExpansive (@plainly_if PROP _ p). +Proof. solve_proper. Qed. +Global Instance plainly_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@plainly_if PROP _ p). +Proof. solve_proper. Qed. +Global Instance plainly_if_mono' p : Proper ((⊢) ==> (⊢)) (@plainly_if PROP _ p). +Proof. solve_proper. Qed. +Global Instance plainly_if_flip_mono' p : + Proper (flip (⊢) ==> flip (⊢)) (@plainly_if PROP _ p). +Proof. solve_proper. Qed. + +Lemma plainly_if_mono p P Q : (P ⊢ Q) → â– ?p P ⊢ â– ?p Q. +Proof. by intros ->. Qed. + +Lemma plainly_if_pure p φ : â– ?p ⌜φ⌠⊣⊢ bi_pure (PROP:=PROP) φ. +Proof. destruct p; simpl; auto using plainly_pure. Qed. +Lemma plainly_if_and p P Q : â– ?p (P ∧ Q) ⊣⊢ â– ?p P ∧ â– ?p Q. +Proof. destruct p; simpl; auto using plainly_and. Qed. +Lemma plainly_if_or_2 p P Q : â– ?p P ∨ â– ?p Q ⊢ â– ?p (P ∨ Q). +Proof. destruct p; simpl; auto using plainly_or_2. Qed. +Lemma plainly_if_or `{!BiPlainlyExist PROP} p P Q : â– ?p (P ∨ Q) ⊣⊢ â– ?p P ∨ â– ?p Q. +Proof. destruct p; simpl; auto using plainly_or. Qed. +Lemma plainly_if_exist_2 {A} p (Ψ : A → PROP) : (∃ a, â– ?p (Ψ a)) ⊢ â– ?p (∃ a, Ψ a). +Proof. destruct p; simpl; auto using plainly_exist_2. Qed. +Lemma plainly_if_exist `{!BiPlainlyExist PROP} {A} p (Ψ : A → PROP) : + â– ?p (∃ a, Ψ a) ⊣⊢ ∃ a, â– ?p (Ψ a). +Proof. destruct p; simpl; auto using plainly_exist. Qed. +Lemma plainly_if_sep_2 `{!BiPositive PROP} p P Q : â– ?p P ∗ â– ?p Q ⊢ â– ?p (P ∗ Q). +Proof. destruct p; simpl; auto using plainly_sep_2. Qed. + +Lemma plainly_if_idemp p P : â– ?p â– ?p P ⊣⊢ â– ?p P. +Proof. destruct p; simpl; auto using plainly_idemp. Qed. + +(* Properties of plain propositions *) +Global Instance Plain_proper : Proper ((≡) ==> iff) (@Plain PROP _). +Proof. solve_proper. Qed. + +Lemma plain_plainly_2 P `{!Plain P} : P ⊢ â– P. +Proof. done. Qed. +Lemma plain_plainly P `{!Plain P, !Absorbing P} : â– P ⊣⊢ P. +Proof. apply (anti_symm _), plain_plainly_2, _. by apply plainly_elim. Qed. +Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ â– Q. +Proof. by intros <-. Qed. + +(* Typeclass instances *) +Global Instance plainly_absorbing P : Absorbing (â– P). +Proof. by rewrite /Absorbing /bi_absorbingly comm plainly_absorb. Qed. +Global Instance plainly_if_absorbing P p : + Absorbing P → Absorbing (plainly_if p P). +Proof. intros; destruct p; simpl; apply _. Qed. + +(* Not an instance, see the bottom of this file *) +Lemma plain_persistent P : Plain P → Persistent P. +Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed. + +(* Not an instance, see the bottom of this file *) +Lemma impl_persistent P Q : + Absorbing P → Plain P → Persistent Q → Persistent (P → Q). +Proof. + intros. by rewrite /Persistent {2}(plain P) -persistently_impl_plainly + -(persistent Q) (plainly_elim_absorbingly P) absorbing. +Qed. + +Global Instance plainly_persistent P : Persistent (â– P). +Proof. by rewrite /Persistent persistently_plainly. Qed. + +Global Instance wand_persistent P Q : + Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q). +Proof. + intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (â– P → Q)%I). + - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q). + by rewrite affinely_plainly_elim. + - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r. +Qed. + +(* Instances for big operators *) +Global Instance plainly_and_homomorphism : + MonoidHomomorphism bi_and bi_and (≡) (@plainly PROP _). +Proof. + split; [split|]; try apply _. apply plainly_and. apply plainly_pure. +Qed. + +Global Instance plainly_or_homomorphism `{!BiPlainlyExist PROP} : + MonoidHomomorphism bi_or bi_or (≡) (@plainly PROP _). +Proof. + split; [split|]; try apply _. apply plainly_or. apply plainly_pure. +Qed. + +Global Instance plainly_sep_weak_homomorphism `{!BiPositive PROP, !BiAffine PROP} : + WeakMonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _). +Proof. split; try apply _. apply plainly_sep. Qed. + +Global Instance plainly_sep_homomorphism `{BiAffine PROP} : + MonoidHomomorphism bi_sep bi_sep (≡) (@plainly PROP _). +Proof. split. apply _. apply plainly_emp. Qed. + +Global Instance plainly_sep_entails_weak_homomorphism : + WeakMonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _). +Proof. split; try apply _. intros P Q; by rewrite plainly_sep_2. Qed. + +Global Instance plainly_sep_entails_homomorphism `{!BiAffine PROP} : + MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@plainly PROP _). +Proof. split. apply _. simpl. rewrite plainly_emp. done. Qed. + +Global Instance limit_preserving_Plain {A:ofeT} `{Cofe A} (Φ : A → PROP) : + NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)). +Proof. intros. apply limit_preserving_entails; solve_proper. Qed. + +(* Plainness instances *) +Global Instance pure_plain φ : Plain (⌜φâŒ%I : PROP). +Proof. by rewrite /Plain plainly_pure. Qed. +Global Instance emp_plain : Plain (PROP:=PROP) emp. +Proof. apply plainly_emp_intro. Qed. +Global Instance and_plain P Q : Plain P → Plain Q → Plain (P ∧ Q). +Proof. intros. by rewrite /Plain plainly_and -!plain. Qed. +Global Instance or_plain P Q : Plain P → Plain Q → Plain (P ∨ Q). +Proof. intros. by rewrite /Plain -plainly_or_2 -!plain. Qed. +Global Instance forall_plain {A} (Ψ : A → PROP) : + (∀ x, Plain (Ψ x)) → Plain (∀ x, Ψ x). +Proof. + intros. rewrite /Plain plainly_forall. apply forall_mono=> x. by rewrite -plain. +Qed. +Global Instance exist_plain {A} (Ψ : A → PROP) : + (∀ x, Plain (Ψ x)) → Plain (∃ x, Ψ x). +Proof. + intros. rewrite /Plain -plainly_exist_2. apply exist_mono=> x. by rewrite -plain. +Qed. + +Global Instance impl_plain P Q : Absorbing P → Plain P → Plain Q → Plain (P → Q). +Proof. + intros. by rewrite /Plain {2}(plain P) -plainly_impl_plainly -(plain Q) + (plainly_elim_absorbingly P) absorbing. +Qed. +Global Instance wand_plain P Q : + Plain P → Plain Q → Absorbing Q → Plain (P -∗ Q). +Proof. + intros. rewrite /Plain {2}(plain P). trans (â– (â– P → Q))%I. + - rewrite -plainly_impl_plainly impl_wand_affinely_plainly -(plain Q). + by rewrite affinely_plainly_elim. + - apply plainly_mono, wand_intro_l. by rewrite sep_and impl_elim_r. +Qed. +Global Instance sep_plain P Q : Plain P → Plain Q → Plain (P ∗ Q). +Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed. + +Global Instance plainly_plain P : Plain (â– P). +Proof. by rewrite /Plain plainly_idemp. Qed. +Global Instance persistently_plain P : Plain P → Plain (bi_persistently P). +Proof. + rewrite /Plain=> HP. rewrite {1}HP plainly_persistently persistently_plainly //. +Qed. +Global Instance affinely_plain P : Plain P → Plain (bi_affinely P). +Proof. rewrite /bi_affinely. apply _. Qed. +Global Instance absorbingly_plain P : Plain P → Plain (bi_absorbingly P). +Proof. rewrite /bi_absorbingly. apply _. Qed. +Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) : + (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx). +Proof. destruct mx; apply _. Qed. + +(* Interaction with equality *) +Lemma plainly_internal_eq {A:ofeT} (a b : A) : plainly (A:=PROP) (a ≡ b) ⊣⊢ a ≡ b. +Proof. + apply (anti_symm (⊢)). + { by rewrite plainly_elim. } + apply (internal_eq_rewrite' a b (λ b, â– (a ≡ b))%I); [solve_proper|done|]. + rewrite -(internal_eq_refl True%I a) plainly_pure; auto. +Qed. + +Lemma plainly_alt P : â– P ⊣⊢ bi_affinely P ≡ emp. +Proof. + rewrite -plainly_affinely. apply (anti_symm (⊢)). + - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l. + + by rewrite affinely_elim_emp left_id. + + by rewrite left_id. + - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly). + by rewrite -plainly_True_emp plainly_pure True_impl. +Qed. + +Lemma plainly_alt_absorbing P `{!Absorbing P} : â– P ⊣⊢ P ≡ True. +Proof. + apply (anti_symm (⊢)). + - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto. + - rewrite internal_eq_sym (internal_eq_rewrite _ _ plainly). + by rewrite plainly_pure True_impl. +Qed. + +Lemma plainly_True_alt P : â– (True -∗ P) ⊣⊢ P ≡ True. +Proof. + apply (anti_symm (⊢)). + - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l; auto. + by rewrite wand_elim_r. + - rewrite internal_eq_sym (internal_eq_rewrite _ _ + (λ Q, â– (True -∗ Q))%I ltac:(shelve)); last solve_proper. + by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl. +Qed. + +(* Interaction with â–· *) +Lemma later_plainly P : â–· â– P ⊣⊢ â– â–· P. +Proof. apply (anti_symm _); auto using later_plainly_1, later_plainly_2. Qed. +Lemma laterN_plainly n P : â–·^n â– P ⊣⊢ â– â–·^n P. +Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_plainly. Qed. + +Lemma later_plainly_if p P : â–· â– ?p P ⊣⊢ â– ?p â–· P. +Proof. destruct p; simpl; auto using later_plainly. Qed. +Lemma laterN_plainly_if n p P : â–·^n â– ?p P ⊣⊢ â– ?p (â–·^n P). +Proof. destruct p; simpl; auto using laterN_plainly. Qed. + +Lemma except_0_plainly_1 P : â—‡ â– P ⊢ â– â—‡ P. +Proof. by rewrite /sbi_except_0 -plainly_or_2 -later_plainly plainly_pure. Qed. +Lemma except_0_plainly `{!BiPlainlyExist PROP} P : â—‡ â– P ⊣⊢ â– â—‡ P. +Proof. by rewrite /sbi_except_0 plainly_or -later_plainly plainly_pure. Qed. + +Global Instance internal_eq_plain {A : ofeT} (a b : A) : + Plain (a ≡ b : PROP)%I. +Proof. by intros; rewrite /Plain plainly_internal_eq. Qed. + +Global Instance later_plain P : Plain P → Plain (â–· P). +Proof. intros. by rewrite /Plain -later_plainly {1}(plain P). Qed. +Global Instance laterN_plain n P : Plain P → Plain (â–·^n P). +Proof. induction n; apply _. Qed. +Global Instance except_0_plain P : Plain P → Plain (â—‡ P). +Proof. rewrite /sbi_except_0; apply _. Qed. + +Global Instance plainly_timeless P `{!BiPlainlyExist PROP} : + Timeless P → Timeless (â– P). +Proof. + intros. rewrite /Timeless /sbi_except_0 later_plainly_1. + by rewrite (timeless P) /sbi_except_0 plainly_or {1}plainly_elim. +Qed. +End plainly_derived. + +(* When declared as an actual instance, [plain_persistent] will cause +failing proof searches to take exponential time, as Coq will try to +apply it the instance at any node in the proof search tree. + +To avoid that, we declare it using a [Hint Immediate], so that it will +only be used at the leaves of the proof search tree, i.e. when the +premise of the hint can be derived from just the current context. *) +Hint Immediate plain_persistent : typeclass_instances. + +(* Not defined using an ordinary [Instance] because the default +[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof +search for the other premises fail. See the proof of [coreP_persistent] for an +example where it would fail with a regular [Instance].*) +Hint Extern 4 (Persistent (_ → _)) => eapply @impl_persistent : typeclass_instances. diff --git a/theories/bi/updates.v b/theories/bi/updates.v index e84991291f1f38ab5290fe928f851f4f99507a9c..cb97dd5e844b843144fb2854eb39c1a27861b0ba 100644 --- a/theories/bi/updates.v +++ b/theories/bi/updates.v @@ -1,6 +1,8 @@ From stdpp Require Import coPset. -From iris.bi Require Import interface derived_laws big_op. +From iris.bi Require Import interface derived_laws big_op plainly. +(* We first define operational type classes for the notations, and then later +bundle these operational type classes with the laws. *) Class BUpd (PROP : Type) : Type := bupd : PROP → PROP. Instance : Params (@bupd) 2. Hint Mode BUpd ! : typeclass_instances. @@ -35,7 +37,6 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope. (** Fancy updates that take a step. *) - Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I (at level 99, E1, E2 at level 50, Q at level 200, format "|={ E1 , E2 }â–·=> Q") : bi_scope. @@ -49,26 +50,101 @@ Notation "P ={ E }â–·=∗ Q" := (P ={E,E}â–·=∗ Q)%I (at level 99, E at level 50, Q at level 200, format "P ={ E }â–·=∗ Q") : bi_scope. -(** BUpd facts *) - -Class BUpdFacts (PROP : sbi) `{BUpd PROP} : Prop := - { bupd_ne :> NonExpansive bupd; - bupd_intro (P : PROP) : P ==∗ P; - bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q; - bupd_trans (P : PROP) : (|==> |==> P) ==∗ P; - bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R; - bupd_plainly (P : PROP) : (|==> bi_plainly P) -∗ P }. -Hint Mode BUpdFacts ! - : typeclass_instances. +(** Bundled versions *) +(* Mixins allow us to create instances easily without having to use Program *) +Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := { + bi_bupd_mixin_bupd_ne : NonExpansive bupd; + bi_bupd_mixin_bupd_intro (P : PROP) : P ==∗ P; + bi_bupd_mixin_bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q; + bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) ==∗ P; + bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R; +}. + +Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := { + bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd E1 E2); + bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P; + bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : â—‡ (|={E1,E2}=> P) ={E1,E2}=∗ P; + bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q; + bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P; + bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) : + E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌠→ P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P; + bi_fupd_mixin_fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q; +}. + +Class BiBUpd (PROP : bi) := { + bi_bupd_bupd :> BUpd PROP; + bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd; +}. +Hint Mode BiBUpd ! : typeclass_instances. +Arguments bi_bupd_bupd : simpl never. + +Class BiFUpd (PROP : sbi) := { + bi_fupd_fupd :> FUpd PROP; + bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd; +}. +Hint Mode BiBUpd ! : typeclass_instances. +Arguments bi_fupd_fupd : simpl never. + +Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} := + bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P. + +Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} := + bupd_plainly (P : PROP) : (|==> â– P) -∗ P. + +Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := { + fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} : + E1 ⊆ E2 → + (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P; + later_fupd_plain E (P : PROP) `{!Plain P} : + (â–· |={E}=> P) ={E}=∗ â–· â—‡ P; +}. + +Section bupd_laws. + Context `{BiBUpd PROP}. + Implicit Types P : PROP. + + Global Instance bupd_ne : NonExpansive (@bupd PROP _). + Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed. + Lemma bupd_intro P : P ==∗ P. + Proof. eapply bi_bupd_mixin_bupd_intro, bi_bupd_mixin. Qed. + Lemma bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q. + Proof. eapply bi_bupd_mixin_bupd_mono, bi_bupd_mixin. Qed. + Lemma bupd_trans (P : PROP) : (|==> |==> P) ==∗ P. + Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed. + Lemma bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R. + Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed. +End bupd_laws. + +Section fupd_laws. + Context `{BiFUpd PROP}. + Implicit Types P : PROP. + + Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2). + Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed. + Lemma fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P. + Proof. eapply bi_fupd_mixin_fupd_intro_mask, bi_fupd_mixin. Qed. + Lemma except_0_fupd E1 E2 (P : PROP) : â—‡ (|={E1,E2}=> P) ={E1,E2}=∗ P. + Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed. + Lemma fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q. + Proof. eapply bi_fupd_mixin_fupd_mono, bi_fupd_mixin. Qed. + Lemma fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P. + Proof. eapply bi_fupd_mixin_fupd_trans, bi_fupd_mixin. Qed. + Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) : + E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌠→ P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P. + Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed. + Lemma fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q. + Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed. +End fupd_laws. Section bupd_derived. - Context `{BUpdFacts PROP}. - Implicit Types P Q R: PROP. + Context `{BiBUpd PROP}. + Implicit Types P Q R : PROP. (* FIXME: Removing the `PROP:=` diverges. *) - Global Instance bupd_proper : Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _. + Global Instance bupd_proper : + Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _. (** BUpd derived rules *) - Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (bupd (PROP:=PROP)). Proof. intros P Q; apply bupd_mono. Qed. Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (bupd (PROP:=PROP)). @@ -82,50 +158,30 @@ Section bupd_derived. Proof. by rewrite bupd_frame_r bi.wand_elim_r. Qed. Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q. Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed. - Lemma bupd_affinely_plainly `{BiAffine PROP} P : (|==> â– P) ⊢ P. - Proof. by rewrite bi.affine_affinely bupd_plainly. Qed. - Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P. - Proof. by rewrite {1}(plain P) bupd_plainly. Qed. End bupd_derived. -Lemma except_0_bupd {PROP : sbi} `{BUpdFacts PROP} (P : PROP) : - â—‡ (|==> P) ⊢ (|==> â—‡ P). -Proof. - rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r. - by rewrite -bupd_intro -bi.or_intro_l. -Qed. - -(** FUpd facts *) - -(* Currently, this requires an SBI, because of [except_0_fupd] and - [later_fupd_plain]. If need be, we can generalize this to BIs by - extracting these propertes as lemmas to be proved by hand. *) -Class FUpdFacts (PROP : sbi) `{BUpd PROP, FUpd PROP} : Prop := - { fupd_bupd_facts :> BUpdFacts PROP; - fupd_ne E1 E2 :> NonExpansive (fupd E1 E2); - fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P; - bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P; - except_0_fupd E1 E2 (P : PROP) : â—‡ (|={E1,E2}=> P) ={E1,E2}=∗ P; - fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q; - fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P; - fupd_mask_frame_r' E1 E2 Ef (P : PROP) : - E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌠→ P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P; - fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q; - fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} : - E1 ⊆ E2 → - (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P; - later_fupd_plain E (P : PROP) `{!Plain P} : (â–· |={E}=> P) ={E}=∗ â–· â—‡ P }. - -Hint Mode FUpdFacts ! - - : typeclass_instances. +Section bupd_derived_sbi. + Context {PROP : sbi} `{BiBUpd PROP}. + Implicit Types P Q R : PROP. + + Lemma except_0_bupd P : â—‡ (|==> P) ⊢ (|==> â—‡ P). + Proof. + rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r. + by rewrite -bupd_intro -bi.or_intro_l. + Qed. + + Lemma bupd_plain P `{BiBUpdPlainly PROP, !Plain P} : (|==> P) ⊢ P. + Proof. by rewrite {1}(plain P) bupd_plainly. Qed. +End bupd_derived_sbi. Section fupd_derived. - Context `{FUpdFacts PROP}. - Implicit Types P Q R: PROP. + Context `{BiFUpd PROP}. + Implicit Types P Q R : PROP. - Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _. + Global Instance fupd_proper E1 E2 : + Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _. (** FUpd derived rules *) - Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd (PROP:=PROP) E1 E2). Proof. intros P Q; apply fupd_mono. Qed. Global Instance fupd_flip_mono' E1 E2 : @@ -133,7 +189,7 @@ Section fupd_derived. Proof. intros P Q; apply fupd_mono. Qed. Lemma fupd_intro E P : P ={E}=∗ P. - Proof. rewrite -bupd_fupd. apply bupd_intro. Qed. + Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed. Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I. Proof. exact: fupd_intro_mask. Qed. Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> â—‡ P) ={E1,E2}=∗ P. @@ -185,7 +241,7 @@ Section fupd_derived. intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep. Qed. - Lemma fupd_plain E1 E2 P Q `{!Plain P} : + Lemma fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P Q `{!Plain P} : E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P. Proof. intros HE. rewrite -(fupd_plain' _ _ E1) //. apply bi.wand_intro_l. @@ -193,7 +249,6 @@ Section fupd_derived. Qed. (** Fancy updates that take a step derived rules. *) - Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}â–·=> P) -∗ (P -∗ Q) -∗ |={E1,E2}â–·=> Q. Proof. apply bi.wand_intro_l. diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v index 65ec13c6fc6ce20756abea1527b53a572c27ca8b..f1fe442394ac9951801c8d78800f44177b3e655c 100644 --- a/theories/proofmode/class_instances.v +++ b/theories/proofmode/class_instances.v @@ -39,24 +39,6 @@ Global Instance from_assumption_absorbingly_r p P Q : FromAssumption p P Q → FromAssumption p P (bi_absorbingly Q). Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed. -Global Instance from_assumption_affinely_plainly_l p P Q : - FromAssumption true P Q → FromAssumption p (â– P) Q. -Proof. - rewrite /FromAssumption /= =><-. - by rewrite affinely_persistently_if_elim plainly_elim_persistently. -Qed. -Global Instance from_assumption_plainly_l_true P Q : - FromAssumption true P Q → FromAssumption true (bi_plainly P) Q. -Proof. - rewrite /FromAssumption /= =><-. - by rewrite persistently_elim plainly_elim_persistently. -Qed. -Global Instance from_assumption_plainly_l_false `{BiAffine PROP} P Q : - FromAssumption true P Q → FromAssumption false (bi_plainly P) Q. -Proof. - rewrite /FromAssumption /= =><-. - by rewrite affine_affinely plainly_elim_persistently. -Qed. Global Instance from_assumption_affinely_persistently_l p P Q : FromAssumption true P Q → FromAssumption p (â–¡ P) Q. Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed. @@ -112,14 +94,12 @@ Global Instance into_pure_affinely P φ : Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed. Global Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (bi_absorbingly P) φ. Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed. -Global Instance into_pure_plainly P φ : IntoPure P φ → IntoPure (bi_plainly P) φ. -Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed. Global Instance into_pure_persistently P φ : IntoPure P φ → IntoPure (bi_persistently P) φ. Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed. -Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ : +Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ : IntoPure P φ → IntoPure ⎡P⎤ φ. -Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed. +Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed. (* FromPure *) Global Instance from_pure_pure a φ : @FromPure PROP a ⌜φ⌠φ. @@ -173,9 +153,6 @@ Proof. by rewrite bi.affinely_if_elim pure_wand_forall pure_impl pure_impl_forall. Qed. -Global Instance from_pure_plainly P φ : - FromPure false P φ → FromPure false (bi_plainly P) φ. -Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed. Global Instance from_pure_persistently P a φ : FromPure true P φ → FromPure a (bi_persistently P) φ. Proof. @@ -192,9 +169,9 @@ Proof. rewrite /FromPure /= affine_affinely //. Qed. Global Instance from_pure_absorbingly P φ : FromPure true P φ → FromPure false (bi_absorbingly P) φ. Proof. rewrite /FromPure=> <- /=. apply persistent_absorbingly_affinely, _. Qed. -Global Instance from_pure_embed `{BiEmbedding PROP PROP'} a P φ : +Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ : FromPure a P φ → FromPure a ⎡P⎤ φ. -Proof. rewrite /FromPure=> <-. by rewrite bi_embed_affinely_if bi_embed_pure. Qed. +Proof. rewrite /FromPure=> <-. by rewrite embed_affinely_if embed_pure. Qed. (* IntoPersistent *) Global Instance into_persistent_persistently p P Q : @@ -206,10 +183,10 @@ Qed. Global Instance into_persistent_affinely p P Q : IntoPersistent p P Q → IntoPersistent p (bi_affinely P) Q | 0. Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed. -Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q : +Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q : IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0. Proof. - rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //. + rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //. Qed. Global Instance into_persistent_here P : IntoPersistent true P P | 1. Proof. by rewrite /IntoPersistent. Qed. @@ -232,54 +209,34 @@ Global Instance from_modal_affinely_persistently_affine_bi P : BiAffine PROP → FromModal modality_persistently (â–¡ P) (â–¡ P) P | 0. Proof. intros. by rewrite /FromModal /= affine_affinely. Qed. -Global Instance from_modal_plainly P : - FromModal modality_plainly (bi_plainly P) (bi_plainly P) P | 2. -Proof. by rewrite /FromModal. Qed. -Global Instance from_modal_affinely_plainly P : - FromModal modality_affinely_plainly (â– P) (â– P) P | 1. -Proof. by rewrite /FromModal. Qed. -Global Instance from_modal_affinely_plainly_affine_bi P : - BiAffine PROP → FromModal modality_plainly (â– P) (â– P) P | 0. -Proof. intros. by rewrite /FromModal /= affine_affinely. Qed. - Global Instance from_modal_absorbingly P : FromModal modality_id (bi_absorbingly P) (bi_absorbingly P) P. Proof. by rewrite /FromModal /= -absorbingly_intro. Qed. (* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer the embedding over the modality. *) -Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) : - FromModal (@modality_embed PROP PROP' _ _) ⎡P⎤ ⎡P⎤ P. +Global Instance from_modal_embed `{BiEmbed PROP PROP'} (P : PROP) : + FromModal (@modality_embed PROP PROP' _) ⎡P⎤ ⎡P⎤ P. Proof. by rewrite /FromModal. Qed. -Global Instance from_modal_id_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : +Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q : FromModal modality_id sel P Q → FromModal modality_id sel ⎡P⎤ ⎡Q⎤ | 100. Proof. by rewrite /FromModal /= =><-. Qed. -Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : +Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q : FromModal modality_affinely sel P Q → FromModal modality_affinely sel ⎡P⎤ ⎡Q⎤ | 100. -Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed. -Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : +Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely. Qed. +Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q : FromModal modality_persistently sel P Q → FromModal modality_persistently sel ⎡P⎤ ⎡Q⎤ | 100. -Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed. -Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : +Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed. +Global Instance from_modal_affinely_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q : FromModal modality_affinely_persistently sel P Q → FromModal modality_affinely_persistently sel ⎡P⎤ ⎡Q⎤ | 100. Proof. - rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently. -Qed. -Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : - FromModal modality_plainly sel P Q → - FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100. -Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed. -Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : - FromModal modality_affinely_plainly sel P Q → - FromModal modality_affinely_plainly sel ⎡P⎤ ⎡Q⎤ | 100. -Proof. - rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly. + rewrite /FromModal /= =><-. by rewrite embed_affinely embed_persistently. Qed. (* IntoWand *) @@ -344,16 +301,6 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x : IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q. Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed. -Global Instance into_wand_affinely_plainly p q R P Q : - IntoWand p q R P Q → IntoWand p q (â– R) P Q. -Proof. by rewrite /IntoWand affinely_plainly_elim. Qed. -Global Instance into_wand_plainly_true q R P Q : - IntoWand true q R P Q → IntoWand true q (bi_plainly R) P Q. -Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed. -Global Instance into_wand_plainly_false `{!BiAffine PROP} q R P Q : - IntoWand false q R P Q → IntoWand false q (bi_plainly R) P Q. -Proof. by rewrite /IntoWand plainly_elim. Qed. - Global Instance into_wand_affinely_persistently p q R P Q : IntoWand p q R P Q → IntoWand p q (â–¡ R) P Q. Proof. by rewrite /IntoWand affinely_persistently_elim. Qed. @@ -363,26 +310,26 @@ Proof. by rewrite /IntoWand /= persistently_idemp. Qed. Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q : IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q. Proof. by rewrite /IntoWand persistently_elim. Qed. -Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q : +Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q : IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤. Proof. - rewrite /IntoWand -!bi_embed_persistently_if -!bi_embed_affinely_if - -bi_embed_wand => -> //. + rewrite /IntoWand -!embed_persistently_if -!embed_affinely_if + -embed_wand => -> //. Qed. (* FromWand *) Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2. Proof. by rewrite /FromWand. Qed. -Global Instance from_wand_embed `{BiEmbedding PROP PROP'} P Q1 Q2 : +Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 : FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. -Proof. by rewrite /FromWand -bi_embed_wand => <-. Qed. +Proof. by rewrite /FromWand -embed_wand => <-. Qed. (* FromImpl *) Global Instance from_impl_impl P1 P2 : FromImpl (P1 → P2) P1 P2. Proof. by rewrite /FromImpl. Qed. -Global Instance from_impl_embed `{BiEmbedding PROP PROP'} P Q1 Q2 : +Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 : FromImpl P Q1 Q2 → FromImpl ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. -Proof. by rewrite /FromImpl -bi_embed_impl => <-. Qed. +Proof. by rewrite /FromImpl -embed_impl => <-. Qed. (* FromAnd *) Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100. @@ -406,15 +353,6 @@ Qed. Global Instance from_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌠⌜φ⌠⌜ψâŒ. Proof. by rewrite /FromAnd pure_and. Qed. -Global Instance from_and_plainly P Q1 Q2 : - FromAnd P Q1 Q2 → - FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). -Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed. -Global Instance from_and_plainly_sep P Q1 Q2 : - FromSep P Q1 Q2 → - FromAnd (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2) | 11. -Proof. rewrite /FromAnd=> <-. by rewrite -plainly_and plainly_and_sep. Qed. - Global Instance from_and_persistently P Q1 Q2 : FromAnd P Q1 Q2 → FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2). @@ -424,9 +362,9 @@ Global Instance from_and_persistently_sep P Q1 Q2 : FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11. Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed. -Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 : +Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 : FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. -Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed. +Proof. by rewrite /FromAnd -embed_and => <-. Qed. Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l : Persistent (Φ 0 x) → @@ -455,18 +393,14 @@ Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed. Global Instance from_sep_absorbingly P Q1 Q2 : FromSep P Q1 Q2 → FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2). Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed. -Global Instance from_sep_plainly P Q1 Q2 : - FromSep P Q1 Q2 → - FromSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). -Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed. Global Instance from_sep_persistently P Q1 Q2 : FromSep P Q1 Q2 → FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2). Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed. -Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 : +Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 : FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. -Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed. +Proof. by rewrite /FromSep -embed_sep => <-. Qed. Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l : FromSep ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y). @@ -511,16 +445,6 @@ Proof. - by rewrite -affinely_and !persistently_affinely. - intros ->. by rewrite affinely_and. Qed. -Global Instance into_and_plainly p P Q1 Q2 : - IntoAnd p P Q1 Q2 → - IntoAnd p (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). -Proof. - rewrite /IntoAnd /=. destruct p; simpl. - - rewrite -plainly_and persistently_plainly -plainly_persistently - -plainly_affinely => ->. - by rewrite plainly_affinely plainly_persistently persistently_plainly. - - intros ->. by rewrite plainly_and. -Qed. Global Instance into_and_persistently p P Q1 Q2 : IntoAnd p P Q1 Q2 → IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2). @@ -529,11 +453,11 @@ Proof. - by rewrite -persistently_and !persistently_idemp. - intros ->. by rewrite persistently_and. Qed. -Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 : +Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 : IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. Proof. - rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if - -!bi_embed_affinely_if=> -> //. + rewrite /IntoAnd -embed_and -!embed_persistently_if + -!embed_affinely_if=> -> //. Qed. (* IntoSep *) @@ -567,9 +491,9 @@ Qed. Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌠⌜φ⌠⌜ψâŒ. Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed. -Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 : +Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 : IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. -Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed. +Proof. rewrite /IntoSep -embed_sep=> -> //. Qed. Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 : IntoSep P Q1 Q2 → IntoSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2) | 0. @@ -581,17 +505,6 @@ Global Instance into_sep_affinely_trim P Q1 Q2 : IntoSep P Q1 Q2 → IntoSep (bi_affinely P) Q1 Q2 | 20. Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed. -Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 : - IntoSep P Q1 Q2 → IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). -Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed. -Global Instance into_sep_plainly_affine P Q1 Q2 : - IntoSep P Q1 Q2 → - TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) → - IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). -Proof. - rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1. -Qed. - Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 : IntoSep P Q1 Q2 → IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2). @@ -638,16 +551,13 @@ Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed. Global Instance from_or_absorbingly P Q1 Q2 : FromOr P Q1 Q2 → FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2). Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed. -Global Instance from_or_plainly P Q1 Q2 : - FromOr P Q1 Q2 → FromOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). -Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed. Global Instance from_or_persistently P Q1 Q2 : FromOr P Q1 Q2 → FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2). Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed. -Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 : +Global Instance from_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 : FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. -Proof. by rewrite /FromOr -bi_embed_or => <-. Qed. +Proof. by rewrite /FromOr -embed_or => <-. Qed. (* IntoOr *) Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q. @@ -660,16 +570,13 @@ Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed. Global Instance into_or_absorbingly P Q1 Q2 : IntoOr P Q1 Q2 → IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2). Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed. -Global Instance into_or_plainly `{BiPlainlyExist PROP} P Q1 Q2 : - IntoOr P Q1 Q2 → IntoOr (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2). -Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed. Global Instance into_or_persistently P Q1 Q2 : IntoOr P Q1 Q2 → IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2). Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed. -Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 : +Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 : IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤. -Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed. +Proof. by rewrite /IntoOr -embed_or => <-. Qed. (* FromExist *) Global Instance from_exist_exist {A} (Φ : A → PROP): FromExist (∃ a, Φ a) Φ. @@ -683,15 +590,12 @@ Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed. Global Instance from_exist_absorbingly {A} P (Φ : A → PROP) : FromExist P Φ → FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I. Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed. -Global Instance from_exist_plainly {A} P (Φ : A → PROP) : - FromExist P Φ → FromExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I. -Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed. Global Instance from_exist_persistently {A} P (Φ : A → PROP) : FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I. Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed. -Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) : +Global Instance from_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) : FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I). -Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed. +Proof. by rewrite /FromExist -embed_exist => <-. Qed. (* IntoExist *) Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ. @@ -718,15 +622,12 @@ Qed. Global Instance into_exist_absorbingly {A} P (Φ : A → PROP) : IntoExist P Φ → IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I. Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed. -Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A → PROP) : - IntoExist P Φ → IntoExist (bi_plainly P) (λ a, bi_plainly (Φ a))%I. -Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed. Global Instance into_exist_persistently {A} P (Φ : A → PROP) : IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I. Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed. -Global Instance into_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) : +Global Instance into_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) : IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I). -Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed. +Proof. by rewrite /IntoExist -embed_exist => <-. Qed. (* IntoForall *) Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ. @@ -734,15 +635,12 @@ Proof. by rewrite /IntoForall. Qed. Global Instance into_forall_affinely {A} P (Φ : A → PROP) : IntoForall P Φ → IntoForall (bi_affinely P) (λ a, bi_affinely (Φ a))%I. Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed. -Global Instance into_forall_plainly {A} P (Φ : A → PROP) : - IntoForall P Φ → IntoForall (bi_plainly P) (λ a, bi_plainly (Φ a))%I. -Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed. Global Instance into_forall_persistently {A} P (Φ : A → PROP) : IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I. Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed. -Global Instance into_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) : +Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) : IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I). -Proof. by rewrite /IntoForall -bi_embed_forall => <-. Qed. +Proof. by rewrite /IntoForall -embed_forall => <-. Qed. (* FromForall *) Global Instance from_forall_forall {A} (Φ : A → PROP) : @@ -774,15 +672,12 @@ Global Instance from_forall_affinely `{BiAffine PROP} {A} P (Φ : A → PROP) : Proof. rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim. Qed. -Global Instance from_forall_plainly {A} P (Φ : A → PROP) : - FromForall P Φ → FromForall (bi_plainly P)%I (λ a, bi_plainly (Φ a))%I. -Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed. Global Instance from_forall_persistently {A} P (Φ : A → PROP) : FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I. Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed. -Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) : +Global Instance from_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) : FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I). -Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed. +Proof. by rewrite /FromForall -embed_forall => <-. Qed. (* IntoInv *) Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N : @@ -843,26 +738,26 @@ Proof. by rewrite affinely_persistently_if_elim sep_elim_l. Qed. -Global Instance make_embed_pure `{BiEmbedding PROP PROP'} φ : +Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ : KnownMakeEmbed ⌜φ⌠⌜φâŒ. -Proof. apply bi_embed_pure. Qed. -Global Instance make_embed_emp `{BiEmbedding PROP PROP'} : +Proof. apply embed_pure. Qed. +Global Instance make_embed_emp `{BiEmbed PROP PROP'} : KnownMakeEmbed emp emp. -Proof. apply bi_embed_emp. Qed. -Global Instance make_embed_default `{BiEmbedding PROP PROP'} P : +Proof. apply embed_emp. Qed. +Global Instance make_embed_default `{BiEmbed PROP PROP'} P : MakeEmbed P ⎡P⎤ | 100. Proof. by rewrite /MakeEmbed. Qed. -Global Instance frame_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') R : +Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R : Frame p R P Q → MakeEmbed Q Q' → KnownFrame p ⎡R⎤ ⎡P⎤ Q'. Proof. rewrite /KnownFrame /Frame /MakeEmbed => <- <-. - rewrite bi_embed_sep bi_embed_affinely_if bi_embed_persistently_if => //. + rewrite embed_sep embed_affinely_if embed_persistently_if => //. Qed. -Global Instance frame_pure_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') φ : +Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ : Frame p ⌜φ⌠P Q → MakeEmbed Q Q' → KnownFrame p ⌜φ⌠⎡P⎤ Q'. Proof. - rewrite /KnownFrame /Frame /MakeEmbed -bi_embed_pure. apply (frame_embed p P Q). + rewrite /KnownFrame /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed. Global Instance make_sep_emp_l P : KnownLMakeSep emp P P. @@ -1083,9 +978,9 @@ Proof. - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x). Qed. -Global Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) : +Global Instance as_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) : AsValid0 φ P → AsValid φ ⎡P⎤. -Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed. +Proof. rewrite /AsValid0 /AsValid=> ->. rewrite embed_valid //. Qed. End bi_instances. Section sbi_instances. @@ -1103,13 +998,26 @@ Global Instance from_assumption_except_0 p P Q : FromAssumption p P Q → FromAssumption p P (â—‡ Q)%I. Proof. rewrite /FromAssumption=>->. apply except_0_intro. Qed. -Global Instance from_assumption_bupd `{BUpdFacts PROP} p P Q : +Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q : FromAssumption p P Q → FromAssumption p P (|==> Q). Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed. -Global Instance from_assumption_fupd `{FUpdFacts PROP} E p P Q : +Global Instance from_assumption_fupd `{BiBUpdFUpd PROP} E p P Q : FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I. Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed. +Global Instance from_assumption_plainly_l_true `{BiPlainly PROP} P Q : + FromAssumption true P Q → FromAssumption true (â– P) Q. +Proof. + rewrite /FromAssumption /= =><-. + by rewrite persistently_elim plainly_elim_persistently. +Qed. +Global Instance from_assumption_plainly_l_false `{BiPlainly PROP, BiAffine PROP} P Q : + FromAssumption true P Q → FromAssumption false (â– P) Q. +Proof. + rewrite /FromAssumption /= =><-. + by rewrite affine_affinely plainly_elim_persistently. +Qed. + (* FromPure *) Global Instance from_pure_internal_eq af {A : ofeT} (a b : A) : @FromPure PROP af (a ≡ b) (a ≡ b). @@ -1121,18 +1029,26 @@ Proof. rewrite /FromPure=> ->. apply laterN_intro. Qed. Global Instance from_pure_except_0 a P φ : FromPure a P φ → FromPure a (â—‡ P) φ. Proof. rewrite /FromPure=> ->. apply except_0_intro. Qed. -Global Instance from_pure_bupd `{BUpdFacts PROP} a P φ : +Global Instance from_pure_bupd `{BiBUpd PROP} a P φ : FromPure a P φ → FromPure a (|==> P) φ. Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed. -Global Instance from_pure_fupd `{FUpdFacts PROP} a E P φ : +Global Instance from_pure_fupd `{BiFUpd PROP} a E P φ : FromPure a P φ → FromPure a (|={E}=> P) φ. Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed. +Global Instance from_pure_plainly `{BiPlainly PROP} P φ : + FromPure false P φ → FromPure false (â– P) φ. +Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed. + (* IntoPure *) Global Instance into_pure_eq {A : ofeT} (a b : A) : Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b). Proof. intros. by rewrite /IntoPure discrete_eq. Qed. +Global Instance into_pure_plainly `{BiPlainly PROP} P φ : + IntoPure P φ → IntoPure (â– P) φ. +Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed. + (* IntoWand *) Global Instance into_wand_later p q R P Q : IntoWand p q R P Q → IntoWand p q (â–· R) (â–· P) (â–· Q). @@ -1161,45 +1077,52 @@ Proof. (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR. Qed. -Global Instance into_wand_bupd `{BUpdFacts PROP} p q R P Q : +Global Instance into_wand_bupd `{BiBUpd PROP} p q R P Q : IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q). Proof. rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR. apply wand_intro_l. by rewrite bupd_sep wand_elim_r. Qed. -Global Instance into_wand_bupd_persistent `{BUpdFacts PROP} p q R P Q : +Global Instance into_wand_bupd_persistent `{BiBUpd PROP} p q R P Q : IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q). Proof. rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR. apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r. Qed. -Global Instance into_wand_bupd_args `{BUpdFacts PROP} p q R P Q : +Global Instance into_wand_bupd_args `{BiBUpd PROP} p q R P Q : IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q). Proof. rewrite /IntoWand' /IntoWand /= => ->. apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r. Qed. -Global Instance into_wand_fupd `{FUpdFacts PROP} E p q R P Q : +Global Instance into_wand_fupd `{BiFUpd PROP} 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 !affinely_persistently_if_elim HR. apply wand_intro_l. by rewrite fupd_sep wand_elim_r. Qed. -Global Instance into_wand_fupd_persistent `{FUpdFacts PROP} E1 E2 p q R P Q : +Global Instance into_wand_fupd_persistent `{BiFUpd PROP} 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 affinely_persistently_if_elim HR. apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r. Qed. -Global Instance into_wand_fupd_args `{FUpdFacts PROP} E1 E2 p q R P Q : +Global Instance into_wand_fupd_args `{BiFUpd PROP} 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 affinely_persistently_if_elim fupd_wand_r. Qed. +Global Instance into_wand_plainly_true `{BiPlainly PROP} q R P Q : + IntoWand true q R P Q → IntoWand true q (â– R) P Q. +Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed. +Global Instance into_wand_plainly_false `{BiPlainly PROP, !BiAffine PROP} q R P Q : + IntoWand false q R P Q → IntoWand false q (â– R) P Q. +Proof. by rewrite /IntoWand plainly_elim. Qed. + (* FromAnd *) Global Instance from_and_later P Q1 Q2 : FromAnd P Q1 Q2 → FromAnd (â–· P) (â–· Q1) (â–· Q2). @@ -1211,6 +1134,10 @@ Global Instance from_and_except_0 P Q1 Q2 : FromAnd P Q1 Q2 → FromAnd (â—‡ P) (â—‡ Q1) (â—‡ Q2). Proof. rewrite /FromAnd=><-. by rewrite except_0_and. Qed. +Global Instance from_and_plainly `{BiPlainly PROP} P Q1 Q2 : + FromAnd P Q1 Q2 → FromAnd (â– P) (â– Q1) (â– Q2). +Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed. + (* FromSep *) Global Instance from_sep_later P Q1 Q2 : FromSep P Q1 Q2 → FromSep (â–· P) (â–· Q1) (â–· Q2). @@ -1222,13 +1149,17 @@ Global Instance from_sep_except_0 P Q1 Q2 : FromSep P Q1 Q2 → FromSep (â—‡ P) (â—‡ Q1) (â—‡ Q2). Proof. rewrite /FromSep=><-. by rewrite except_0_sep. Qed. -Global Instance from_sep_bupd `{BUpdFacts PROP} P Q1 Q2 : +Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 : FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2). Proof. rewrite /FromSep=><-. apply bupd_sep. Qed. -Global Instance from_sep_fupd `{FUpdFacts PROP} E P Q1 Q2 : +Global Instance from_sep_fupd `{BiFUpd PROP} E P Q1 Q2 : FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2). Proof. rewrite /FromSep =><-. apply fupd_sep. Qed. +Global Instance from_sep_plainly `{BiPlainly PROP} P Q1 Q2 : + FromSep P Q1 Q2 → FromSep (â– P) (â– Q1) (â– Q2). +Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed. + (* IntoAnd *) Global Instance into_and_later p P Q1 Q2 : IntoAnd p P Q1 Q2 → IntoAnd p (â–· P) (â–· Q1) (â–· Q2). @@ -1252,6 +1183,16 @@ Proof. affinely_persistently_if_elim except_0_and. Qed. +Global Instance into_and_plainly `{BiPlainly PROP} p P Q1 Q2 : + IntoAnd p P Q1 Q2 → IntoAnd p (â– P) (â– Q1) (â– Q2). +Proof. + rewrite /IntoAnd /=. destruct p; simpl. + - rewrite -plainly_and persistently_plainly -plainly_persistently + -plainly_affinely => ->. + by rewrite plainly_affinely plainly_persistently persistently_plainly. + - intros ->. by rewrite plainly_and. +Qed. + (* IntoSep *) Global Instance into_sep_later P Q1 Q2 : IntoSep P Q1 Q2 → IntoSep (â–· P) (â–· Q1) (â–· Q2). @@ -1275,6 +1216,18 @@ Proof. by rewrite -(False_elim Q1) -(False_elim Q2). Qed. +Global Instance into_sep_plainly `{BiPlainly PROP, BiPositive PROP} P Q1 Q2 : + IntoSep P Q1 Q2 → IntoSep (â– P) (â– Q1) (â– Q2). +Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed. + +Global Instance into_sep_plainly_affine `{BiPlainly PROP} P Q1 Q2 : + IntoSep P Q1 Q2 → + TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) → + IntoSep (â– P) (â– Q1) (â– Q2). +Proof. + rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1. +Qed. + (* FromOr *) Global Instance from_or_later P Q1 Q2 : FromOr P Q1 Q2 → FromOr (â–· P) (â–· Q1) (â–· Q2). @@ -1286,19 +1239,23 @@ Global Instance from_or_except_0 P Q1 Q2 : FromOr P Q1 Q2 → FromOr (â—‡ P) (â—‡ Q1) (â—‡ Q2). Proof. rewrite /FromOr=><-. by rewrite except_0_or. Qed. -Global Instance from_or_bupd `{BUpdFacts PROP} P Q1 Q2 : +Global Instance from_or_bupd `{BiBUpd PROP} P Q1 Q2 : FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2). Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto using or_intro_l, or_intro_r. Qed. -Global Instance from_or_fupd `{FUpdFacts PROP} E1 E2 P Q1 Q2 : +Global Instance from_or_fupd `{BiFUpd PROP} 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 fupd_mono; [apply bi.or_intro_l|apply bi.or_intro_r]. Qed. +Global Instance from_or_plainly `{BiPlainly PROP} P Q1 Q2 : + FromOr P Q1 Q2 → FromOr (â– P) (â– Q1) (â– Q2). +Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed. + (* IntoOr *) Global Instance into_or_later P Q1 Q2 : IntoOr P Q1 Q2 → IntoOr (â–· P) (â–· Q1) (â–· Q2). @@ -1310,6 +1267,10 @@ Global Instance into_or_except_0 P Q1 Q2 : IntoOr P Q1 Q2 → IntoOr (â—‡ P) (â—‡ Q1) (â—‡ Q2). Proof. rewrite /IntoOr=>->. by rewrite except_0_or. Qed. +Global Instance into_or_plainly `{BiPlainly PROP, BiPlainlyExist PROP} P Q1 Q2 : + IntoOr P Q1 Q2 → IntoOr (â– P) (â– Q1) (â– Q2). +Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed. + (* FromExist *) Global Instance from_exist_later {A} P (Φ : A → PROP) : FromExist P Φ → FromExist (â–· P) (λ a, â–· (Φ a))%I. @@ -1325,17 +1286,21 @@ Global Instance from_exist_except_0 {A} P (Φ : A → PROP) : FromExist P Φ → FromExist (â—‡ P) (λ a, â—‡ (Φ a))%I. Proof. rewrite /FromExist=> <-. by rewrite except_0_exist_2. Qed. -Global Instance from_exist_bupd `{BUpdFacts PROP} {A} P (Φ : A → PROP) : +Global Instance from_exist_bupd `{BiBUpd PROP} {A} P (Φ : A → PROP) : FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I. Proof. rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a). Qed. -Global Instance from_exist_fupd `{FUpdFacts PROP} {A} E1 E2 P (Φ : A → PROP) : +Global Instance from_exist_fupd `{BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) : 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 from_exist_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) : + FromExist P Φ → FromExist (â– P) (λ a, â– (Φ a))%I. +Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed. + (* IntoExist *) Global Instance into_exist_later {A} P (Φ : A → PROP) : IntoExist P Φ → Inhabited A → IntoExist (â–· P) (λ a, â–· (Φ a))%I. @@ -1347,6 +1312,10 @@ Global Instance into_exist_except_0 {A} P (Φ : A → PROP) : IntoExist P Φ → Inhabited A → IntoExist (â—‡ P) (λ a, â—‡ (Φ a))%I. Proof. rewrite /IntoExist=> HP ?. by rewrite HP except_0_exist. Qed. +Global Instance into_exist_plainly `{BiPlainlyExist PROP} {A} P (Φ : A → PROP) : + IntoExist P Φ → IntoExist (â– P) (λ a, â– (Φ a))%I. +Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed. + (* IntoForall *) Global Instance into_forall_later {A} P (Φ : A → PROP) : IntoForall P Φ → IntoForall (â–· P) (λ a, â–· (Φ a))%I. @@ -1368,6 +1337,10 @@ Proof. by rewrite -(pure_intro True%I) // /bi_affinely right_id emp_wand. Qed. +Global Instance into_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) : + IntoForall P Φ → IntoForall (â– P) (λ a, â– (Φ a))%I. +Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed. + (* FromForall *) Global Instance from_forall_later {A} P (Φ : A → PROP) : FromForall P Φ → FromForall (â–· P)%I (λ a, â–· (Φ a))%I. @@ -1376,20 +1349,24 @@ Global Instance from_forall_except_0 {A} P (Φ : A → PROP) : FromForall P Φ → FromForall (â—‡ P)%I (λ a, â—‡ (Φ a))%I. Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed. +Global Instance from_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) : + FromForall P Φ → FromForall (â– P)%I (λ a, â– (Φ a))%I. +Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed. + (* IsExcept0 *) Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P). Proof. by rewrite /IsExcept0 except_0_idemp. Qed. Global Instance is_except_0_later P : IsExcept0 (â–· P). Proof. by rewrite /IsExcept0 except_0_later. Qed. -Global Instance is_except_0_embed `{SbiEmbedding PROP PROP'} P : +Global Instance is_except_0_embed `{SbiEmbed PROP PROP'} P : IsExcept0 P → IsExcept0 ⎡P⎤. -Proof. by rewrite /IsExcept0 -sbi_embed_except_0=>->. Qed. -Global Instance is_except_0_bupd `{BUpdFacts PROP} P : IsExcept0 P → IsExcept0 (|==> P). +Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed. +Global Instance is_except_0_bupd `{BiBUpd PROP} P : IsExcept0 P → IsExcept0 (|==> P). Proof. rewrite /IsExcept0=> HP. by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P). Qed. -Global Instance is_except_0_fupd `{FUpdFacts PROP} E1 E2 P : +Global Instance is_except_0_fupd `{BiFUpd PROP} E1 E2 P : IsExcept0 (|={E1,E2}=> P). Proof. by rewrite /IsExcept0 except_0_fupd. Qed. @@ -1403,17 +1380,27 @@ Proof. by rewrite /FromModal. Qed. Global Instance from_modal_except_0 P : FromModal modality_id (â—‡ P) (â—‡ P) P. Proof. by rewrite /FromModal /= -except_0_intro. Qed. -Global Instance from_modal_bupd `{BUpdFacts PROP} P : +Global Instance from_modal_bupd `{BiBUpd PROP} P : FromModal modality_id (|==> P) (|==> P) P. Proof. by rewrite /FromModal /= -bupd_intro. Qed. -Global Instance from_modal_fupd E P `{FUpdFacts PROP} : +Global Instance from_modal_fupd E P `{BiFUpd PROP} : FromModal modality_id (|={E}=> P) (|={E}=> P) P. Proof. by rewrite /FromModal /= -fupd_intro. Qed. -Global Instance from_modal_later_embed `{SbiEmbedding PROP PROP'} `(sel : A) n P Q : +Global Instance from_modal_later_embed `{SbiEmbed PROP PROP'} `(sel : A) n P Q : FromModal (modality_laterN n) sel P Q → FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤. -Proof. rewrite /FromModal /= =><-. by rewrite sbi_embed_laterN. Qed. +Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed. + +Global Instance from_modal_plainly `{BiPlainly PROP} P : + FromModal modality_plainly (â– P) (â– P) P | 2. +Proof. by rewrite /FromModal. Qed. + +Global Instance from_modal_plainly_embed + `{BiPlainly PROP, BiPlainly PROP', SbiEmbed PROP PROP'} `(sel : A) P Q : + FromModal modality_plainly sel P Q → + FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100. +Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed. (* IntoInternalEq *) Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) : @@ -1425,16 +1412,16 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed. Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P : IntoInternalEq P x y → IntoInternalEq (bi_absorbingly P) x y. Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed. -Global Instance into_internal_eq_plainly {A : ofeT} (x y : A) P : - IntoInternalEq P x y → IntoInternalEq (bi_plainly P) x y. +Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P : + IntoInternalEq P x y → IntoInternalEq (â– P) x y. Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed. Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P : IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y. Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed. Global Instance into_internal_eq_embed - `{SbiEmbedding PROP PROP'} {A : ofeT} (x y : A) P : + `{SbiEmbed PROP PROP'} {A : ofeT} (x y : A) P : IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y. -Proof. rewrite /IntoInternalEq=> ->. by rewrite sbi_embed_internal_eq. Qed. +Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed. (* IntoExcept0 *) Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P. @@ -1450,15 +1437,15 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_affinely_2. Qed. Global Instance into_except_0_absorbingly P Q : IntoExcept0 P Q → IntoExcept0 (bi_absorbingly P) (bi_absorbingly Q). Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed. -Global Instance into_except_0_plainly `{BiPlainlyExist PROP} P Q : - IntoExcept0 P Q → IntoExcept0 (bi_plainly P) (bi_plainly Q). +Global Instance into_except_0_plainly `{BiPlainly PROP, BiPlainlyExist PROP} P Q : + IntoExcept0 P Q → IntoExcept0 (â– P) (â– Q). Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed. Global Instance into_except_0_persistently P Q : IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q). Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed. -Global Instance into_except_0_embed `{SbiEmbedding PROP PROP'} P Q : +Global Instance into_except_0_embed `{SbiEmbed PROP PROP'} P Q : IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤. -Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_embed_except_0. Qed. +Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed. (* ElimModal *) Global Instance elim_modal_timeless P Q : @@ -1467,21 +1454,21 @@ Proof. intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I). by rewrite (into_except_0 P) -except_0_sep wand_elim_r. Qed. -Global Instance elim_modal_bupd `{BUpdFacts PROP} P Q : +Global Instance elim_modal_bupd `{BiBUpd PROP} P Q : ElimModal True (|==> P) P (|==> Q) (|==> Q). Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed. -Global Instance elim_modal_bupd_plain_goal `{BUpdFacts PROP} P Q : +Global Instance elim_modal_bupd_plain_goal `{BiBUpdPlainly PROP} P Q : Plain Q → ElimModal True (|==> P) P Q Q. Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed. -Global Instance elim_modal_bupd_plain `{BUpdFacts PROP} P Q : +Global Instance elim_modal_bupd_plain `{BiBUpdPlainly PROP} P Q : Plain P → ElimModal True (|==> P) P Q Q. Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed. -Global Instance elim_modal_bupd_fupd `{FUpdFacts PROP} E1 E2 P Q : +Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} E1 E2 P Q : ElimModal True (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10. Proof. by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans. Qed. -Global Instance elim_modal_fupd_fupd `{FUpdFacts PROP} E1 E2 E3 P Q : +Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} E1 E2 E3 P Q : ElimModal True (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q). Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed. @@ -1510,17 +1497,17 @@ Proof. by rewrite -except_0_sep wand_elim_r except_0_later. Qed. -Global Instance add_modal_bupd `{BUpdFacts PROP} P Q : AddModal (|==> P) P (|==> Q). +Global Instance add_modal_bupd `{BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q). Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed. -Global Instance add_modal_fupd `{FUpdFacts PROP} E1 E2 P Q : +Global Instance add_modal_fupd `{BiFUpd PROP} E1 E2 P Q : AddModal (|={E1}=> P) P (|={E1,E2}=> Q). Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed. (* Frame *) -Global Instance frame_eq_embed `{SbiEmbedding PROP PROP'} p P Q (Q' : PROP') +Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP') {A : ofeT} (a b : A) : Frame p (a ≡ b) P Q → MakeEmbed Q Q' → KnownFrame p (a ≡ b) ⎡P⎤ Q'. -Proof. rewrite /KnownFrame /Frame /MakeEmbed -sbi_embed_internal_eq. apply (frame_embed p P Q). Qed. +Proof. rewrite /KnownFrame /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed. Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0. Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed. @@ -1546,10 +1533,10 @@ Proof. by rewrite laterN_affinely_persistently_if_2 laterN_sep. Qed. -Global Instance frame_bupd `{BUpdFacts PROP} p R P Q : +Global Instance frame_bupd `{BiBUpd PROP} p R P Q : Frame p R P Q → KnownFrame p R (|==> P) (|==> Q). Proof. rewrite /KnownFrame /Frame=><-. by rewrite bupd_frame_l. Qed. -Global Instance frame_fupd `{FUpdFacts PROP} p E1 E2 R P Q : +Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q : Frame p R P Q → KnownFrame p R (|={E1,E2}=> P) (|={E1,E2}=> Q). Proof. rewrite /KnownFrame /Frame=><-. by rewrite fupd_frame_l. Qed. @@ -1629,15 +1616,15 @@ Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Global Instance into_later_absorbingly n P Q : IntoLaterN false n P Q → IntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q). Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed. -Global Instance into_later_plainly n P Q : - IntoLaterN false n P Q → IntoLaterN false n (bi_plainly P) (bi_plainly Q). +Global Instance into_later_plainly `{BiPlainly PROP} n P Q : + IntoLaterN false n P Q → IntoLaterN false n (â– P) (â– Q). Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed. Global Instance into_later_persistently n P Q : IntoLaterN false n P Q → IntoLaterN false n (bi_persistently P) (bi_persistently Q). Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed. -Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q : +Global Instance into_later_embed`{SbiEmbed PROP PROP'} n P Q : IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤. -Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed. +Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed. Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 : IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 → diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v index 5786a01a7b83abacdeef05ec58eeaab2234ac439..119c45711e554f1c0e2e7b6004be20f0a00c0b2c 100644 --- a/theories/proofmode/classes.v +++ b/theories/proofmode/classes.v @@ -215,7 +215,8 @@ Hint Mode IntoForall + - ! - : typeclass_instances. Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) := from_forall : (∀ x, Φ x) ⊢ P. -Arguments from_forall {_ _} _ _ {_}. +Arguments FromForall {_ _} _%I _%I : simpl never. +Arguments from_forall {_ _} _%I _%I {_}. Hint Mode FromForall + - ! - : typeclass_instances. Class IsExcept0 {PROP : sbi} (Q : PROP) := is_except_0 : â—‡ Q ⊢ Q. diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v index 8fcfc827a9fa7e302292bc728f778235490eb5b9..af0e205e4b230eeb9e69a8946510fbad729997a3 100644 --- a/theories/proofmode/modality_instances.v +++ b/theories/proofmode/modality_instances.v @@ -34,43 +34,32 @@ Section bi_modalities. Definition modality_affinely_persistently := Modality _ modality_affinely_persistently_mixin. - Lemma modality_plainly_mixin : - modality_mixin (@bi_plainly PROP) (MIEnvForall Plain) MIEnvClear. - Proof. - split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro, - plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances. - Qed. - Definition modality_plainly := - Modality _ modality_plainly_mixin. - - Lemma modality_affinely_plainly_mixin : - modality_mixin (λ P : PROP, â– P)%I (MIEnvForall Plain) MIEnvIsEmpty. - Proof. - split; simpl; split_and?; eauto using equiv_entails_sym, - affinely_plainly_emp, affinely_intro, - plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp, - affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances. - Qed. - Definition modality_affinely_plainly := - Modality _ modality_affinely_plainly_mixin. - - Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} : - modality_mixin (@bi_embed PROP PROP' _) + Lemma modality_embed_mixin `{BiEmbed PROP PROP'} : + modality_mixin (@embed PROP PROP' _) (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed). Proof. split; simpl; split_and?; - eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and. + eauto using equiv_entails_sym, embed_emp, embed_sep, embed_and. - intros P Q. rewrite /IntoEmbed=> ->. - by rewrite bi_embed_affinely bi_embed_persistently. + by rewrite embed_affinely embed_persistently. - by intros P Q ->. Qed. - Definition modality_embed `{BiEmbedding PROP PROP'} := + Definition modality_embed `{BiEmbed PROP PROP'} := Modality _ modality_embed_mixin. End bi_modalities. Section sbi_modalities. Context {PROP : sbi}. + Lemma modality_plainly_mixin `{BiPlainly PROP} : + modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear. + Proof. + split; simpl; split_and?; eauto using equiv_entails_sym, plainly_intro, + plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances. + Qed. + Definition modality_plainly `{BiPlainly PROP} := + Modality _ modality_plainly_mixin. + Lemma modality_laterN_mixin n : modality_mixin (@sbi_laterN PROP n) (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)). diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v index d60a2635dab284e36feb439b4d75d49e25c1229b..179150e9073598be1418444aaa7af2dade29ead7 100644 --- a/theories/proofmode/monpred.v +++ b/theories/proofmode/monpred.v @@ -1,4 +1,5 @@ From iris.bi Require Export monpred. +From iris.bi Require Import plainly. From iris.proofmode Require Import tactics class_instances. Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I) @@ -33,6 +34,7 @@ End modalities. Section bi. Context {I : biIndex} {PROP : bi}. +Local Notation monPredI := (monPredI I PROP). Local Notation monPred := (monPred I PROP). Local Notation MakeMonPredAt := (@MakeMonPredAt I PROP). Implicit Types P Q R : monPred. @@ -116,6 +118,9 @@ Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) ⌜i ⊑ Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed. Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100. Proof. by rewrite /MakeMonPredAt. Qed. +Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P ð“Ÿ : + MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|==> P)%I (|==> ð“Ÿ)%I. +Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed. Global Instance from_assumption_make_monPred_at_l p i j P ð“Ÿ : MakeMonPredAt i P 𓟠→ IsBiIndexRel j i → FromAssumption p (P j) ð“Ÿ. @@ -287,21 +292,6 @@ Proof. by rewrite monPred_at_exist. Qed. -Global Instance foram_forall_monPred_at_plainly i P Φ : - (∀ i, MakeMonPredAt i P (Φ i)) → - FromForall (bi_plainly P i) (λ j, bi_plainly (Φ j)). -Proof. - rewrite /FromForall /MakeMonPredAt=>H. rewrite monPred_at_plainly. - by setoid_rewrite H. -Qed. -Global Instance into_forall_monPred_at_plainly i P Φ : - (∀ i, MakeMonPredAt i P (Φ i)) → - IntoForall (bi_plainly P i) (λ j, bi_plainly (Φ j)). -Proof. - rewrite /IntoForall /MakeMonPredAt=>H. rewrite monPred_at_plainly. - by setoid_rewrite H. -Qed. - Global Instance from_forall_monPred_at_absolutely P (Φ : I → PROP) i : (∀ i, MakeMonPredAt i P (Φ i)) → FromForall ((∀ᵢ P) i)%I Φ. Proof. @@ -316,12 +306,12 @@ Qed. Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i : (∀ i, MakeMonPredAt i P (Φ i)) → FromExist ((∃ᵢ P) i) Φ. Proof. - rewrite /FromExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H. + rewrite /FromExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H. Qed. Global Instance into_exist_monPred_at_ex P (Φ : I → PROP) i : (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist ((∃ᵢ P) i) Φ. Proof. - rewrite /IntoExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H. + rewrite /IntoExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H. Qed. Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i : @@ -358,7 +348,36 @@ Qed. Global Instance into_embed_absolute P : Absolute P → IntoEmbed P (∀ i, P i). -Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed. +Proof. + rewrite /IntoEmbed=> ?. + by rewrite {1}(absolute_absolutely P) monPred_absolutely_unfold. +Qed. + +Global Instance elim_modal_embed_bupd_goal `{BiBUpd PROP} φ P P' ð“ ð“ ' : + ElimModal φ P P' (|==> ⎡ð“ ⎤)%I (|==> ⎡ð“ '⎤)%I → + ElimModal φ P P' ⎡|==> ð“ ⎤ ⎡|==> ð“ '⎤. +Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed. +Global Instance elim_modal_embed_bupd_hyp `{BiBUpd PROP} φ ð“Ÿ P' Q Q' : + ElimModal φ (|==> ⎡ð“ŸâŽ¤)%I P' Q Q' → + ElimModal φ ⎡|==> ð“ŸâŽ¤ P' Q Q'. +Proof. by rewrite /ElimModal monPred_bupd_embed. Qed. + +Global Instance add_modal_embed_bupd_goal `{BiBUpd PROP} P P' ð“ : + AddModal P P' (|==> ⎡ð“ ⎤)%I → AddModal P P' ⎡|==> ð“ ⎤. +Proof. by rewrite /AddModal !monPred_bupd_embed. Qed. + +Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q Q' i : + ElimModal φ ð“Ÿ ð“Ÿ' (|==> Q i) (|==> Q' i) → + ElimModal φ ð“Ÿ ð“Ÿ' ((|==> Q) i) ((|==> Q') i). +Proof. by rewrite /ElimModal !monPred_at_bupd. Qed. +Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ P ð“Ÿ' ð“ ð“ ' i: + ElimModal φ (|==> P i) ð“Ÿ' ð“ ð“ ' → + ElimModal φ ((|==> P) i) ð“Ÿ' ð“ ð“ '. +Proof. by rewrite /ElimModal monPred_at_bupd. Qed. + +Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q i : + AddModal ð“Ÿ ð“Ÿ' (|==> Q i)%I → AddModal ð“Ÿ ð“Ÿ' ((|==> Q) i). +Proof. by rewrite /AddModal !monPred_at_bupd. Qed. End bi. (* When P and/or Q are evars when doing typeclass search on [IntoWand @@ -391,6 +410,21 @@ Implicit Types ð“Ÿ ð“ ð“¡ : PROP. Implicit Types φ : Prop. Implicit Types i j : I. +Global Instance from_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ : + (∀ i, MakeMonPredAt i P (Φ i)) → + FromForall ((â– P) i) (λ j, â– (Φ j))%I. +Proof. + rewrite /FromForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly. + by setoid_rewrite HPΦ. +Qed. +Global Instance into_forall_monPred_at_plainly `{BiPlainly PROP} i P Φ : + (∀ i, MakeMonPredAt i P (Φ i)) → + IntoForall ((â– P) i) (λ j, â– (Φ j))%I. +Proof. + rewrite /IntoForall /MakeMonPredAt=>HPΦ. rewrite monPred_at_plainly. + by setoid_rewrite HPΦ. +Qed. + Global Instance is_except_0_monPred_at i P : IsExcept0 P → IsExcept0 (P i). Proof. rewrite /IsExcept0=>- [/(_ i)]. by rewrite monPred_at_except_0. Qed. @@ -407,10 +441,7 @@ Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed. Global Instance make_monPred_at_laterN i n P ð“ : MakeMonPredAt i P ð“ → MakeMonPredAt i (â–·^n P)%I (â–·^n ð“ )%I. Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed. -Global Instance make_monPred_at_bupd `{BUpdFacts PROP} i P ð“Ÿ : - MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|==> P)%I (|==> ð“Ÿ)%I. -Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed. -Global Instance make_monPred_at_fupd `{FUpdFacts PROP} i E1 E2 P ð“Ÿ : +Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P ð“Ÿ : MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> ð“Ÿ)%I. Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed. @@ -440,55 +471,29 @@ Proof. by rewrite monPred_at_later. Qed. -Global Instance elim_modal_embed_bupd_goal `{BUpdFacts PROP} φ P P' ð“ ð“ ' : - ElimModal φ P P' (|==> ⎡ð“ ⎤)%I (|==> ⎡ð“ '⎤)%I → - ElimModal φ P P' ⎡|==> ð“ ⎤ ⎡|==> ð“ '⎤. -Proof. by rewrite /ElimModal !monPred_bupd_embed. Qed. -Global Instance elim_modal_embed_bupd_hyp `{BUpdFacts PROP} φ ð“Ÿ P' Q Q' : - ElimModal φ (|==> ⎡ð“ŸâŽ¤)%I P' Q Q' → - ElimModal φ ⎡|==> ð“ŸâŽ¤ P' Q Q'. -Proof. by rewrite /ElimModal monPred_bupd_embed. Qed. - -Global Instance add_modal_embed_bupd_goal `{BUpdFacts PROP} P P' ð“ : - AddModal P P' (|==> ⎡ð“ ⎤)%I → AddModal P P' ⎡|==> ð“ ⎤. -Proof. by rewrite /AddModal !monPred_bupd_embed. Qed. - -Global Instance elim_modal_at_bupd_goal `{BUpdFacts PROP} φ ð“Ÿ ð“Ÿ' Q Q' i : - ElimModal φ ð“Ÿ ð“Ÿ' (|==> Q i) (|==> Q' i) → - ElimModal φ ð“Ÿ ð“Ÿ' ((|==> Q) i) ((|==> Q') i). -Proof. by rewrite /ElimModal !monPred_at_bupd. Qed. -Global Instance elim_modal_at_bupd_hyp `{BUpdFacts PROP} φ P ð“Ÿ' ð“ ð“ ' i: - ElimModal φ (|==> P i) ð“Ÿ' ð“ ð“ ' → - ElimModal φ ((|==> P) i) ð“Ÿ' ð“ ð“ '. -Proof. by rewrite /ElimModal monPred_at_bupd. Qed. - -Global Instance add_modal_at_bupd_goal `{BUpdFacts PROP} φ ð“Ÿ ð“Ÿ' Q i : - AddModal ð“Ÿ ð“Ÿ' (|==> Q i)%I → AddModal ð“Ÿ ð“Ÿ' ((|==> Q) i). -Proof. by rewrite /AddModal !monPred_at_bupd. Qed. - -Global Instance elim_modal_embed_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 P P' ð“ ð“ ' : +Global Instance elim_modal_embed_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 P P' ð“ ð“ ' : ElimModal φ P P' (|={E1,E3}=> ⎡ð“ ⎤)%I (|={E2,E3}=> ⎡ð“ '⎤)%I → ElimModal φ P P' ⎡|={E1,E3}=> ð“ ⎤ ⎡|={E2,E3}=> ð“ '⎤. Proof. by rewrite /ElimModal !monPred_fupd_embed. Qed. -Global Instance elim_modal_embed_fupd_hyp `{FUpdFacts PROP} φ E1 E2 ð“Ÿ P' Q Q' : +Global Instance elim_modal_embed_fupd_hyp `{BiFUpd PROP} φ E1 E2 ð“Ÿ P' Q Q' : ElimModal φ (|={E1,E2}=> ⎡ð“ŸâŽ¤)%I P' Q Q' → ElimModal φ ⎡|={E1,E2}=> ð“ŸâŽ¤ P' Q Q'. Proof. by rewrite /ElimModal monPred_fupd_embed. Qed. -Global Instance add_modal_embed_fupd_goal `{FUpdFacts PROP} E1 E2 P P' ð“ : +Global Instance add_modal_embed_fupd_goal `{BiFUpd PROP} E1 E2 P P' ð“ : AddModal P P' (|={E1,E2}=> ⎡ð“ ⎤)%I → AddModal P P' ⎡|={E1,E2}=> ð“ ⎤. Proof. by rewrite /AddModal !monPred_fupd_embed. Qed. -Global Instance elim_modal_at_fupd_goal `{FUpdFacts PROP} φ E1 E2 E3 ð“Ÿ ð“Ÿ' Q Q' i : +Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 ð“Ÿ ð“Ÿ' Q Q' i : ElimModal φ ð“Ÿ ð“Ÿ' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) → ElimModal φ ð“Ÿ ð“Ÿ' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i). Proof. by rewrite /ElimModal !monPred_at_fupd. Qed. -Global Instance elim_modal_at_fupd_hyp `{FUpdFacts PROP} φ E1 E2 P ð“Ÿ' ð“ ð“ ' i : +Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ E1 E2 P ð“Ÿ' ð“ ð“ ' i : ElimModal φ (|={E1,E2}=> P i) ð“Ÿ' ð“ ð“ ' → ElimModal φ ((|={E1,E2}=> P) i) ð“Ÿ' ð“ ð“ '. Proof. by rewrite /ElimModal monPred_at_fupd. Qed. -Global Instance add_modal_at_fupd_goal `{FUpdFacts PROP} E1 E2 ð“Ÿ ð“Ÿ' Q i : +Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 ð“Ÿ ð“Ÿ' Q i : AddModal ð“Ÿ ð“Ÿ' (|={E1,E2}=> Q i) → AddModal ð“Ÿ ð“Ÿ' ((|={E1,E2}=> Q) i). Proof. by rewrite /AddModal !monPred_at_fupd. Qed. diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index 29d90f3df3d5035436c118a77aee63dad266115e..b4bdc052d8e83a9dbf6c8afe9e1fa56bbe489e21 100644 --- a/theories/proofmode/tactics.v +++ b/theories/proofmode/tactics.v @@ -1963,7 +1963,7 @@ Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros. Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit. Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit. Hint Extern 1 (envs_entails _ (â–· _)) => iNext. -Hint Extern 1 (envs_entails _ (bi_plainly _)) => iAlways. +Hint Extern 1 (envs_entails _ (â– _)) => iAlways. Hint Extern 1 (envs_entails _ (bi_persistently _)) => iAlways. Hint Extern 1 (envs_entails _ (bi_affinely _)) => iAlways. Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _. diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v index ae928b8abccf2b7f9cc1eee8a80b5733fd3d2001..5ae50a06ebd978e0ce85aaeb0ebdf2650f0439ac 100644 --- a/theories/tests/proofmode_monpred.v +++ b/theories/tests/proofmode_monpred.v @@ -96,21 +96,15 @@ Section tests. ignore hint modes. So we assume the instances in a way that cannot be used by type class resolution, and then declare the instance. as such. *) - Context (BU0 : BUpd PROP * unit). - Instance BU : BUpd PROP := fst BU0. - Context (FU0 : FUpd PROP * unit). - Instance FU : FUpd PROP := fst FU0. - Context (FUF0 : FUpdFacts PROP * unit). - Instance FUF : FUpdFacts PROP := fst FUF0. + Context (FU0 : BiFUpd PROP * unit). + Instance FU : BiFUpd PROP := fst FU0. Lemma test_apply_fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P. - Proof. iIntros. by iApply fupd_intro_mask. Qed. + Proof. iIntros. by iApply @fupd_intro_mask. Qed. Lemma test_apply_fupd_intro_mask_2 E1 E2 P : E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P. - Proof. - iIntros. iFrame. by iApply fupd_intro_mask'. - Qed. + Proof. iIntros. iFrame. by iApply @fupd_intro_mask'. Qed. Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) : Q ∗ â–¡ ⎡P⎤ ⊢ Q ∗ ⎡P ∗ P⎤. @@ -121,5 +115,4 @@ Section tests. Lemma test_iNext_Bi P : @bi_entails monPredI (â–· P) (â–· P). Proof. iIntros "H". by iNext. Qed. - End tests.