class Iris.CMRA (α : Type u_1) extends Iris.OFE α : Type u_1

• Equiv : α → α → Prop
• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• equiv_dist {x y : α} : Equiv x y ↔ ∀ (n : Nat), Dist n x y
• dist_lt {n : Nat} {x y : α} {m : Nat} : Dist n x y → m < n → Dist m x y
• pcore : α → Option α
• op : α → α → α
• ValidN : Nat → α → Prop
• Valid : α → Prop
• op_ne {x : α} : OFE.NonExpansive (op x)
• pcore_ne {n : Nat} {x y cx : α} : OFE.Dist n x y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ OFE.Dist n cx cy
• validN_ne {n : Nat} {x y : α} : OFE.Dist n x y → ✓{n} x → ✓{n} y
• valid_iff_validN {x : α} : ✓ x ↔ ∀ (n : Nat), ✓{n} x
• validN_succ {x : α} {n : Nat} : ✓{n.succ} x → ✓{n} x
• validN_op_left {n : Nat} {x y : α} : ✓{n} x • y → ✓{n} x
• assoc {x y z : α} : OFE.Equiv (x • (y • z)) ((x • y) • z)
• comm {x y : α} : OFE.Equiv (x • y) (y • x)
• pcore_op_left {x cx : α} : pcore x = some cx → OFE.Equiv (cx • x) x
• pcore_idem {x cx : α} : pcore x = some cx → OFE.Equiv (pcore cx) (some cx)
• pcore_op_mono {x cx : α} : pcore x = some cx → ∀ (y : α), ∃ (cy : α), OFE.Equiv (pcore (x • y)) (some (cx • cy))
• extend {n : Nat} {x y₁ y₂ : α} : ✓{n} x → OFE.Dist n x (y₁ • y₂) → (z₁ : α) ×' (z₂ : α) ×' OFE.Equiv x (z₁ • z₂) ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂

theorem Iris.pcore_op_mono_of_core_op_mono {α : Type u_1} [OFE α] (op : α → α → α) (pcore : α → Option α) (h : ∀ (x cx y : α), (∃ (z : α), OFE.Equiv y (op x z)) → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ ∃ (z : α), OFE.Equiv cy (op cx z)) (x cx : α) (e : pcore x = some cx) (y : α) : ∃ (cy : α), OFE.Equiv (pcore (op x y)) (some (op cx cy))

Reduction of pcore_op_mono to regular monotonicity

def Iris.CMRA.«term_•_» : Lean.TrailingParserDescr

Equations

• Iris.CMRA.«term_•_» = Lean.ParserDescr.trailingNode `Iris.CMRA.«term_•_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " • ") (Lean.ParserDescr.cat `term 61))

def Iris.CMRA.Included {α : Type u_1} [CMRA α] (x y : α) : Prop

Equations

• (x ≼ y) = ∃ (z : α), Iris.OFE.Equiv y (x • z)

def Iris.CMRA.«term_≼_» : Lean.TrailingParserDescr

Equations

• Iris.CMRA.«term_≼_» = Lean.ParserDescr.trailingNode `Iris.CMRA.«term_≼_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼ ") (Lean.ParserDescr.cat `term 51))

def Iris.CMRA.IncludedN {α : Type u_1} [CMRA α] (n : Nat) (x y : α) : Prop

Equations

• (x ≼{n} y) = ∃ (z : α), Iris.OFE.Dist n y (x • z)

def Iris.CMRA.«term_≼{_}_» : Lean.TrailingParserDescr

Equations

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

def Iris.CMRA.op? {α : Type u_1} [CMRA α] (x : α) : Option α → α

Equations

• x •? some y = x • y
• x •? none = x

def Iris.CMRA.«term_•?_» : Lean.TrailingParserDescr

Equations

• Iris.CMRA.«term_•?_» = Lean.ParserDescr.trailingNode `Iris.CMRA.«term_•?_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " •? ") (Lean.ParserDescr.cat `term 61))

def Iris.CMRA.«term✓_» : Lean.ParserDescr

Equations

• Iris.CMRA.«term✓_» = Lean.ParserDescr.node `Iris.CMRA.«term✓_» 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "✓ ") (Lean.ParserDescr.cat `term 50))

def Iris.CMRA.«term✓{_}_» : Lean.ParserDescr

Equations

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

class Iris.CMRA.CoreId {α : Type u_1} [CMRA α] (x : α) : Prop

• core_id : OFE.Equiv (pcore x) (some x)

class Iris.CMRA.Exclusive {α : Type u_1} [CMRA α] (x : α) : Prop

• exclusive0_l (y : α) : ¬✓{0} x • y

class Iris.CMRA.Cancelable {α : Type u_1} [CMRA α] (x : α) : Prop

• cancelableN {n : Nat} {y z : α} : ✓{n} x • y → OFE.Dist n (x • y) (x • z) → OFE.Dist n y z

class Iris.CMRA.IdFree {α : Type u_1} [CMRA α] (x : α) : Prop

• id_free0_r (y : α) : ✓{0} x → ¬OFE.Dist 0 (x • y) x

class Iris.CMRA.IsTotal (α : Type u_1) [CMRA α] : Prop

• total (x : α) : ∃ (cx : α), pcore x = some cx

def Iris.CMRA.core {α : Type u_1} [CMRA α] (x : α) : α

Equations

• Iris.CMRA.core x = (Iris.CMRA.pcore x).getD x

class Iris.CMRA.Discrete (α : Type u_1) [CMRA α] extends Iris.OFE.Discrete α : Prop

• discrete_0 {x y : α} : Dist 0 x y → Equiv x y
• discrete_valid {x : α} : ✓{0} x → ✓ x

class Iris.UCMRA (α : Type u_1) extends Iris.CMRA α : Type u_1

• Equiv : α → α → Prop
• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• equiv_dist {x y : α} : Equiv x y ↔ ∀ (n : Nat), Dist n x y
• dist_lt {n : Nat} {x y : α} {m : Nat} : Dist n x y → m < n → Dist m x y
• pcore : α → Option α
• op : α → α → α
• ValidN : Nat → α → Prop
• Valid : α → Prop
• op_ne {x : α} : OFE.NonExpansive (op x)
• pcore_ne {n : Nat} {x y cx : α} : OFE.Dist n x y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ OFE.Dist n cx cy
• validN_ne {n : Nat} {x y : α} : OFE.Dist n x y → ✓{n} x → ✓{n} y
• valid_iff_validN {x : α} : ✓ x ↔ ∀ (n : Nat), ✓{n} x
• validN_succ {x : α} {n : Nat} : ✓{n.succ} x → ✓{n} x
• validN_op_left {n : Nat} {x y : α} : ✓{n} x • y → ✓{n} x
• assoc {x y z : α} : OFE.Equiv (x • (y • z)) ((x • y) • z)
• comm {x y : α} : OFE.Equiv (x • y) (y • x)
• pcore_op_left {x cx : α} : pcore x = some cx → OFE.Equiv (cx • x) x
• pcore_idem {x cx : α} : pcore x = some cx → OFE.Equiv (pcore cx) (some cx)
• pcore_op_mono {x cx : α} : pcore x = some cx → ∀ (y : α), ∃ (cy : α), OFE.Equiv (pcore (x • y)) (some (cx • cy))
• extend {n : Nat} {x y₁ y₂ : α} : ✓{n} x → OFE.Dist n x (y₁ • y₂) → (z₁ : α) ×' (z₂ : α) ×' OFE.Equiv x (z₁ • z₂) ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂
• unit : α
• unit_valid : ✓ unit
• unit_left_id {x : α} : OFE.Equiv (unit • x) x
• pcore_unit : OFE.Equiv (CMRA.pcore unit) (some unit)

