class Iris.Plainly (PROP : Type u_1) : Type u_1

• plainly : PROP → PROP

def Iris.«term■_» : Lean.ParserDescr

Equations

• Iris.«term■_» = Lean.ParserDescr.node `Iris.«term■_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "■ ") (Lean.ParserDescr.cat `term 40))

def Iris.Plainly.plainlyIf {PROP : Type u_1} [BI.BIBase PROP] [Plainly PROP] (p : Bool) (P : PROP) : PROP

Equations

• iprop(■?p P) = if p = true then iprop(■ P) else P

def Iris.«term■?___» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

class Iris.BIPlainly (PROP : Type u_1) [BI PROP] extends Iris.Plainly PROP : Type u_1

• plainly : PROP → PROP
• ne : OFE.NonExpansive plainly
• mono {P Q : PROP} : (P ⊢ Q) → ■ P ⊢ ■ Q
• elim_persistently {P : PROP} : ■ P ⊢ <pers> P
• idem {P : PROP} : ■ P ⊢ ■ ■ P
• plainly_sForall_2 {Φ : PROP → Prop} : (BI.forall fun (p : PROP) => iprop(⌜Φ p⌝ → ■ p)) ⊢ ■ BI.sForall Φ
• plainly_impl_plainly {P Q : PROP} : (■ P → ■ Q) ⊢ ■ (■ P → Q)
• emp_intro {P : PROP} : P ⊢ ■ emp
• plainly_absorb {P Q : PROP} : ■ P ∗ Q ⊢ ■ P
• later_plainly {P : PROP} : BI.later iprop(■ P) ⊣⊢ ■ BI.later P

class Iris.BIPersistentlyImplPlainly (PROP : Type u_1) [BI PROP] [BIPlainly PROP] : Prop

• pers_impl_plainly (P Q : PROP) : (■ P → <pers> Q) ⊢ <pers> (■ P → Q)

class Iris.BIPlainlyExists (PROP : Type u_1) [BI PROP] [BIPlainly PROP] : Prop

• plainly_sExists_1 {Φ : PROP → Prop} : ■ BI.sExists Φ ⊢ BI.exists fun (p : PROP) => iprop(⌜Φ p⌝ ∧ ■ p)

class Iris.BI.Plain {PROP : Type u_1} [BI PROP] [Plainly PROP] [BIPlainly PROP] (P : PROP) : Prop

• plain : P ⊢ ■ P

instance Iris.BI.instPlainPlainly {PROP : Type u_1} [BI PROP] [BIPlainly PROP] (P : PROP) : Plain iprop(■ P)

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

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

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

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

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

theorem Iris.BI.plainly_and_sep_elim {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ P ∧ Q ⊢ (emp ∧ P) ∗ Q

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

theorem Iris.BI.plainly_and_emp_elim {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P : PROP} : emp ∧ ■ P ⊢ P

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

theorem Iris.BI.plainly_elim {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P : PROP} [Absorbing P] : ■ P ⊢ P

theorem Iris.BI.plainly_idemp {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P : PROP} : ■ ■ P ⊣⊢ ■ P

theorem Iris.BI.plainly_intro' {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} (H : ■ P ⊢ Q) : ■ P ⊢ ■ Q

theorem Iris.BI.plainly_pure {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {φ : Prop} : ■ ⌜φ⌝ ⊣⊢ ⌜φ⌝

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

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

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

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

theorem Iris.BI.plainly_and {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ (P ∧ Q) ⊣⊢ ■ P ∧ ■ Q

theorem Iris.BI.plainly_or_2 {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ P ∨ ■ Q ⊢ ■ (P ∨ Q)

theorem Iris.BI.plainly_or {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} [BIPlainlyExists PROP] : ■ (P ∨ Q) ⊣⊢ ■ P ∨ ■ Q

theorem Iris.BI.plainly_impl {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ (P → Q) ⊢ ■ P → ■ Q

theorem Iris.BI.plainly_emp_2 {PROP : Type u_1} [BI PROP] [BIPlainly PROP] : ⊢ ■ emp

theorem Iris.BI.plainly_sep_dup {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P : PROP} : ■ P ⊣⊢ ■ P ∗ ■ P

theorem Iris.BI.plainly_and_sep_l_1 {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ P ∧ Q ⊢ ■ P ∗ Q

theorem Iris.BI.plainly_and_sep_r_1 {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : P ∧ ■ Q ⊢ P ∗ ■ Q

theorem Iris.BI.plainly_true_emp {PROP : Type u_1} [BI PROP] [BIPlainly PROP] : ■ True ⊣⊢ ■ emp

theorem Iris.BI.plainly_and_sep {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ (P ∧ Q) ⊢ ■ (P ∗ Q)

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

theorem Iris.BI.intuitionistically_plainly_elim {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P : PROP} : □ ■ P ⊢ □ P

theorem Iris.BI.intuitionistically_plainly {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P : PROP} : □ ■ P ⊢ ■ □ P

theorem Iris.BI.and_sep_plainly {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q

theorem Iris.BI.plainly_sep_2 {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : ■ P ∗ ■ Q ⊢ ■ (P ∗ Q)

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

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

theorem Iris.BI.plainly_entails_l {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} (H : P ⊢ ■ Q) : P ⊢ ■ Q ∗ P

theorem Iris.BI.plainly_entails_r {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} (H : P ⊢ ■ Q) : P ⊢ P ∗ ■ Q

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

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

theorem Iris.BI.impl_wand_affinely_plainly {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q)

theorem Iris.BI.persistently_wand_affinely_plainly {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} [BIPersistentlyImplPlainly PROP] : (<affine> ■ P -∗ <pers> Q) ⊢ <pers> (<affine> ■ P -∗ Q)

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

theorem Iris.BI.plainly_emp {PROP : Type u_1} [BI PROP] [BIPlainly PROP] [BIAffine PROP] : ■ emp ⊣⊢ emp

theorem Iris.BI.plainly_and_sep_l {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} [BIAffine PROP] : ■ P ∧ Q ⊣⊢ ■ P ∗ Q

theorem Iris.BI.plainly_and_sep_r {PROP : Type u_1} [BI PROP] [BIPlainly PROP] {P Q : PROP} [BIAffine PROP] : P ∧ ■ Q ⊣⊢ P ∗ ■ Q

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

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