def Iris.Set (α : Type u_1) : Type u_1

Equations

• Iris.Set α = (α → Prop)

def Iris.Set.univ {α : Type u_1} : Set α

Equations

• Iris.Set.univ x✝ = True

def Iris.Subset {α : Type u_1} (x y : Set α) : Prop

Equations

• Iris.Subset x y = ∀ (a : α), x a → y a

def Iris.Disjoint {α : Type u_1} (x y : Set α) : Prop

Equations

• Iris.Disjoint x y = ∀ (a : α), ¬(x a ∧ y a)

def Iris.union {α : Type u_1} (x y : Set α) : Set α

Equations

• Iris.union x y a = (x a ∨ y a)

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

• bupd : 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.«term_==∗_» : Lean.TrailingParserDescr

Equations

• Iris.«term_==∗_» = Lean.ParserDescr.trailingNode `Iris.«term_==∗_» 1022 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ==∗ ") (Lean.ParserDescr.cat `term 25))

class Iris.FUpd (PROP : Type u_1) (MASK : Type u_2) : Type (max u_1 u_2)

• fupd : Set MASK → Set MASK → PROP → PROP

def Iris.«term|={_,_}=>_» : Lean.ParserDescr

Equations

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

def Iris.«term_={_,_}=∗_» : Lean.TrailingParserDescr

Equations

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

def Iris.«term|={_}=>_» : Lean.ParserDescr

Equations

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

def Iris.«term_={_}=∗_» : Lean.TrailingParserDescr

Equations

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

def Iris.«term|={_}[_]▷=>_» : Lean.ParserDescr

Equations

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

def Iris.«term_={_}[_]▷=∗_» : Lean.TrailingParserDescr

Equations

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

def Iris.«term|={_}▷=>_» : Lean.ParserDescr

Equations

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

def Iris.«term_={_}▷=∗_» : Lean.TrailingParserDescr

Equations

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

def Iris.«term|={_}[_]▷^_=>_» : Lean.ParserDescr

Equations

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

def Iris.«term_={_}[_]▷^_=∗_» : Lean.TrailingParserDescr

Equations

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

def Iris.«term|={_}▷^_=>_» : Lean.ParserDescr

Equations

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

def Iris.«term_={_}▷^_=∗_» : Lean.TrailingParserDescr

Equations

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

class Iris.BIUpdate (PROP : Type u_1) [BI PROP] extends Iris.BUpd PROP : Type u_1

• bupd : PROP → PROP
• bupd_ne : OFE.NonExpansive bupd
• intro {P : PROP} : P ⊢ |==> P
• mono {P Q : PROP} : (P ⊢ Q) → |==> P ⊢ |==> Q
• trans {P : PROP} : |==> |==> P ⊢ |==> P
• frame_r {P R : PROP} : |==> P ∗ R ⊢ |==> (P ∗ R)

class Iris.BIFUpdate (PROP : Type u_1) (MASK : Type u_2) [BI PROP] extends Iris.FUpd PROP MASK : Type (max u_1 u_2)

• fupd : Set MASK → Set MASK → PROP → PROP
• ne {E1 E2 : Set MASK} : OFE.NonExpansive (fupd E1 E2)
• subset {E1 E2 : Set MASK} : Subset E2 E1 → ⊢ fupd E1 E2 (fupd E2 E1 iprop(emp))
• except0 {E1 E2 : Set MASK} (P : PROP) : ◇ fupd E1 E2 P ⊢ fupd E1 E2 P
• trans {E1 E2 E3 : Set MASK} (P : PROP) : fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P
• mask_frame_r' {E1 E2 Ef : Set MASK} (P : PROP) : Disjoint E1 Ef → fupd E1 E2 iprop(⌜Disjoint E2 Ef⌝ → P) ⊢ fupd (union E1 Ef) (union E2 Ef) P
• frame_r {E1 E2 : Set MASK} (P R : PROP) : fupd E1 E2 P ∗ R ⊢ fupd E1 E2 iprop(P ∗ R)

