From iris.algebra Require Export ofe. Set Primitive Projections. Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity). Reserved Notation "'emp'". Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝"). Reserved Notation "P ∗ Q" (at level 80, right associativity). 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 (bi_entails : PROP → PROP → Prop). Context (bi_emp : PROP). Context (bi_pure : Prop → PROP). Context (bi_and : PROP → PROP → PROP). Context (bi_or : PROP → PROP → PROP). Context (bi_impl : PROP → PROP → PROP). Context (bi_forall : ∀ A, (A → PROP) → PROP). Context (bi_exist : ∀ A, (A → PROP) → PROP). Context (bi_internal_eq : ∀ A : ofeT, A → A → 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_later : PROP → PROP). Local Infix "⊢" := bi_entails. Local Notation "'emp'" := bi_emp. Local Notation "'True'" := (bi_pure True). Local Notation "'False'" := (bi_pure False). Local Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp). Local Infix "∧" := bi_and. Local Infix "∨" := bi_or. Local Infix "→" := bi_impl. Local Notation "∀ x .. y , P" := (bi_forall _ (λ x, .. (bi_forall _ (λ y, P)) ..)). Local Notation "∃ x .. y , P" := (bi_exist _ (λ x, .. (bi_exist _ (λ y, P)) ..)). Local Notation "x ≡ y" := (bi_internal_eq _ x y). Local Infix "∗" := bi_sep. Local Infix "-∗" := bi_wand. Local Notation "▷ P" := (sbi_later P). Record BiMixin := { bi_mixin_entails_po : PreOrder bi_entails; bi_mixin_equiv_spec P Q : equiv P Q ↔ (P ⊢ Q) ∧ (Q ⊢ P); (* Non-expansiveness *) bi_mixin_pure_ne n : Proper (iff ==> dist n) bi_pure; bi_mixin_and_ne : NonExpansive2 bi_and; bi_mixin_or_ne : NonExpansive2 bi_or; bi_mixin_impl_ne : NonExpansive2 bi_impl; bi_mixin_forall_ne A n : Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A); bi_mixin_exist_ne A n : 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; bi_mixin_internal_eq_ne (A : ofeT) : NonExpansive2 (bi_internal_eq A); (* Higher-order logic *) bi_mixin_pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝; bi_mixin_pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P; bi_mixin_pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝; bi_mixin_and_elim_l P Q : P ∧ Q ⊢ P; bi_mixin_and_elim_r P Q : P ∧ Q ⊢ Q; bi_mixin_and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R; bi_mixin_or_intro_l P Q : P ⊢ P ∨ Q; bi_mixin_or_intro_r P Q : Q ⊢ P ∨ Q; bi_mixin_or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R; bi_mixin_impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R; bi_mixin_impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R; bi_mixin_forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a; bi_mixin_forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a; bi_mixin_exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a; bi_mixin_exist_elim {A} (Φ : A → PROP) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q; (* Equality *) bi_mixin_internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a; bi_mixin_internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) : NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b; bi_mixin_fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g; bi_mixin_sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y; bi_mixin_discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝; (* BI connectives *) bi_mixin_sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'; bi_mixin_emp_sep_1 P : P ⊢ emp ∗ P; bi_mixin_emp_sep_2 P : emp ∗ P ⊢ P; bi_mixin_sep_comm' P Q : P ∗ Q ⊢ Q ∗ P; bi_mixin_sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R); 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 *) 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); bi_mixin_prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢ bi_internal_eq (OfeT PROP prop_ofe_mixin) P Q; (* The following two laws are very similar, and indeed they hold not just for □ and ■, 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 *) bi_mixin_persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q; bi_mixin_persistently_idemp_2 P : bi_persistently P ⊢ bi_persistently (bi_persistently P); bi_mixin_plainly_persistently_1 P : bi_plainly (bi_persistently P) ⊢ bi_plainly P; bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) : (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a); bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) : bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a); bi_mixin_persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P; bi_mixin_persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q; }. Record SbiMixin := { sbi_mixin_later_contractive : Contractive sbi_later; sbi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y); sbi_mixin_later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y; sbi_mixin_later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q; sbi_mixin_löb P : (▷ P → P) ⊢ P; sbi_mixin_later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a; sbi_mixin_later_exist_false {A} (Φ : A → PROP) : (▷ ∃ 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 : bi_persistently (▷ P) ⊢ ▷ bi_persistently P; sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P); }. End bi_mixin. Structure bi := Bi { bi_car :> Type; bi_dist : Dist bi_car; bi_equiv : Equiv bi_car; bi_entails : bi_car → bi_car → Prop; bi_emp : bi_car; bi_pure : Prop → bi_car; bi_and : bi_car → bi_car → bi_car; bi_or : bi_car → bi_car → bi_car; bi_impl : bi_car → bi_car → bi_car; bi_forall : ∀ A, (A → bi_car) → bi_car; bi_exist : ∀ A, (A → bi_car) → bi_car; bi_internal_eq : ∀ A : ofeT, A → A → 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_ofe_mixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall bi_exist bi_internal_eq bi_sep bi_wand bi_plainly bi_persistently; }. Coercion bi_ofeC (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP). Canonical Structure bi_ofeC. Instance: Params (@bi_entails) 1. Instance: Params (@bi_emp) 1. Instance: Params (@bi_pure) 1. Instance: Params (@bi_and) 1. Instance: Params (@bi_or) 1. Instance: Params (@bi_impl) 1. Instance: Params (@bi_forall) 2. Instance: Params (@bi_exist) 2. Instance: Params (@bi_internal_eq) 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. Arguments bi_car : simpl never. Arguments bi_dist : simpl never. Arguments bi_equiv : simpl never. Arguments bi_entails {PROP} _%I _%I : simpl never, rename. Arguments bi_emp {PROP} : simpl never, rename. Arguments bi_pure {PROP} _%stdpp : simpl never, rename. Arguments bi_and {PROP} _%I _%I : simpl never, rename. Arguments bi_or {PROP} _%I _%I : simpl never, rename. Arguments bi_impl {PROP} _%I _%I : simpl never, rename. Arguments bi_forall {PROP _} _%I : simpl never, rename. Arguments bi_exist {PROP _} _%I : simpl never, rename. Arguments bi_internal_eq {PROP _} _ _ : 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 { sbi_car :> Type; sbi_dist : Dist sbi_car; sbi_equiv : Equiv sbi_car; sbi_entails : sbi_car → sbi_car → Prop; sbi_emp : sbi_car; sbi_pure : Prop → sbi_car; sbi_and : sbi_car → sbi_car → sbi_car; sbi_or : sbi_car → sbi_car → sbi_car; sbi_impl : sbi_car → sbi_car → sbi_car; sbi_forall : ∀ A, (A → sbi_car) → sbi_car; sbi_exist : ∀ A, (A → sbi_car) → sbi_car; sbi_internal_eq : ∀ A : ofeT, A → A → 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_later : sbi_car → sbi_car; sbi_ofe_mixin : OfeMixin sbi_car; sbi_bi_mixin : BiMixin sbi_ofe_mixin sbi_entails 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; sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl sbi_forall sbi_exist sbi_internal_eq sbi_sep sbi_plainly sbi_persistently sbi_later; }. Arguments sbi_car : simpl never. Arguments sbi_entails {PROP} _%I _%I : simpl never, rename. Arguments bi_emp {PROP} : simpl never, rename. Arguments bi_pure {PROP} _%stdpp : simpl never, rename. Arguments bi_and {PROP} _%I _%I : simpl never, rename. Arguments bi_or {PROP} _%I _%I : simpl never, rename. Arguments bi_impl {PROP} _%I _%I : simpl never, rename. Arguments bi_forall {PROP _} _%I : simpl never, rename. Arguments bi_exist {PROP _} _%I : simpl never, rename. Arguments bi_internal_eq {PROP _} _ _ : 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. Coercion sbi_ofeC (PROP : sbi) : ofeT := OfeT PROP (sbi_ofe_mixin PROP). Canonical Structure sbi_ofeC. Coercion sbi_bi (PROP : sbi) : bi := {| bi_ofe_mixin := sbi_ofe_mixin PROP; bi_bi_mixin := sbi_bi_mixin PROP |}. Canonical Structure sbi_bi. Arguments sbi_car : simpl never. Arguments sbi_dist : simpl never. Arguments sbi_equiv : simpl never. Arguments sbi_entails {PROP} _%I _%I : simpl never, rename. Arguments sbi_emp {PROP} : simpl never, rename. Arguments sbi_pure {PROP} _%stdpp : simpl never, rename. Arguments sbi_and {PROP} _%I _%I : simpl never, rename. Arguments sbi_or {PROP} _%I _%I : simpl never, rename. Arguments sbi_impl {PROP} _%I _%I : simpl never, rename. Arguments sbi_forall {PROP _} _%I : simpl never, rename. Arguments sbi_exist {PROP _} _%I : simpl never, rename. Arguments sbi_internal_eq {PROP _} _ _ : 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_later {PROP} _%I : simpl never, rename. Hint Extern 0 (bi_entails _ _) => reflexivity. Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP). Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True). Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope. Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope. Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) (at level 95, no associativity) : stdpp_scope. Notation "(⊣⊢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope. Notation "P -∗ Q" := (P ⊢ Q) : stdpp_scope. Notation "'emp'" := (bi_emp) : bi_scope. Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope. Notation "'True'" := (bi_pure True) : bi_scope. Notation "'False'" := (bi_pure False) : bi_scope. Infix "∧" := bi_and : bi_scope. Notation "(∧)" := bi_and (only parsing) : bi_scope. Infix "∨" := bi_or : bi_scope. Notation "(∨)" := bi_or (only parsing) : bi_scope. Infix "→" := bi_impl : bi_scope. Infix "∗" := bi_sep : bi_scope. Notation "(∗)" := bi_sep (only parsing) : bi_scope. Notation "P -∗ Q" := (bi_wand P Q) : bi_scope. Notation "∀ x .. y , P" := (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope. Notation "∃ x .. y , P" := (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope. Infix "≡" := bi_internal_eq : bi_scope. Notation "▷ P" := (sbi_later P) : bi_scope. Coercion bi_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P. Coercion sbi_valid {PROP : sbi} : PROP → Prop := bi_valid. Arguments bi_valid {_} _%I : simpl never. Typeclasses Opaque bi_valid. Module bi. Section bi_laws. Context {PROP : bi}. Implicit Types φ : Prop. Implicit Types P Q R : PROP. Implicit Types A : Type. (* About the entailment *) Global Instance entails_po : PreOrder (@bi_entails PROP). Proof. eapply bi_mixin_entails_po, bi_bi_mixin. Qed. Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P). Proof. eapply bi_mixin_equiv_spec, bi_bi_mixin. Qed. (* Non-expansiveness *) Global Instance pure_ne n : Proper (iff ==> dist n) (@bi_pure PROP). Proof. eapply bi_mixin_pure_ne, bi_bi_mixin. Qed. Global Instance and_ne : NonExpansive2 (@bi_and PROP). Proof. eapply bi_mixin_and_ne, bi_bi_mixin. Qed. Global Instance or_ne : NonExpansive2 (@bi_or PROP). Proof. eapply bi_mixin_or_ne, bi_bi_mixin. Qed. Global Instance impl_ne : NonExpansive2 (@bi_impl PROP). Proof. eapply bi_mixin_impl_ne, bi_bi_mixin. Qed. Global Instance forall_ne A n : Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_forall PROP A). Proof. eapply bi_mixin_forall_ne, bi_bi_mixin. Qed. Global Instance exist_ne A n : Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_exist PROP A). Proof. eapply bi_mixin_exist_ne, bi_bi_mixin. Qed. 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. (* Higher-order logic *) Lemma pure_intro P (φ : Prop) : φ → P ⊢ ⌜ φ ⌝. Proof. eapply bi_mixin_pure_intro, bi_bi_mixin. Qed. Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P. Proof. eapply bi_mixin_pure_elim', bi_bi_mixin. Qed. Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝ : PROP) ⊢ ⌜ ∀ a, φ a ⌝. Proof. eapply bi_mixin_pure_forall_2, bi_bi_mixin. Qed. Lemma and_elim_l P Q : P ∧ Q ⊢ P. Proof. eapply bi_mixin_and_elim_l, bi_bi_mixin. Qed. Lemma and_elim_r P Q : P ∧ Q ⊢ Q. Proof. eapply bi_mixin_and_elim_r, bi_bi_mixin. Qed. Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R. Proof. eapply bi_mixin_and_intro, bi_bi_mixin. Qed. Lemma or_intro_l P Q : P ⊢ P ∨ Q. Proof. eapply bi_mixin_or_intro_l, bi_bi_mixin. Qed. Lemma or_intro_r P Q : Q ⊢ P ∨ Q. Proof. eapply bi_mixin_or_intro_r, bi_bi_mixin. Qed. Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R. Proof. eapply bi_mixin_or_elim, bi_bi_mixin. Qed. Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R. Proof. eapply bi_mixin_impl_intro_r, bi_bi_mixin. Qed. Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R. Proof. eapply bi_mixin_impl_elim_l', bi_bi_mixin. Qed. Lemma forall_intro {A} P (Ψ : A → PROP) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a. Proof. eapply bi_mixin_forall_intro, bi_bi_mixin. Qed. Lemma forall_elim {A} {Ψ : A → PROP} a : (∀ a, Ψ a) ⊢ Ψ a. Proof. eapply (bi_mixin_forall_elim _ bi_entails), bi_bi_mixin. Qed. Lemma exist_intro {A} {Ψ : A → PROP} a : Ψ a ⊢ ∃ a, Ψ a. Proof. eapply bi_mixin_exist_intro, bi_bi_mixin. Qed. Lemma exist_elim {A} (Φ : A → PROP) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q. Proof. eapply bi_mixin_exist_elim, bi_bi_mixin. Qed. (* Equality *) Global Instance internal_eq_ne (A : ofeT) : NonExpansive2 (@bi_internal_eq PROP A). Proof. eapply bi_mixin_internal_eq_ne, bi_bi_mixin. Qed. Lemma internal_eq_refl {A : ofeT} P (a : A) : P ⊢ a ≡ a. Proof. eapply bi_mixin_internal_eq_refl, bi_bi_mixin. Qed. Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → PROP) : NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b. Proof. eapply bi_mixin_internal_eq_rewrite, bi_bi_mixin. Qed. Lemma fun_ext {A} {B : A → ofeT} (f g : ofe_fun B) : (∀ x, f x ≡ g x) ⊢ (f ≡ g : PROP). Proof. eapply bi_mixin_fun_ext, bi_bi_mixin. Qed. Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ (x ≡ y : PROP). Proof. eapply bi_mixin_sig_eq, bi_bi_mixin. Qed. Lemma discrete_eq_1 {A : ofeT} (a b : A) : Discrete a → a ≡ b ⊢ (⌜a ≡ b⌝ : PROP). Proof. eapply bi_mixin_discrete_eq_1, bi_bi_mixin. Qed. (* BI connectives *) Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'. Proof. eapply bi_mixin_sep_mono, bi_bi_mixin. Qed. Lemma emp_sep_1 P : P ⊢ emp ∗ P. Proof. eapply bi_mixin_emp_sep_1, bi_bi_mixin. Qed. Lemma emp_sep_2 P : emp ∗ P ⊢ P. Proof. eapply bi_mixin_emp_sep_2, bi_bi_mixin. Qed. Lemma sep_comm' P Q : P ∗ Q ⊢ Q ∗ P. Proof. eapply (bi_mixin_sep_comm' _ bi_entails), bi_bi_mixin. Qed. Lemma sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R). Proof. eapply bi_mixin_sep_assoc', bi_bi_mixin. Qed. Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R. 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 prop_ext P Q : bi_plainly ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q. Proof. eapply (bi_mixin_prop_ext _ bi_entails), 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. 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 plainly_persistently_1 P : bi_plainly (bi_persistently P) ⊢ bi_plainly P. Proof. eapply (bi_mixin_plainly_persistently_1 _ bi_entails), 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. Lemma persistently_exist_1 {A} (Ψ : A → PROP) : bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a). Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed. Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P. Proof. eapply (bi_mixin_persistently_absorbing _ bi_entails), bi_bi_mixin. Qed. Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q. Proof. eapply bi_mixin_persistently_and_sep_elim, bi_bi_mixin. Qed. End bi_laws. Section sbi_laws. Context {PROP : sbi}. Implicit Types φ : Prop. Implicit Types P Q R : PROP. Global Instance later_contractive : Contractive (@sbi_later PROP). Proof. eapply sbi_mixin_later_contractive, sbi_sbi_mixin. Qed. Lemma later_eq_1 {A : ofeT} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y : PROP). Proof. eapply sbi_mixin_later_eq_1, sbi_sbi_mixin. Qed. Lemma later_eq_2 {A : ofeT} (x y : A) : ▷ (x ≡ y) ⊢ (Next x ≡ Next y : PROP). Proof. eapply sbi_mixin_later_eq_2, sbi_sbi_mixin. Qed. Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q. Proof. eapply sbi_mixin_later_mono, sbi_sbi_mixin. Qed. Lemma löb P : (▷ P → P) ⊢ P. Proof. eapply sbi_mixin_löb, sbi_sbi_mixin. Qed. Lemma later_forall_2 {A} (Φ : A → PROP) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a. Proof. eapply sbi_mixin_later_forall_2, sbi_sbi_mixin. Qed. Lemma later_exist_false {A} (Φ : A → PROP) : (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a). Proof. eapply sbi_mixin_later_exist_false, sbi_sbi_mixin. Qed. 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. Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P. 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. End sbi_laws. End bi. (* Typically, embeddings are used to *define* the destination BI. Hence we cannot ask B to be a BI. *) Class BiEmbedding (A B : Type) := bi_embedding : A → B. Arguments bi_embedding {_ _ _} _%I : simpl never. Notation "⎡ P ⎤" := (bi_embedding P) : bi_scope. Instance: Params (@bi_embedding) 3. Typeclasses Opaque bi_embedding. Class BiMorphism {PROP1 PROP2 : bi} (f : PROP1 → PROP2) := { bi_mor_ne :> NonExpansive f; bi_mor_mono :> Proper ((⊢) ==> (⊢)) f; bi_mor_emp : f emp ⊣⊢ emp; bi_mor_impl_2 P Q : (f P → f Q)%I ⊢ f (P → Q)%I; bi_mor_forall_2 A (Φ : A → PROP1) : (∀ x, f (Φ x)) ⊢ f (∀ x, Φ x); bi_mor_exist_1 A (Φ : A → PROP1) : f (∃ x, Φ x) ⊢ ∃ x, f (Φ x); bi_mor_internal_eq_1 (A : ofeT) (x y : A) : f (x ≡ y) ⊢ (x ≡ y); bi_mor_sep P Q : f (P ∗ Q) ⊣⊢ (f P ∗ f Q); bi_mor_wand_2 P Q : (f P -∗ f Q) ⊢ f (P -∗ Q); bi_mor_plainly P : f (bi_plainly P) ⊣⊢ bi_plainly (f P); bi_mor_persistently P : f (bi_persistently P) ⊣⊢ bi_persistently (f P) }. Class SbiMorphism {PROP1 PROP2 : sbi} (f : PROP1 → PROP2) := { sbi_mor_bi_mor :> BiMorphism f; sbi_mor_later P : f (▷ P) ⊣⊢ ▷ f P }.