instance Iris.CMRA.instNonExpansiveOptionPcore {α : Type u_1} [CMRA α] : OFE.NonExpansive pcore

theorem Iris.CMRA.coreId_of_eqv {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) (h : CoreId x₁) : CoreId x₂

theorem Iris.CMRA.coreId_iff {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) : CoreId x₁ ↔ CoreId x₂

Op

theorem Iris.CMRA.op_right_eqv {α : Type u_1} [CMRA α] (x : α) {y z : α} (e : OFE.Equiv y z) : OFE.Equiv (x • y) (x • z)

theorem Iris.OFE.Equiv.op_r {α : Type u_1} [CMRA α] {x y z : α} : Equiv y z → Equiv (x • y) (x • z)

theorem Iris.CMRA.op_right_dist {α : Type u_1} [CMRA α] {n : Nat} (x : α) {y z : α} (e : OFE.Dist n y z) : OFE.Dist n (x • y) (x • z)

theorem Iris.OFE.Dist.op_r {α : Type u_1} [CMRA α] {n : Nat} {x y z : α} : Dist n y z → Dist n (x • y) (x • z)

theorem Iris.CMRA.op_commN {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : OFE.Dist n (x • y) (y • x)

theorem Iris.CMRA.op_assocN {α : Type u_1} [CMRA α] {n : Nat} {x y z : α} : OFE.Dist n (x • (y • z)) ((x • y) • z)

theorem Iris.CMRA.op_left_eqv {α : Type u_1} [CMRA α] {x y : α} (z : α) (e : OFE.Equiv x y) : OFE.Equiv (x • z) (y • z)

theorem Iris.OFE.Equiv.op_l {α : Type u_1} [CMRA α] {x y z : α} : Equiv x y → Equiv (x • z) (y • z)

theorem Iris.CMRA.op_left_dist {α : Type u_1} [CMRA α] {n : Nat} {x y : α} (z : α) (e : OFE.Dist n x y) : OFE.Dist n (x • z) (y • z)

theorem Iris.OFE.Dist.op_l {α : Type u_1} [CMRA α] {n : Nat} {x y z : α} : Dist n x y → Dist n (x • z) (y • z)

theorem Iris.OFE.Dist.op {α : Type u_1} [CMRA α] {n : Nat} {x x' y y' : α} (ex : Dist n x x') (ey : Dist n y y') : Dist n (x • y) (x' • y')

theorem Iris.CMRA.op_eqv {α : Type u_1} [CMRA α] {x x' y y' : α} (ex : OFE.Equiv x x') (ey : OFE.Equiv y y') : OFE.Equiv (x • y) (x' • y')

theorem Iris.OFE.Equiv.op {α : Type u_1} [CMRA α] {x x' y y' : α} : Equiv x x' → Equiv y y' → Equiv (x • y) (x' • y')

theorem Iris.CMRA.op_proper2 {α : Type u_1} [CMRA α] {x₁ x₂ y₁ y₂ : α} (H1 : OFE.Equiv x₁ x₂) (H2 : OFE.Equiv y₁ y₂) : OFE.Equiv (x₁ • y₁) (x₂ • y₂)

theorem Iris.OFE.Dist.opM {α : Type u_1} [CMRA α] {n : Nat} {x₁ x₂ : α} {y₁ y₂ : Option α} (H1 : Dist n x₁ x₂) (H2 : Dist n y₁ y₂) : Dist n (x₁ •? y₁) (x₂ •? y₂)

theorem Iris.OFE.Equiv.opM {α : Type u_1} [CMRA α] {x₁ x₂ : α} {y₁ y₂ : Option α} (H1 : Equiv x₁ x₂) (H2 : Equiv y₁ y₂) : Equiv (x₁ •? y₁) (x₂ •? y₂)

theorem Iris.CMRA.opM_left_eqv {α : Type u_1} [CMRA α] {x y : α} (z : Option α) (e : OFE.Equiv x y) : OFE.Equiv (x •? z) (y •? z)

theorem Iris.CMRA.opM_right_eqv {α : Type u_1} [CMRA α] (x : α) {y z : Option α} (e : OFE.Equiv y z) : OFE.Equiv (x •? y) (x •? z)

theorem Iris.CMRA.opM_left_dist {α : Type u_1} [CMRA α] {n : Nat} {x y : α} (z : Option α) (e : OFE.Dist n x y) : OFE.Dist n (x •? z) (y •? z)

theorem Iris.CMRA.opM_right_dist {α : Type u_1} [CMRA α] {n : Nat} (x : α) {y z : Option α} (e : OFE.Dist n y z) : OFE.Dist n (x •? y) (x •? z)

theorem Iris.CMRA.op_opM_assoc {α : Type u_1} [CMRA α] (x y : α) (mz : Option α) : OFE.Equiv ((x • y) •? mz) (x • (y •? mz))

theorem Iris.CMRA.op_opM_assoc_dist {α : Type u_1} [CMRA α] {n : Nat} (x y : α) (mz : Option α) : OFE.Dist n ((x • y) •? mz) (x • (y •? mz))

Validity

theorem Iris.CMRA.Valid.validN {α : Type u_1} [CMRA α] {x : α} {n : Nat} : ✓ x → ✓{n} x

theorem Iris.CMRA.valid_mapN {α : Type u_1} [CMRA α] {x y : α} (f : ∀ (n : Nat), ✓{n} x → ✓{n} y) (v : ✓ x) : ✓ y

theorem Iris.CMRA.validN_of_eqv {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : OFE.Equiv x y → ✓{n} x → ✓{n} y

theorem Iris.CMRA.validN_iff {α : Type u_1} [CMRA α] {n : Nat} {x y : α} (e : OFE.Dist n x y) : ✓{n} x ↔ ✓{n} y

theorem Iris.OFE.Dist.validN {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : Dist n x y → (✓{n} x ↔ ✓{n} y)

theorem Iris.CMRA.valid_of_eqv {α : Type u_1} [CMRA α] {x y : α} : OFE.Equiv x y → ✓ x → ✓ y

theorem Iris.CMRA.valid_iff {α : Type u_1} [CMRA α] {x y : α} (e : OFE.Equiv x y) : ✓ x ↔ ✓ y

theorem Iris.OFE.Equiv.valid {α : Type u_1} [CMRA α] {x y : α} : Equiv x y → (✓ x ↔ ✓ y)

theorem Iris.CMRA.validN_of_le {α : Type u_1} [CMRA α] {n n' : Nat} {x : α} : n' ≤ n → ✓{n} x → ✓{n'} x

theorem Iris.CMRA.valid0_of_validN {α : Type u_1} [CMRA α] {n : Nat} {x : α} : ✓{n} x → ✓{0} x

theorem Iris.CMRA.validN_op_right {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : ✓{n} x • y → ✓{n} y

theorem Iris.CMRA.valid_op_right {α : Type u_1} [CMRA α] (x y : α) : ✓ x • y → ✓ y

theorem Iris.CMRA.valid_op_left {α : Type u_1} [CMRA α] {x y : α} : ✓ x • y → ✓ x

theorem Iris.CMRA.validN_opM {α : Type u_1} [CMRA α] {n : Nat} {x : α} {my : Option α} : ✓{n} x •? my → ✓{n} x

theorem Iris.CMRA.valid_opM {α : Type u_1} [CMRA α] {x : α} {my : Option α} : ✓ x •? my → ✓ x

theorem Iris.CMRA.validN_op_opM_left {α : Type u_1} [CMRA α] {n : Nat} {x y : α} {mz : Option α} : ✓{n} (x • y) •? mz → ✓{n} x •? mz

theorem Iris.CMRA.validN_op_opM_right {α : Type u_1} [CMRA α] {n : Nat} {x y : α} {mz : Option α} (h : ✓{n} (x • y) •? mz) : ✓{n} y •? mz

Core

theorem Iris.CMRA.pcore_proper {α : Type u_1} [CMRA α] {x y : α} (cx : α) (e : OFE.Equiv x y) (ps : pcore x = some cx) : ∃ (cy : α), pcore y = some cy ∧ OFE.Equiv cx cy

theorem Iris.CMRA.pcore_proper' {α : Type u_1} [CMRA α] {x y : α} (e : OFE.Equiv x y) : OFE.Equiv (pcore x) (pcore y)

theorem Iris.CMRA.pcore_op_left' {α : Type u_1} [CMRA α] {x cx : α} (e : OFE.Equiv (pcore x) (some cx)) : OFE.Equiv (cx • x) x

theorem Iris.CMRA.pcore_op_right {α : Type u_1} [CMRA α] {x cx : α} (e : pcore x = some cx) : OFE.Equiv (x • cx) x

theorem Iris.CMRA.pcore_op_right' {α : Type u_1} [CMRA α] {x cx : α} (e : OFE.Equiv (pcore x) (some cx)) : OFE.Equiv (x • cx) x

theorem Iris.CMRA.pcore_idem' {α : Type u_1} [CMRA α] {x cx : α} (e : OFE.Equiv (pcore x) (some cx)) : OFE.Equiv (pcore cx) (some cx)

theorem Iris.CMRA.pcore_op_self {α : Type u_1} [CMRA α] {x cx : α} (e : pcore x = some cx) : OFE.Equiv (cx • cx) cx

theorem Iris.CMRA.pcore_op_self' {α : Type u_1} [CMRA α] {x cx : α} (e : OFE.Equiv (pcore x) (some cx)) : OFE.Equiv (cx • cx) cx

theorem Iris.CMRA.pcore_validN {α : Type u_1} [CMRA α] {n : Nat} {x cx : α} (e : pcore x = some cx) (v : ✓{n} x) : ✓{n} cx

theorem Iris.CMRA.pcore_valid {α : Type u_1} [CMRA α] {x cx : α} (e : pcore x = some cx) : ✓ x → ✓ cx

Exclusive elements

theorem Iris.CMRA.not_valid_exclN_op_left {α : Type u_1} [CMRA α] {n : Nat} {x : α} [Exclusive x] {y : α} : ¬✓{n} x • y

theorem Iris.CMRA.not_valid_exclN_op_right {α : Type u_1} [CMRA α] {n : Nat} {x : α} [Exclusive x] {y : α} : ¬✓{n} y • x

theorem Iris.CMRA.not_valid_excl_op_left {α : Type u_1} [CMRA α] {x : α} [Exclusive x] {y : α} : ¬✓ x • y

theorem Iris.CMRA.not_excl_op_right {α : Type u_1} [CMRA α] {x : α} [Exclusive x] {y : α} : ¬✓ y • x

theorem Iris.CMRA.none_of_excl_valid_op {α : Type u_1} [CMRA α] {n : Nat} {x : α} [Exclusive x] {my : Option α} : ✓{n} x •? my → my = none

theorem Iris.CMRA.not_valid_of_exclN_inc {α : Type u_1} [CMRA α] {n : Nat} {x : α} [Exclusive x] {y : α} : x ≼{n} y → ¬✓{n} y

theorem Iris.CMRA.not_valid_of_excl_inc {α : Type u_1} [CMRA α] {x : α} [Exclusive x] {y : α} : x ≼ y → ¬✓ y

theorem Iris.CMRA.Exclusive.of_eqv {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) (h : Exclusive x₁) : Exclusive x₂

theorem Iris.CMRA.exclusive_iff {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) : Exclusive x₁ ↔ Exclusive x₂

theorem Iris.OFE.Dist.exclusive {α : Type u_1} [CMRA α] {x₁ x₂ : α} : Equiv x₁ x₂ → (CMRA.Exclusive x₁ ↔ CMRA.Exclusive x₂)

Order

theorem Iris.CMRA.inc_of_eqv_of_inc {α : Type u_1} [CMRA α] {a b c : α} (e : OFE.Equiv a b) : b ≼ c → a ≼ c

instance Iris.CMRA.instTransEquivIncluded {α : Type u_1} [CMRA α] : Trans OFE.Equiv Included Included

Equations

• Iris.CMRA.instTransEquivIncluded = { trans := ⋯ }

theorem Iris.CMRA.inc_of_inc_of_eqv {α : Type u_1} [CMRA α] {a b c : α} : a ≼ b → OFE.Equiv b c → a ≼ c

instance Iris.CMRA.instTransIncludedEquiv {α : Type u_1} [CMRA α] : Trans Included OFE.Equiv Included

Equations

• Iris.CMRA.instTransIncludedEquiv = { trans := ⋯ }

theorem Iris.CMRA.incN_of_incN_of_dist {α : Type u_1} [CMRA α] {n : Nat} {a b c : α} : a ≼{n} b → OFE.Dist n b c → a ≼{n} c

instance Iris.CMRA.instTransIncludedNDist {α : Type u_1} [CMRA α] {n : Nat} : Trans (IncludedN n) (OFE.Dist n) (IncludedN n)

Equations

• Iris.CMRA.instTransIncludedNDist = { trans := ⋯ }

theorem Iris.CMRA.incN_of_dist_of_incN {α : Type u_1} [CMRA α] {n : Nat} {a b c : α} (e : OFE.Dist n a b) : b ≼{n} c → a ≼{n} c

instance Iris.CMRA.instTransDistIncludedN {α : Type u_1} [CMRA α] {n : Nat} : Trans (OFE.Dist n) (IncludedN n) (IncludedN n)

Equations

• Iris.CMRA.instTransDistIncludedN = { trans := ⋯ }

theorem Iris.CMRA.incN_of_inc {α : Type u_1} [CMRA α] (n : Nat) {x y : α} : x ≼ y → x ≼{n} y

theorem Iris.CMRA.Included.incN {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼ y → x ≼{n} y

theorem Iris.CMRA.inc_iff_left {α : Type u_1} [CMRA α] {a b c : α} (e : OFE.Equiv a b) : a ≼ c ↔ b ≼ c

theorem Iris.OFE.Equiv.inc_l {α : Type u_1} [CMRA α] {a b c : α} : Equiv a b → (a ≼ c ↔ b ≼ c)

theorem Iris.CMRA.inc_iff_right {α : Type u_1} [CMRA α] {b c a : α} (e : OFE.Equiv b c) : a ≼ b ↔ a ≼ c

theorem Iris.OFE.Equiv.inc_r {α : Type u_1} [CMRA α] {b c a : α} : Equiv b c → (a ≼ b ↔ a ≼ c)

theorem Iris.CMRA.inc_iff {α : Type u_1} [CMRA α] {a a' b b' : α} (ea : OFE.Equiv a a') (eb : OFE.Equiv b b') : a ≼ b ↔ a' ≼ b'

theorem Iris.OFE.Equiv.inc {α : Type u_1} [CMRA α] {a a' b b' : α} : Equiv a a' → Equiv b b' → (a ≼ b ↔ a' ≼ b')

theorem Iris.CMRA.incN_iff_left {α : Type u_1} [CMRA α] {n : Nat} {a b c : α} (e : OFE.Dist n a b) : a ≼{n} c ↔ b ≼{n} c

theorem Iris.OFE.Dist.incN_l {α : Type u_1} [CMRA α] {n : Nat} {a b c : α} : Dist n a b → (a ≼{n} c ↔ b ≼{n} c)

theorem Iris.CMRA.incN_iff_right {α : Type u_1} [CMRA α] {n : Nat} {b c a : α} (e : OFE.Dist n b c) : a ≼{n} b ↔ a ≼{n} c

theorem Iris.OFE.Dist.incN_r {α : Type u_1} [CMRA α] {n : Nat} {b c a : α} : Dist n b c → (a ≼{n} b ↔ a ≼{n} c)

theorem Iris.CMRA.incN_iff {α : Type u_1} [CMRA α] {n : Nat} {a a' b b' : α} (ea : OFE.Dist n a a') (eb : OFE.Dist n b b') : a ≼{n} b ↔ a' ≼{n} b'

theorem Iris.OFE.Dist.incN {α : Type u_1} [CMRA α] {n : Nat} {a a' b b' : α} : Dist n a a' → Dist n b b' → (a ≼{n} b ↔ a' ≼{n} b')

theorem Iris.CMRA.inc_trans {α : Type u_1} [CMRA α] {x y z : α} : x ≼ y → y ≼ z → x ≼ z

theorem Iris.CMRA.Included.trans {α : Type u_1} [CMRA α] {x y z : α} : x ≼ y → y ≼ z → x ≼ z

instance Iris.CMRA.instTransIncluded {α : Type u_1} [CMRA α] : Trans Included Included Included

Equations

• Iris.CMRA.instTransIncluded = { trans := ⋯ }

theorem Iris.CMRA.incN_trans {α : Type u_1} [CMRA α] {n : Nat} {x y z : α} : x ≼{n} y → y ≼{n} z → x ≼{n} z

theorem Iris.CMRA.IncludedN.trans {α : Type u_1} [CMRA α] {n : Nat} {x y z : α} : x ≼{n} y → y ≼{n} z → x ≼{n} z

instance Iris.CMRA.instTransIncludedN {α : Type u_1} [CMRA α] {n : Nat} : Trans (IncludedN n) (IncludedN n) (IncludedN n)

Equations

• Iris.CMRA.instTransIncludedN = { trans := ⋯ }

theorem Iris.CMRA.valid_of_inc {α : Type u_1} [CMRA α] {x y : α} : x ≼ y → ✓ y → ✓ x

theorem Iris.CMRA.validN_of_incN {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼{n} y → ✓{n} y → ✓{n} x

theorem Iris.CMRA.IncludedN.validN {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼{n} y → ✓{n} y → ✓{n} x

theorem Iris.CMRA.validN_of_inc {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼ y → ✓{n} y → ✓{n} x

theorem Iris.CMRA.Included.validN {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼ y → ✓{n} y → ✓{n} x

theorem Iris.CMRA.incN_of_incN_le {α : Type u_1} [CMRA α] {n n' : Nat} {x y : α} (l1 : n' ≤ n) : x ≼{n} y → x ≼{n'} y

theorem Iris.CMRA.inc0_of_incN {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼{n} y → x ≼{0} y

theorem Iris.CMRA.IncludedN.le {α : Type u_1} [CMRA α] {n n' : Nat} {x y : α} : n' ≤ n → x ≼{n} y → x ≼{n'} y

theorem Iris.CMRA.incN_of_incN_succ {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼{n.succ} y → x ≼{n} y

theorem Iris.CMRA.IncludedN.succ {α : Type u_1} [CMRA α] {n : Nat} {x y : α} : x ≼{n.succ} y → x ≼{n} y

theorem Iris.CMRA.incN_op_left {α : Type u_1} [CMRA α] (n : Nat) (x y : α) : x ≼{n} x • y

theorem Iris.CMRA.inc_op_left {α : Type u_1} [CMRA α] (x y : α) : x ≼ x • y

theorem Iris.CMRA.inc_op_right {α : Type u_1} [CMRA α] (x y : α) : y ≼ x • y

theorem Iris.CMRA.incN_op_right {α : Type u_1} [CMRA α] (n : Nat) (x y : α) : y ≼{n} x • y

theorem Iris.CMRA.pcore_mono {α : Type u_1} [CMRA α] {cx x y : α} : x ≼ y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ cy

theorem Iris.CMRA.pcore_mono' {α : Type u_1} [CMRA α] {x y cx : α} (le : x ≼ y) (e : OFE.Equiv (pcore x) (some cx)) : ∃ (cy : α), pcore y = some cy ∧ cx ≼ cy

theorem Iris.CMRA.pcore_monoN' {α : Type u_1} [CMRA α] {n : Nat} {x y cx : α} : x ≼{n} y → OFE.Dist n (pcore x) (some cx) → ∃ (cy : α), pcore y = some cy ∧ cx ≼{n} cy

theorem Iris.CMRA.pcore_inc_self {α : Type u_1} [CMRA α] {x cx : α} (e : pcore x = some cx) : cx ≼ x

theorem Iris.CMRA.op_mono_right {α : Type u_1} [CMRA α] {x y : α} (z : α) : x ≼ y → z • x ≼ z • y

theorem Iris.CMRA.op_monoN_right {α : Type u_1} [CMRA α] {n : Nat} {x y : α} (z : α) : x ≼{n} y → z • x ≼{n} z • y

theorem Iris.CMRA.op_monoN_left {α : Type u_1} [CMRA α] {n : Nat} {x y : α} (z : α) (h : x ≼{n} y) : x • z ≼{n} y • z

theorem Iris.CMRA.op_mono_left {α : Type u_1} [CMRA α] {x y : α} (z : α) (h : x ≼ y) : x • z ≼ y • z

theorem Iris.CMRA.op_monoN {α : Type u_1} [CMRA α] {n : Nat} {x x' y y' : α} (hx : x ≼{n} x') (hy : y ≼{n} y') : x • y ≼{n} x' • y'

theorem Iris.CMRA.op_mono {α : Type u_1} [CMRA α] {x x' y y' : α} (hx : x ≼ x') (hy : y ≼ y') : x • y ≼ x' • y'

theorem Iris.CMRA.op_self {α : Type u_1} [CMRA α] (x : α) [CoreId x] : OFE.Equiv (x • x) x

theorem Iris.CMRA.op_core_right_of_inc {α : Type u_1} [CMRA α] {x y : α} [CoreId x] : x ≼ y → OFE.Equiv (x • y) y

theorem Iris.CMRA.included_dist_l {α : Type u_1} [CMRA α] {n : Nat} {x1 x2 x1' : α} : x1 ≼ x2 → OFE.Dist n x1' x1 → ∃ (x2' : α), x1' ≼ x2' ∧ OFE.Dist n x2' x2

theorem Iris.CMRA.op_core_left_of_inc {α : Type u_1} [CMRA α] {x y : α} [CoreId x] (le : x ≼ y) : OFE.Equiv (y • x) y

theorem Iris.CMRA.CoreId.of_pcore_eq_some {α : Type u_1} [CMRA α] {x y : α} (e : pcore x = some y) : CoreId y

theorem Iris.CMRA.pcore_eq_core {α : Type u_1} [CMRA α] [IsTotal α] (x : α) : pcore x = some (core x)

theorem Iris.CMRA.op_core {α : Type u_1} [CMRA α] [IsTotal α] (x : α) : OFE.Equiv (x • core x) x

theorem Iris.CMRA.core_op {α : Type u_1} [CMRA α] [IsTotal α] (x : α) : OFE.Equiv (core x • x) x

theorem Iris.CMRA.op_core_dist {α : Type u_1} [CMRA α] [IsTotal α] {n : Nat} (x : α) : OFE.Dist n (x • core x) x

theorem Iris.CMRA.core_op_dist {α : Type u_1} [CMRA α] [IsTotal α] {n : Nat} (x : α) : OFE.Dist n (core x • x) x

theorem Iris.CMRA.core_op_core {α : Type u_1} [CMRA α] [IsTotal α] {x : α} : OFE.Equiv (core x • core x) (core x)

theorem Iris.CMRA.validN_core {α : Type u_1} [CMRA α] [IsTotal α] {n : Nat} {x : α} (v : ✓{n} x) : ✓{n} core x

theorem Iris.CMRA.valid_core {α : Type u_1} [CMRA α] [IsTotal α] {x : α} (v : ✓ x) : ✓ core x

instance Iris.CMRA.instCoreIdCore {α : Type u_1} [CMRA α] [IsTotal α] (y : α) : CoreId (core y)

theorem Iris.CMRA.core_ne {α : Type u_1} [CMRA α] [IsTotal α] : OFE.NonExpansive core

theorem Iris.OFE.Dist.core {α : Type u_1} [CMRA α] [CMRA.IsTotal α] {n : Nat} {x₁ x₂ : α} : Dist n x₁ x₂ → Dist n (CMRA.core x₁) (CMRA.core x₂)

theorem Iris.OFE.Equiv.core {α : Type u_1} [CMRA α] [CMRA.IsTotal α] {x₁ x₂ : α} : Equiv x₁ x₂ → Equiv (CMRA.core x₁) (CMRA.core x₂)

theorem Iris.CMRA.core_eqv_self {α : Type u_1} [CMRA α] [IsTotal α] (x : α) [CoreId x] : OFE.Equiv (core x) x

theorem Iris.CMRA.coreId_iff_core_eqv_self {α : Type u_1} [CMRA α] [IsTotal α] {x : α} : CoreId x ↔ OFE.Equiv (core x) x

theorem Iris.CMRA.core_idem {α : Type u_1} [CMRA α] [IsTotal α] (x : α) : OFE.Equiv (core (core x)) (core x)

theorem Iris.CMRA.inc_refl {α : Type u_1} [CMRA α] [IsTotal α] (x : α) : x ≼ x

theorem Iris.CMRA.Included.rfl {α : Type u_1} [CMRA α] [IsTotal α] {x : α} : x ≼ x

theorem Iris.CMRA.incN_refl {α : Type u_1} [CMRA α] [IsTotal α] {n : Nat} (x : α) : x ≼{n} x

theorem Iris.CMRA.IncludedN.rfl {α : Type u_1} [CMRA α] [IsTotal α] {n : Nat} {x : α} : x ≼{n} x

theorem Iris.CMRA.core_inc_self {α : Type u_1} [CMRA α] [IsTotal α] {x : α} [CoreId x] : core x ≼ x

theorem Iris.CMRA.core_incN_core {α : Type u_1} [CMRA α] [IsTotal α] {n : Nat} {x y : α} (inc : x ≼{n} y) : core x ≼{n} core y

theorem Iris.CMRA.core_op_mono {α : Type u_1} [CMRA α] [IsTotal α] (x y : α) : core x ≼ core (x • y)

theorem Iris.CMRA.core_mono {α : Type u_1} [CMRA α] [IsTotal α] {x y : α} (Hinc : x ≼ y) : core x ≼ core y

theorem Iris.CMRA.discrete_inc_l {α : Type u_1} [CMRA α] {x y : α} [HD : OFE.DiscreteE x] (Hv : ✓{0} y) (Hle : x ≼{0} y) : x ≼ y

theorem Iris.CMRA.discrete_inc_r {α : Type u_1} [CMRA α] {x y : α} [HD : OFE.DiscreteE y] : x ≼{0} y → x ≼ y

instance Iris.CMRA.discrete_op {α : Type u_1} [CMRA α] {x y : α} (Hv : ✓{0} x • y) [Hx : OFE.DiscreteE x] [Hy : OFE.DiscreteE y] : OFE.DiscreteE (x • y)

theorem Iris.CMRA.valid_iff_validN' {α : Type u_1} [CMRA α] [Discrete α] (n : Nat) {x : α} : ✓ x ↔ ✓{n} x

theorem Iris.CMRA.valid_0_iff_validN {α : Type u_1} [CMRA α] [Discrete α] (n : Nat) {x : α} : ✓{0} x ↔ ✓{n} x

theorem Iris.CMRA.inc_iff_incN {α : Type u_1} [CMRA α] [OFE.Discrete α] (n : Nat) {x y : α} : x ≼ y ↔ x ≼{n} y

theorem Iris.CMRA.inc_0_iff_incN {α : Type u_1} [CMRA α] [OFE.Discrete α] (n : Nat) {x y : α} : x ≼{0} y ↔ x ≼{n} y

theorem Iris.CMRA.cancelable {α : Type u_1} [CMRA α] {x y z : α} [Cancelable x] (v : ✓ x • y) (e : OFE.Equiv (x • y) (x • z)) : OFE.Equiv y z

theorem Iris.CMRA.discrete_cancelable {α : Type u_1} [CMRA α] {x : α} [Discrete α] (H : ∀ {y z : α}, ✓ x • y → OFE.Equiv (x • y) (x • z) → OFE.Equiv y z) : Cancelable x

instance Iris.CMRA.cancelable_op {α : Type u_1} [CMRA α] {x y : α} [Cancelable x] [Cancelable y] : Cancelable (x • y)

instance Iris.CMRA.exclusive_cancelable {α : Type u_1} [CMRA α] {x : α} [Exclusive x] : Cancelable x

theorem Iris.CMRA.Cancelable.of_eqv {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) (h : Cancelable x₁) : Cancelable x₂

theorem Iris.CMRA.cancelable_iff {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) : Cancelable x₁ ↔ Cancelable x₂

theorem Iris.OFE.Equiv.cancelable {α : Type u_1} [CMRA α] {x₁ x₂ : α} : Equiv x₁ x₂ → (CMRA.Cancelable x₁ ↔ CMRA.Cancelable x₂)

theorem Iris.CMRA.op_opM_cancel_dist {α : Type u_1} [CMRA α] {n : Nat} {mw : Option α} {x y z : α} [Cancelable x] (vxy : ✓{n} x • y) (h : OFE.Dist n (x • y) ((x • z) •? mw)) : OFE.Dist n y (z •? mw)

theorem Iris.CMRA.IdFree.of_dist {α : Type u_1} [CMRA α] {x₁ x₂ : α} {n : Nat} (e : OFE.Dist n x₁ x₂) (h : IdFree x₁) : IdFree x₂

theorem Iris.OFE.Dist.idFree {α : Type u_1} [CMRA α] {n : Nat} {x₁ x₂ : α} (e : Dist n x₁ x₂) : CMRA.IdFree x₁ ↔ CMRA.IdFree x₂

theorem Iris.CMRA.IdFree.of_eqv {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) (h : IdFree x₁) : IdFree x₂

theorem Iris.CMRA.idFree_iff {α : Type u_1} [CMRA α] {x₁ x₂ : α} (e : OFE.Equiv x₁ x₂) : IdFree x₁ ↔ IdFree x₂

theorem Iris.OFE.Equiv.idFree {α : Type u_1} [CMRA α] {x₁ x₂ : α} : Equiv x₁ x₂ → (CMRA.IdFree x₁ ↔ CMRA.IdFree x₂)

theorem Iris.CMRA.id_freeN_r {α : Type u_1} [CMRA α] {n n' : Nat} {x : α} [IdFree x] {y : α} (v : ✓{n} x) : ¬OFE.Dist n' (x • y) x

theorem Iris.CMRA.id_freeN_l {α : Type u_1} [CMRA α] {n n' : Nat} {x : α} [IdFree x] {y : α} (v : ✓{n} x) : ¬OFE.Dist n' (y • x) x

theorem Iris.CMRA.id_free_r {α : Type u_1} [CMRA α] {x : α} [IdFree x] {y : α} (v : ✓ x) : ¬OFE.Equiv (x • y) x

theorem Iris.CMRA.id_free_l {α : Type u_1} [CMRA α] {x : α} [IdFree x] {y : α} (v : ✓ x) : ¬OFE.Equiv (y • x) x

theorem Iris.CMRA.discrete_id_free {α : Type u_1} [CMRA α] {x : α} [Discrete α] (H : ∀ (y : α), ✓ x → ¬OFE.Equiv (x • y) x) : IdFree x

instance Iris.CMRA.idFree_op_r {α : Type u_1} [CMRA α] {x y : α} [IdFree y] [Cancelable x] : IdFree (x • y)

instance Iris.CMRA.idFree_op_l {α : Type u_1} [CMRA α] {x y : α} [IdFree x] [Cancelable y] : IdFree (x • y)

instance Iris.CMRA.exclusive_idFree {α : Type u_1} [CMRA α] {x : α} [Exclusive x] : IdFree x

theorem Iris.CMRA.unit_validN {α : Type u_1} [UCMRA α] {n : Nat} : ✓{n} unit

theorem Iris.CMRA.incN_unit {α : Type u_1} [UCMRA α] {n : Nat} {x : α} : unit ≼{n} x

theorem Iris.CMRA.inc_unit {α : Type u_1} [UCMRA α] {x : α} : unit ≼ x

theorem Iris.CMRA.unit_left_id_dist {α : Type u_1} [UCMRA α] {n : Nat} (x : α) : OFE.Dist n (unit • x) x

theorem Iris.CMRA.unit_right_id {α : Type u_1} [UCMRA α] {x : α} : OFE.Equiv (x • unit) x

theorem Iris.CMRA.unit_right_id_dist {α : Type u_1} [UCMRA α] {n : Nat} (x : α) : OFE.Dist n (x • unit) x

instance Iris.CMRA.unit_CoreId {α : Type u_1} [UCMRA α] : CoreId unit

instance Iris.CMRA.unit_total {α : Type u_1} [UCMRA α] : IsTotal α

instance Iris.CMRA.empty_cancelable {α : Type u_1} [UCMRA α] : Cancelable unit

theorem Iris.OFE.Dist.to_incN {α : Type u_1} [UCMRA α] {n : Nat} {x y : α} (H : Dist n x y) : x ≼{n} y

theorem Iris.CMRA.assoc_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x y z : α} : x • (y • z) = (x • y) • z

theorem Iris.CMRA.comm_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x y : α} : x • y = y • x

theorem Iris.CMRA.pcore_op_left_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x cx : α} (h : pcore x = some cx) : cx • x = x

theorem Iris.CMRA.pcore_idem_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x cx : α} (h : pcore x = some cx) : pcore cx = some cx

theorem Iris.CMRA.op_opM_assoc_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x y : α} {mz : Option α} : (x • y) •? mz = x • (y •? mz)

theorem Iris.CMRA.pcore_op_right_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x cx : α} (h : pcore x = some cx) : x • cx = x

theorem Iris.CMRA.pcore_op_self_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x cx : α} (h : pcore x = some cx) : cx • cx = cx

theorem Iris.CMRA.core_id_dup_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x : α} [CoreId x] : x • x = x

theorem Iris.CMRA.op_core_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x : α} [IsTotal α] : x • core x = x

theorem Iris.CMRA.core_op_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x : α} [IsTotal α] : core x • x = x

theorem Iris.CMRA.core_idem_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x : α} [IsTotal α] : core (core x) = core x

theorem Iris.CMRA.core_op_core_L {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x : α} [IsTotal α] : core x • core x = core x

theorem Iris.CMRA.coreId_iff_core_eq_self {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x : α} [IsTotal α] : CoreId x ↔ core x = x

theorem Iris.CMRA.core_eq_self {α : Type u_1} [CMRA α] [OFE.Leibniz α] {x : α} [IsTotal α] [c : CoreId x] : core x = x

theorem Iris.CMRA.unit_left_id_L {α : Type u_1} [UCMRA α] [OFE.Leibniz α] {x : α} : unit • x = x

theorem Iris.CMRA.unit_right_id_L {α : Type u_1} [UCMRA α] [OFE.Leibniz α] {x : α} : x • unit = x

structure Iris.CMRA.Hom (α : Type u_1) (β : Type u_2) [CMRA α] [CMRA β] extends α -n> β : Type (max u_1 u_2)

A morphism between CMRAs, written α -C> β, is defined to be a non-expansive function which preserves validN, pcore and op.

• f : α → β
• ne : NonExpansive self.f
• validN {n : Nat} {x : α} : ✓{n} x → ✓{n} self.f x
• pcore (x : α) : OFE.Equiv (Option.map self.f (pcore x)) (pcore (self.f x))
• op (x y : α) : OFE.Equiv (self.f (x • y)) (self.f x • self.f y)

theorem Iris.CMRA.Hom.ext_iff {α : Type u_1} {β : Type u_2} {inst✝ : CMRA α} {inst✝¹ : CMRA β} {x y : α -C> β} : x = y ↔ x.f = y.f

theorem Iris.CMRA.Hom.ext {α : Type u_1} {β : Type u_2} {inst✝ : CMRA α} {inst✝¹ : CMRA β} {x y : α -C> β} (f : x.f = y.f) : x = y

def Iris.CMRA.«term_-C>_» : Lean.TrailingParserDescr

A morphism between CMRAs, written α -C> β, is defined to be a non-expansive function which preserves validN, pcore and op.

Equations

• Iris.CMRA.«term_-C>_» = Lean.ParserDescr.trailingNode `Iris.CMRA.«term_-C>_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -C> ") (Lean.ParserDescr.cat `term 25))

instance Iris.CMRA.instCoeFunHomForall {α : Type u_1} [CMRA α] {β : Type u_2} [CMRA β] : CoeFun (α -C> β) fun (x : α -C> β) => α → β

Equations

• Iris.CMRA.instCoeFunHomForall = { coe := fun (F : α -C> β) => F.f }

instance Iris.CMRA.instOFEHom {α : Type u_1} [CMRA α] {β : Type u_2} [CMRA β] : OFE (α -C> β)

Equations

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

def Iris.CMRA.Hom.id {α : Type u_1} [CMRA α] : α -C> α

Equations

• Iris.CMRA.Hom.id = { toHom := Iris.OFE.Hom.id, validN := ⋯, pcore := ⋯, op := ⋯ }

theorem Iris.CMRA.Hom.eqv {α : Type u_2} [CMRA α] {β : Type u_1} [CMRA β] (f : α -C> β) {x₁ x₂ : α} (X : OFE.Equiv x₁ x₂) : OFE.Equiv (f.f x₁) (f.f x₂)

theorem Iris.CMRA.Hom.core {α : Type u_2} [CMRA α] {β : Type u_1} [CMRA β] (f : α -C> β) {x : α} : OFE.Equiv (core (f.f x)) (f.f (core x))

theorem Iris.CMRA.Hom.mono {α : Type u_2} [CMRA α] {β : Type u_1} [CMRA β] (f : α -C> β) {x₁ x₂ : α} : x₁ ≼ x₂ → f.f x₁ ≼ f.f x₂

theorem Iris.CMRA.Hom.monoN {α : Type u_2} [CMRA α] {β : Type u_1} [CMRA β] (f : α -C> β) (n : Nat) {x₁ x₂ : α} : x₁ ≼{n} x₂ → f.f x₁ ≼{n} f.f x₂

theorem Iris.CMRA.Hom.valid {α : Type u_2} [CMRA α] {β : Type u_1} [CMRA β] (f : α -C> β) {x : α} (H : ✓ x) : ✓ f.f x

class Iris.RFunctor (F : COFE.OFunctorPre) : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

• cmra {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : CMRA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
• map_ne {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : OFE.NonExpansive₂ map
• map_id {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (x : F α β) : OFE.Equiv ((map OFE.Hom.id OFE.Hom.id).f x) x
• map_comp {α₁ α₂ α₃ : Type u_1} {β₁ β₂ β₃ : Type u_2} [OFE α₁] [OFE α₂] [OFE α₃] [OFE β₁] [OFE β₂] [OFE β₃] (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) : OFE.Equiv ((map (f.comp g) (g'.comp f')).f x) ((map g g').f ((map f f').f x))

class Iris.RFunctorContractive (F : COFE.OFunctorPre) extends Iris.RFunctor F : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

• cmra {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : CMRA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
• map_ne {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : OFE.NonExpansive₂ map
• map_id {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (x : F α β) : OFE.Equiv ((map OFE.Hom.id OFE.Hom.id).f x) x
• map_comp {α₁ α₂ α₃ : Type u_1} {β₁ β₂ β₃ : Type u_2} [OFE α₁] [OFE α₂] [OFE α₃] [OFE β₁] [OFE β₂] [OFE β₃] (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) : OFE.Equiv ((map (f.comp g) (g'.comp f')).f x) ((map g g').f ((map f f').f x))
• map_contractive {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : OFE.Contractive (Function.uncurry RFunctor.map)

def Iris.RFunctor.ap (F : COFE.OFunctorPre) (T : Type u_1) [RFunctor F] [OFE T] : Type u_2

Equations

• Iris.RFunctor.ap F T = F T T

instance Iris.RFunctor.toOFunctor {F : COFE.OFunctorPre} [R : RFunctor F] : COFE.OFunctor F

Equations

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

instance Iris.RFunctorContractive.toOFunctorContractive {F : COFE.OFunctorPre} [RFunctorContractive F] : COFE.OFunctorContractive F

Equations

• Iris.RFunctorContractive.toOFunctorContractive = { toOFunctor := Iris.RFunctor.toOFunctor, map_contractive := ⋯ }

class Iris.URFunctor (F : COFE.OFunctorPre) : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

• cmra {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : UCMRA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
• map_ne {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : OFE.NonExpansive₂ map
• map_id {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (x : F α β) : OFE.Equiv ((map OFE.Hom.id OFE.Hom.id).f x) x
• map_comp {α₁ α₂ α₃ : Type u_1} {β₁ β₂ β₃ : Type u_2} [OFE α₁] [OFE α₂] [OFE α₃] [OFE β₁] [OFE β₂] [OFE β₃] (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) : OFE.Equiv ((map (f.comp g) (g'.comp f')).f x) ((map g g').f ((map f f').f x))

class Iris.URFunctorContractive (F : COFE.OFunctorPre) extends Iris.URFunctor F : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

• cmra {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : UCMRA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
• map_ne {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : OFE.NonExpansive₂ map
• map_id {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (x : F α β) : OFE.Equiv ((map OFE.Hom.id OFE.Hom.id).f x) x
• map_comp {α₁ α₂ α₃ : Type u_1} {β₁ β₂ β₃ : Type u_2} [OFE α₁] [OFE α₂] [OFE α₃] [OFE β₁] [OFE β₂] [OFE β₃] (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) : OFE.Equiv ((map (f.comp g) (g'.comp f')).f x) ((map g g').f ((map f f').f x))
• map_contractive {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [OFE α₁] [OFE α₂] [OFE β₁] [OFE β₂] : OFE.Contractive (Function.uncurry URFunctor.map)

instance Iris.URFunctor.toRFunctor {F : COFE.OFunctorPre} [UF : URFunctor F] : RFunctor F

Equations

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

instance Iris.URFunctorContractive.toRFunctorContractive {F : COFE.OFunctorPre} [URFunctorContractive F] : RFunctorContractive F

Equations

• Iris.URFunctorContractive.toRFunctorContractive = { toRFunctor := Iris.URFunctor.toRFunctor, map_contractive := ⋯ }

instance Iris.COFE.OFunctor.constOF_RFunctor {B : Type} [CMRA B] : RFunctor (constOF B)

Equations

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

instance Iris.OFunctor.constOF_RFunctorContractive {B : Type} [CMRA B] : RFunctorContractive (COFE.constOF B)

Equations

• Iris.OFunctor.constOF_RFunctorContractive = { toRFunctor := Iris.COFE.OFunctor.constOF_RFunctor, map_contractive := ⋯ }

instance Iris.cmraDiscreteFunO {α : Type u_1} (β : α → Type u_2) [(x : α) → CMRA (β x)] [∀ (x : α), CMRA.IsTotal (β x)] : CMRA ((x : α) → β x)

Equations

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

instance Iris.ucmraDiscreteFunO {α : Type u_1} (β : α → Type u_2) [(x : α) → UCMRA (β x)] : UCMRA ((x : α) → β x)

Equations

• Iris.ucmraDiscreteFunO β = { toCMRA := Iris.cmraDiscreteFunO β, unit := fun (x : α) => Iris.UCMRA.unit, unit_valid := ⋯, unit_left_id := ⋯, pcore_unit := ⋯ }

instance Iris.urFunctorDiscreteFunOF {C : Type u_1} (F : C → COFE.OFunctorPre) [(c : C) → URFunctor (F c)] : URFunctor (DiscreteFunOF F)

Equations

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

instance Iris.DiscreteFunOF_URFC {C : Type u_1} (F : C → COFE.OFunctorPre) [HURF : (c : C) → URFunctorContractive (F c)] : URFunctorContractive (DiscreteFunOF F)

Equations

• Iris.DiscreteFunOF_URFC F = { toURFunctor := Iris.urFunctorDiscreteFunOF F, map_contractive := ⋯ }

def Iris.optionCore {α : Type u_1} [CMRA α] (x : Option α) : Option α

Equations

• Iris.optionCore x = x.bind Iris.CMRA.pcore

def Iris.optionOp {α : Type u_1} [CMRA α] (x y : Option α) : Option α

Equations

• Iris.optionOp (some x') (some y') = some (x' • y')
• Iris.optionOp none y = y
• Iris.optionOp x none = x

def Iris.optionValidN {α : Type u_1} [CMRA α] (n : Nat) : Option α → Prop

Equations

• Iris.optionValidN n (some y) = (✓{n} y)
• Iris.optionValidN n none = True

def Iris.optionValid {α : Type u_1} [CMRA α] : Option α → Prop

Equations

• Iris.optionValid (some y) = (✓ y)
• Iris.optionValid none = True

instance Iris.cmraOption {α : Type u_1} [CMRA α] : CMRA (Option α)

Equations

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

instance Iris.ucmraOption {α : Type u_1} [CMRA α] : UCMRA (Option α)

Equations

• Iris.ucmraOption = { toCMRA := Iris.cmraOption, unit := none, unit_valid := True.intro, unit_left_id := ⋯, pcore_unit := ⋯ }

theorem Iris.CMRA.equiv_of_some_equiv_some {α : Type u_1} [CMRA α] {x y : α} (h : OFE.Equiv (some x) (some y)) : OFE.Equiv x y

theorem Iris.CMRA.dist_of_some_dist_some {α : Type u_1} [CMRA α] {n : Nat} {x y : α} (h : OFE.Dist n (some x) (some y)) : OFE.Dist n x y

theorem Iris.CMRA.op_some_opM_assoc {α : Type u_1} [CMRA α] (x y : α) (mz : Option α) : OFE.Equiv ((x • y) •? mz) (x •? (some y • mz))

theorem Iris.CMRA.op_some_opM_assoc_dist {α : Type u_1} [CMRA α] {n : Nat} (x y : α) (mz : Option α) : OFE.Dist n ((x • y) •? mz) (x •? (some y • mz))

theorem Iris.CMRA.some_inc_some_of_dist_opM {α : Type u_1} [CMRA α] {n : Nat} {x y : α} {mz : Option α} (h : OFE.Dist n x (y •? mz)) : some y ≼{n} some x

theorem Iris.CMRA.inc_of_some_inc_some {α : Type u_1} [CMRA α] [IsTotal α] {x y : α} (h : some y ≼ some x) : y ≼ x

theorem Iris.CMRA.incN_of_some_incN_some {α : Type u_1} [CMRA α] {n : Nat} [IsTotal α] {x y : α} : some y ≼{n} some x → y ≼{n} x

theorem Iris.CMRA.exists_op_some_eqv_some {α : Type u_1} [CMRA α] (x : Option α) (y : α) : ∃ (z : α), OFE.Equiv (x • some y) (some z)

theorem Iris.CMRA.exists_op_some_dist_some {α : Type u_1} [CMRA α] {n : Nat} (x : Option α) (y : α) : ∃ (z : α), OFE.Dist n (x • some y) (some z)

theorem Iris.not_valid_some_exclN_op_left {α : Type u_1} [CMRA α] {n : Nat} {x : α} [CMRA.Exclusive x] {y : α} : ¬✓{n} some x • some y

theorem Iris.validN_op_unit {α : Type u_1} [CMRA α] {n : Nat} {x : Option α} (vx : ✓{n} x) : ✓{n} x • UCMRA.unit

instance Iris.cmraUnit : CMRA Unit

Equations

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

@[reducible, inline]

abbrev Iris.Prod.pcore {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] (x : α × β) : Option (α × β)

Equations

• Iris.Prod.pcore x = (Iris.CMRA.pcore x.fst).bind fun (a : α) => (Iris.CMRA.pcore x.snd).bind fun (b : β) => pure (a, b)

@[reducible, inline]

abbrev Iris.Prod.op {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] (x y : α × β) : α × β

Equations

• Iris.Prod.op x y = (x.fst • y.fst, x.snd • y.snd)

@[reducible, inline]

abbrev Iris.Prod.ValidN {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] (n : Nat) (x : α × β) : Prop

Equations

• Iris.Prod.ValidN n x = (✓{n} x.fst ∧ ✓{n} x.snd)

@[reducible, inline]

abbrev Iris.Prod.Valid {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] (x : α × β) : Prop

Equations

• Iris.Prod.Valid x = (✓ x.fst ∧ ✓ x.snd)

instance Iris.Prod.cmraProd {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] : CMRA (α × β)

Equations

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

theorem Iris.Prod.valid_fst {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] {x : α × β} (h : ✓ x) : ✓ x.fst

theorem Iris.Prod.valid_snd {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] {x : α × β} (h : ✓ x) : ✓ x.snd

theorem Iris.Prod.validN_fst {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] {n : Nat} {x : α × β} (h : ✓{n} x) : ✓{n} x.fst

theorem Iris.Prod.validN_snd {α : Type u_1} {β : Type u_2} [CMRA α] [CMRA β] {n : Nat} {x : α × β} (h : ✓{n} x) : ✓{n} x.snd

instance Iris.urFunctorOptionOF (F : COFE.OFunctorPre) [RFunctor F] : URFunctor (OptionOF F)

Equations

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

instance Iris.urFunctorContractiveOptionOF (F : COFE.OFunctorPre) [RFunctorContractive F] : URFunctorContractive (OptionOF F)

Equations

• Iris.urFunctorContractiveOptionOF F = { toURFunctor := Iris.urFunctorOptionOF F, map_contractive := ⋯ }

@[reducible, inline]

abbrev Iris.GenMap (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

Equations

• Iris.GenMap α β = (α → Option β)

@[reducible, inline]

abbrev Iris.GenMapOF (C : Type u_1) (F : COFE.OFunctorPre) : COFE.OFunctorPre

Equations

• Iris.GenMapOF C F = Iris.DiscreteFunOF fun (x : C) => Iris.OptionOF F