class Iris.BI.BIBase (PROP : Type u) : Type u

Require the definitions of the separation logic connectives and units on a carrier type PROP.

• Entails : PROP → PROP → Prop
• emp : PROP
• pure : Prop → PROP
• and : PROP → PROP → PROP
• or : PROP → PROP → PROP
• imp : PROP → PROP → PROP
• sForall : (PROP → Prop) → PROP
• sExists : (PROP → Prop) → PROP
• sep : PROP → PROP → PROP
• wand : PROP → PROP → PROP
• persistently : PROP → PROP
• later : PROP → PROP

def Iris.BI.BIBase.forall {PROP : Type u_1} [BIBase PROP] {α : Sort u_2} (P : α → PROP) : PROP

Equations

• Iris.BI.BIBase.forall P = Iris.BI.BIBase.sForall fun (p : PROP) => ∃ (a : α), P a = p

def Iris.BI.BIBase.exists {PROP : Type u_1} [BIBase PROP] {α : Sort u_2} (P : α → PROP) : PROP

Equations

• Iris.BI.BIBase.exists P = Iris.BI.BIBase.sExists fun (p : PROP) => ∃ (a : α), P a = p

def Iris.BI.BIBase.«term_⊢_» : Lean.TrailingParserDescr

Entailment on separation logic propositions.

Equations

• Iris.BI.BIBase.«term_⊢_» = Lean.ParserDescr.trailingNode `Iris.BI.BIBase.«term_⊢_» 25 29 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 25))

def Iris.BI.BIBase.«term⌜_⌝» : Lean.ParserDescr

Embedding of pure Lean proposition as separation logic proposition.

Equations

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

def Iris.BI.BIBase.«term_∗_» : Lean.TrailingParserDescr

Separating conjunction.

Equations

• Iris.BI.BIBase.«term_∗_» = Lean.ParserDescr.trailingNode `Iris.BI.BIBase.«term_∗_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗ ") (Lean.ParserDescr.cat `term 35))

def Iris.BI.BIBase.«term_-∗_» : Lean.TrailingParserDescr

Separating implication.

Equations

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

def Iris.BI.BIBase.«term<pers>_» : Lean.ParserDescr

Persistency modality. persistently is a primitive of BI.

Equations

• Iris.BI.BIBase.«term<pers>_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term<pers>_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "<pers> ") (Lean.ParserDescr.cat `term 40))

def Iris.BI.BIBase.«term▷_» : Lean.ParserDescr

Later modality. later is a primitive of BI.

Equations

• Iris.BI.BIBase.«term▷_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term▷_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "▷ ") (Lean.ParserDescr.cat `term 40))

def Iris.BI.BIBase.«term_↔_» : Lean.TrailingParserDescr

Bidirectional implication on separation logic propositions.

Equations

• Iris.BI.BIBase.«term_↔_» = Lean.ParserDescr.trailingNode `Iris.BI.BIBase.«term_↔_» 27 28 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↔ ") (Lean.ParserDescr.cat `term 28))

def Iris.BI.BIBase.«term_∗-∗_» : Lean.TrailingParserDescr

Bidrectional separating implication on separation logic propositions.

Equations

• Iris.BI.BIBase.«term_∗-∗_» = Lean.ParserDescr.trailingNode `Iris.BI.BIBase.«term_∗-∗_» 27 28 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗-∗ ") (Lean.ParserDescr.cat `term 28))

def Iris.BI.BIBase.«term∃_,_» : Lean.ParserDescr

Existential quantification on separation logic propositions.

Equations

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

def Iris.BI.BIBase.iff {PROP : Type u_1} [BIBase PROP] (P Q : PROP) : PROP

Equations

• iprop(P ↔ Q) = iprop((P → Q) ∧ (Q → P))

def Iris.BI.BIBase.wandIff {PROP : Type u_1} [BIBase PROP] (P Q : PROP) : PROP

Equations

• iprop(P ∗-∗ Q) = iprop((P -∗ Q) ∧ (Q -∗ P))

def Iris.BI.BIBase.«term<affine>_» : Lean.ParserDescr

Affine modality.

def affinely (P) := emp ∧ P

Equations

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

def Iris.BI.BIBase.«term<absorb>_» : Lean.ParserDescr

Absorbing modality, absorbingly.

def absorbingly (P) := True ∗ P

Equations

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

def Iris.BI.BIBase.affinely {PROP : Type u_1} [BIBase PROP] (P : PROP) : PROP

Equations

• iprop(<affine> P) = iprop(emp ∧ P)

def Iris.BI.BIBase.absorbingly {PROP : Type u_1} [BIBase PROP] (P : PROP) : PROP

Equations

• iprop(<absorb> P) = iprop(True ∗ P)

structure Iris.BI.BIBase.BiEntails {PROP : Type u_1} [BIBase PROP] (P Q : PROP) : Prop

• mp : P ⊢ Q
• mpr : Q ⊢ P

