Entails

instance Iris.BI.entails_trans {PROP : Type u_1} [BI PROP] : Trans Entails Entails Entails

Equations

• Iris.BI.entails_trans = { trans := ⋯ }

instance Iris.BI.entails_antisymm {PROP : Type u_1} [BI PROP] : Std.Antisymmetric BiEntails Entails

instance Iris.BI.equiv_trans {PROP : Type u_1} [BI PROP] : Trans BiEntails BiEntails BiEntails

Equations

• Iris.BI.equiv_trans = { trans := ⋯ }

Logic

theorem Iris.BI.and_elim_l' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : P ⊢ R) : P ∧ Q ⊢ R

theorem Iris.BI.and_elim_r' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : Q ⊢ R) : P ∧ Q ⊢ R

theorem Iris.BI.or_intro_l' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : P ⊢ Q) : P ⊢ Q ∨ R

theorem Iris.BI.or_intro_r' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : P ⊢ R) : P ⊢ Q ∨ R

theorem Iris.BI.and_symm {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∧ Q ⊢ Q ∧ P

theorem Iris.BI.or_symm {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∨ Q ⊢ Q ∨ P

theorem Iris.BI.imp_intro' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : Q ∧ P ⊢ R) : P ⊢ Q → R

theorem Iris.BI.mp {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h1 : P ⊢ Q → R) (h2 : P ⊢ Q) : P ⊢ R

theorem Iris.BI.imp_elim' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : Q ⊢ P → R) : P ∧ Q ⊢ R

theorem Iris.BI.imp_elim_l {PROP : Type u_1} [BI PROP] {P Q : PROP} : (P → Q) ∧ P ⊢ Q

theorem Iris.BI.imp_elim_r {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∧ (P → Q) ⊢ Q

theorem Iris.BI.false_elim {PROP : Type u_1} [BI PROP] {P : PROP} : False ⊢ P

theorem Iris.BI.true_intro {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊢ True

theorem Iris.BI.and_mono {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊢ Q) (h2 : P' ⊢ Q') : P ∧ P' ⊢ Q ∧ Q'

theorem Iris.BI.and_mono_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊢ P') : P ∧ Q ⊢ P' ∧ Q

theorem Iris.BI.and_mono_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : P ∧ Q ⊢ P ∧ Q'

theorem Iris.BI.and_congr {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : P ∧ P' ⊣⊢ Q ∧ Q'

theorem Iris.BI.and_congr_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : P ∧ Q ⊣⊢ P' ∧ Q

theorem Iris.BI.and_congr_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : P ∧ Q ⊣⊢ P ∧ Q'

theorem Iris.BI.or_mono {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊢ Q) (h2 : P' ⊢ Q') : P ∨ P' ⊢ Q ∨ Q'

theorem Iris.BI.or_mono_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊢ P') : P ∨ Q ⊢ P' ∨ Q

theorem Iris.BI.or_mono_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : P ∨ Q ⊢ P ∨ Q'

theorem Iris.BI.or_congr {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : P ∨ P' ⊣⊢ Q ∨ Q'

theorem Iris.BI.or_congr_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : P ∨ Q ⊣⊢ P' ∨ Q

theorem Iris.BI.or_congr_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : P ∨ Q ⊣⊢ P ∨ Q'

theorem Iris.BI.imp_mono {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : Q ⊢ P) (h2 : P' ⊢ Q') : (P → P') ⊢ Q → Q'

theorem Iris.BI.imp_mono_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P' ⊢ P) : (P → Q) ⊢ P' → Q

theorem Iris.BI.imp_mono_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : (P → Q) ⊢ P → Q'

theorem Iris.BI.imp_congr {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : (P → P') ⊣⊢ (Q → Q')

theorem Iris.BI.imp_congr_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P → Q) ⊣⊢ (P' → Q)

theorem Iris.BI.imp_congr_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P → Q) ⊣⊢ (P → Q')

theorem Iris.BI.forall_ne {PROP : Type u_1} {α : Sort u_2} {n : Nat} [BI PROP] {Φ Ψ : α → PROP} (h : ∀ (a : α), OFE.Dist n (Φ a) (Ψ a)) : OFE.Dist n («forall» fun (a : α) => Φ a) («forall» fun (a : α) => Ψ a)

theorem Iris.BI.forall_intro {PROP : Type u_1} {α : Sort u_2} [BI PROP] {P : PROP} {Ψ : α → PROP} (h : ∀ (a : α), P ⊢ Ψ a) : P ⊢ «forall» fun (a : α) => Ψ a

theorem Iris.BI.forall_elim {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Ψ : α → PROP} (a : α) : («forall» fun (a : α) => Ψ a) ⊢ Ψ a

theorem Iris.BI.forall_mono {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ Ψ : α → PROP} (h : ∀ (a : α), Φ a ⊢ Ψ a) : («forall» fun (a : α) => Φ a) ⊢ «forall» fun (a : α) => Ψ a

theorem Iris.BI.forall_congr {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ Ψ : α → PROP} (h : ∀ (a : α), Φ a ⊣⊢ Ψ a) : («forall» fun (a : α) => Φ a) ⊣⊢ «forall» fun (a : α) => Ψ a

theorem Iris.BI.exists_ne {PROP : Type u_1} {α : Sort u_2} {n : Nat} [BI PROP] {Φ Ψ : α → PROP} (h : ∀ (a : α), OFE.Dist n (Φ a) (Ψ a)) : OFE.Dist n («exists» fun (a : α) => Φ a) («exists» fun (a : α) => Ψ a)

theorem Iris.BI.exists_intro {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Ψ : α → PROP} (a : α) : Ψ a ⊢ «exists» fun (a : α) => Ψ a

theorem Iris.BI.exists_elim {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} {Q : PROP} (h : ∀ (a : α), Φ a ⊢ Q) : («exists» fun (a : α) => Φ a) ⊢ Q

theorem Iris.BI.exists_mono {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ Ψ : α → PROP} (h : ∀ (a : α), Φ a ⊢ Ψ a) : («exists» fun (a : α) => Φ a) ⊢ «exists» fun (a : α) => Ψ a

theorem Iris.BI.exists_congr {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ Ψ : α → PROP} (h : ∀ (a : α), Φ a ⊣⊢ Ψ a) : («exists» fun (a : α) => Φ a) ⊣⊢ «exists» fun (a : α) => Ψ a

theorem Iris.BI.and_self {PROP : Type u_1} [BI PROP] {P : PROP} : P ∧ P ⊣⊢ P

instance Iris.BI.instIdempotentBiEntailsAnd {PROP : Type u_1} [BI PROP] : Std.Idempotent BiEntails and

theorem Iris.BI.or_self {PROP : Type u_1} [BI PROP] {P : PROP} : P ∨ P ⊣⊢ P

instance Iris.BI.instIdempotentBiEntailsOr {PROP : Type u_1} [BI PROP] : Std.Idempotent BiEntails or

theorem Iris.BI.and_comm {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∧ Q ⊣⊢ Q ∧ P

instance Iris.BI.instCommutativeBiEntailsAnd {PROP : Type u_1} [BI PROP] : Std.Commutative BiEntails and

theorem Iris.BI.or_comm {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∨ Q ⊣⊢ Q ∨ P

instance Iris.BI.instCommutativeBiEntailsOr {PROP : Type u_1} [BI PROP] : Std.Commutative BiEntails or

theorem Iris.BI.true_and {PROP : Type u_1} [BI PROP] {P : PROP} : True ∧ P ⊣⊢ P

instance Iris.BI.instLeftIdBiEntailsPureTrueAnd {PROP : Type u_1} [BI PROP] : Std.LeftId BiEntails iprop(True) and

theorem Iris.BI.and_true {PROP : Type u_1} [BI PROP] {P : PROP} : P ∧ True ⊣⊢ P

instance Iris.BI.instRightIdBiEntailsPureTrueAnd {PROP : Type u_1} [BI PROP] : Std.RightId BiEntails iprop(True) and

theorem Iris.BI.false_and {PROP : Type u_1} [BI PROP] {P : PROP} : False ∧ P ⊣⊢ False

theorem Iris.BI.and_false {PROP : Type u_1} [BI PROP] {P : PROP} : P ∧ False ⊣⊢ False

theorem Iris.BI.true_or {PROP : Type u_1} [BI PROP] {P : PROP} : True ∨ P ⊣⊢ True

theorem Iris.BI.or_true {PROP : Type u_1} [BI PROP] {P : PROP} : P ∨ True ⊣⊢ True

theorem Iris.BI.false_or {PROP : Type u_1} [BI PROP] {P : PROP} : False ∨ P ⊣⊢ P

instance Iris.BI.instLeftIdBiEntailsPureFalseOr {PROP : Type u_1} [BI PROP] : Std.LeftId BiEntails iprop(False) or

theorem Iris.BI.or_false {PROP : Type u_1} [BI PROP] {P : PROP} : P ∨ False ⊣⊢ P

instance Iris.BI.instRightIdBiEntailsPureFalseOr {PROP : Type u_1} [BI PROP] : Std.RightId BiEntails iprop(False) or

theorem Iris.BI.and_assoc {PROP : Type u_1} [BI PROP] {P Q R : PROP} : (P ∧ Q) ∧ R ⊣⊢ P ∧ Q ∧ R

theorem Iris.BI.or_assoc {PROP : Type u_1} [BI PROP] {P Q R : PROP} : (P ∨ Q) ∨ R ⊣⊢ P ∨ Q ∨ R

theorem Iris.BI.true_imp {PROP : Type u_1} [BI PROP] {P : PROP} : (True → P) ⊣⊢ P

instance Iris.BI.instLeftIdBiEntailsPureTrueAnd_1 {PROP : Type u_1} [BI PROP] : Std.LeftId BiEntails iprop(True) and

theorem Iris.BI.imp_self {PROP : Type u_1} [BI PROP] {P Q : PROP} : Q ⊢ P → P

theorem Iris.BI.imp_trans {PROP : Type u_1} [BI PROP] {P Q R : PROP} : (P → Q) ∧ (Q → R) ⊢ P → R

theorem Iris.BI.false_imp {PROP : Type u_1} [BI PROP] {P : PROP} : (False → P) ⊣⊢ True

instance Iris.BI.instLawfulBigOpAndPureTrueBiEntails {PROP : Type u_1} [BI PROP] : Std.LawfulBigOp and iprop(True) BiEntails

theorem Iris.BI.and_left_comm {PROP : Type u_1} [BI PROP] {P Q R : PROP} : P ∧ Q ∧ R ⊣⊢ Q ∧ P ∧ R

instance Iris.BI.instAssociativeBiEntailsAnd {PROP : Type u_1} [BI PROP] : Std.Associative BiEntails and

theorem Iris.BI.and_or_l {PROP : Type u_1} [BI PROP] {P Q R : PROP} : P ∧ (Q ∨ R) ⊣⊢ P ∧ Q ∨ P ∧ R

theorem Iris.BI.and_exists_l {PROP : Type u_1} {α : Sort u_2} [BI PROP] {P : PROP} {Ψ : α → PROP} : (P ∧ «exists» fun (a : α) => Ψ a) ⊣⊢ «exists» fun (a : α) => iprop(P ∧ Ψ a)

theorem Iris.BI.or_eq_ite {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∨ Q ⊣⊢ «exists» fun (b : Bool) => if b = true then P else Q

theorem Iris.BI.exists_intro' {PROP : Type u_1} {α : Sort u_2} [BI PROP] {P : PROP} {Ψ : α → PROP} (a : α) (h : P ⊢ Ψ a) : P ⊢ «exists» fun (a : α) => Ψ a

BI

theorem Iris.BI.sep_mono_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊢ P') : P ∗ Q ⊢ P' ∗ Q

theorem Iris.BI.sep_mono_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : P ∗ Q ⊢ P ∗ Q'

theorem Iris.BI.sep_congr {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : P ∗ P' ⊣⊢ Q ∗ Q'

theorem Iris.BI.sep_congr_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : P ∗ Q ⊣⊢ P' ∗ Q

theorem Iris.BI.sep_congr_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : P ∗ Q ⊣⊢ P ∗ Q'

theorem Iris.BI.wand_mono {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : Q ⊢ P) (h2 : P' ⊢ Q') : (P -∗ P') ⊢ Q -∗ Q'

theorem Iris.BI.wand_mono_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P' ⊢ P) : (P -∗ Q) ⊢ P' -∗ Q

theorem Iris.BI.wand_mono_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊢ Q') : (P -∗ Q) ⊢ P -∗ Q'

theorem Iris.BI.wand_congr {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : (P -∗ P') ⊣⊢ (Q -∗ Q')

theorem Iris.BI.wand_congr_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P -∗ Q) ⊣⊢ (P' -∗ Q)

theorem Iris.BI.wand_congr_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P -∗ Q) ⊣⊢ (P -∗ Q')

theorem Iris.BI.sep_comm {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∗ Q ⊣⊢ Q ∗ P

instance Iris.BI.instCommutativeBiEntailsSep {PROP : Type u_1} [BI PROP] : Std.Commutative BiEntails sep

theorem Iris.BI.sep_assoc {PROP : Type u_1} [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ P ∗ Q ∗ R

instance Iris.BI.instAssociativeBiEntailsSep {PROP : Type u_1} [BI PROP] : Std.Associative BiEntails sep

theorem Iris.BI.sep_left_comm {PROP : Type u_1} [BI PROP] {P Q R : PROP} : P ∗ Q ∗ R ⊣⊢ Q ∗ P ∗ R

theorem Iris.BI.sep_right_comm {PROP : Type u_1} [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ (P ∗ R) ∗ Q

theorem Iris.BI.sep_sep_sep_comm {PROP : Type u_1} [BI PROP] {P Q R S : PROP} : (P ∗ Q) ∗ R ∗ S ⊣⊢ (P ∗ R) ∗ Q ∗ S

instance Iris.BI.instLeftIdBiEntailsEmpSep {PROP : Type u_1} [BI PROP] : Std.LeftId BiEntails iprop(emp) sep

theorem Iris.BI.sep_emp {PROP : Type u_1} [BI PROP] {P : PROP} : P ∗ emp ⊣⊢ P

instance Iris.BI.instRightIdBiEntailsEmpSep {PROP : Type u_1} [BI PROP] : Std.RightId BiEntails iprop(emp) sep

instance Iris.BI.instLawfulBigOpSepEmpBiEntails {PROP : Type u_1} [BI PROP] : Std.LawfulBigOp sep iprop(emp) BiEntails

theorem Iris.BI.true_sep_2 {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊢ True ∗ P

theorem Iris.BI.wand_intro' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : Q ∗ P ⊢ R) : P ⊢ Q -∗ R

theorem Iris.BI.wand_elim' {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h : Q ⊢ P -∗ R) : P ∗ Q ⊢ R

theorem Iris.BI.wand_elim_l {PROP : Type u_1} [BI PROP] {P Q : PROP} : (P -∗ Q) ∗ P ⊢ Q

theorem Iris.BI.wand_elim_r {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∗ (P -∗ Q) ⊢ Q

theorem Iris.BI.sep_or_l {PROP : Type u_1} [BI PROP] {P Q R : PROP} : P ∗ (Q ∨ R) ⊣⊢ P ∗ Q ∨ P ∗ R

theorem Iris.BI.sep_or_r {PROP : Type u_1} [BI PROP] {P Q R : PROP} : (P ∨ Q) ∗ R ⊣⊢ P ∗ R ∨ Q ∗ R

theorem Iris.BI.sep_exists_l {PROP : Type u_1} {α : Sort u_2} [BI PROP] {P : PROP} {Ψ : α → PROP} : (P ∗ «exists» fun (a : α) => Ψ a) ⊣⊢ «exists» fun (a : α) => iprop(P ∗ Ψ a)

theorem Iris.BI.sep_exists_r {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} {Q : PROP} : («exists» fun (a : α) => Φ a) ∗ Q ⊣⊢ «exists» fun (a : α) => iprop(Φ a ∗ Q)

theorem Iris.BI.wand_rfl {PROP : Type u_1} [BI PROP] {P : PROP} : ⊢ P -∗ P

theorem Iris.BI.wandIff_congr {PROP : Type u_1} [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') : (P ∗-∗ P') ⊣⊢ (Q ∗-∗ Q')

theorem Iris.BI.wandIff_congr_l {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P ∗-∗ Q) ⊣⊢ (P' ∗-∗ Q)

theorem Iris.BI.wandIff_congr_r {PROP : Type u_1} [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P ∗-∗ Q) ⊣⊢ (P ∗-∗ Q')

theorem Iris.BI.wandIff_refl {PROP : Type u_1} [BI PROP] {P : PROP} : ⊢ P ∗-∗ P

theorem Iris.BI.wand_entails {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : ⊢ P -∗ Q) : P ⊢ Q

theorem Iris.BI.entails_wand {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : ⊢ P -∗ Q

theorem Iris.BI.equiv_wandIff {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : ⊢ P ∗-∗ Q

theorem Iris.BI.wandIff_equiv {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : ⊢ P ∗-∗ Q) : P ⊣⊢ Q

Pure

theorem Iris.BI.pure_elim {PROP : Type u_1} [BI PROP] (φ : Prop) {Q R : PROP} (h1 : Q ⊢ ⌜φ⌝) (h2 : φ → Q ⊢ R) : Q ⊢ R

theorem Iris.BI.pure_mono {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} (h : φ1 → φ2) : ⌜φ1⌝ ⊢ ⌜φ2⌝

theorem Iris.BI.pure_congr {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} (h : φ1 ↔ φ2) : ⌜φ1⌝ ⊣⊢ ⌜φ2⌝

theorem Iris.BI.pure_elim_l {PROP : Type u_1} [BI PROP] {φ : Prop} {Q R : PROP} (h : φ → Q ⊢ R) : ⌜φ⌝ ∧ Q ⊢ R

theorem Iris.BI.pure_elim_r {PROP : Type u_1} [BI PROP] {φ : Prop} {Q R : PROP} (h : φ → Q ⊢ R) : Q ∧ ⌜φ⌝ ⊢ R

theorem Iris.BI.pure_true {PROP : Type u_1} [BI PROP] {φ : Prop} (h : φ) : ⌜φ⌝ ⊣⊢ True

theorem Iris.BI.pure_and {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} : ⌜φ1⌝ ∧ ⌜φ2⌝ ⊣⊢ ⌜φ1 ∧ φ2⌝

theorem Iris.BI.pure_or {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} : ⌜φ1⌝ ∨ ⌜φ2⌝ ⊣⊢ ⌜φ1 ∨ φ2⌝

theorem Iris.BI.pure_imp_2 {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} : ⌜φ1 → φ2⌝ ⊢ ⌜φ1⌝ → ⌜φ2⌝

theorem Iris.BI.pure_imp {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} : (⌜φ1⌝ → ⌜φ2⌝) ⊣⊢ ⌜φ1 → φ2⌝

theorem Iris.BI.pure_forall_2 {PROP : Type u_1} {α : Sort u_2} [BI PROP] {φ : α → Prop} : ⌜∀ (x : α), φ x⌝ ⊢ «forall» fun (x : α) => iprop(⌜φ x⌝)

theorem Iris.BI.pure_forall {PROP : Type u_1} {α : Sort u_2} [BI PROP] {φ : α → Prop} : («forall» fun (x : α) => iprop(⌜φ x⌝)) ⊣⊢ ⌜∀ (x : α), φ x⌝

theorem Iris.BI.pure_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] {φ : α → Prop} : («exists» fun (x : α) => iprop(⌜φ x⌝)) ⊣⊢ ⌜∃ (x : α), φ x⌝

Affine

theorem Iris.BI.affinely_ne {PROP : Type u_1} [BI PROP] : OFE.NonExpansive affinely

theorem Iris.BI.affinely_congr {PROP : Type u_1} [BI PROP] {P P' : PROP} (h : P ⊣⊢ P') : <affine> P ⊣⊢ <affine> P'

theorem Iris.BI.affinely_elim_emp {PROP : Type u_1} [BI PROP] {P : PROP} : <affine> P ⊢ emp

theorem Iris.BI.affinely_elim {PROP : Type u_1} [BI PROP] {P : PROP} : <affine> P ⊢ P

theorem Iris.BI.affinely_mono {PROP : Type u_1} [BI PROP] {P Q : PROP} : (P ⊢ Q) → <affine> P ⊢ <affine> Q

theorem Iris.BI.affinely_idem {PROP : Type u_1} [BI PROP] {P : PROP} : <affine> <affine> P ⊣⊢ <affine> P

theorem Iris.BI.affinely_intro' {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ <affine> Q) : <affine> P ⊢ <affine> Q

theorem Iris.BI.affinely_false {PROP : Type u_1} [BI PROP] : <affine> False ⊣⊢ False

theorem Iris.BI.affinely_emp {PROP : Type u_1} [BI PROP] : <affine> emp ⊣⊢ emp

theorem Iris.BI.affinely_or {PROP : Type u_1} [BI PROP] {P Q : PROP} : <affine> (P ∨ Q) ⊣⊢ <affine> P ∨ <affine> Q

theorem Iris.BI.affinely_and {PROP : Type u_1} [BI PROP] {P Q : PROP} : <affine> (P ∧ Q) ⊣⊢ <affine> P ∧ <affine> Q

theorem Iris.BI.affinely_sep_2 {PROP : Type u_1} [BI PROP] {P Q : PROP} : <affine> P ∗ <affine> Q ⊢ <affine> (P ∗ Q)

theorem Iris.BI.affinely_sep_r {PROP : Type u_1} [BI PROP] [BIPositive PROP] {P Q : PROP} : <affine> (P ∗ Q) ⊢ P ∗ <affine> Q

theorem Iris.BI.affinely_sep {PROP : Type u_1} [BI PROP] [BIPositive PROP] {P Q : PROP} : <affine> (P ∗ Q) ⊣⊢ <affine> P ∗ <affine> Q

theorem Iris.BI.affinely_forall_1 {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : (<affine> «forall» fun (a : α) => Φ a) ⊢ «forall» fun (a : α) => iprop(<affine> Φ a)

theorem Iris.BI.affinely_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : (<affine> «exists» fun (a : α) => Φ a) ⊣⊢ «exists» fun (a : α) => iprop(<affine> Φ a)

theorem Iris.BI.affinely_true {PROP : Type u_1} [BI PROP] : <affine> True ⊣⊢ emp

theorem Iris.BI.affinely_and_l {PROP : Type u_1} [BI PROP] {P Q : PROP} : <affine> P ∧ Q ⊣⊢ <affine> (P ∧ Q)

theorem Iris.BI.affinely_and_r {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∧ <affine> Q ⊣⊢ <affine> (P ∧ Q)

theorem Iris.BI.affinely_and_lr {PROP : Type u_1} [BI PROP] {P Q : PROP} : <affine> P ∧ Q ⊣⊢ P ∧ <affine> Q

Affine instances

instance Iris.BI.emp_affine {PROP : Type u_1} [BI PROP] : Affine iprop(emp)

theorem Iris.BI.affine_mono {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ Q) [Affine Q] : Affine P

instance Iris.BI.false_affine {PROP : Type u_1} [BI PROP] : Affine iprop(False)

instance Iris.BI.and_affine_l {PROP : Type u_1} [BI PROP] (P Q : PROP) [Affine P] : Affine iprop(P ∧ Q)

instance Iris.BI.and_affine_r {PROP : Type u_1} [BI PROP] (P Q : PROP) [Affine Q] : Affine iprop(P ∧ Q)

instance Iris.BI.or_affine {PROP : Type u_1} [BI PROP] (P Q : PROP) [Affine P] [Affine Q] : Affine iprop(P ∨ Q)

instance Iris.BI.forall_affine {α : Sort u_1} {PROP : Type u_2} [Inhabited α] [BI PROP] (Φ : α → PROP) [∀ (x : α), Affine (Φ x)] : Affine («forall» fun (x : α) => Φ x)

instance Iris.BI.exists_affine {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) [∀ (x : α), Affine (Φ x)] : Affine («exists» fun (x : α) => Φ x)

instance Iris.BI.sep_affine {PROP : Type u_1} [BI PROP] (P Q : PROP) [Affine P] [Affine Q] : Affine iprop(P ∗ Q)

instance Iris.BI.affinely_affine {PROP : Type u_1} [BI PROP] (P : PROP) : Affine iprop(<affine> P)

Absorbing

theorem Iris.BI.absorbingly_ne {PROP : Type u_1} [BI PROP] : OFE.NonExpansive absorbingly

theorem Iris.BI.absorbingly_congr {PROP : Type u_1} [BI PROP] {P P' : PROP} (h : P ⊣⊢ P') : <absorb> P ⊣⊢ <absorb> P'

theorem Iris.BI.absorbingly_intro {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊢ <absorb> P

theorem Iris.BI.absorbingly_mono {PROP : Type u_1} [BI PROP] {P Q : PROP} : (P ⊢ Q) → <absorb> P ⊢ <absorb> Q

theorem Iris.BI.absorbingly_idem {PROP : Type u_1} [BI PROP] {P : PROP} : <absorb> <absorb> P ⊣⊢ <absorb> P

instance Iris.BI.absorbingly_absorbing {PROP : Type u_1} [BI PROP] (P : PROP) : Absorbing iprop(<absorb> P)

theorem Iris.BI.absorbingly_pure {PROP : Type u_1} {φ : Prop} [BI PROP] : <absorb> ⌜φ⌝ ⊣⊢ ⌜φ⌝

instance Iris.BI.pureAbsorbing {PROP : Type u_1} (φ : Prop) [BI PROP] : Absorbing iprop(⌜φ⌝)

theorem Iris.BI.absorbingly_true {PROP : Type u_1} [BI PROP] : <absorb> True ⊣⊢ True

theorem Iris.BI.absorbingly_or {PROP : Type u_1} [BI PROP] {P Q : PROP} : <absorb> (P ∨ Q) ⊣⊢ <absorb> P ∨ <absorb> Q

theorem Iris.BI.absorbingly_and_1 {PROP : Type u_1} [BI PROP] {P Q : PROP} : <absorb> (P ∧ Q) ⊢ <absorb> P ∧ <absorb> Q

theorem Iris.BI.absorbingly_forall_1 {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : (<absorb> «forall» fun (a : α) => Φ a) ⊢ «forall» fun (a : α) => iprop(<absorb> Φ a)

theorem Iris.BI.absorbingly_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : (<absorb> «exists» fun (a : α) => Φ a) ⊣⊢ «exists» fun (a : α) => iprop(<absorb> Φ a)

theorem Iris.BI.absorbingly_sep {PROP : Type u_1} [BI PROP] {P Q : PROP} : <absorb> (P ∗ Q) ⊣⊢ <absorb> P ∗ <absorb> Q

theorem Iris.BI.absorbingly_emp {PROP : Type u_1} [BI PROP] : <absorb> emp ⊣⊢ True

theorem Iris.BI.absorbingly_wand_1 {PROP : Type u_1} [BI PROP] {P Q : PROP} : <absorb> (P -∗ Q) ⊢ <absorb> P -∗ <absorb> Q

theorem Iris.BI.absorbingly_sep_l {PROP : Type u_1} [BI PROP] {P Q : PROP} : <absorb> P ∗ Q ⊣⊢ <absorb> (P ∗ Q)

theorem Iris.BI.absorbingly_sep_r {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∗ <absorb> Q ⊣⊢ <absorb> (P ∗ Q)

theorem Iris.BI.absorbingly_sep_lr {PROP : Type u_1} [BI PROP] {P Q : PROP} : <absorb> P ∗ Q ⊣⊢ P ∗ <absorb> Q

theorem Iris.BI.affinely_absorbingly {PROP : Type u_1} [BI PROP] [BIPositive PROP] {P : PROP} : <affine> <absorb> P ⊣⊢ <affine> P

Absorbing instances

instance Iris.BI.pure_absorbing {PROP : Type u_1} [BI PROP] (φ : Prop) : Absorbing iprop(⌜φ⌝)

instance Iris.BI.and_absorbing {PROP : Type u_1} [BI PROP] (P Q : PROP) [Absorbing P] [Absorbing Q] : Absorbing iprop(P ∧ Q)

instance Iris.BI.or_absorbing {PROP : Type u_1} [BI PROP] (P Q : PROP) [Absorbing P] [Absorbing Q] : Absorbing iprop(P ∨ Q)

instance Iris.BI.forall_absorbing {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) [∀ (x : α), Absorbing (Φ x)] : Absorbing («forall» fun (x : α) => Φ x)

instance Iris.BI.exists_absorbing {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) [∀ (x : α), Absorbing (Φ x)] : Absorbing («exists» fun (x : α) => Φ x)

instance Iris.BI.sep_absorbing_l {PROP : Type u_1} [BI PROP] (P Q : PROP) [Absorbing P] : Absorbing iprop(P ∗ Q)

instance Iris.BI.sep_absorbing_r {PROP : Type u_1} [BI PROP] (P Q : PROP) [Absorbing Q] : Absorbing iprop(P ∗ Q)

@[instance 1010]

instance Iris.BI.biaffine_absorbing {PROP : Type u_1} [BI PROP] [BIAffine PROP] (P : PROP) : Absorbing P

Affine / Absorbing Propositions

theorem Iris.BI.affine_affinely {PROP : Type u_1} [BI PROP] (P : PROP) [Affine P] : <affine> P ⊣⊢ P

theorem Iris.BI.biaffine_iff_true_emp {PROP : Type u_1} [BI PROP] : BIAffine PROP ↔ True ⊢ emp

theorem Iris.BI.biaffine_of_true_affine {PROP : Type u_1} [BI PROP] [Affine iprop(True)] : BIAffine PROP

theorem Iris.BI.absorbing_absorbingly {PROP : Type u_1} [BI PROP] {P : PROP} [Absorbing P] : <absorb> P ⊣⊢ P

theorem Iris.BI.absorbing_of_emp_absorbing {PROP : Type u_1} [BI PROP] [Absorbing iprop(emp)] (P : PROP) : Absorbing P

theorem Iris.BI.sep_elim_l {PROP : Type u_1} [BI PROP] {P Q : PROP} [Std.TCOr (Affine Q) (Absorbing P)] : P ∗ Q ⊢ P

theorem Iris.BI.sep_elim_r {PROP : Type u_1} [BI PROP] {P Q : PROP} [Std.TCOr (Affine P) (Absorbing Q)] : P ∗ Q ⊢ Q

instance Iris.BI.wand_absorbing_l {PROP : Type u_1} [BI PROP] (P Q : PROP) [Absorbing P] : Absorbing iprop(P -∗ Q)

instance Iris.BI.wand_absorbing_r {PROP : Type u_1} [BI PROP] (P Q : PROP) [Absorbing Q] : Absorbing iprop(P -∗ Q)

theorem Iris.BI.sep_and {PROP : Type u_1} [BI PROP] {P Q : PROP} [Std.TCOr (Affine P) (Absorbing Q)] [Std.TCOr (Affine Q) (Absorbing P)] : P ∗ Q ⊢ P ∧ Q

theorem Iris.BI.affinely_intro {PROP : Type u_1} [BI PROP] {P Q : PROP} [Affine P] (h : P ⊢ Q) : P ⊢ <affine> Q

theorem Iris.BI.emp_and {PROP : Type u_1} [BI PROP] {P : PROP} [Affine P] : emp ∧ P ⊣⊢ P

instance Iris.BI.instLeftIdBiEntailsEmpAndOfBIAffine {PROP : Type u_1} [BI PROP] [BIAffine PROP] : Std.LeftId BiEntails iprop(emp) and

theorem Iris.BI.and_emp {PROP : Type u_1} [BI PROP] {P : PROP} [Affine P] : P ∧ emp ⊣⊢ P

instance Iris.BI.instRightIdBiEntailsEmpAndOfBIAffine {PROP : Type u_1} [BI PROP] [BIAffine PROP] : Std.RightId BiEntails iprop(emp) and

theorem Iris.BI.emp_or {PROP : Type u_1} [BI PROP] {P : PROP} [Affine P] : emp ∨ P ⊣⊢ emp

theorem Iris.BI.or_emp {PROP : Type u_1} [BI PROP] {P : PROP} [Affine P] : P ∨ emp ⊣⊢ emp

theorem Iris.BI.true_emp {PROP : Type u_1} [BI PROP] [h : BIAffine PROP] : True ⊣⊢ emp

instance Iris.BI.instAbsorbingOfBIAffine {PROP : Type u_1} [BI PROP] [BIAffine PROP] (P : PROP) : Absorbing P

theorem Iris.BI.true_sep {PROP : Type u_1} [BI PROP] {P : PROP} [Absorbing P] : True ∗ P ⊣⊢ P

instance Iris.BI.instLeftIdBiEntailsPureTrueSepOfBIAffine {PROP : Type u_1} [BI PROP] [BIAffine PROP] : Std.LeftId BiEntails iprop(True) sep

theorem Iris.BI.sep_true {PROP : Type u_1} [BI PROP] {P : PROP} [Absorbing P] : P ∗ True ⊣⊢ P

instance Iris.BI.instRightIdBiEntailsPureTrueSepOfBIAffine {PROP : Type u_1} [BI PROP] [BIAffine PROP] : Std.RightId BiEntails iprop(True) sep

instance Iris.BI.instBIPositiveOfBIAffine {PROP : Type u_1} [BI PROP] [BIAffine PROP] : BIPositive PROP

theorem Iris.BI.imp_wand_1 {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P Q : PROP} : (P → Q) ⊢ P -∗ Q

theorem Iris.BI.pure_sep {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} : ⌜φ1⌝ ∗ ⌜φ2⌝ ⊣⊢ ⌜φ1 ∧ φ2⌝

theorem Iris.BI.pure_wand_2 {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} : ⌜φ1 → φ2⌝ ⊢ ⌜φ1⌝ -∗ ⌜φ2⌝

theorem Iris.BI.pure_wand {PROP : Type u_1} [BI PROP] {φ1 φ2 : Prop} : (⌜φ1⌝ -∗ ⌜φ2⌝) ⊣⊢ ⌜φ1 → φ2⌝

Properties of the persistence modality

theorem Iris.BI.persistently_congr {PROP : Type u_1} [BI PROP] {P P' : PROP} (h : P ⊣⊢ P') : <pers> P ⊣⊢ <pers> P'

instance Iris.BI.persistently_persistent {PROP : Type u_1} [BI PROP] (P : PROP) : Persistent iprop(<pers> P)

theorem Iris.BI.persistently_absorb_r {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∗ <pers> Q ⊢ <pers> Q

theorem Iris.BI.absorbingly_persistently {PROP : Type u_1} [BI PROP] {P : PROP} : <absorb> <pers> P ⊣⊢ <pers> P

instance Iris.BI.persistently_absorbing {PROP : Type u_1} [BI PROP] (P : PROP) : Absorbing iprop(<pers> P)

theorem Iris.BI.persistently_forall_1 {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Ψ : α → PROP} : (<pers> «forall» fun (a : α) => Ψ a) ⊢ «forall» fun (a : α) => iprop(<pers> Ψ a)

theorem Iris.BI.persistently_forall {PROP : Type u_1} {α : Sort u_2} [BI PROP] [h : BIPersistentlyForall PROP] {Ψ : α → PROP} : (<pers> «forall» fun (a : α) => Ψ a) ⊣⊢ «forall» fun (a : α) => iprop(<pers> Ψ a)

theorem Iris.BI.persistently_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Ψ : α → PROP} : (<pers> «exists» fun (a : α) => Ψ a) ⊣⊢ «exists» fun (a : α) => iprop(<pers> Ψ a)

theorem Iris.BI.persistently_and {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q

theorem Iris.BI.persistently_ite {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : iprop(<pers> if p = true then P else Q) = if p = true then iprop(<pers> P) else iprop(<pers> Q)

theorem Iris.BI.persistently_or {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> (P ∨ Q) ⊣⊢ <pers> P ∨ <pers> Q

theorem Iris.BI.persistently_imp_1 {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> (P → Q) ⊢ <pers> P → <pers> Q

theorem Iris.BI.persistently_emp_intro {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊢ <pers> emp

theorem Iris.BI.persistently_emp {PROP : Type u_1} [BI PROP] : <pers> emp ⊣⊢ True

theorem Iris.BI.persistently_true {PROP : Type u_1} [BI PROP] : <pers> True ⊣⊢ True

theorem Iris.BI.persistently_affinely {PROP : Type u_1} [BI PROP] {P : PROP} : <pers> <affine> P ⊣⊢ <pers> P

theorem Iris.BI.persistently_and_affinely_sep {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> P ∧ Q ⊢ <affine> P ∗ Q

theorem Iris.BI.persistently_and_sep_assoc {PROP : Type u_1} [BI PROP] {P Q R : PROP} : <pers> P ∧ Q ∗ R ⊣⊢ (<pers> P ∧ Q) ∗ R

theorem Iris.BI.intuitionistically_elim {PROP : Type u_1} [BI PROP] {P : PROP} : □ P ⊢ P

theorem Iris.BI.absorbingly_of_persistently {PROP : Type u_1} [BI PROP] {P : PROP} : <pers> P ⊢ <absorb> P

theorem Iris.BI.persistently_elim {PROP : Type u_1} [BI PROP] {P : PROP} [Absorbing P] : <pers> P ⊢ P

theorem Iris.BI.persistently_idem {PROP : Type u_1} [BI PROP] {P : PROP} : <pers> <pers> P ⊣⊢ <pers> P

theorem Iris.BI.persistently_intro' {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : <pers> P ⊢ Q) : <pers> P ⊢ <pers> Q

theorem Iris.BI.persistently_pure {PROP : Type u_1} {φ : Prop} [BI PROP] : <pers> ⌜φ⌝ ⊣⊢ ⌜φ⌝

theorem Iris.BI.persistently_and_imp_sep {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> P ∧ Q ⊢ <pers> P ∗ Q

theorem Iris.BI.and_persistently_imp_sep {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∧ <pers> Q ⊢ P ∗ <pers> Q

theorem Iris.BI.persistently_sep_persistently {PROP : Type u_1} [BI PROP] {P : PROP} : <pers> P ∗ <pers> P ⊣⊢ <pers> P

theorem Iris.BI.persistently_and_sep {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> (P ∧ Q) ⊢ <pers> (P ∗ Q)

theorem Iris.BI.persistently_and_persistently_sep {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> P ∧ <pers> Q ⊣⊢ <pers> P ∗ <pers> Q

theorem Iris.BI.persistently_sep_2 {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q)

theorem Iris.BI.persistently_sep {PROP : Type u_1} [BI PROP] [BIPositive PROP] {P Q : PROP} : <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q

theorem Iris.BI.self_sep_persistently {PROP : Type u_1} [BI PROP] {P : PROP} : P ∗ <pers> P ⊣⊢ <pers> P

theorem Iris.BI.affinely_sep_persistently {PROP : Type u_1} [BI PROP] {P : PROP} : <affine> P ∗ <pers> P ⊣⊢ <pers> P

theorem Iris.BI.persistently_wand_1 {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q

theorem Iris.BI.persistently_entails_l {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ <pers> Q) : P ⊢ <pers> Q ∗ P

theorem Iris.BI.persistently_entails_r {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ <pers> Q) : P ⊢ P ∗ <pers> Q

theorem Iris.BI.persistently_imp_wand_2 {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> (P -∗ Q) ⊢ <pers> (P → Q)

theorem Iris.BI.imp_wand_persistently_2 {PROP : Type u_1} [BI PROP] {P Q : PROP} : (<pers> P -∗ Q) ⊢ <pers> P → Q

theorem Iris.BI.persistently_emp' {PROP : Type u_1} [BI PROP] [BIAffine PROP] : <pers> emp ⊣⊢ emp

theorem Iris.BI.persistently_and_iff_sep {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P Q : PROP} : <pers> P ∧ Q ⊣⊢ <pers> P ∗ Q

theorem Iris.BI.and_persistently_iff_sep {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P Q : PROP} : P ∧ <pers> Q ⊣⊢ P ∗ <pers> Q

theorem Iris.BI.persistently_imp_wand {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P Q : PROP} : <pers> (P → Q) ⊣⊢ <pers> (P -∗ Q)

theorem Iris.BI.imp_wand_persistently {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P Q : PROP} : (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q)

theorem Iris.BI.wand_iff_exists_persistently {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P Q : PROP} : (P -∗ Q) ⊣⊢ «exists» fun (R : PROP) => iprop(R ∗ <pers> (P ∗ R → Q))

theorem Iris.BI.persistently_and_emp {PROP : Type u_1} {P : PROP} [BI PROP] : <pers> P ⊣⊢ <pers> (emp ∧ P)

theorem Iris.BI.persistently_and_sep_elim_emp {PROP : Type u_1} {P Q : PROP} [BI PROP] : <pers> P ∧ Q ⊢ (emp ∧ P) ∗ Q

theorem Iris.BI.persistently_and_emp_elim {PROP : Type u_1} {P : PROP} [BI PROP] : emp ∧ <pers> P ⊢ P

Persistence instances

instance Iris.BI.pure_persistent {PROP : Type u_1} (φ : Prop) [BI PROP] : Persistent iprop(⌜φ⌝)

instance Iris.BI.emp_persistent {PROP : Type u_1} [BI PROP] : Persistent iprop(emp)

instance Iris.BI.and_persistent {PROP : Type u_1} [BI PROP] (P Q : PROP) [Persistent P] [Persistent Q] : Persistent iprop(P ∧ Q)

instance Iris.BI.or_persistent {PROP : Type u_1} [BI PROP] (P Q : PROP) [Persistent P] [Persistent Q] : Persistent iprop(P ∨ Q)

theorem Iris.BI.sForall_persistent {PROP : Type u_1} [BI PROP] [h : BIPersistentlyForall PROP] (Ψ : PROP → Prop) (H : ∀ (p : PROP), Ψ p → Persistent p) : Persistent (sForall Ψ)

instance Iris.BI.forall_persistent {PROP : Type u_1} {α : Sort u_2} [BI PROP] [BIPersistentlyForall PROP] (Ψ : α → PROP) [h : ∀ (x : α), Persistent (Ψ x)] : Persistent («forall» fun (x : α) => Ψ x)

theorem Iris.BI.sExists_persistent {PROP : Type u_1} [BI PROP] (Ψ : PROP → Prop) (H : ∀ (p : PROP), Ψ p → Persistent p) : Persistent (sExists Ψ)

instance Iris.BI.exists_persistent {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Ψ : α → PROP) [h : ∀ (x : α), Persistent (Ψ x)] : Persistent («exists» fun (x : α) => Ψ x)

instance Iris.BI.sep_persistent {PROP : Type u_1} [BI PROP] (P Q : PROP) [Persistent P] [Persistent Q] : Persistent iprop(P ∗ Q)

instance Iris.BI.affinely_persistent {PROP : Type u_1} [BI PROP] (P : PROP) [Persistent P] : Persistent iprop(<affine> P)

instance Iris.BI.absorbingly_persistent {PROP : Type u_1} [BI PROP] (P : PROP) [Persistent P] : Persistent iprop(<absorb> P)

The intuitionistic modality

theorem Iris.BI.intuitionistically_ne {PROP : Type u_1} [BI PROP] : OFE.NonExpansive intuitionistically

theorem Iris.BI.intuitionistically_congr {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : □ P ⊣⊢ □ Q

theorem Iris.BI.intuitionistically_mono {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : □ P ⊢ □ Q

instance Iris.BI.intuitionistically_affine {PROP : Type u_1} [BI PROP] (P : PROP) : Affine iprop(□ P)

instance Iris.BI.intuitionistically_persistent {PROP : Type u_1} [BI PROP] (P : PROP) : Persistent iprop(□ P)

theorem Iris.BI.intuitionistically_def {PROP : Type u_1} [BI PROP] {P : PROP} : iprop(□ P) = iprop(<affine> <pers> P)

theorem Iris.BI.intuitionistically_elim_emp {PROP : Type u_1} [BI PROP] {P : PROP} : □ P ⊢ emp

theorem Iris.BI.intuitionistically_emp {PROP : Type u_1} [BI PROP] : □ emp ⊣⊢ emp

theorem Iris.BI.intuitionistically_false {PROP : Type u_1} [BI PROP] : □ False ⊣⊢ False

theorem Iris.BI.intuitionistically_true {PROP : Type u_1} [BI PROP] : □ True ⊣⊢ emp

theorem Iris.BI.intuitionistically_and {PROP : Type u_1} [BI PROP] {P Q : PROP} : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q

theorem Iris.BI.intuitionistically_forall_1 {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : (□ «forall» fun (x : α) => Φ x) ⊢ «forall» fun (x : α) => iprop(□ Φ x)

theorem Iris.BI.intuitionistically_or {PROP : Type u_1} [BI PROP] {P Q : PROP} : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q

theorem Iris.BI.intuitionistically_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : (□ «exists» fun (x : α) => Φ x) ⊣⊢ «exists» fun (x : α) => iprop(□ Φ x)

theorem Iris.BI.intuitionistically_sep_2 {PROP : Type u_1} [BI PROP] {P Q : PROP} : □ P ∗ □ Q ⊢ □ (P ∗ Q)

theorem Iris.BI.intuitionistically_sep {PROP : Type u_1} [BI PROP] [BIPositive PROP] {P Q : PROP} : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q

theorem Iris.BI.intuitionistically_idem {PROP : Type u_1} [BI PROP] {P : PROP} : □ □ P ⊣⊢ □ P

theorem Iris.BI.intuitionistically_intro' {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : □ P ⊢ Q) : □ P ⊢ □ Q

theorem Iris.BI.persistently_of_intuitionistically {PROP : Type u_1} [BI PROP] {P : PROP} : □ P ⊢ <pers> P

theorem Iris.BI.intuitionistically_persistently {PROP : Type u_1} [BI PROP] {P : PROP} : □ <pers> P ⊣⊢ □ P

theorem Iris.BI.intuitionistically_of_intuitionistic {PROP : Type u_1} [BI PROP] {P : PROP} [Affine P] [Persistent P] : □ P ⊣⊢ P

theorem Iris.BI.affinely_of_intuitionistically {PROP : Type u_1} [BI PROP] {P : PROP} : □ P ⊢ <affine> P

theorem Iris.BI.intuitionistically_affinely {PROP : Type u_1} [BI PROP] {P : PROP} : □ <affine> P ⊣⊢ □ P

theorem Iris.BI.persistently_and_intuitionistically_sep_l {PROP : Type u_1} [BI PROP] {P Q : PROP} : <pers> P ∧ Q ⊣⊢ □ P ∗ Q

theorem Iris.BI.persistently_and_intuitionistically_sep_r {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∧ <pers> Q ⊣⊢ P ∗ □ Q

theorem Iris.BI.and_sep_intuitionistically {PROP : Type u_1} [BI PROP] {P Q : PROP} : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q

theorem Iris.BI.intuitionistically_and_sep {PROP : Type u_1} [BI PROP] {P Q : PROP} : □ (P ∧ Q) ⊣⊢ □ P ∗ □ Q

theorem Iris.BI.intuitionistically_sep_idem {PROP : Type u_1} [BI PROP] {P : PROP} : □ P ∗ □ P ⊣⊢ □ P

theorem Iris.BI.intuitionistically_wand {PROP : Type u_1} [BI PROP] {P Q : PROP} : (□ P -∗ Q) ⊣⊢ (<pers> P → Q)

theorem Iris.BI.affinely_self_sep_intuitionistically {PROP : Type u_1} [BI PROP] {P : PROP} : <affine> (P ∗ □ P) ⊣⊢ □ P

theorem Iris.BI.intuitionistically_imp_wand_2 {PROP : Type u_1} [BI PROP] {P Q : PROP} : □ (P -∗ Q) ⊢ □ (P → Q)

theorem Iris.BI.imp_iff_exists_persistently {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P Q : PROP} : (P → Q) ⊣⊢ «exists» fun (R : PROP) => iprop(R ∧ <pers> (P ∧ R -∗ Q))

theorem Iris.BI.intuitionistically_iff_persistently {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P : PROP} : □ P ⊣⊢ <pers> P

Conditional affinely modality

@[simp]

theorem Iris.BI.affinelyIf_false {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(<affine>?false P) = P

@[simp]

theorem Iris.BI.affinelyIf_true {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(<affine>?true P) = iprop(<affine> P)

theorem Iris.BI.affinelyIf_ne {PROP : Type u_1} {p : Bool} [BI PROP] : OFE.NonExpansive (affinelyIf p)

theorem Iris.BI.affinelyIf_mono {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : <affine>?p P ⊢ <affine>?p Q

theorem Iris.BI.affinelyIf_congr {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : <affine>?p P ⊣⊢ <affine>?p Q

instance Iris.BI.affinelyIf_affine {PROP : Type u_1} (p : Bool) [BI PROP] (P : PROP) [Affine P] : Affine iprop(<affine>?p P)

instance Iris.BI.affinelyIf_persistent {PROP : Type u_1} (p : Bool) [BI PROP] (P : PROP) [Persistent P] : Persistent iprop(<affine>?p P)

theorem Iris.BI.affinelyIf_flag_mono {PROP : Type u_1} {p q : Bool} [BI PROP] {P : PROP} (h : q = true → p = true) : <affine>?p P ⊢ <affine>?q P

theorem Iris.BI.affinelyIf_elim {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : <affine>?p P ⊢ P

theorem Iris.BI.affinely_affinelyIf {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : <affine> P ⊢ <affine>?p P

theorem Iris.BI.affinelyIf_intro' {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : (P ⊢ <affine>?p Q) → <affine>?p P ⊢ <affine>?p Q

theorem Iris.BI.affinelyIf_emp {PROP : Type u_1} {p : Bool} [BI PROP] : <affine>?p emp ⊣⊢ emp

theorem Iris.BI.affinelyIf_and {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <affine>?p (P ∧ Q) ⊣⊢ <affine>?p P ∧ <affine>?p Q

theorem Iris.BI.affinelyIf_or {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <affine>?p (P ∨ Q) ⊣⊢ <affine>?p P ∨ <affine>?p Q

theorem Iris.BI.affinelyIf_exists {PROP : Type u_1} {α : Sort u_2} {p : Bool} [BI PROP] {Ψ : α → PROP} : (<affine>?p «exists» fun (a : α) => Ψ a) ⊣⊢ «exists» fun (a : α) => iprop(<affine>?p Ψ a)

theorem Iris.BI.affinelyIf_forall_1 {PROP : Type u_1} {α : Sort u_2} {p : Bool} [BI PROP] {Ψ : α → PROP} : (<affine>?p «forall» fun (a : α) => Ψ a) ⊢ «forall» fun (a : α) => iprop(<affine>?p Ψ a)

theorem Iris.BI.affinelyIf_sep_2 {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <affine>?p P ∗ <affine>?p Q ⊢ <affine>?p (P ∗ Q)

theorem Iris.BI.affinelyIf_sep {PROP : Type u_1} {p : Bool} [BI PROP] [BIPositive PROP] {P Q : PROP} : <affine>?p (P ∗ Q) ⊣⊢ <affine>?p P ∗ <affine>?p Q

theorem Iris.BI.affinelyIf_idem {PROP : Type u_1} {p : Bool} [BI PROP] [BIPositive PROP] {P : PROP} : <affine>?p <affine>?p P ⊣⊢ <affine>?p P

theorem Iris.BI.affinelyIf_and_l {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <affine>?p P ∧ Q ⊣⊢ <affine>?p (P ∧ Q)

theorem Iris.BI.affinelyIf_and_r {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : P ∧ <affine>?p Q ⊣⊢ <affine>?p (P ∧ Q)

theorem Iris.BI.affinelyIf_and_lr {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <affine>?p P ∧ Q ⊣⊢ P ∧ <affine>?p Q

Conditional absorbingly modality

@[simp]

theorem Iris.BI.absorbinglyIf_false {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(<absorb>?false P) = P

@[simp]

theorem Iris.BI.absorbinglyIf_true {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(<absorb>?true P) = iprop(<absorb> P)

theorem Iris.BI.absorbinglyIf_ne {PROP : Type u_1} {p : Bool} [BI PROP] : OFE.NonExpansive (absorbinglyIf p)

theorem Iris.BI.absorbinglyIf_mono {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : <absorb>?p P ⊢ <absorb>?p Q

theorem Iris.BI.absorbinglyIf_congr {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : <absorb>?p P ⊣⊢ <absorb>?p Q

instance Iris.BI.absorbinglyIf_persistent {PROP : Type u_1} (p : Bool) [BI PROP] (P : PROP) [Persistent P] : Persistent iprop(<absorb>?p P)

theorem Iris.BI.absorbingly_of_absorbinglyIf {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : <absorb>?p P ⊢ <absorb> P

theorem Iris.BI.absorbinglyIf_intro {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : P ⊢ <absorb>?p P

theorem Iris.BI.absorbinglyIf_flag_mono {PROP : Type u_1} {p q : Bool} [BI PROP] {P : PROP} (h : p = true → q = true) : <absorb>?p P ⊢ <absorb>?q P

theorem Iris.BI.absorbinglyIf_idem {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : <absorb>?p <absorb>?p P ⊣⊢ <absorb>?p P

theorem Iris.BI.absorbinglyIf_pure {PROP : Type u_1} {p : Bool} [BI PROP] {φ : Prop} : <absorb>?p ⌜φ⌝ ⊣⊢ ⌜φ⌝

theorem Iris.BI.absorbinglyIf_or {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <absorb>?p (P ∨ Q) ⊣⊢ <absorb>?p P ∨ <absorb>?p Q

theorem Iris.BI.absorbinglyIf_and_1 {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <absorb>?p (P ∧ Q) ⊢ <absorb>?p P ∧ <absorb>?p Q

theorem Iris.BI.absorbinglyIf_forall_1 {PROP : Type u_1} {α : Sort u_2} {p : Bool} [BI PROP] {Φ : α → PROP} : (<absorb>?p «forall» fun (a : α) => Φ a) ⊢ «forall» fun (a : α) => iprop(<absorb>?p Φ a)

theorem Iris.BI.absorbinglyIf_exists {PROP : Type u_1} {α : Sort u_2} {p : Bool} [BI PROP] {Φ : α → PROP} : (<absorb>?p «exists» fun (a : α) => Φ a) ⊣⊢ «exists» fun (a : α) => iprop(<absorb>?p Φ a)

theorem Iris.BI.absorbinglyIf_sep {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <absorb>?p (P ∗ Q) ⊣⊢ <absorb>?p P ∗ <absorb>?p Q

theorem Iris.BI.absorbinglyIf_wand_1 {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <absorb>?p (P -∗ Q) ⊢ <absorb>?p P -∗ <absorb>?p Q

theorem Iris.BI.absorbinglyIf_sep_l {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <absorb>?p P ∗ Q ⊣⊢ <absorb>?p (P ∗ Q)

theorem Iris.BI.absorbinglyIf_sep_r {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : P ∗ <absorb>?p Q ⊣⊢ <absorb>?p (P ∗ Q)

theorem Iris.BI.absorbinglyIf_sep_lr {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <absorb>?p P ∗ Q ⊣⊢ P ∗ <absorb>?p Q

theorem Iris.BI.affinelyIf_absorbinglyIf {PROP : Type u_1} {p : Bool} [BI PROP] [BIPositive PROP] {P : PROP} : <affine>?p <absorb>?p P ⊣⊢ <affine>?p P

Conditional persistently

@[simp]

theorem Iris.BI.persistentlyIf_false {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(<pers>?false P) = P

@[simp]

theorem Iris.BI.persistentlyIf_true {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(<pers>?true P) = iprop(<pers> P)

theorem Iris.BI.persistentlyIf_ne {PROP : Type u_1} {p : Bool} [BI PROP] : OFE.NonExpansive (persistentlyIf p)

theorem Iris.BI.persistentlyIf_mono {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : <pers>?p P ⊢ <pers>?p Q

theorem Iris.BI.persistentlyIf_congr {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : <pers>?p P ⊣⊢ <pers>?p Q

instance Iris.BI.persistentlyIf_absorbing {PROP : Type u_1} [BI PROP] (P : PROP) (p : Bool) [Absorbing P] : Absorbing iprop(<pers>?p P)

theorem Iris.BI.persistentlyIf_pure {PROP : Type u_1} {p : Bool} [BI PROP] {φ : Prop} : <pers>?p ⌜φ⌝ ⊣⊢ ⌜φ⌝

theorem Iris.BI.persistentlyIf_and {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <pers>?p (P ∧ Q) ⊣⊢ <pers>?p P ∧ <pers>?p Q

theorem Iris.BI.persistentlyIf_or {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <pers>?p (P ∨ Q) ⊣⊢ <pers>?p P ∨ <pers>?p Q

theorem Iris.BI.persistentlyIf_forall_1 {PROP : Type u_1} {α : Sort u_2} {p : Bool} [BI PROP] {Φ : α → PROP} : (<pers>?p «forall» fun (a : α) => Φ a) ⊢ «forall» fun (a : α) => iprop(<pers>?p Φ a)

theorem Iris.BI.persistentlyIf_exists {PROP : Type u_1} {α : Sort u_2} {p : Bool} [BI PROP] {Φ : α → PROP} : (<pers>?p «exists» fun (a : α) => Φ a) ⊣⊢ «exists» fun (a : α) => iprop(<pers>?p Φ a)

theorem Iris.BI.persistentlyIf_sep_2 {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : <pers>?p P ∗ <pers>?p Q ⊢ <pers>?p (P ∗ Q)

theorem Iris.BI.persistentlyIf_sep {PROP : Type u_1} {p : Bool} [BI PROP] [BIPositive PROP] {P Q : PROP} : <pers>?p (P ∗ Q) ⊣⊢ <pers>?p P ∗ <pers>?p Q

theorem Iris.BI.persistentlyIf_idem {PROP : Type u_1} {p : Bool} [BI PROP] [BIPositive PROP] {P : PROP} : <pers>?p <pers>?p P ⊣⊢ <pers>?p P

theorem Iris.BI.persistentlyIf_persistently {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : <pers>?p <pers> P ⊣⊢ <pers> P

theorem Iris.BI.persistentlyIf_intutitionistically {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : <pers>?p □ P ⊢ <pers> P

Conditional intuitionistically

@[simp]

theorem Iris.BI.intuitionisticallyIf_false' {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(□?false P) = P

@[simp]

theorem Iris.BI.intuitionisticallyIf_true {PROP : Type u_1} [BI PROP] (P : PROP) : iprop(□?true P) = iprop(□ P)

theorem Iris.BI.intuitionisticallyIf_ne {PROP : Type u_1} {p : Bool} [BI PROP] : OFE.NonExpansive (intuitionisticallyIf p)

theorem Iris.BI.intuitionisticallyIf_mono {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : □?p P ⊢ □?p Q

theorem Iris.BI.intuitionisticallyIf_congr {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : □?p P ⊣⊢ □?p Q

instance Iris.BI.intuitionisticallyIf_affine {PROP : Type u_1} (p : Bool) [BI PROP] (P : PROP) [Affine P] : Affine iprop(□?p P)

theorem Iris.BI.intuitionisticallyIf_flag_mono {PROP : Type u_1} {p q : Bool} [BI PROP] {P : PROP} (h : q = true → p = true) : □?p P ⊢ □?q P

theorem Iris.BI.intuitionisticallyIf_elim {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : □?p P ⊢ P

theorem Iris.BI.intuitionisticallyIf_of_intuitionistically {PROP : Type u_1} (p : Bool) [BI PROP] {P : PROP} : □ P ⊢ □?p P

theorem Iris.BI.intuitionisticallyIf_intro' {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : (□?p P ⊢ Q) → □?p P ⊢ □?p Q

theorem Iris.BI.intuitionisticallyIf_emp {PROP : Type u_1} {p : Bool} [BI PROP] : □?p emp ⊣⊢ emp

theorem Iris.BI.intuitionisticallyIf_false {PROP : Type u_1} {p : Bool} [BI PROP] : □?p False ⊣⊢ False

theorem Iris.BI.intuitionisticallyIf_and {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q

theorem Iris.BI.intuitionisticallyIf_or {PROP : Type u_1} (p : Bool) [BI PROP] {P Q : PROP} : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q

theorem Iris.BI.intuitionisticallyIf_exists {PROP : Type u_1} {α : Sort u_2} {p : Bool} [BI PROP] {Ψ : α → PROP} : (□?p «exists» fun (a : α) => Ψ a) ⊣⊢ «exists» fun (a : α) => iprop(□?p Ψ a)

theorem Iris.BI.intuitionisticallyIf_sep_2 {PROP : Type u_1} {p : Bool} [BI PROP] {P Q : PROP} : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q)

theorem Iris.BI.intuitionisticallyIf_sep {PROP : Type u_1} {p : Bool} [BI PROP] [BIPositive PROP] {P Q : PROP} : □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q

theorem Iris.BI.intuitionisticallyIf_idem {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : □?p □?p P ⊣⊢ □?p P

theorem Iris.BI.intuitionisticallyIf_def' {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : iprop(□?p P) = iprop(<affine>?p <pers>?p P)

theorem Iris.BI.intuitionisticallyIf_comm {PROP : Type u_1} {p q : Bool} [BI PROP] {P : PROP} : iprop(□?p □?q P) = iprop(□?q □?p P)

theorem Iris.BI.intuitionisticallyIf_comm' {PROP : Type u_1} {p q : Bool} [BI PROP] {P : PROP} : □?p □?q P ⊣⊢ □?q □?p P

theorem Iris.BI.intuitionisticallyIf_affinely {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : □?p <affine> P ⊣⊢ <affine> □?p P

theorem Iris.BI.intuitionisticallyIf_intutitionistically {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : □?p □ P ⊣⊢ □ P

theorem Iris.BI.affinelyIf_of_intuitionisticallyIf {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : □?p P ⊢ <affine>?p P

Properties of persistent propositions

theorem Iris.BI.persistent_congr {PROP : Type u_1} [BI PROP] {P Q : PROP} (H : P ⊣⊢ Q) : Persistent P ↔ Persistent Q

theorem Iris.BI.persistently_intro {PROP : Type u_1} [BI PROP] {P : PROP} [Persistent P] : P ⊢ <pers> P

theorem Iris.BI.persistently_iff {PROP : Type u_1} [BI PROP] {P : PROP} [Persistent P] [Absorbing P] : <pers> P ⊣⊢ P

theorem Iris.BI.persistently_intro'' {PROP : Type u_1} {Q : PROP} [BI PROP] {P : PROP} [Persistent P] (h : P ⊢ Q) : P ⊢ <pers> Q

theorem Iris.BI.persistent_and_affinely_sep_l_1 {PROP : Type u_1} [BI PROP] {P Q : PROP} [Persistent P] : P ∧ Q ⊢ <affine> P ∗ Q

theorem Iris.BI.persistent_and_affinely_sep_r_1 {PROP : Type u_1} [BI PROP] {P Q : PROP} [Persistent Q] : P ∧ Q ⊢ P ∗ <affine> Q

theorem Iris.BI.persistent_and_affinely_sep_l {PROP : Type u_1} [BI PROP] {P Q : PROP} [Persistent P] [Absorbing P] : P ∧ Q ⊣⊢ <affine> P ∗ Q

theorem Iris.BI.persistent_and_affinely_sep_r {PROP : Type u_1} [BI PROP] {P Q : PROP} [Persistent Q] [Absorbing Q] : P ∧ Q ⊣⊢ P ∗ <affine> Q

theorem Iris.BI.persistent_and_sep_1 {PROP : Type u_1} [BI PROP] {P Q : PROP} [Std.TCOr (Persistent P) (Persistent Q)] : P ∧ Q ⊢ P ∗ Q

theorem Iris.BI.absorbingly_intuitionistically {PROP : Type u_1} [BI PROP] {P : PROP} : <absorb> □ P ⊣⊢ <pers> P

theorem Iris.BI.absorbingly_affinely_intro_of_persistent {PROP : Type u_1} [BI PROP] {P : PROP} [Persistent P] : P ⊢ <absorb> <affine> P

instance Iris.BI.imp_absorbing {PROP : Type u_1} [BI PROP] (P Q : PROP) [Persistent P] [Absorbing P] [Absorbing Q] : Absorbing iprop(P → Q)

theorem Iris.BI.bigOp_sep_nil {PROP : Type u_1} [BI PROP] : [∗] [] ⊣⊢ emp

theorem Iris.BI.bigOp_and_nil {PROP : Type u_1} [BI PROP] : [∧] [] ⊣⊢ True

theorem Iris.BI.bigOp_sep_cons {PROP : Type u_1} [BI PROP] {P : PROP} {Ps : List PROP} : [∗] (P :: Ps) ⊣⊢ P ∗ [∗] Ps

theorem Iris.BI.bigOp_and_cons {PROP : Type u_1} [BI PROP] {P : PROP} {Ps : List PROP} : [∧] (P :: Ps) ⊣⊢ P ∧ [∧] Ps

Reduction to boolean comparisons

theorem Iris.BI.and_forall_bool {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∧ Q ⊣⊢ «forall» fun (b : Bool) => if b = true then P else Q

theorem Iris.BI.or_exists_bool {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∨ Q ⊣⊢ «exists» fun (b : Bool) => if b = true then P else Q

Later

theorem Iris.BI.later_congr {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : later P ⊣⊢ later Q

theorem Iris.BI.later_true {PROP : Type u_1} [BI PROP] : later iprop(True) ⊣⊢ True

theorem Iris.BI.later_emp {PROP : Type u_1} [BI PROP] [BIAffine PROP] : later iprop(emp) ⊣⊢ emp

theorem Iris.BI.later_forall_2 {PROP : Type u_1} [BI PROP] {α : Sort u_2} {Φ : α → PROP} : («forall» fun (a : α) => later (Φ a)) ⊢ later («forall» fun (a : α) => Φ a)

theorem Iris.BI.later_forall {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : later («forall» fun (a : α) => Φ a) ⊣⊢ «forall» fun (a : α) => later (Φ a)

theorem Iris.BI.later_exists_2 {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : («exists» fun (a : α) => later (Φ a)) ⊢ later («exists» fun (a : α) => Φ a)

theorem Iris.BI.later_exists_false {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} : later («exists» fun (a : α) => Φ a) ⊢ later iprop(False) ∨ «exists» fun (a : α) => later (Φ a)

theorem Iris.BI.later_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] [Inhabited α] {Φ : α → PROP} : («exists» fun (a : α) => later (Φ a)) ⊣⊢ later («exists» fun (a : α) => Φ a)

theorem Iris.BI.later_and {PROP : Type u_1} [BI PROP] {P Q : PROP} : later iprop(P ∧ Q) ⊣⊢ later P ∧ later Q

theorem Iris.BI.later_or {PROP : Type u_1} [BI PROP] {P Q : PROP} : later iprop(P ∨ Q) ⊣⊢ later P ∨ later Q

theorem Iris.BI.later_impl {PROP : Type u_1} [BI PROP] {P Q : PROP} : later iprop(P → Q) ⊢ later P → later Q

theorem Iris.BI.later_wand {PROP : Type u_1} [BI PROP] {P Q : PROP} : later iprop(P -∗ Q) ⊢ later P -∗ later Q

theorem Iris.BI.later_iff {PROP : Type u_1} [BI PROP] {P Q : PROP} : later iprop(P ↔ Q) ⊢ (later P ↔ later Q)

theorem Iris.BI.later_wand_iff {PROP : Type u_1} [BI PROP] {P Q : PROP} : later iprop(P ∗-∗ Q) ⊢ later P ∗-∗ later Q

theorem Iris.BI.later_affinely_2 {PROP : Type u_1} [BI PROP] {P : PROP} : <affine> later P ⊢ later iprop(<affine> P)

theorem Iris.BI.later_intuitionistically_2 {PROP : Type u_1} [BI PROP] {P : PROP} : □ later P ⊢ later iprop(□ P)

theorem Iris.BI.later_intuitionisticallyIf_2 {PROP : Type u_1} {p : Bool} [BI PROP] {P : PROP} : □?p later P ⊢ later iprop(□?p P)

theorem Iris.BI.later_absorbingly {PROP : Type u_1} [BI PROP] {P : PROP} : later iprop(<absorb> P) ⊣⊢ <absorb> later P

theorem Iris.BI.later_affinely {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P : PROP} : <affine> later P ⊣⊢ later iprop(<affine> P)

theorem Iris.BI.later_intuitionistically {PROP : Type u_1} [BI PROP] [BIAffine PROP] {P : PROP} : □ later P ⊣⊢ later iprop(□ P)

theorem Iris.BI.later_intuitionisticallyIf {PROP : Type u_1} {p : Bool} [BI PROP] [BIAffine PROP] {P : PROP} : □?p later P ⊣⊢ later iprop(□?p P)

instance Iris.BI.later_persistent {PROP : Type u_1} [BI PROP] {P : PROP} [Persistent P] : Persistent (later P)

instance Iris.BI.later_absorbing {PROP : Type u_1} [BI PROP] {P : PROP} [Absorbing P] : Absorbing (later P)

theorem Iris.BI.entails_impl_true {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ⊢ Q ↔ True ⊢ P → Q

theorem Iris.BI.loeb {PROP : Type u_1} [BI PROP] [BILoeb PROP] {P : PROP} : (later P → P) ⊢ P

theorem Iris.BI.loeb_weak_of_strong {PROP : Type u_1} [BI PROP] {P : PROP} (H : ∀ (P : PROP), (later P → P) ⊢ P) (H' : later P ⊢ P) : True ⊢ P

theorem Iris.BI.loeb_wand_intuitionistically {PROP : Type u_1} [BI PROP] [BILoeb PROP] {P : PROP} : □ (□ later P -∗ P) ⊢ P

theorem Iris.BI.loeb_wand {PROP : Type u_1} [BI PROP] [BILoeb PROP] {P : PROP} : □ (later P -∗ P) ⊢ P