def Iris.liftRel {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) (A : α → Prop) (B : β → Prop) : Prop

Equations

• Iris.liftRel R A B = ((∀ (a : α), A a → ∃ (b : β), B b ∧ R a b) ∧ ∀ (b : β), B b → ∃ (a : α), A a ∧ R a b)

theorem Iris.liftRel_eq {α : Sort u_1} {A B : α → Prop} : liftRel Eq A B ↔ A = B

class Iris.BI (PROP : Type u_1) extends Iris.COFE PROP, Iris.BI.BIBase PROP : Type u_1

Require that a separation logic with carrier type PROP fulfills all necessary axioms.

• Equiv : PROP → PROP → Prop
• Dist : Nat → PROP → PROP → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• equiv_dist {x y : PROP} : Equiv x y ↔ ∀ (n : Nat), Dist n x y
• dist_lt {n : Nat} {x y : PROP} {m : Nat} : Dist n x y → m < n → Dist m x y
• compl : Chain PROP → PROP
• conv_compl {n : Nat} {c : Chain PROP} : OFE.Dist n (compl c) (c.chain n)
• 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
• entails_preorder : Std.Preorder Entails
• equiv_iff {P Q : PROP} : OFE.Equiv P Q ↔ P ⊣⊢ Q
• and_ne : OFE.NonExpansive₂ and
• or_ne : OFE.NonExpansive₂ or
• imp_ne : OFE.NonExpansive₂ imp
• sForall_ne {n : Nat} {P₁ P₂ : PROP → Prop} : liftRel (fun (x1 x2 : PROP) => OFE.Dist n x1 x2) P₁ P₂ → OFE.Dist n (sForall P₁) (sForall P₂)
• sExists_ne {n : Nat} {P₁ P₂ : PROP → Prop} : liftRel (fun (x1 x2 : PROP) => OFE.Dist n x1 x2) P₁ P₂ → OFE.Dist n (sExists P₁) (sExists P₂)
• sep_ne : OFE.NonExpansive₂ sep
• wand_ne : OFE.NonExpansive₂ wand
• persistently_ne : OFE.NonExpansive persistently
• later_ne : OFE.NonExpansive later
• pure_intro {φ : Prop} {P : PROP} : φ → P ⊢ ⌜φ⌝
• pure_elim' {φ : Prop} {P : PROP} : (φ → True ⊢ P) → ⌜φ⌝ ⊢ P
• and_elim_l {P Q : PROP} : P ∧ Q ⊢ P
• and_elim_r {P Q : PROP} : P ∧ Q ⊢ Q
• and_intro {P Q R : PROP} : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R
• or_intro_l {P Q : PROP} : P ⊢ P ∨ Q
• or_intro_r {P Q : PROP} : Q ⊢ P ∨ Q
• or_elim {P Q R : PROP} : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R
• imp_intro {P Q R : PROP} : (P ∧ Q ⊢ R) → P ⊢ Q → R
• imp_elim {P Q R : PROP} : (P ⊢ Q → R) → P ∧ Q ⊢ R
• sForall_intro {P : PROP} {Ψ : PROP → Prop} : (∀ (p : PROP), Ψ p → P ⊢ p) → P ⊢ sForall Ψ
• sForall_elim {Ψ : PROP → Prop} {p : PROP} : Ψ p → sForall Ψ ⊢ p
• sExists_intro {Ψ : PROP → Prop} {p : PROP} : Ψ p → p ⊢ sExists Ψ
• sExists_elim {Φ : PROP → Prop} {Q : PROP} : (∀ (p : PROP), Φ p → p ⊢ Q) → sExists Φ ⊢ Q
• sep_mono {P P' Q Q' : PROP} : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'
• emp_sep {P : PROP} : emp ∗ P ⊣⊢ P
• sep_symm {P Q : PROP} : P ∗ Q ⊢ Q ∗ P
• sep_assoc_l {P Q R : PROP} : (P ∗ Q) ∗ R ⊢ P ∗ Q ∗ R
• wand_intro {P Q R : PROP} : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R
• wand_elim {P Q R : PROP} : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R
• persistently_mono {P Q : PROP} : (P ⊢ Q) → <pers> P ⊢ <pers> Q
• persistently_idem_2 {P : PROP} : <pers> P ⊢ <pers> <pers> P
• persistently_emp_2 : ⊢ <pers> emp
• persistently_and_2 {P Q : PROP} : <pers> P ∧ <pers> Q ⊢ <pers> (P ∧ Q)
• persistently_sExists_1 {Ψ : PROP → Prop} : <pers> sExists Ψ ⊢ «exists» fun (p : PROP) => iprop(⌜Ψ p⌝ ∧ <pers> p)
• persistently_absorb_l {P Q : PROP} : <pers> P ∗ Q ⊢ <pers> P
• persistently_and_l {P Q : PROP} : <pers> P ∧ Q ⊢ P ∗ Q
• later_mono {P Q : PROP} : (P ⊢ Q) → later P ⊢ later Q
• later_intro {P : PROP} : P ⊢ later P
• later_sForall_2 {Φ : PROP → Prop} : («forall» fun (p : PROP) => iprop(⌜Φ p⌝ → later p)) ⊢ later (sForall Φ)
• later_sExists_false {Φ : PROP → Prop} : later (sExists Φ) ⊢ later iprop(False) ∨ «exists» fun (p : PROP) => iprop(⌜Φ p⌝ ∧ later p)
• later_sep {P Q : PROP} : later iprop(P ∗ Q) ⊣⊢ later P ∗ later Q
• later_persistently {P : PROP} : later iprop(<pers> P) ⊣⊢ <pers> later P
• later_false_em {P : PROP} : later P ⊢ later iprop(False) ∨ (later iprop(False) → P)

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

@[simp]

theorem Iris.BI.BIBase.Entails.rfl {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊢ P

theorem Iris.BI.BIBase.Entails.of_eq {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P = Q) : P ⊢ Q

@[simp]

theorem Iris.BI.BIBase.BiEntails.rfl {PROP : Type u_1} [BI PROP] {P : PROP} : P ⊣⊢ P

theorem Iris.BI.BIBase.BiEntails.of_eq {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P = Q) : P ⊣⊢ Q

theorem Iris.BI.BIBase.BiEntails.symm {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : Q ⊣⊢ P

theorem Iris.BI.BIBase.BiEntails.trans {PROP : Type u_1} [BI PROP] {P Q R : PROP} (h1 : P ⊣⊢ Q) (h2 : Q ⊣⊢ R) : P ⊣⊢ R