def Iris.BI.BIBase.«term⊢_» : Lean.ParserDescr

Entailment on separation logic propositions with an empty context.

Equations

• Iris.BI.BIBase.«term⊢_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term⊢_» 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢ ") (Lean.ParserDescr.cat `term 25))

def Iris.BI.BIBase.«term_⊣⊢_» : Lean.TrailingParserDescr

Bidirectional entailment on separation logic propositions.

Equations

• Iris.BI.BIBase.«term_⊣⊢_» = Lean.ParserDescr.trailingNode `Iris.BI.BIBase.«term_⊣⊢_» 25 29 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊣⊢ ") (Lean.ParserDescr.cat `term 29))

def Iris.BI.BIBase.«term□_» : Lean.ParserDescr

Intuitionistic modality.

def intuitionistically (P) := <affine> <pers> P

Equations

• Iris.BI.BIBase.«term□_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term□_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□ ") (Lean.ParserDescr.cat `term 40))

def Iris.BI.BIBase.intuitionistically {PROP : Type u_1} [BIBase PROP] (P : PROP) : PROP

Equations

• iprop(□ P) = iprop(<affine> <pers> P)

def Iris.BI.BIBase.«term<pers>?___» : Lean.ParserDescr

Conditional persistency modality.

def persistentlyIf (p : Bool) (P : PROP) := if p then <pers> P else P

Equations

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

def Iris.BI.BIBase.«term<affine>?___» : Lean.ParserDescr

Conditional affine modality.

def affinelyIf (p : Bool) (P : PROP) := if p then <affine> P else P

Equations

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

def Iris.BI.BIBase.«term<absorb>?___» : Lean.ParserDescr

Conditional absorbing modality.

def absorbinglyIf (p : Bool) (P : PROP) := if p then <absorb> P else P

Equations

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

def Iris.BI.BIBase.«term□?___» : Lean.ParserDescr

Conditional intuitionistic modality.

def intuitionisticallyIf (p : Bool) (P : PROP) := if p then □ P else P

Equations

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

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

Equations

• iprop(<pers>?p P) = if p = true then iprop(<pers> P) else P

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

Equations

• iprop(<affine>?p P) = if p = true then iprop(<affine> P) else P

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

Equations

• iprop(<absorb>?p P) = if p = true then iprop(<absorb> P) else P

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

Equations

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

def Iris.BI.BIBase.bigAnd {PROP : Type u_1} [BIBase PROP] (Ps : List PROP) : PROP

Fold the conjunction ∧ over a list of separation logic propositions.

Equations

• ([∧] Ps) = Iris.Std.bigOp Iris.BI.BIBase.and iprop(True) Ps

def Iris.BI.BIBase.bigOr {PROP : Type u_1} [BIBase PROP] (Ps : List PROP) : PROP

Fold the disjunction ∨ over a list of separation logic propositions.

Equations

• ([∨] Ps) = Iris.Std.bigOp Iris.BI.BIBase.or iprop(False) Ps

def Iris.BI.BIBase.bigSep {PROP : Type u_1} [BIBase PROP] (Ps : List PROP) : PROP

Fold the separating conjunction ∗ over a list of separation logic propositions.

Equations

• ([∗] Ps) = Iris.Std.bigOp Iris.BI.BIBase.sep iprop(emp) Ps

def Iris.BI.BIBase.«term[∧]_» : Lean.ParserDescr

Equations

• Iris.BI.BIBase.«term[∧]_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term[∧]_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[∧] ") (Lean.ParserDescr.cat `term 1024))

def Iris.BI.BIBase.«term[∨]_» : Lean.ParserDescr

Equations

• Iris.BI.BIBase.«term[∨]_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term[∨]_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[∨] ") (Lean.ParserDescr.cat `term 1024))

def Iris.BI.BIBase.«term[∗]_» : Lean.ParserDescr

Equations

• Iris.BI.BIBase.«term[∗]_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term[∗]_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[∗] ") (Lean.ParserDescr.cat `term 1024))

def Iris.BI.BIBase.«term▷^[_]_» : Lean.ParserDescr

Iterated later modality.

Equations

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

def Iris.BI.BIBase.laterN {PROP : Type u_1} [BIBase PROP] (n : Nat) (P : PROP) : PROP

Equations

• iprop(▷^[Nat.zero]P) = P
• iprop(▷^[n'.succ]P) = Iris.BI.BIBase.later iprop(▷^[n']P)

def Iris.BI.BIBase.«term◇_» : Lean.ParserDescr

Except-0 modality

Equations

• Iris.BI.BIBase.«term◇_» = Lean.ParserDescr.node `Iris.BI.BIBase.«term◇_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇ ") (Lean.ParserDescr.cat `term 40))

def Iris.BI.BIBase.except0 {PROP : Type u_1} [BIBase PROP] (P : PROP) : PROP

Equations

• iprop(◇ P) = iprop(Iris.BI.BIBase.later iprop(False) ∨ P)