class Iris.BIUpdateFUpdate {MASK : Type u_1} (PROP : Type u_2) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP MASK] : Prop

• fupd_of_bupd {P : PROP} {E : Set MASK} : (⊢ |==> P) → ⊢ fupd E E P

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

• bupd_plainly {P : PROP} : |==> ■ P ⊢ P

class Iris.BIFUpdatePlainly (PROP : Type u_1) (MASK : Type u_2) [BI PROP] [BIFUpdate PROP MASK] [BIPlainly PROP] : Prop

• fupd_plainly_keep_l (E E' : Set MASK) (P R : PROP) : (R -∗ fupd E E' iprop(■ P)) ∗ R ⊢ fupd E E iprop(P ∗ R)
• fupd_plainly_later (E : Set MASK) (P : PROP) : BI.later (fupd E E iprop(■ P)) ⊢ fupd E E (BI.later iprop(◇ P))
• fupd_plainly_sForall_2 (E : Set MASK) (Φ : PROP → Prop) : (BI.forall fun (p : PROP) => iprop(⌜Φ p⌝ → fupd E E iprop(■ p))) ⊢ fupd E E (BI.sForall Φ)

theorem Iris.bupd_frame_l {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P Q : PROP} : P ∗ |==> Q ⊢ |==> (P ∗ Q)

theorem Iris.bupd_wand_l {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P Q : PROP} : (P -∗ Q) ∗ |==> P ⊢ |==> Q

theorem Iris.bupd_wand_r {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P Q : PROP} : |==> P ∗ (P -∗ Q) ⊢ |==> Q

theorem Iris.bupd_sep {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P Q : PROP} : |==> P ∗ |==> Q ⊢ |==> (P ∗ Q)

theorem Iris.bupd_idem {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P : PROP} : |==> |==> P ⊣⊢ |==> P

theorem Iris.bupd_or {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P Q : PROP} : |==> P ∨ |==> Q ⊢ |==> (P ∨ Q)

theorem Iris.bupd_and {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P Q : PROP} : |==> (P ∧ Q) ⊢ |==> P ∧ |==> Q

theorem Iris.bupd_exist {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {A : Type} {Φ : A → PROP} : (BI.exists fun (x : A) => iprop(|==> Φ x)) ⊢ |==> BI.exists fun (x : A) => Φ x

theorem Iris.bupd_forall {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {A : Type} {Φ : A → PROP} : (|==> BI.forall fun (x : A) => Φ x) ⊢ BI.forall fun (x : A) => iprop(|==> Φ x)

theorem Iris.bupd_except0 {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P : PROP} : ◇ |==> P ⊢ |==> ◇ P

instance Iris.instAbsorbingBupd {PROP : Type u_1} [BI PROP] [BIUpdate PROP] {P : PROP} [BI.Absorbing P] : BI.Absorbing iprop(|==> P)

theorem Iris.bupd_elim {PROP : Type u_1} [BI PROP] [BIUpdate PROP] [BIPlainly PROP] [BIBUpdatePlainly PROP] {P : PROP} [BI.Plain P] : |==> P ⊢ P

theorem Iris.bupd_plain_forall {PROP : Type u_1} [BI PROP] [BIUpdate PROP] [BIPlainly PROP] [BIBUpdatePlainly PROP] {A : Type} (Φ : A → PROP) [∀ (x : A), BI.Plain (Φ x)] : (|==> BI.forall fun (x : A) => Φ x) ⊣⊢ BI.forall fun (x : A) => iprop(|==> Φ x)

instance Iris.instPlainBupd {PROP : Type u_1} [BI PROP] [BIUpdate PROP] [BIPlainly PROP] [BIBUpdatePlainly PROP] {P : PROP} [BI.Plain P] : BI.Plain iprop(|==> P)