Ordered resource algebras and their morphisms.

Copyright (c) The Iris-Lean Contributors.

class Iris.Op (α : Type u_1) [OFE α] : Type u_1

The underlying operation of a resource.

• op : α → α → α

  The composition operation.

• op_ne {x : α} : OFE.NonExpansive (op x)
• assoc {x y z : α} : x • (y • z) = (x • y) • z
• comm {x y : α} : x • y = y • x

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

The composition operation.

Equations

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

def Iris.Op.optionalOp {α : Type u_1} [OFE α] [Op α] (x : α) : Option α → α

The composition operation with an optional right argument.

Equations

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

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

The composition operation with an optional right argument.

Equations

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

class Iris.PCore (α : Type u_1) [OFE α] : Type u_1

The partial core operator for a resource algebra.

• pcore : α → Option α

  The partial core of a resource.

• 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
• pcore_idem {x cx : α} : pcore x = some cx → pcore cx = some cx

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

The total core operation.

Equations

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

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

A resource algebra whose core is total.

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

class Iris.Validity (α : Type u_1) [OFE α] : Type u_1

The validity predicates of a resource algebra.

• ValidN : Nat → α → Prop

  The step-indexed validity predicate.

• Valid : α → Prop

  The validity predicate.

• 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

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

The validity predicate.

Equations

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

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

The step-indexed validity predicate.

Equations

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

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

class Iris.Ordered (α : Type u_1) [OFE α] : Type u_1

The ordering predicate on a resource algebra.

• OrderN : Nat → α → α → Prop

  The indexed ordering predicate. This is the generic ORA order predicate; if your ORA is OrdInc, the lemma ordN_incN converts it to the extension order typical of Iris CMRAs.

• Order : α → α → Prop

  The ordering predicate. This is the generic ORA order predicate; if your ORA is OrdInc, the lemma ord_inc converts it to the extension order typical of Iris CMRAs.

• ordN_ne {n : Nat} {x x' y y' : α} : OFE.Dist n x x' → OFE.Dist n y y' → x ≼ₒ{n} y → x' ≼ₒ{n} y'
• ordN_succ {n : Nat} {x y : α} : x ≼ₒ{n.succ} y → x ≼ₒ{n} y
• ordN_trans {n : Nat} {x y z : α} : x ≼ₒ{n} y → y ≼ₒ{n} z → x ≼ₒ{n} z
• ord_trans {x y z : α} : x ≼ₒ y → y ≼ₒ z → x ≼ₒ z
• ordN_of_ord {x y : α} (n : Nat) : x ≼ₒ y → x ≼ₒ{n} y

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

The indexed ordering predicate. This is the generic ORA order predicate; if your ORA is OrdInc, the lemma ordN_incN converts it to the extension order typical of Iris CMRAs.

Equations

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

def Iris.Ordered.«term_≼ₒ_» : Lean.TrailingParserDescr

The ordering predicate. This is the generic ORA order predicate; if your ORA is OrdInc, the lemma ord_inc converts it to the extension order typical of Iris CMRAs.

Equations

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

def Iris.Ordered.OrderNR {α : Type u_1} [OFE α] [Ordered α] (n : Nat) (x y : α) : Prop

The reflexive closure of the step-indexed order.

Equations

• (x ≼ₒ*{n} y) = (Iris.OFE.Dist n x y ∨ x ≼ₒ{n} y)

def Iris.Ordered.«term_≼ₒ*{_}_» : Lean.TrailingParserDescr

The reflexive closure of the step-indexed order.

Equations

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

def Iris.Ordered.OrderR {α : Type u_1} [OFE α] [Ordered α] (x y : α) : Prop

The reflexive closure of the order.

Equations

• (x ≼ₒ* y) = (x = y ∨ x ≼ₒ y)

def Iris.Ordered.«term_≼ₒ*_» : Lean.TrailingParserDescr

The reflexive closure of the order.

Equations

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

theorem Iris.Ordered.OrderN.ordNR {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x y : α} : x ≼ₒ{n} y → x ≼ₒ*{n} y

theorem Iris.Ordered.Order.ordR {α : Type u_1} [OFE α] [Ordered α] {x y : α} : x ≼ₒ y → x ≼ₒ* y

theorem Iris.Ordered.OrderNR.rfl {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x : α} : x ≼ₒ*{n} x

theorem Iris.Ordered.OrderR.rfl {α : Type u_1} [OFE α] [Ordered α] {x : α} : x ≼ₒ* x

theorem Iris.Ordered.OrderNR.ne {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x x' y y' : α} (ex : OFE.Dist n x x') (ey : OFE.Dist n y y') : x ≼ₒ*{n} y → x' ≼ₒ*{n} y'

theorem Iris.Ordered.OrderNR.succ {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x y : α} : x ≼ₒ*{n.succ} y → x ≼ₒ*{n} y

theorem Iris.Ordered.OrderNR.trans {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x y z : α} : x ≼ₒ*{n} y → y ≼ₒ*{n} z → x ≼ₒ*{n} z

theorem Iris.Ordered.OrderR.trans {α : Type u_1} [OFE α] [Ordered α] {x y z : α} : x ≼ₒ* y → y ≼ₒ* z → x ≼ₒ* z

theorem Iris.Ordered.OrderR.ordNR {α : Type u_1} [OFE α] [Ordered α] (n : Nat) {x y : α} : x ≼ₒ* y → x ≼ₒ*{n} y

class Iris.OrderRefl (α : Type u_1) [OFE α] [Ordered α] : Prop

Reflexivity of the order: the order law of unital algebras (UORA), also enjoyed by total algebras under their extension inclusion.

• ord_refl (x : α) : x ≼ₒ x

class Iris.Increasing {α : Type u_1} [OFE α] [Op α] [Ordered α] (x : α) : Prop

An element x is increasing if composing with it never shrinks a resource. Cores and units are increasing; in an affine algebra every element is.

• increasing (y : α) : y ≼ₒ x • y

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

The step-indexed extension inclusion: y is x composed with some frame. This is the inclusion of classical resource algebras.

Equations

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

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

The step-indexed extension inclusion: y is x composed with some frame. This is the inclusion of classical resource algebras.

Equations

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

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

The extension inclusion: y is x composed with some frame.

Equations

• (x ≼ y) = ∃ (z : α), y = x • z

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

The extension inclusion: y is x composed with some frame.

Equations

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

class Iris.IncOrd (α : Type u_1) [OFE α] [Op α] [Ordered α] : Prop

The extension inclusion is contained in the order: every element is increasing.

• inc_ord {x y : α} : x ≼ y → x ≼ₒ y

@[reducible]

def Iris.ORA.Affine (α : Type u_1) [OFE α] [Op α] [Ordered α] : Prop

An algebra is affine when extension inclusion implies its resource order.

Equations

• Iris.ORA.Affine α = Iris.IncOrd α

class Iris.OrdInc (α : Type u_1) [OFE α] [Op α] [Ordered α] : Prop

The order is contained in the extension inclusion: every ordered pair has a frame.

• ord_inc {x y : α} : x ≼ₒ y → x ≼ y
• ordN_incN {n : Nat} {x y : α} : x ≼ₒ{n} y → x ≼{n} y

class Iris.IsInc (α : Type u_1) [OFE α] [Op α] [Ordered α] extends Iris.IncOrd α, Iris.OrdInc α : Prop

The order is the extension inclusion.

• inc_ord {x y : α} : x ≼ y → x ≼ₒ y
• ord_inc {x y : α} : x ≼ₒ y → x ≼ y
• ordN_incN {n : Nat} {x y : α} : x ≼ₒ{n} y → x ≼{n} y

theorem Iris.IncOrd.increasing {α : Type u_1} [OFE α] [Op α] [Ordered α] [IncOrd α] (x : α) : Increasing x

theorem Iris.IncOrd.of_increasing {α : Type u_1} [OFE α] [Op α] [Ordered α] (h : ∀ (x : α), Increasing x) : IncOrd α

instance Iris.instIncreasingOfIncOrd {α : Type u_1} [OFE α] [Op α] [Ordered α] [IncOrd α] (x : α) : Increasing x

theorem Iris.inc_iff_ord {α : Type u_1} [OFE α] [Op α] [Ordered α] [IncOrd α] [OrdInc α] {x y : α} : x ≼ y ↔ x ≼ₒ y

theorem Iris.IncOrd.incN_ordN {α : Type u_1} [OFE α] [Op α] [Ordered α] [IncOrd α] {n : Nat} {x y : α} : x ≼{n} y → x ≼ₒ{n} y

theorem Iris.incN_iff_ordN {α : Type u_1} [OFE α] [Op α] [Ordered α] [IncOrd α] [OrdInc α] {n : Nat} {x y : α} : x ≼{n} y ↔ x ≼ₒ{n} y

Order-free theory

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

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

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

theorem Iris.ORA.validN_of_le {α : Type u_1} [OFE α] [Validity α] {n n' : Nat} {x : α} (le : n' ≤ n) : ✓{n} x → ✓{n'} x

theorem Iris.ORA.validN_of_lt {α : Type u_1} [OFE α] [Validity α] {n n' : Nat} {x : α} (lt : n' < n) : ✓{n} x → ✓{n'} x

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

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

A resource equal to its own partial core.

• core_id : pcore x = some x

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

theorem Iris.ORA.core_eqv_self {α : Type u_1} [OFE α] [PCore α] (x : α) [CoreId x] : core x = x

class Iris.ORA.Exclusive {α : Type u_1} [OFE α] [Op α] [Validity α] (x : α) : Prop

A resource that cannot be composed validly with any further resource.

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

class Iris.ORA.Cancelable {α : Type u_1} [OFE α] [Op α] [Validity α] (x : α) : Prop

A resource cancellable from valid compositions at each step index.

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

class Iris.ORA.IdFree {α : Type u_1} [OFE α] [Op α] [Validity α] (x : α) : Prop

A valid resource that cannot absorb a right factor at index zero.

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

Op

theorem Iris.ORA.op_right_dist {α : Type u_1} [OFE α] [Op α] {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} [OFE α] [Op α] {n : Nat} {x y z : α} : Dist n y z → Dist n (x • y) (x • z)

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

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

theorem Iris.ORA.op_left_dist {α : Type u_1} [OFE α] [Op α] {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} [OFE α] [Op α] {n : Nat} {x y z : α} : Dist n x y → Dist n (x • z) (y • z)

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

theorem Iris.OFE.Dist.opM {α : Type u_1} [OFE α] [Op α] {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.ORA.opM_left_dist {α : Type u_1} [OFE α] [Op α] {n : Nat} {x y : α} (z : Option α) (e : OFE.Dist n x y) : OFE.Dist n (x •? z) (y •? z)

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

instance Iris.ORA.cmra_op_ne2 {α : Type u_1} [OFE α] [Op α] : OFE.NonExpansive₂ op

instance Iris.ORA.instNonExpansive₂OptionOptionalOp {α : Type u_1} [OFE α] [Op α] : OFE.NonExpansive₂ optionalOp

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

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

theorem Iris.ORA.incN_ne {α : Type u_1} [OFE α] [Op α] {n : Nat} {x x' y y' : α} (ex : OFE.Dist n x x') (ey : OFE.Dist n y y') : x ≼{n} y → x' ≼{n} y'

theorem Iris.ORA.incN_of_incN_of_dist {α : Type u_1} [OFE α] [Op α] {n : Nat} {a b c : α} (h : a ≼{n} b) (e : OFE.Dist n b c) : a ≼{n} c

@[instance_reducible]

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

Equations

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

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

@[instance_reducible]

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

Equations

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

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

theorem Iris.ORA.incN_iff_left {α : Type u_1} [OFE α] [Op α] {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} [OFE α] [Op α] {n : Nat} {a b c : α} : Dist n a b → (a ≼{n} c ↔ b ≼{n} c)

theorem Iris.ORA.incN_iff_right {α : Type u_1} [OFE α] [Op α] {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} [OFE α] [Op α] {n : Nat} {b c a : α} : Dist n b c → (a ≼{n} b ↔ a ≼{n} c)

theorem Iris.ORA.incN_dist_iff {α : Type u_1} [OFE α] [Op α] {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} [OFE α] [Op α] {n : Nat} {a a' b b' : α} : Dist n a a' → Dist n b b' → (a ≼{n} b ↔ a' ≼{n} b')

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

@[instance_reducible]

instance Iris.ORA.instTransIncluded {α : Type u_1} [OFE α] [Op α] : Trans Included Included Included

Equations

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

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

@[instance_reducible]

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[reducible]

def Iris.ORA.extOrdered {α : Type u_1} [OFE α] [Op α] : Ordered α

Equip a resource operation with its extension-inclusion order.

Equations

• Iris.ORA.extOrdered = { OrderN := Iris.IncludedN, Order := Iris.Included, ordN_ne := ⋯, ordN_succ := ⋯, ordN_trans := ⋯, ord_trans := ⋯, ordN_of_ord := ⋯ }

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

theorem Iris.ORA.incN_map {α : Type u_2} [OFE α] [Op α] {β : Type u_1} [OFE β] [Op β] (f : α → β) [OFE.NonExpansive f] (hop : ∀ (x y : α), f (x • y) = f x • f y) {n : Nat} {x y : α} : x ≼{n} y → f x ≼{n} f y

theorem Iris.ORA.inc_map {α : Type u_2} [OFE α] [Op α] {β : Type u_1} [OFE β] [Op β] (f : α → β) (hop : ∀ (x y : α), f (x • y) = f x • f y) {x y : α} : x ≼ y → f x ≼ f y

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

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

theorem Iris.ORA.inc_of_inc0 {α : Type u_1} [OFE α] [Op α] [OFE.Discrete α] {x y : α} : x ≼{0} y → x ≼ y

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

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

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

theorem Iris.ORA.not_valid_excl_op_left {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} [Exclusive x] {y : α} : ¬✓ x • y

theorem Iris.ORA.not_excl_op_right {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} [Exclusive x] {y : α} : ¬✓ y • x

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

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

theorem Iris.ORA.not_valid_of_excl_inc {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} [Exclusive x] {y : α} : x ≼ y → ¬✓ y

theorem Iris.ORA.cancelable {α : Type u_1} [OFE α] [Op α] [Validity α] {x y z : α} [Cancelable x] (v : ✓ x • y) (e : x • y = x • z) : y = z

instance Iris.ORA.exclusive_cancelable {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} [Exclusive x] : Cancelable x

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

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

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

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

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

theorem Iris.ORA.id_free_r {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} [IdFree x] {y : α} (v : ✓ x) : ¬x • y = x

theorem Iris.ORA.id_free_l {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} [IdFree x] {y : α} (v : ✓ x) : ¬y • x = x

instance Iris.ORA.exclusive_idFree {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} [Exclusive x] : IdFree x

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

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

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

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

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

theorem Iris.ORA.coreId_iff_core_eqv_self {α : Type u_1} [OFE α] [PCore α] [IsTotal α] {x : α} : CoreId x ↔ core x = x

theorem Iris.ORA.core_idem {α : Type u_1} [OFE α] [PCore α] [IsTotal α] (x : α) : core (core x) = core x

Ordered resource algebras

class Iris.ORA (α : Type u_1) extends Iris.OFE α, Iris.Op α, Iris.PCore α, Iris.Validity α, Iris.Ordered α : Type u_1

An ordered resource algebra: composition, core and validity together with the laws relating them, and a step-indexed order that they respect. The order is neither required to be reflexive (OrderRefl) nor to contain the extension inclusion (IncOrd).

• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• eq_dist' {x y : α} : 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
• op : α → α → α
• op_ne {x : α} : OFE.NonExpansive (op x)
• assoc {x y z : α} : x • (y • z) = (x • y) • z
• comm {x y : α} : x • y = y • x
• pcore : α → Option α
• 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
• pcore_idem {x cx : α} : pcore x = some cx → pcore cx = some cx
• ValidN : Nat → α → Prop
• Valid : α → Prop
• 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
• OrderN : Nat → α → α → Prop
• Order : α → α → Prop
• ordN_ne {n : Nat} {x x' y y' : α} : OFE.Dist n x x' → OFE.Dist n y y' → x ≼ₒ{n} y → x' ≼ₒ{n} y'
• ordN_succ {n : Nat} {x y : α} : x ≼ₒ{n.succ} y → x ≼ₒ{n} y
• ordN_trans {n : Nat} {x y z : α} : x ≼ₒ{n} y → y ≼ₒ{n} z → x ≼ₒ{n} z
• ord_trans {x y z : α} : x ≼ₒ y → y ≼ₒ z → x ≼ₒ z
• ordN_of_ord {x y : α} (n : Nat) : x ≼ₒ y → x ≼ₒ{n} y
• validN_op_left {n : Nat} {x y : α} : ✓{n} x • y → ✓{n} x
• pcore_op_left {x cx : α} : pcore x = some cx → cx • x = x
• extend {n : Nat} {x y₁ y₂ : α} : ✓{n} x → OFE.Dist n x (y₁ • y₂) → (z₁ : α) ×' (z₂ : α) ×' x = z₁ • z₂ ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂

  Split a valid resource into factors matching an approximate decomposition.

• op_monoN_left_ord {n : Nat} {x y : α} (z : α) : x ≼ₒ{n} y → x • z ≼ₒ{n} y • z
• op_mono_left_ord {x y : α} (z : α) : x ≼ₒ y → x • z ≼ₒ y • z
• validN_of_ordN {n : Nat} {x y : α} : x ≼ₒ{n} y → ✓{n} y → ✓{n} x
• pcore_monoN_ord {n : Nat} {x y cx : α} : x ≼ₒ{n} y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ{n} cy
• pcore_mono_ord {x y cx : α} : x ≼ₒ y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ cy
• pcore_order_op {x cx : α} : pcore x = some cx → ∀ (y : α), ∃ (cxy : α), pcore (x • y) = some cxy ∧ cx ≼ₒ cxy
• pcore_increasing {x cx : α} : pcore x = some cx → Increasing cx
• increasing_closed {n : Nat} {x y : α} : Increasing x → x ≼ₒ*{n} y → Increasing y
• ordN_extend {n : Nat} {x y : α} : ✓{n} y → x ≼ₒ{n} y → ∃ (z : α), z ≼ₒ{n.succ} y ∧ OFE.Dist n z x

Validity

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

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

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

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

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

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

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

Core

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

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

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

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

theorem Iris.ORA.op_self {α : Type u_1} [ORA α] (x : α) [CoreId x] : x • x = x

Total cores

theorem Iris.ORA.op_core {α : Type u_1} [ORA α] [IsTotal α] (x : α) : x • core x = x

theorem Iris.ORA.core_op {α : Type u_1} [ORA α] [IsTotal α] (x : α) : core x • x = x

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

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

theorem Iris.ORA.core_op_core {α : Type u_1} [ORA α] [IsTotal α] {x : α} : core x • core x = core x

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

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

instance Iris.ORA.instOrderReflOfIsTotal {α : Type u_1} [ORA α] [IsTotal α] : OrderRefl α

Discrete elements

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

The extension inclusion

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

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

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

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

theorem Iris.ORA.op_core_right_of_inc {α : Type u_1} [ORA α] {x y : α} [CoreId x] : x ≼ y → x • y = y

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

theorem Iris.ORA.incN_extend {α : Type u_1} [ORA α] {n : Nat} {x y : α} (v : ✓{n} y) : x ≼{n} y → ∃ (z : α), z ≼{n.succ} y ∧ OFE.Dist n z x

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

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

theorem Iris.ORA.incN_of_dist {α : Type u_1} [ORA α] [IsTotal α] {n : Nat} {x y : α} (h : OFE.Dist n x y) : x ≼{n} y

theorem Iris.OFE.Dist.to_incN {α : Type u_1} [ORA α] [IsTotal α] {n : Nat} {x y : α} : Dist n x y → x ≼{n} y

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

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

class Iris.CMRAData (α : Type u_1) [OFE α] extends Iris.Op α, Iris.PCore α, Iris.Validity α : Type u_1

A classical resource algebra: composition, core and validity together with the laws relating them, and the monotonicity of the partial core along frames. It is not itself an ordered resource algebra; ORA.ofCMRAData makes one of it, taking the order to be the extension inclusion.

• op : α → α → α
• op_ne {x : α} : OFE.NonExpansive (op x)
• assoc {x y z : α} : x • (y • z) = (x • y) • z
• comm {x y : α} : x • y = y • x
• pcore : α → Option α
• 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
• pcore_idem {x cx : α} : pcore x = some cx → pcore cx = some cx
• ValidN : Nat → α → Prop
• Valid : α → Prop
• 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
• pcore_op_left {x cx : α} : PCore.pcore x = some cx → cx • x = x
• extend {n : Nat} {x y₁ y₂ : α} : ✓{n} x → OFE.Dist n x (y₁ • y₂) → (z₁ : α) ×' (z₂ : α) ×' x = z₁ • z₂ ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂

  Decompose a valid classical resource along an approximate composition.

• pcore_op_mono {x cx : α} : PCore.pcore x = some cx → ∀ (y : α), ∃ (cy : α), PCore.pcore (x • y) = some (cx • cy)

theorem Iris.CMRAData.pcore_op_mono_of_pcore_mono {α : Type u_1} [OFE α] [Op α] [PCore α] (h : ∀ {x y cx : α}, x ≼ y → PCore.pcore x = some cx → ∃ (cy : α), PCore.pcore y = some cy ∧ cx ≼ cy) {x cx : α} (e : PCore.pcore x = some cx) (y : α) : ∃ (cy : α), PCore.pcore (x • y) = some (cx • cy)

The frame law follows from monotonicity of the partial core along the extension inclusion, the form of the law in Iris-Rocq (cmra_pcore_mono).

theorem Iris.CMRAData.pcore_op_mono_of_core_mono {α : Type u_1} [OFE α] [Op α] [PCore α] [IsTotal α] (h : ∀ (x y : α), x ≼ y → PCore.core x ≼ PCore.core y) {x cx : α} (e : PCore.pcore x = some cx) (y : α) : ∃ (cy : α), PCore.pcore (x • y) = some (cx • cy)

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

theorem Iris.CMRAData.incN_extend {α : Type u_1} [OFE α] [CMRAData α] {n : Nat} {x y : α} (v : ✓{n} y) : x ≼{n} y → ∃ (z : α), z ≼{n.succ} y ∧ OFE.Dist n z x

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

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

theorem Iris.CMRAData.pcore_monoN {α : Type u_1} [OFE α] [CMRAData α] {n : Nat} {x y cx : α} (h : x ≼{n} y) (e : PCore.pcore x = some cx) : ∃ (cy : α), PCore.pcore y = some cy ∧ cx ≼{n} cy

theorem Iris.CMRAData.core_incN_core {α : Type u_1} [OFE α] [CMRAData α] [IsTotal α] {n : Nat} {x y : α} (le : x ≼{n} y) : PCore.core x ≼{n} PCore.core y

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

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

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

theorem Iris.CMRAData.increasing {α : Type u_1} [OFE α] [CMRAData α] (x : α) : Increasing x

instance Iris.CMRAData.instOrderRefl {α : Type u_1} [OFE α] [CMRAData α] [IsTotal α] : OrderRefl α

@[reducible]

def Iris.CMRAData.toORA {α : Type u_1} [OFE α] [CMRAData α] : ORA α

Give classical resource algebra data its extension-inclusion order.

Equations

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

theorem Iris.CMRAData.isInc {α : Type u_1} [OFE α] [CMRAData α] : IsInc α

class Iris.CMRA (α : Type u_1) extends Iris.ORA α, Iris.IsInc α : Type u_1

An ordered resource algebra whose order is exactly extension inclusion.

• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• eq_dist' {x y : α} : 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
• op : α → α → α
• op_ne {x : α} : OFE.NonExpansive (op x)
• assoc {x y z : α} : x • (y • z) = (x • y) • z
• comm {x y : α} : x • y = y • x
• pcore : α → Option α
• 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
• pcore_idem {x cx : α} : pcore x = some cx → pcore cx = some cx
• ValidN : Nat → α → Prop
• Valid : α → Prop
• 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
• OrderN : Nat → α → α → Prop
• Order : α → α → Prop
• ordN_ne {n : Nat} {x x' y y' : α} : OFE.Dist n x x' → OFE.Dist n y y' → x ≼ₒ{n} y → x' ≼ₒ{n} y'
• ordN_succ {n : Nat} {x y : α} : x ≼ₒ{n.succ} y → x ≼ₒ{n} y
• ordN_trans {n : Nat} {x y z : α} : x ≼ₒ{n} y → y ≼ₒ{n} z → x ≼ₒ{n} z
• ord_trans {x y z : α} : x ≼ₒ y → y ≼ₒ z → x ≼ₒ z
• ordN_of_ord {x y : α} (n : Nat) : x ≼ₒ y → x ≼ₒ{n} y
• validN_op_left {n : Nat} {x y : α} : ✓{n} x • y → ✓{n} x
• pcore_op_left {x cx : α} : pcore x = some cx → cx • x = x
• extend {n : Nat} {x y₁ y₂ : α} : ✓{n} x → OFE.Dist n x (y₁ • y₂) → (z₁ : α) ×' (z₂ : α) ×' x = z₁ • z₂ ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂
• op_monoN_left_ord {n : Nat} {x y : α} (z : α) : x ≼ₒ{n} y → x • z ≼ₒ{n} y • z
• op_mono_left_ord {x y : α} (z : α) : x ≼ₒ y → x • z ≼ₒ y • z
• validN_of_ordN {n : Nat} {x y : α} : x ≼ₒ{n} y → ✓{n} y → ✓{n} x
• pcore_monoN_ord {n : Nat} {x y cx : α} : x ≼ₒ{n} y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ{n} cy
• pcore_mono_ord {x y cx : α} : x ≼ₒ y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ cy
• pcore_order_op {x cx : α} : pcore x = some cx → ∀ (y : α), ∃ (cxy : α), pcore (x • y) = some cxy ∧ cx ≼ₒ cxy
• pcore_increasing {x cx : α} : pcore x = some cx → Increasing cx
• increasing_closed {n : Nat} {x y : α} : Increasing x → x ≼ₒ*{n} y → Increasing y
• ordN_extend {n : Nat} {x y : α} : ✓{n} y → x ≼ₒ{n} y → ∃ (z : α), z ≼ₒ{n.succ} y ∧ OFE.Dist n z x
• inc_ord {x y : α} : x ≼ y → x ≼ₒ y
• ord_inc {x y : α} : x ≼ₒ y → x ≼ y
• ordN_incN {n : Nat} {x y : α} : x ≼ₒ{n} y → x ≼{n} y

@[instance_reducible, instance 100]

instance Iris.CMRA.ofIsInc {α : Type u_1} [ORA α] [IsInc α] : CMRA α

Equations

• Iris.CMRA.ofIsInc = { toORA := inst✝¹, toIsInc := inst✝ }

@[reducible]

def Iris.ORA.ofCMRAData {α : Type u_1} [OFE α] (d : CMRAData α) : CMRA α

Construct a classical ordered resource algebra from its operation and core.

Equations

• Iris.ORA.ofCMRAData d = { toORA := Iris.CMRAData.toORA, toIsInc := ⋯ }

theorem Iris.CMRA.ord_of_ord0 {α : Type u_1} [CMRA α] [OFE.Discrete α] {x y : α} (h : x ≼ₒ{0} y) : x ≼ₒ y

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

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

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

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

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

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

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

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

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

Discrete and affine algebras

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

An algebra with discrete equivalence, validity, and resource order.

• discrete_0 {x y : α} : Dist 0 x y → x = y
• discrete_valid {x : α} : ✓{0} x → ✓ x
• discrete_ord {x y : α} : x ≼ₒ{0} y → x ≼ₒ y

Unital algebras

class Iris.UORA (α : Type u_1) extends Iris.ORA α, Iris.OrderRefl α : Type u_1

A unital ordered resource algebra: an ordered resource algebra with a unit, whose order is reflexive.

• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• eq_dist' {x y : α} : 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
• op : α → α → α
• op_ne {x : α} : OFE.NonExpansive (op x)
• assoc {x y z : α} : x • (y • z) = (x • y) • z
• comm {x y : α} : x • y = y • x
• pcore : α → Option α
• 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
• pcore_idem {x cx : α} : pcore x = some cx → pcore cx = some cx
• ValidN : Nat → α → Prop
• Valid : α → Prop
• 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
• OrderN : Nat → α → α → Prop
• Order : α → α → Prop
• ordN_ne {n : Nat} {x x' y y' : α} : OFE.Dist n x x' → OFE.Dist n y y' → x ≼ₒ{n} y → x' ≼ₒ{n} y'
• ordN_succ {n : Nat} {x y : α} : x ≼ₒ{n.succ} y → x ≼ₒ{n} y
• ordN_trans {n : Nat} {x y z : α} : x ≼ₒ{n} y → y ≼ₒ{n} z → x ≼ₒ{n} z
• ord_trans {x y z : α} : x ≼ₒ y → y ≼ₒ z → x ≼ₒ z
• ordN_of_ord {x y : α} (n : Nat) : x ≼ₒ y → x ≼ₒ{n} y
• validN_op_left {n : Nat} {x y : α} : ✓{n} x • y → ✓{n} x
• pcore_op_left {x cx : α} : pcore x = some cx → cx • x = x
• extend {n : Nat} {x y₁ y₂ : α} : ✓{n} x → OFE.Dist n x (y₁ • y₂) → (z₁ : α) ×' (z₂ : α) ×' x = z₁ • z₂ ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂
• op_monoN_left_ord {n : Nat} {x y : α} (z : α) : x ≼ₒ{n} y → x • z ≼ₒ{n} y • z
• op_mono_left_ord {x y : α} (z : α) : x ≼ₒ y → x • z ≼ₒ y • z
• validN_of_ordN {n : Nat} {x y : α} : x ≼ₒ{n} y → ✓{n} y → ✓{n} x
• pcore_monoN_ord {n : Nat} {x y cx : α} : x ≼ₒ{n} y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ{n} cy
• pcore_mono_ord {x y cx : α} : x ≼ₒ y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ cy
• pcore_order_op {x cx : α} : pcore x = some cx → ∀ (y : α), ∃ (cxy : α), pcore (x • y) = some cxy ∧ cx ≼ₒ cxy
• pcore_increasing {x cx : α} : pcore x = some cx → Increasing cx
• increasing_closed {n : Nat} {x y : α} : Increasing x → x ≼ₒ*{n} y → Increasing y
• ordN_extend {n : Nat} {x y : α} : ✓{n} y → x ≼ₒ{n} y → ∃ (z : α), z ≼ₒ{n.succ} y ∧ OFE.Dist n z x
• ord_refl (x : α) : x ≼ₒ x
• unit : α

  The unit resource.

• unit_valid : ✓ unit
• unit_left_id {x : α} : unit • x = x
• pcore_unit : PCore.pcore unit = some unit

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

The unit of a classical unital resource algebra; the input of UORA.ofUCMRAData.

• unit : α

  The proposed unit of a classical resource algebra.

• unit_valid : ✓ unit
• unit_left_id {x : α} : unit • x = x
• pcore_unit : PCore.pcore unit = some unit

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

A classical resource algebra equipped with a unit.

• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• eq_dist' {x y : α} : 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
• op : α → α → α
• op_ne {x : α} : OFE.NonExpansive (op x)
• assoc {x y z : α} : x • (y • z) = (x • y) • z
• comm {x y : α} : x • y = y • x
• pcore : α → Option α
• 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
• pcore_idem {x cx : α} : pcore x = some cx → pcore cx = some cx
• ValidN : Nat → α → Prop
• Valid : α → Prop
• 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
• OrderN : Nat → α → α → Prop
• Order : α → α → Prop
• ordN_ne {n : Nat} {x x' y y' : α} : OFE.Dist n x x' → OFE.Dist n y y' → x ≼ₒ{n} y → x' ≼ₒ{n} y'
• ordN_succ {n : Nat} {x y : α} : x ≼ₒ{n.succ} y → x ≼ₒ{n} y
• ordN_trans {n : Nat} {x y z : α} : x ≼ₒ{n} y → y ≼ₒ{n} z → x ≼ₒ{n} z
• ord_trans {x y z : α} : x ≼ₒ y → y ≼ₒ z → x ≼ₒ z
• ordN_of_ord {x y : α} (n : Nat) : x ≼ₒ y → x ≼ₒ{n} y
• validN_op_left {n : Nat} {x y : α} : ✓{n} x • y → ✓{n} x
• pcore_op_left {x cx : α} : pcore x = some cx → cx • x = x
• extend {n : Nat} {x y₁ y₂ : α} : ✓{n} x → OFE.Dist n x (y₁ • y₂) → (z₁ : α) ×' (z₂ : α) ×' x = z₁ • z₂ ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂
• op_monoN_left_ord {n : Nat} {x y : α} (z : α) : x ≼ₒ{n} y → x • z ≼ₒ{n} y • z
• op_mono_left_ord {x y : α} (z : α) : x ≼ₒ y → x • z ≼ₒ y • z
• validN_of_ordN {n : Nat} {x y : α} : x ≼ₒ{n} y → ✓{n} y → ✓{n} x
• pcore_monoN_ord {n : Nat} {x y cx : α} : x ≼ₒ{n} y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ{n} cy
• pcore_mono_ord {x y cx : α} : x ≼ₒ y → pcore x = some cx → ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ cy
• pcore_order_op {x cx : α} : pcore x = some cx → ∀ (y : α), ∃ (cxy : α), pcore (x • y) = some cxy ∧ cx ≼ₒ cxy
• pcore_increasing {x cx : α} : pcore x = some cx → Increasing cx
• increasing_closed {n : Nat} {x y : α} : Increasing x → x ≼ₒ*{n} y → Increasing y
• ordN_extend {n : Nat} {x y : α} : ✓{n} y → x ≼ₒ{n} y → ∃ (z : α), z ≼ₒ{n.succ} y ∧ OFE.Dist n z x
• inc_ord {x y : α} : x ≼ y → x ≼ₒ y
• ord_inc {x y : α} : x ≼ₒ y → x ≼ y
• ordN_incN {n : Nat} {x y : α} : x ≼ₒ{n} y → x ≼{n} y
• ord_refl (x : α) : x ≼ₒ x
• unit : α
• unit_valid : ✓ UCMRA.unit
• unit_left_id {x : α} : UCMRA.unit • x = x
• pcore_unit : PCore.pcore UCMRA.unit = some UCMRA.unit

@[instance_reducible, instance 100]

instance Iris.UCMRA.ofIsInc {α : Type u_1} [UORA α] [IsInc α] : UCMRA α

Equations

• Iris.UCMRA.ofIsInc = { toCMRA := Iris.CMRA.ofIsInc, toOrderRefl := ⋯, unit := Iris.UORA.unit, unit_valid := ⋯, unit_left_id := ⋯, pcore_unit := ⋯ }

@[reducible]

def Iris.UORA.ofUCMRAData {α : Type u_1} [CMRA α] (d : UCMRAData α) : UCMRA α

Add a specified unit to a classical resource algebra.

Equations

• Iris.UORA.ofUCMRAData d = { toCMRA := inst✝, toOrderRefl := ⋯, unit := Iris.UCMRAData.unit, unit_valid := ⋯, unit_left_id := ⋯, pcore_unit := ⋯ }

class Iris.IsUnit {α : Type u_1} [OFE α] [Op α] [PCore α] [Validity α] (ε : α) : Prop

The laws asserting that a specified resource is a valid unit with itself as core.

• unit_valid : ✓ ε
• unit_left_id {x : α} : ε • x = x
• pcore_unit : PCore.pcore ε = some ε

instance Iris.instIsUnitUnit {α : Type u_1} [UORA α] : IsUnit UORA.unit

Order

theorem Iris.ORA.ordN_of_ordN_of_dist {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {a b c : α} (h : a ≼ₒ{n} b) (e : OFE.Dist n b c) : a ≼ₒ{n} c

@[instance_reducible]

instance Iris.ORA.instTransOrderNDist {α : Type u_1} [OFE α] [Ordered α] {n : Nat} : Trans (OrderN n) (OFE.Dist n) (OrderN n)

Equations

• Iris.ORA.instTransOrderNDist = { trans := ⋯ }

theorem Iris.ORA.ordN_of_dist_of_ordN {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {a b c : α} (e : OFE.Dist n a b) (h : b ≼ₒ{n} c) : a ≼ₒ{n} c

@[instance_reducible]

instance Iris.ORA.instTransDistOrderN {α : Type u_1} [OFE α] [Ordered α] {n : Nat} : Trans (OFE.Dist n) (OrderN n) (OrderN n)

Equations

• Iris.ORA.instTransDistOrderN = { trans := ⋯ }

theorem Iris.Ordered.Order.ordN {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x y : α} : x ≼ₒ y → x ≼ₒ{n} y

theorem Iris.ORA.ordN_iff_left {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {a b c : α} (e : OFE.Dist n a b) : a ≼ₒ{n} c ↔ b ≼ₒ{n} c

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

theorem Iris.ORA.ordN_iff_right {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {b c a : α} (e : OFE.Dist n b c) : a ≼ₒ{n} b ↔ a ≼ₒ{n} c

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

theorem Iris.ORA.ordN_dist_iff {α : Type u_1} [OFE α] [Ordered α] {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.ordN {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {a a' b b' : α} : Dist n a a' → Dist n b b' → (a ≼ₒ{n} b ↔ a' ≼ₒ{n} b')

theorem Iris.Ordered.Order.trans {α : Type u_1} [OFE α] [Ordered α] {x y z : α} : x ≼ₒ y → y ≼ₒ z → x ≼ₒ z

@[instance_reducible]

instance Iris.ORA.instTransOrder {α : Type u_1} [OFE α] [Ordered α] : Trans Order Order Order

Equations

• Iris.ORA.instTransOrder = { trans := ⋯ }

theorem Iris.Ordered.OrderN.trans {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x y z : α} : x ≼ₒ{n} y → y ≼ₒ{n} z → x ≼ₒ{n} z

@[instance_reducible]

instance Iris.ORA.instTransOrderN {α : Type u_1} [OFE α] [Ordered α] {n : Nat} : Trans (OrderN n) (OrderN n) (OrderN n)

Equations

• Iris.ORA.instTransOrderN = { trans := ⋯ }

theorem Iris.ORA.ordN_of_ordN_le {α : Type u_1} [OFE α] [Ordered α] {n n' : Nat} {x y : α} (l1 : n' ≤ n) : x ≼ₒ{n} y → x ≼ₒ{n'} y

theorem Iris.ORA.ord0_of_ordN {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x y : α} : x ≼ₒ{n} y → x ≼ₒ{0} y

theorem Iris.Ordered.OrderN.le {α : Type u_1} [OFE α] [Ordered α] {n n' : Nat} {x y : α} : n' ≤ n → x ≼ₒ{n} y → x ≼ₒ{n'} y

theorem Iris.Ordered.OrderN.succ {α : Type u_1} [OFE α] [Ordered α] {n : Nat} {x y : α} : x ≼ₒ{n.succ} y → x ≼ₒ{n} y

theorem Iris.ORA.ordN_refl {α : Type u_1} [OFE α] [Ordered α] [OrderRefl α] {n : Nat} (x : α) : x ≼ₒ{n} x

theorem Iris.Ordered.Order.rfl {α : Type u_1} [OFE α] [Ordered α] [OrderRefl α] {x : α} : x ≼ₒ x

theorem Iris.Ordered.OrderN.rfl {α : Type u_1} [OFE α] [Ordered α] [OrderRefl α] {n : Nat} {x : α} : x ≼ₒ{n} x

theorem Iris.ORA.ordN_of_dist {α : Type u_1} [OFE α] [Ordered α] [OrderRefl α] {n : Nat} {x y : α} (h : OFE.Dist n x y) : x ≼ₒ{n} y

theorem Iris.OFE.Dist.to_ordN {α : Type u_1} [OFE α] [Ordered α] [OrderRefl α] {n : Nat} {x y : α} : Dist n x y → x ≼ₒ{n} y

theorem Iris.ORA.valid_of_ord {α : Type u_1} [ORA α] {x y : α} (h : x ≼ₒ y) : ✓ y → ✓ x

theorem Iris.Ordered.OrderN.validN {α : Type u_1} [ORA α] {n : Nat} {x y : α} : x ≼ₒ{n} y → ✓{n} y → ✓{n} x

theorem Iris.ORA.validN_of_ord {α : Type u_1} [ORA α] {n : Nat} {x y : α} (h : x ≼ₒ y) : ✓{n} y → ✓{n} x

theorem Iris.Ordered.Order.validN {α : Type u_1} [ORA α] {n : Nat} {x y : α} : x ≼ₒ y → ✓{n} y → ✓{n} x

theorem Iris.ORA.pcore_monoN_ord' {α : Type u_1} [ORA α] {n : Nat} {x y cx : α} (h : x ≼ₒ{n} y) (e : OFE.Dist n (pcore x) (some cx)) : ∃ (cy : α), pcore y = some cy ∧ cx ≼ₒ{n} cy

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

theorem Iris.ORA.pcore_monoN' {α : Type u_1} [ORA α] [OrdInc α] {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.ORA.pcore_op_mono {α : Type u_1} [ORA α] [OrdInc α] {x cx : α} (e : pcore x = some cx) (y : α) : ∃ (cy : α), pcore (x • y) = some (cx • cy)

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

theorem Iris.ORA.op_mono_right_ord {α : Type u_1} [ORA α] {x y : α} (z : α) (h : x ≼ₒ y) : z • x ≼ₒ z • y

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

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

theorem Iris.ORA.optionalOp_monoN_left_ord {α : Type u_1} [ORA α] {n : Nat} {x y : α} (mz : Option α) (h : x ≼ₒ{n} y) : x •? mz ≼ₒ{n} y •? mz

theorem Iris.ORA.optionalOp_mono_left_ord {α : Type u_1} [ORA α] {x y : α} (mz : Option α) (h : x ≼ₒ y) : x •? mz ≼ₒ y •? mz

theorem Iris.Ordered.OrderNR.op_left {α : Type u_1} [ORA α] {n : Nat} {x y : α} (z : α) : x ≼ₒ*{n} y → x • z ≼ₒ*{n} y • z

theorem Iris.Ordered.OrderR.op_left {α : Type u_1} [ORA α] {x y : α} (z : α) : x ≼ₒ* y → x • z ≼ₒ* y • z

theorem Iris.Ordered.OrderNR.validN {α : Type u_1} [ORA α] {n : Nat} {x y : α} : x ≼ₒ*{n} y → ✓{n} y → ✓{n} x

theorem Iris.Ordered.OrderR.validN {α : Type u_1} [ORA α] {n : Nat} {x y : α} : x ≼ₒ* y → ✓{n} y → ✓{n} x

theorem Iris.ORA.op_extend_ord {α : Type u_1} [ORA α] {n : Nat} {x y₁ y₂ : α} (v : ✓{n} x) (h : y₁ • y₂ ≼ₒ{n} x) : ∃ (z₁ : α), ∃ (z₂ : α), z₁ • z₂ ≼ₒ{n.succ} x ∧ OFE.Dist n z₁ y₁ ∧ OFE.Dist n z₂ y₂

Increasing elements

theorem Iris.Increasing.of_ordNR {α : Type u_1} [ORA α] {n : Nat} {x y : α} (h : Increasing x) (hxy : x ≼ₒ*{n} y) : Increasing y

theorem Iris.Increasing.of_dist {α : Type u_1} [ORA α] {n : Nat} {x y : α} (h : Increasing x) (e : OFE.Dist n x y) : Increasing y

theorem Iris.Increasing.of_ordN {α : Type u_1} [ORA α] {n : Nat} {x y : α} (h : Increasing x) (hxy : x ≼ₒ{n} y) : Increasing y

theorem Iris.Increasing.of_ord {α : Type u_1} [ORA α] {x y : α} (h : Increasing x) (hxy : x ≼ₒ y) : Increasing y

theorem Iris.Increasing.of_ordR {α : Type u_1} [ORA α] {x y : α} (h : Increasing x) : x ≼ₒ* y → Increasing y

theorem Iris.Increasing.ordN {α : Type u_1} [ORA α] {n : Nat} {x : α} (h : Increasing x) (y : α) : y ≼ₒ{n} x • y

instance Iris.Increasing.op {α : Type u_1} [ORA α] (x y : α) [Increasing x] [Increasing y] : Increasing (x • y)

instance Iris.instIncreasingOfCoreId {α : Type u_1} [ORA α] (x : α) [ORA.CoreId x] : Increasing x

theorem Iris.ORA.core_ordN_core {α : Type u_1} [ORA α] [IsTotal α] {n : Nat} {x y : α} (le : x ≼ₒ{n} y) : core x ≼ₒ{n} core y

theorem Iris.ORA.core_mono_ord {α : Type u_1} [ORA α] [IsTotal α] {x y : α} (le : x ≼ₒ y) : core x ≼ₒ core y

theorem Iris.ORA.core_op_mono_ord {α : Type u_1} [ORA α] [IsTotal α] (x y : α) : core x ≼ₒ core (x • y)

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

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

theorem Iris.ORA.core_mono {α : Type u_1} [ORA α] [IsTotal α] [OrdInc α] {x y : α} : x ≼ y → core x ≼ core y

instance Iris.ORA.increasing_core {α : Type u_1} [ORA α] [IsTotal α] (x : α) : Increasing (core x)

Composition with increasing elements

theorem Iris.ORA.ord_op_right {α : Type u_1} [ORA α] (x y : α) [Increasing x] : y ≼ₒ x • y

theorem Iris.ORA.ord_op_left {α : Type u_1} [ORA α] (x y : α) [Increasing y] : x ≼ₒ x • y

theorem Iris.ORA.ordN_op_left {α : Type u_1} [ORA α] (n : Nat) (x y : α) [Increasing y] : x ≼ₒ{n} x • y

theorem Iris.ORA.ordN_op_right {α : Type u_1} [ORA α] (n : Nat) (x y : α) [Increasing x] : y ≼ₒ{n} x • y

theorem Iris.ORA.pcore_ord_self {α : Type u_1} [ORA α] {x cx : α} [Increasing x] (e : pcore x = some cx) : cx ≼ₒ x

theorem Iris.ORA.core_ord_self {α : Type u_1} [ORA α] [IsTotal α] {x : α} [Increasing x] : core x ≼ₒ x

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

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

theorem Iris.ORA.ord_iff_ordN {α : Type u_1} [ORA α] [Discrete α] (n : Nat) {x y : α} : x ≼ₒ y ↔ x ≼ₒ{n} y

theorem Iris.ORA.ord_0_iff_ordN {α : Type u_1} [ORA α] [Discrete α] (n : Nat) {x y : α} : x ≼ₒ{0} y ↔ x ≼ₒ{n} y

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

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

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

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

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

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

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

theorem Iris.ORA.unit_right_id {α : Type u_1} [UORA α] {x : α} : x • unit = x

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

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

theorem Iris.ORA.inc_unit {α : Type u_1} [UORA α] {x : α} : unit ≼ x

instance Iris.ORA.unit_CoreId {α : Type u_1} [UORA α] : CoreId unit

instance Iris.ORA.unit_total {α : Type u_1} [UORA α] : IsTotal α

instance Iris.ORA.empty_cancelable {α : Type u_1} [UORA α] : Cancelable unit

theorem Iris.ORA.increasing_iff_unit_ord {α : Type u_1} [UORA α] {x : α} : Increasing x ↔ unit ≼ₒ x

theorem Iris.ORA.ordN_op_right_of_unit_ordN {α : Type u_1} [UORA α] {n : Nat} {x : α} (y : α) (h : unit ≼ₒ{n} x) : y ≼ₒ{n} x • y

theorem Iris.ORA.unit_ord_core {α : Type u_1} [UORA α] (x : α) : unit ≼ₒ core x

theorem Iris.ORA.unit_ordN_core {α : Type u_1} [UORA α] {n : Nat} (x : α) : unit ≼ₒ{n} core x

theorem Iris.ORA.exists_op_ordN_iff_ordN {α : Type u_1} [UORA α] [IncOrd α] {n : Nat} {x y : α} : (∃ (c : α), x • c ≼ₒ{n} y) ↔ x ≼ₒ{n} y

theorem Iris.ORA.exists_op_ord_iff_ord {α : Type u_1} [UORA α] [IncOrd α] {x y : α} : (∃ (c : α), x • c ≼ₒ y) ↔ x ≼ₒ y

theorem Iris.ORA.exists_op_ordN_iff_incN {α : Type u_1} [UORA α] [OrdInc α] {n : Nat} {x y : α} : (∃ (c : α), x • c ≼ₒ{n} y) ↔ x ≼{n} y

theorem Iris.ORA.exists_op_ord_iff_inc {α : Type u_1} [UORA α] [OrdInc α] {x y : α} : (∃ (c : α), x • c ≼ₒ y) ↔ x ≼ y

theorem Iris.ORA.ordN_unit {α : Type u_1} [UORA α] {n : Nat} {x : α} [Increasing x] : unit ≼ₒ{n} x

theorem Iris.ORA.ord_unit {α : Type u_1} [UORA α] {x : α} [Increasing x] : unit ≼ₒ x

instance Iris.ORA.ucmraMonoidOps {α : Type u_1} [UORA α] : Algebra.MonoidOps op unit

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

A morphism between CMRAs 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 : α) : Option.map self.f (PCore.pcore x) = PCore.pcore (self.f x)
• op (x y : α) : self.f (x • y) = self.f x • self.f y

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

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

• f : α → β
• ne : NonExpansive self.f
• validN {n : Nat} {x : α} : ✓{n} x → ✓{n} self.f x
• pcore (x : α) : Option.map self.f (PCore.pcore x) = PCore.pcore (self.f x)
• op (x y : α) : self.f (x • y) = self.f x • self.f y
• monoN_ord {n : Nat} {x₁ x₂ : α} : x₁ ≼ₒ{n} x₂ → self.f x₁ ≼ₒ{n} self.f x₂
• mono_ord {x₁ x₂ : α} : x₁ ≼ₒ x₂ → self.f x₁ ≼ₒ self.f x₂
• increasing {x : α} : Increasing x → Increasing (self.f x)

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

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

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

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Iris.ORA.instOFEHom = { Dist := fun (n : Nat) (f g : α -C> β) => Iris.OFE.Dist n f.toHom g.toHom, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

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

The identity morphism of an ordered resource algebra.

Equations

• Iris.ORA.Hom.id = { toHom := Iris.OFE.Hom.id, validN := ⋯, pcore := ⋯, op := ⋯, monoN_ord := ⋯, mono_ord := ⋯, increasing := ⋯ }

def Iris.ORA.Hom.comp {α : Type u_1} [ORA α] {β : Type u_2} {γ : Type u_3} [ORA β] [ORA γ] (g : β -C> γ) (f : α -C> β) : α -C> γ

Composition of ordered resource algebra morphisms.

Equations

• g.comp f = { toHom := g.comp f.toHom, validN := ⋯, pcore := ⋯, op := ⋯, monoN_ord := ⋯, mono_ord := ⋯, increasing := ⋯ }

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

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

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

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

@[reducible]

def Iris.CMRA.Hom.toORA {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [OrdInc α] [IncOrd β] (g : Hom α β) : α -C> β

A morphism between classical resource algebras needs only the classical fields: under the extension order, monoN_ord, mono_ord and increasing follow from op.

Equations

• g.toORA = { toCMRAHom := g, monoN_ord := ⋯, mono_ord := ⋯, increasing := ⋯ }

class Iris.RFunctor (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

A mixed-variance family of ordered resource algebras with a non-expansive action.

• cmra {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : ORA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂

  The contravariant and covariant action on non-expansive maps.

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

class Iris.RFunctorContractive (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) extends Iris.RFunctor F : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

A resource functor whose action on morphisms is contractive.

• cmra {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : ORA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
• map_ne {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : OFE.NonExpansive₂ map
• map_id {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] (x : F α β) : (map OFE.Hom.id OFE.Hom.id).f x = x
• map_comp {α₁ α₂ α₃ : Type u_1} {β₁ β₂ β₃ : Type u_2} [COFE α₁] [COFE α₂] [COFE α₃] [COFE β₁] [COFE β₂] [COFE β₃] (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) : (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} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : OFE.Contractive (Function.uncurry RFunctor.map)

@[instance_reducible]

instance Iris.RFunctor.toOFunctor {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [R : RFunctor F] : COFE.OFunctor F

Equations

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

@[instance_reducible]

instance Iris.RFunctorContractive.toOFunctorContractive {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [RFunctorContractive F] : COFE.OFunctorContractive F

Equations

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

class Iris.URFunctor (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

A resource functor whose values are unital ordered resource algebras.

• cmra {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : UORA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂

  The action on morphisms of a unital resource functor.

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

class Iris.URFunctorContractive (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) extends Iris.URFunctor F : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

A unital resource functor with a contractive action on morphisms.

• cmra {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : UORA (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -C> F α₂ β₂
• map_ne {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : OFE.NonExpansive₂ map
• map_id {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] (x : F α β) : (map OFE.Hom.id OFE.Hom.id).f x = x
• map_comp {α₁ α₂ α₃ : Type u_1} {β₁ β₂ β₃ : Type u_2} [COFE α₁] [COFE α₂] [COFE α₃] [COFE β₁] [COFE β₂] [COFE β₃] (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) (x : F α₁ β₁) : (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} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : OFE.Contractive (Function.uncurry URFunctor.map)

class Iris.RFunctorAffine (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [RFunctor F] : Prop

A resource functor whose values have increasing composition.

• affine {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : IncOrd (F α β)

@[instance_reducible]

instance Iris.URFunctor.toRFunctor {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [UF : URFunctor F] : RFunctor F

Equations

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

@[instance_reducible]

instance Iris.URFunctorContractive.toRFunctorContractive {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [URFunctorContractive F] : RFunctorContractive F

Equations

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

theorem Iris.RFunctorContractive.map_distLater {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [RFunctorContractive F] [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] {n : Nat} {f₁ f₂ : α₂ -n> α₁} {g₁ g₂ : β₁ -n> β₂} (hf : OFE.DistLater n f₁ f₂) (hg : OFE.DistLater n g₁ g₂) (x : F α₁ β₁) : OFE.Dist n ((RFunctor.map f₁ g₁).f x) ((RFunctor.map f₂ g₂).f x)

theorem Iris.URFunctorContractive.map_distLater {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [URFunctorContractive F] [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] {n : Nat} {f₁ f₂ : α₂ -n> α₁} {g₁ g₂ : β₁ -n> β₂} (hf : OFE.DistLater n f₁ f₂) (hg : OFE.DistLater n g₁ g₂) (x : F α₁ β₁) : OFE.Dist n ((URFunctor.map f₁ g₁).f x) ((URFunctor.map f₂ g₂).f x)

@[instance_reducible]

instance Iris.rFunctorComposeOF {F₁ : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2} {F₂ : (α β : Type u_3) → [COFE α] → [COFE β] → Type u_1} [COFE.OFunctor F₂] [(α β : Type u_3) → [inst : COFE α] → [inst_1 : COFE β] → IsCOFE (F₂ α β)] [RFunctor F₁] : RFunctor (ComposeOF F₁ F₂)

Equations

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

@[instance_reducible]

instance Iris.urFunctorComposeOF {F₁ : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2} {F₂ : (α β : Type u_3) → [COFE α] → [COFE β] → Type u_1} [COFE.OFunctor F₂] [(α β : Type u_3) → [inst : COFE α] → [inst_1 : COFE β] → IsCOFE (F₂ α β)] [URFunctor F₁] : URFunctor (ComposeOF F₁ F₂)

Equations

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

instance Iris.instRFunctorAffineComposeOF {F₁ : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2} {F₂ : (α β : Type u_3) → [COFE α] → [COFE β] → Type u_1} [COFE.OFunctor F₂] [(α β : Type u_3) → [inst : COFE α] → [inst_1 : COFE β] → IsCOFE (F₂ α β)] [RFunctor F₁] [RFunctorAffine F₁] : RFunctorAffine (ComposeOF F₁ F₂)

@[instance_reducible]

instance Iris.rFunctorComposeOFContractiveLeft {F₁ : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2} {F₂ : (α β : Type u_3) → [COFE α] → [COFE β] → Type u_1} [COFE.OFunctor F₂] [(α β : Type u_3) → [inst : COFE α] → [inst_1 : COFE β] → IsCOFE (F₂ α β)] [RFunctorContractive F₁] : RFunctorContractive (ComposeOF F₁ F₂)

Equations

• Iris.rFunctorComposeOFContractiveLeft = { toRFunctor := Iris.rFunctorComposeOF, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.urFunctorComposeOFContractiveLeft {F₁ : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2} {F₂ : (α β : Type u_3) → [COFE α] → [COFE β] → Type u_1} [COFE.OFunctor F₂] [(α β : Type u_3) → [inst : COFE α] → [inst_1 : COFE β] → IsCOFE (F₂ α β)] [URFunctorContractive F₁] : URFunctorContractive (ComposeOF F₁ F₂)

Equations

• Iris.urFunctorComposeOFContractiveLeft = { toURFunctor := Iris.urFunctorComposeOF, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.rFunctorComposeOFContractiveRight {F₁ : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2} {F₂ : (α β : Type u_3) → [COFE α] → [COFE β] → Type u_1} [COFE.OFunctorContractive F₂] [(α β : Type u_3) → [inst : COFE α] → [inst_1 : COFE β] → IsCOFE (F₂ α β)] [RFunctor F₁] : RFunctorContractive (ComposeOF F₁ F₂)

Equations

• Iris.rFunctorComposeOFContractiveRight = { toRFunctor := Iris.rFunctorComposeOF, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.urFunctorComposeOFContractiveRight {F₁ : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2} {F₂ : (α β : Type u_3) → [COFE α] → [COFE β] → Type u_1} [COFE.OFunctorContractive F₂] [(α β : Type u_3) → [inst : COFE α] → [inst_1 : COFE β] → IsCOFE (F₂ α β)] [URFunctor F₁] : URFunctorContractive (ComposeOF F₁ F₂)

Equations

• Iris.urFunctorComposeOFContractiveRight = { toURFunctor := Iris.urFunctorComposeOF, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.COFE.OFunctor.constOFRFunctor {B : Type u_1} [ORA B] : RFunctor ((fun (B : Type u_1) (A : Type u_2) (C : Type u_3) [COFE A] [COFE C] => B) B)

Equations

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

instance Iris.COFE.OFunctor.constOF_RFunctorAffine {B : Type u_1} [ORA B] [IncOrd B] : RFunctorAffine ((fun (B : Type u_1) (A : Type u_2) (C : Type u_3) [COFE A] [COFE C] => B) B)

@[instance_reducible]

instance Iris.OFunctor.constOFRFunctorContractive {B : Type u_1} [ORA B] : RFunctorContractive ((fun (B : Type u_1) (A : Type u_2) (C : Type u_3) [COFE A] [COFE C] => B) B)

Equations

• Iris.OFunctor.constOFRFunctorContractive = { toRFunctor := Iris.COFE.OFunctor.constOFRFunctor, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.COFE.OFunctor.constOFURFunctor {B : Type u_1} [UORA B] : URFunctor ((fun (B : Type u_1) (A : Type u_2) (C : Type u_3) [COFE A] [COFE C] => B) B)

Equations

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

@[instance_reducible]

instance Iris.OFunctor.constOFURFunctorContractive {B : Type u_1} [UORA B] : URFunctorContractive ((fun (B : Type u_1) (A : Type u_2) (C : Type u_3) [COFE A] [COFE C] => B) B)

Equations

• Iris.OFunctor.constOFURFunctorContractive = { toURFunctor := Iris.COFE.OFunctor.constOFURFunctor, map_contractive := ⋯ }

Transporting a CMRA equality

Rocq bundles a CMRA as a record, so a proof of A = B transports the whole algebra. In Lean ORA is a type class, and an equality of carriers says nothing about the two instances, so the transport lemmas are replaced by transpAp and the OFE.transpAp_* family in Iris.Instances.IProp.Instance, which carry the equality of the instances explicitly.

@[reducible]

def Iris.DiscreteFun.raOrdered {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] : Ordered ((x : α) → β x)

The resource order on dependent functions.

Equations

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

theorem Iris.DiscreteFun.ordNR_apply {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] {n : Nat} {f g : (x : α) → β x} (h : f ≼ₒ*{n} g) (x : α) : f x ≼ₒ*{n} g x

@[reducible]

def Iris.DiscreteFun.raOp {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] : Op ((x : α) → β x)

Composition on dependent functions.

Equations

• Iris.DiscreteFun.raOp = { op := fun (f g : (x : α) → β x) (x : α) => f x • g x, op_ne := ⋯, assoc := ⋯, comm := ⋯ }

@[reducible]

def Iris.DiscreteFun.raPCore {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] : PCore ((x : α) → β x)

The partial core on dependent functions.

Equations

• Iris.DiscreteFun.raPCore = { pcore := fun (f : (x : α) → β x) => some fun (x : α) => Iris.PCore.core (f x), pcore_ne := ⋯, pcore_idem := ⋯ }

@[reducible]

def Iris.DiscreteFun.raValid {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] : Validity ((x : α) → β x)

Validity on dependent functions.

Equations

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

theorem Iris.DiscreteFun.increasing_apply {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] {f : (x : α) → β x} (h : Increasing f) (x : α) : Increasing (f x)

theorem Iris.DiscreteFun.increasing_iff {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] {f : (x : α) → β x} : Increasing f ↔ ∀ (x : α), Increasing (f x)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

theorem Iris.DiscreteFun.op_apply {α : Type u_2} {β : α → Type u_1} [(x : α) → ORA (β x)] (f g : (x : α) → β x) (x : α) : (f • g) x = f x • g x

theorem Iris.DiscreteFun.core_apply {α : Type u_2} {β : α → Type u_1} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] (f : (x : α) → β x) (x : α) : PCore.core f x = PCore.core (f x)

theorem Iris.DiscreteFun.unit_apply {α : Type u_2} {β : α → Type u_1} [(x : α) → UORA (β x)] (x : α) : UORA.unit x = UORA.unit

instance Iris.DiscreteFun.instDiscreteEForallUnit {α : Type u_2} {β : α → Type u_1} [(x : α) → UORA (β x)] [∀ (x : α), OFE.DiscreteE UORA.unit] : OFE.DiscreteE UORA.unit

theorem Iris.DiscreteFun.ord_apply {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] {f g : (x : α) → β x} (h : f ≼ₒ g) (x : α) : f x ≼ₒ g x

theorem Iris.DiscreteFun.ord_iff {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] {f g : (x : α) → β x} : f ≼ₒ g ↔ ∀ (x : α), f x ≼ₒ g x

theorem Iris.DiscreteFun.ordN_iff {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] {n : Nat} {f g : (x : α) → β x} : f ≼ₒ{n} g ↔ ∀ (x : α), f x ≼ₒ{n} g x

theorem Iris.DiscreteFun.inc_apply {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] {f g : (x : α) → β x} : f ≼ g → ∀ (x : α), f x ≼ g x

theorem Iris.DiscreteFun.inc_iff {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] {f g : (x : α) → β x} : f ≼ g ↔ ∀ (x : α), f x ≼ g x

Note: The finiteness assumption from Iris-Rocq is removed using choice.

theorem Iris.DiscreteFun.incN_apply {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] {n : Nat} {f g : (x : α) → β x} : f ≼{n} g → ∀ (x : α), f x ≼{n} g x

theorem Iris.DiscreteFun.incN_iff {α : Type u_1} {β : α → Type u_2} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] {n : Nat} {f g : (x : α) → β x} : f ≼{n} g ↔ ∀ (x : α), f x ≼{n} g x

Note: The finiteness assumption from Iris-Rocq is removed using choice.

instance Iris.DiscreteFun.instOrderRefl {α : Type u_2} {β : α → Type u_1} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] [∀ (x : α), OrderRefl (β x)] : OrderRefl ((x : α) → β x)

instance Iris.DiscreteFun.instIncOrd {α : Type u_2} {β : α → Type u_1} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] [∀ (x : α), IncOrd (β x)] : IncOrd ((x : α) → β x)

instance Iris.DiscreteFun.instOrdInc {α : Type u_2} {β : α → Type u_1} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] [∀ (x : α), OrdInc (β x)] : OrdInc ((x : α) → β x)

instance Iris.DiscreteFun.instIsInc {α : Type u_2} {β : α → Type u_1} [(x : α) → ORA (β x)] [∀ (x : α), IsTotal (β x)] [∀ (x : α), IsInc (β x)] : IsInc ((x : α) → β x)

def Iris.mapCodHomC {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} [(x : α) → UORA (β₁ x)] [(x : α) → UORA (β₂ x)] (F : (x : α) → β₁ x -C> β₂ x) : ((x : α) → β₁ x) -C> (x : α) → β₂ x

Apply a family of resource morphisms pointwise to dependent functions.

Equations

• Iris.mapCodHomC F = { toHom := Iris.OFE.mapCodHom fun (x : α) => (F x).toHom, validN := ⋯, pcore := ⋯, op := ⋯, monoN_ord := ⋯, mono_ord := ⋯, increasing := ⋯ }

@[instance_reducible]

instance Iris.urFunctorDiscreteFunOF {C : Type u_1} (F : C → (α : Type u_2) → (β : Type u_3) → [COFE α] → [COFE β] → Type u_4) [(c : C) → URFunctor (F c)] : URFunctor (DiscreteFunOF F)

Equations

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

instance Iris.instRFunctorAffineDiscreteFunOF {C : Type u_1} (F : C → (α : Type u_2) → (β : Type u_3) → [COFE α] → [COFE β] → Type u_4) [(c : C) → URFunctor (F c)] [∀ (c : C), RFunctorAffine (F c)] : RFunctorAffine (DiscreteFunOF F)

@[instance_reducible]

instance Iris.DiscreteFunOFURFC {C : Type u_1} (F : C → (α : Type u_2) → (β : Type u_3) → [COFE α] → [COFE β] → Type u_4) [HURF : (c : C) → URFunctorContractive (F c)] : URFunctorContractive (DiscreteFunOF F)

Equations

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

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

Lift the partial core to an optional resource.

Equations

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

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

Compose optional resources, taking absence as the unit.

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} [ORA α] (n : Nat) : Option α → Prop

Step-indexed validity of an optional resource; absence is valid.

Equations

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

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

Validity of an optional resource; absence is valid.

Equations

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

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

The step-indexed order on Option α: none lies below none and below every increasing element, some is monotone up to n-equivalence, and nothing but none lies below none.

Equations

• Iris.optionOrderN n none none = True
• Iris.optionOrderN n none (some y) = Iris.Increasing y
• Iris.optionOrderN n (some x_2) (some y) = (x_2 ≼ₒ*{n} y)
• Iris.optionOrderN n (some val) none = False

def Iris.optionOrder {α : Type u_1} [ORA α] : Option α → Option α → Prop

Resource order on optional values, with absence below increasing resources.

Equations

• Iris.optionOrder none none = True
• Iris.optionOrder none (some y) = Iris.Increasing y
• Iris.optionOrder (some x_2) (some y) = (x_2 ≼ₒ* y)
• Iris.optionOrder (some val) none = False

@[reducible]

def Iris.Option.raOp {α : Type u_1} [ORA α] : Op (Option α)

Composition on optional resources.

Equations

• Iris.Option.raOp = { op := Iris.optionOp, op_ne := ⋯, assoc := ⋯, comm := ⋯ }

@[reducible]

def Iris.Option.raPCore {α : Type u_1} [ORA α] : PCore (Option α)

The partial core on optional resources.

Equations

• Iris.Option.raPCore = { pcore := fun (x : Option α) => some (Iris.optionCore x), pcore_ne := ⋯, pcore_idem := ⋯ }

@[reducible]

def Iris.Option.raValid {α : Type u_1} [ORA α] : Validity (Option α)

Validity on optional resources.

Equations

• Iris.Option.raValid = { ValidN := Iris.optionValidN, Valid := Iris.optionValid, validN_ne := ⋯, valid_iff_validN := ⋯, validN_succ := ⋯ }

@[reducible]

def Iris.Option.raOrdered {α : Type u_1} [ORA α] : Ordered (Option α)

The resource order on optional resources.

Equations

• Iris.Option.raOrdered = { OrderN := Iris.optionOrderN, Order := Iris.optionOrder, ordN_ne := ⋯, ordN_succ := ⋯, ordN_trans := ⋯, ord_trans := ⋯, ordN_of_ord := ⋯ }

theorem Iris.Option.some_ordN_some_iff {α : Type u_1} [ORA α] {n : Nat} {a b : α} : some a ≼ₒ{n} some b ↔ OFE.Dist n a b ∨ a ≼ₒ{n} b

theorem Iris.Option.some_ord_some_iff {α : Type u_1} [ORA α] {a b : α} : some a ≼ₒ some b ↔ a = b ∨ a ≼ₒ b

theorem Iris.Option.none_ordN_some_iff {α : Type u_1} [ORA α] {n : Nat} {b : α} : none ≼ₒ{n} some b ↔ Increasing b

theorem Iris.Option.none_ord_some_iff {α : Type u_1} [ORA α] {b : α} : none ≼ₒ some b ↔ Increasing b

theorem Iris.Option.not_some_ordN_none {α : Type u_1} [ORA α] {n : Nat} {a : α} : ¬some a ≼ₒ{n} none

theorem Iris.Option.eq_none_of_ordN_none {α : Type u_1} [ORA α] {n : Nat} {ma : Option α} : ma ≼ₒ{n} none → ma = none

theorem Iris.Option.exists_of_some_ordN {α : Type u_1} [ORA α] {n : Nat} {a : α} {mb : Option α} : some a ≼ₒ{n} mb → ∃ (b : α), mb = some b ∧ some a ≼ₒ{n} some b

theorem Iris.Option.exists_of_some_ord {α : Type u_1} [ORA α] {a : α} {mb : Option α} : some a ≼ₒ mb → ∃ (b : α), mb = some b ∧ some a ≼ₒ some b

theorem Iris.Option.not_some_ord_none {α : Type u_1} [ORA α] {a : α} : ¬some a ≼ₒ none

instance Iris.Option.instOrderRefl {α : Type u_1} [ORA α] : OrderRefl (Option α)

theorem Iris.Option.increasing_some_iff {α : Type u_1} [ORA α] {a : α} : Increasing (some a) ↔ Increasing a

instance Iris.Option.instIncreasingNone {α : Type u_1} [ORA α] : Increasing none

theorem Iris.Option.increasing_pcore {α : Type u_1} [ORA α] (x : α) : Increasing (PCore.pcore x)

theorem Iris.Option.none_ord_pcore {α : Type u_1} [ORA α] (x : α) : none ≼ₒ PCore.pcore x

theorem Iris.Option.none_ordN_pcore {α : Type u_1} [ORA α] {n : Nat} (x : α) : none ≼ₒ{n} PCore.pcore x

theorem Iris.Option.pcore_ordN_pcore {α : Type u_1} [ORA α] {n : Nat} {x y : α} : x ≼ₒ*{n} y → PCore.pcore x ≼ₒ{n} PCore.pcore y

theorem Iris.Option.pcore_ord_pcore {α : Type u_1} [ORA α] {x y : α} : x ≼ₒ* y → PCore.pcore x ≼ₒ PCore.pcore y

theorem Iris.Option.pcore_ord_pcore_op {α : Type u_1} [ORA α] (x y : α) : PCore.pcore x ≼ₒ PCore.pcore (x • y)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Iris.ucmraOption {α : Type u_1} [ORA α] : UORA (Option α)

Equations

• Iris.ucmraOption = { toORA := Iris.cmraOption, toOrderRefl := ⋯, unit := none, unit_valid := trivial, unit_left_id := ⋯, pcore_unit := ⋯ }

theorem Iris.Option.some_op {α : Type u_1} [ORA α] (a b : α) : some (a • b) = some a • some b

theorem Iris.Option.some_valid {α : Type u_1} [ORA α] {a : α} : ✓ some a ↔ ✓ a

theorem Iris.Option.some_validN {α : Type u_1} [ORA α] {n : Nat} {a : α} : ✓{n} some a ↔ ✓{n} a

theorem Iris.Option.pcore_some {α : Type u_1} [ORA α] (a : α) : PCore.pcore (some a) = some (PCore.pcore a)

theorem Iris.Option.some_core {α : Type u_1} [ORA α] [IsTotal α] (a : α) : some (PCore.core a) = PCore.core (some a)

instance Iris.Option.some_core_id {α : Type u_1} [ORA α] (a : α) [ORA.CoreId a] : ORA.CoreId (some a)

instance Iris.Option.none_core_id {α : Type u_1} [ORA α] : ORA.CoreId none

instance Iris.Option.option_core_id {α : Type u_1} [ORA α] (ma : Option α) [∀ (x : α), ORA.CoreId x] : ORA.CoreId ma

theorem Iris.Option.op_none_iff {α : Type u_1} [ORA α] (ma mb : Option α) : ma • mb = none ↔ ma = none ∧ mb = none

theorem Iris.Option.op_isSome {α : Type u_1} [ORA α] (ma mb : Option α) : (ma • mb).isSome = true ↔ ma.isSome = true ∨ mb.isSome = true

theorem Iris.Option.op_none_left_id {α : Type u_1} [ORA α] (a : Option α) : none • a = a

theorem Iris.Option.op_none_right_id {α : Type u_1} [ORA α] (a : Option α) : a • none = a

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

theorem Iris.Option.eq_none_of_op_eq_none_left {α : Type u_1} [ORA α] {x y : Option α} (h : x • y = none) : x = none

theorem Iris.Option.eq_none_of_op_eq_none_right {α : Type u_1} [ORA α] {x y : Option α} (h : x • y = none) : y = none

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

theorem Iris.Option.some_op_opM {α : Type u_1} [ORA α] {a : α} {ma : Option α} : some a • ma = some (a •? ma)

theorem Iris.Option.opM_opM_assoc {α : Type u_1} [ORA α] {x : α} {y z : Option α} : (x •? y) •? z = x •? (y • z)

theorem Iris.Option.opM_opM_swap {α : Type u_1} [ORA α] {x : α} {y z : Option α} : (x •? y) •? z = (x •? z) •? y

theorem Iris.Option.opM_map_some {α : Type u_1} [ORA α] {ma₁ ma₂ : Option α} : ma₁ •? Option.map some ma₂ = ma₁ • ma₂

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

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

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

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

theorem Iris.Option.exclusiveN_some_left {α : Type u_1} [ORA α] {n : Nat} {a : α} [ORA.Exclusive a] {mb : Option α} (h : ✓{n} some a • mb) : mb = none

theorem Iris.Option.exclusiveN_some_right {α : Type u_1} [ORA α] {n : Nat} {a : α} [ORA.Exclusive a] {mb : Option α} (h : ✓{n} mb • some a) : mb = none

theorem Iris.Option.exclusive_some_left {α : Type u_1} [ORA α] {a : α} [ORA.Exclusive a] {mb : Option α} (h : ✓ some a • mb) : mb = none

theorem Iris.Option.exclusive_some_right {α : Type u_1} [ORA α] {a : α} [ORA.Exclusive a] {mb : Option α} (h : ✓ mb • some a) : mb = none

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

The order on Option α

theorem Iris.Option.dist_or_ordN_of_some_ordN_some {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : some a ≼ₒ{n} some b) : OFE.Dist n a b ∨ a ≼ₒ{n} b

theorem Iris.Option.some_ordN_some_of_dist_or_ordN {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : OFE.Dist n a b ∨ a ≼ₒ{n} b) : some a ≼ₒ{n} some b

theorem Iris.Option.some_ordN_some_of_ordN {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : a ≼ₒ{n} b) : some a ≼ₒ{n} some b

theorem Iris.Option.some_ordN_some_of_dist {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : OFE.Dist n a b) : some a ≼ₒ{n} some b

theorem Iris.Option.isSome_of_some_ordN {α : Type u_1} [ORA α] {n : Nat} {a : α} {mb : Option α} (h : some a ≼ₒ{n} mb) : mb.isSome = true

theorem Iris.Option.eq_or_ord_of_some_ord_some {α : Type u_1} [ORA α] {a b : α} (h : some a ≼ₒ some b) : a = b ∨ a ≼ₒ b

theorem Iris.Option.some_ord_some_of_eq_or_ord {α : Type u_1} [ORA α] {a b : α} (h : a = b ∨ a ≼ₒ b) : some a ≼ₒ some b

theorem Iris.Option.some_ord_some_of_ord {α : Type u_1} [ORA α] {a b : α} (h : a ≼ₒ b) : some a ≼ₒ some b

theorem Iris.Option.some_ord_some_of_eq {α : Type u_1} [ORA α] {a b : α} (h : a = b) : some a ≼ₒ some b

theorem Iris.Option.isSome_of_some_ord {α : Type u_1} [ORA α] {a : α} {mb : Option α} (h : some a ≼ₒ mb) : mb.isSome = true

theorem Iris.Option.isSome_monoN_ord {α : Type u_1} [ORA α] {n : Nat} {ma mb : Option α} (h : ma ≼ₒ{n} mb) : ma.isSome = true → mb.isSome = true

theorem Iris.Option.isSome_mono_ord {α : Type u_1} [ORA α] {ma mb : Option α} (h : ma ≼ₒ mb) : ma.isSome = true → mb.isSome = true

theorem Iris.Option.ord_of_some_ord_some {α : Type u_1} [ORA α] [OrderRefl α] {x y : α} (H : some y ≼ₒ some x) : y ≼ₒ x

theorem Iris.Option.ordN_of_some_ordN_some {α : Type u_1} [ORA α] [OrderRefl α] {n : Nat} {x y : α} (H : some y ≼ₒ{n} some x) : y ≼ₒ{n} x

theorem Iris.Option.some_ord_some_iff_orderRefl {α : Type u_1} [ORA α] [OrderRefl α] {a b : α} : some a ≼ₒ some b ↔ a ≼ₒ b

theorem Iris.Option.some_ordN_some_iff_orderRefl {α : Type u_1} [ORA α] [OrderRefl α] {n : Nat} {a b : α} : some a ≼ₒ{n} some b ↔ a ≼ₒ{n} b

theorem Iris.Option.validN_of_ordN_validN {α : Type u_1} [ORA α] {n : Nat} {a b : α} (Hv : ✓{n} a) (Hinc : some b ≼ₒ{n} some a) : ✓{n} b

theorem Iris.Option.valid_of_ord_valid {α : Type u_1} [ORA α] {a b : α} (Hv : ✓ a) (Hinc : some b ≼ₒ some a) : ✓ b

theorem Iris.Option.ord_iff {α : Type u_1} [ORA α] [IncOrd α] {ma mb : Option α} : ma ≼ₒ mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ (a = b ∨ a ≼ₒ b)

theorem Iris.Option.ordN_iff {α : Type u_1} [ORA α] [IncOrd α] {n : Nat} {ma mb : Option α} : ma ≼ₒ{n} mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ (OFE.Dist n a b ∨ a ≼ₒ{n} b)

theorem Iris.Option.ord_iff_orderRefl {α : Type u_1} [ORA α] [IncOrd α] [OrderRefl α] {ma mb : Option α} : ma ≼ₒ mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ a ≼ₒ b

theorem Iris.Option.ordN_iff_orderRefl {α : Type u_1} [ORA α] [IncOrd α] [OrderRefl α] {n : Nat} {ma mb : Option α} : ma ≼ₒ{n} mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ a ≼ₒ{n} b

theorem Iris.Option.eqv_of_ord_exclusive {α : Type u_1} [ORA α] {a : α} [OrdInc α] [ORA.Exclusive a] {b : α} (H : some a ≼ₒ some b) (Hv : ✓ b) : a = b

theorem Iris.Option.dist_of_ord_exclusive {α : Type u_1} [ORA α] {a : α} [OrdInc α] [ORA.Exclusive a] {n : Nat} {b : α} (H : some a ≼ₒ{n} some b) (Hv : ✓{n} b) : OFE.Dist n a b

theorem Iris.Option.map_mono_ord {α : Type u_2} [ORA α] {β : Type u_1} [ORA β] [IncOrd β] (f : α → β) {ma mb : Option α} (hf : ∀ (x y : α), x ≼ₒ y → f x ≼ₒ f y) (h : ma ≼ₒ mb) : Option.map f ma ≼ₒ Option.map f mb

instance Iris.Option.instIncOrd {α : Type u_1} [ORA α] [IncOrd α] : IncOrd (Option α)

instance Iris.Option.instOrdInc {α : Type u_1} [ORA α] [OrdInc α] : OrdInc (Option α)

instance Iris.Option.instIsInc {α : Type u_1} [ORA α] [IsInc α] : IsInc (Option α)

The extension inclusion on Option α

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

theorem Iris.Option.some_ordN_some_of_dist_opM {α : Type u_1} [ORA α] [IncOrd α] {n : Nat} {x y : α} {mz : Option α} (H : OFE.Dist n x (y •? mz)) : some y ≼ₒ{n} some x

theorem Iris.Option.inc_of_some_inc_some {α : Type u_1} [ORA α] [IsTotal α] {x y : α} (H : some y ≼ some x) : y ≼ x

theorem Iris.Option.some_incN_some_iff_some {α : Type u_1} [ORA α] [IsTotal α] {n : Nat} {x y : α} : some y ≼{n} some x → y ≼{n} x

theorem Iris.Option.inc_iff {α : Type u_1} [ORA α] {ma mb : Option α} : ma ≼ mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ (a = b ∨ a ≼ b)

theorem Iris.Option.incN_iff {α : Type u_1} [ORA α] {n : Nat} {ma mb : Option α} : ma ≼{n} mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ (OFE.Dist n a b ∨ a ≼{n} b)

theorem Iris.Option.inc_iff_isTotal {α : Type u_1} [ORA α] [IsTotal α] {ma mb : Option α} : ma ≼ mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ a ≼ b

theorem Iris.Option.incN_iff_is_total {α : Type u_1} [ORA α] [IsTotal α] {n : Nat} {ma mb : Option α} : ma ≼{n} mb ↔ ma = none ∨ ∃ (a : α), ∃ (b : α), ma = some a ∧ mb = some b ∧ a ≼{n} b

theorem Iris.Option.some_incN_some_iff {α : Type u_1} [ORA α] {n : Nat} {a b : α} : some a ≼{n} some b ↔ OFE.Dist n a b ∨ a ≼{n} b

theorem Iris.Option.dist_or_incN_of_some_incN_some {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : some a ≼{n} some b) : OFE.Dist n a b ∨ a ≼{n} b

theorem Iris.Option.some_incN_some_of_dist_or_incN {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : OFE.Dist n a b ∨ a ≼{n} b) : some a ≼{n} some b

theorem Iris.Option.some_incN_some_of_incN {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : a ≼{n} b) : some a ≼{n} some b

theorem Iris.Option.some_incN_some_of_dist {α : Type u_1} [ORA α] {n : Nat} {a b : α} (h : OFE.Dist n a b) : some a ≼{n} some b

theorem Iris.Option.isSome_of_some_incN {α : Type u_1} [ORA α] {n : Nat} {a : α} {mb : Option α} (h : some a ≼{n} mb) : mb.isSome = true

theorem Iris.Option.some_inc_some_iff {α : Type u_1} [ORA α] {a b : α} : some a ≼ some b ↔ a = b ∨ a ≼ b

theorem Iris.Option.eq_or_inc_of_some_inc_some {α : Type u_1} [ORA α] {a b : α} (h : some a ≼ some b) : a = b ∨ a ≼ b

theorem Iris.Option.some_inc_some_of_eq_or_inc {α : Type u_1} [ORA α] {a b : α} (h : a = b ∨ a ≼ b) : some a ≼ some b

theorem Iris.Option.some_inc_some_of_inc {α : Type u_1} [ORA α] {a b : α} (h : a ≼ b) : some a ≼ some b

theorem Iris.Option.some_inc_some_of_eq {α : Type u_1} [ORA α] {a b : α} (h : a = b) : some a ≼ some b

theorem Iris.Option.isSome_of_some_inc {α : Type u_1} [ORA α] {a : α} {mb : Option α} (h : some a ≼ mb) : mb.isSome = true

theorem Iris.Option.isSome_monoN {α : Type u_1} [ORA α] {n : Nat} {ma mb : Option α} (h : ma ≼{n} mb) : ma.isSome = true → mb.isSome = true

theorem Iris.Option.isSome_mono {α : Type u_1} [ORA α] {ma mb : Option α} (h : ma ≼ mb) : ma.isSome = true → mb.isSome = true

theorem Iris.Option.eqv_of_inc_exclusive {α : Type u_1} [ORA α] {a : α} [ORA.Exclusive a] {b : α} (H : some a ≼ some b) (Hv : ✓ b) : a = b

theorem Iris.Option.dist_of_inc_exclusive {α : Type u_1} [ORA α] {a : α} [ORA.Exclusive a] {n : Nat} {b : α} (H : some a ≼{n} some b) (Hv : ✓{n} b) : OFE.Dist n a b

theorem Iris.Option.some_inc_some_iff_is_total {α : Type u_1} [ORA α] [IsTotal α] {a b : α} : some a ≼ some b ↔ a ≼ b

theorem Iris.Option.map_mono {α : Type u_2} [ORA α] {β : Type u_1} [ORA β] (f : α → β) {ma mb : Option α} (hf : ∀ (x y : α), x ≼ y → f x ≼ f y) (h : ma ≼ mb) : Option.map f ma ≼ Option.map f mb

theorem Iris.Option.some_incN_some_iff_is_total {α : Type u_1} [ORA α] [IsTotal α] {n : Nat} {a b : α} : some a ≼{n} some b ↔ a ≼{n} b

instance Iris.Option.instCancelableOptionSomeOfIdFree {α : Type u_1} [ORA α] {a : α} [ORA.IdFree a] [ORA.Cancelable a] : ORA.Cancelable (some a)

instance Iris.Option.instCancelableOptionOfIdFree {α : Type u_1} [ORA α] {ma : Option α} [∀ (a : α), ORA.IdFree a] [∀ (a : α), ORA.Cancelable a] : ORA.Cancelable ma

theorem Iris.Option.validN_of_incN_validN {α : Type u_1} [ORA α] {n : Nat} {a b : α} (Hv : ✓{n} a) (Hinc : some b ≼{n} some a) : ✓{n} b

theorem Iris.Option.valid_of_inc_valid {α : Type u_1} [ORA α] {a b : α} (Hv : ✓ a) (Hinc : some b ≼ some a) : ✓ b

theorem Iris.Option.some_inc_some_iff_opM {α : Type u_1} [ORA α] {a b : α} : some a ≼ some b ↔ ∃ (mc : Option α), b = a •? mc

theorem Iris.Option.some_incN_some_iff_opM {α : Type u_1} [ORA α] {n : Nat} {a b : α} : some a ≼{n} some b ↔ ∃ (mc : Option α), OFE.Dist n b (a •? mc)

instance Iris.Option.instDiscreteOption {α : Type u_1} [ORA α] [ORA.Discrete α] : ORA.Discrete (Option α)

@[instance_reducible]

def Iris.Unit.cmraData : CMRAData Unit

The classical resource algebra on the one-element type.

Equations

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

@[instance_reducible]

instance Iris.cmraUnit : CMRA Unit

Equations

• Iris.cmraUnit = Iris.ORA.ofCMRAData Iris.Unit.cmraData

@[instance_reducible]

def Iris.Unit.ucmraData : UCMRAData Unit

The unique element is the unit of the one-element resource algebra.

Equations

• Iris.Unit.ucmraData = { unit := (), unit_valid := True.intro, unit_left_id := @Iris.Unit.ucmraData._proof_1, pcore_unit := Iris.Unit.ucmraData._proof_2 }

@[instance_reducible]

instance Iris.ucmraUnit : UCMRA Unit

Equations

• Iris.ucmraUnit = Iris.UORA.ofUCMRAData Iris.Unit.ucmraData

instance Iris.instDiscreteUnit : ORA.Discrete Unit

@[instance_reducible]

def Iris.Empty.cmraData : CMRAData Empty

The classical resource algebra on the empty type.

Equations

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

@[instance_reducible]

instance Iris.cmraEmpty : CMRA Empty

Equations

• Iris.cmraEmpty = Iris.ORA.ofCMRAData Iris.Empty.cmraData

instance Iris.instDiscreteEmpty : ORA.Discrete Empty

instance Iris.instCoreIdEmpty (x : Empty) : ORA.CoreId x

instance Iris.instCancelableEmpty (x : Empty) : ORA.Cancelable x

@[reducible, inline]

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

The partial core of a pair, defined when both component cores exist.

Equations

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

@[reducible, inline]

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

Componentwise composition of a pair of resources.

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} [ORA α] [ORA β] (n : Nat) (x : α × β) : Prop

A pair is valid at an index when both components are valid there.

Equations

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

@[reducible, inline]

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

A pair is valid when both components are valid.

Equations

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

@[reducible, inline]

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

The componentwise step-indexed order on resource pairs.

Equations

• Iris.Prod.OrderN n x y = (x.fst ≼ₒ{n} y.fst ∧ x.snd ≼ₒ{n} y.snd)

@[reducible, inline]

abbrev Iris.Prod.Order {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] (x y : α × β) : Prop

The componentwise order on resource pairs.

Equations

• Iris.Prod.Order x y = (x.fst ≼ₒ y.fst ∧ x.snd ≼ₒ y.snd)

@[reducible]

def Iris.Prod.raOp {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] : Op (α × β)

Composition on resource pairs.

Equations

• Iris.Prod.raOp = { op := Iris.Prod.op, op_ne := ⋯, assoc := ⋯, comm := ⋯ }

@[reducible]

def Iris.Prod.raPCore {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] : PCore (α × β)

The partial core on resource pairs.

Equations

• Iris.Prod.raPCore = { pcore := Iris.Prod.pcore, pcore_ne := ⋯, pcore_idem := ⋯ }

@[reducible]

def Iris.Prod.raValid {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] : Validity (α × β)

Validity on resource pairs.

Equations

• Iris.Prod.raValid = { ValidN := Iris.Prod.ValidN, Valid := Iris.Prod.Valid, validN_ne := ⋯, valid_iff_validN := ⋯, validN_succ := ⋯ }

@[reducible]

def Iris.Prod.raOrdered {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] : Ordered (α × β)

The resource order on resource pairs.

Equations

• Iris.Prod.raOrdered = { OrderN := Iris.Prod.OrderN, Order := Iris.Prod.Order, ordN_ne := ⋯, ordN_succ := ⋯, ordN_trans := ⋯, ord_trans := ⋯, ordN_of_ord := ⋯ }

theorem Iris.Prod.pcore_eq_some {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x cx : α × β} : PCore.pcore x = some cx ↔ PCore.pcore x.fst = some cx.fst ∧ PCore.pcore x.snd = some cx.snd

theorem Iris.Prod.increasing_iff {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x : α × β} : Increasing x ↔ Increasing x.fst ∧ Increasing x.snd

theorem Iris.Prod.ordNR_fst {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {n : Nat} {x y : α × β} (h : x ≼ₒ*{n} y) : x.fst ≼ₒ*{n} y.fst

theorem Iris.Prod.ordNR_snd {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {n : Nat} {x y : α × β} (h : x ≼ₒ*{n} y) : x.snd ≼ₒ*{n} y.snd

@[instance_reducible]

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

Equations

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

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

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

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

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

theorem Iris.Prod.mk_op_mk {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] (a a' : α) (b b' : β) : (a, b) • (a', b') = (a • a', b • b')

theorem Iris.Prod.mk_valid {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] (a : α) (b : β) : ✓ (a, b) ↔ ✓ a ∧ ✓ b

theorem Iris.Prod.mk_validN {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} (a : α) (b : β) : ✓{n} (a, b) ↔ ✓{n} a ∧ ✓{n} b

theorem Iris.Prod.mk_pcore {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] (a : α) (b : β) : PCore.pcore (a, b) = (PCore.pcore a).bind fun (c₁ : α) => (PCore.pcore b).bind fun (c₂ : β) => some (c₁, c₂)

theorem Iris.Prod.mk_core {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [IsTotal α] [IsTotal β] (a : α) (b : β) : PCore.core (a, b) = (PCore.core a, PCore.core b)

theorem Iris.Prod.ord_def {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x y : α × β} : x ≼ₒ y ↔ x.fst ≼ₒ y.fst ∧ x.snd ≼ₒ y.snd

theorem Iris.Prod.ordN_def {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {n : Nat} {x y : α × β} : x ≼ₒ{n} y ↔ x.fst ≼ₒ{n} y.fst ∧ x.snd ≼ₒ{n} y.snd

theorem Iris.Prod.mk_ord_mk {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] (a a' : α) (b b' : β) : (a, b) ≼ₒ (a', b') ↔ a ≼ₒ a' ∧ b ≼ₒ b'

theorem Iris.Prod.mk_ordN_mk {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} (a a' : α) (b b' : β) : (a, b) ≼ₒ{n} (a', b') ↔ a ≼ₒ{n} a' ∧ b ≼ₒ{n} b'

theorem Iris.Prod.inc_def {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x y : α × β} : x ≼ y ↔ x.fst ≼ y.fst ∧ x.snd ≼ y.snd

theorem Iris.Prod.incN_def {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {n : Nat} {x y : α × β} : x ≼{n} y ↔ x.fst ≼{n} y.fst ∧ x.snd ≼{n} y.snd

theorem Iris.Prod.mk_inc_mk {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] (a a' : α) (b b' : β) : (a, b) ≼ (a', b') ↔ a ≼ a' ∧ b ≼ b'

theorem Iris.Prod.mk_incN_mk {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} (a a' : α) (b b' : β) : (a, b) ≼{n} (a', b') ↔ a ≼{n} a' ∧ b ≼{n} b'

instance Iris.Prod.instIsTotalProd {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [IsTotal α] [IsTotal β] : IsTotal (α × β)

instance Iris.Prod.instCmraDiscreteProd {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [ORA.Discrete α] [ORA.Discrete β] : ORA.Discrete (α × β)

instance Iris.Prod.instOrderRefl {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [OrderRefl α] [OrderRefl β] : OrderRefl (α × β)

instance Iris.Prod.instIncOrd {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [IncOrd α] [IncOrd β] : IncOrd (α × β)

instance Iris.Prod.instOrdInc {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [OrdInc α] [OrdInc β] : OrdInc (α × β)

instance Iris.Prod.instIsInc {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [IsInc α] [IsInc β] : IsInc (α × β)

instance Iris.Prod.instCoreIdPair {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x : α} {y : β} [ORA.CoreId x] [ORA.CoreId y] : ORA.CoreId (x, y)

instance Iris.Prod.instExclusivePairLeft {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x : α} [ORA.Exclusive x] {y : β} : ORA.Exclusive (x, y)

instance Iris.Prod.instExclusivePairRight {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {x : α} {y : β} [ORA.Exclusive y] : ORA.Exclusive (x, y)

instance Iris.Prod.instCancelablePair {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x : α} {y : β} [ORA.Cancelable x] [ORA.Cancelable y] : ORA.Cancelable (x, y)

instance Iris.Prod.instIdFreePairLeft {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {x : α} [ORA.IdFree x] {y : β} : ORA.IdFree (x, y)

instance Iris.Prod.instIdFreePairRight {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {x : α} {y : β} [ORA.IdFree y] : ORA.IdFree (x, y)

@[instance_reducible]

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

Equations

• Iris.Prod.ucmraProd = { toORA := Iris.Prod.cmraProd, toOrderRefl := ⋯, unit := (Iris.UORA.unit, Iris.UORA.unit), unit_valid := ⋯, unit_left_id := ⋯, pcore_unit := ⋯ }

theorem Iris.Prod.mk_split {α : Type u_1} {β : Type u_2} [UORA α] [UORA β] (a : α) (b : β) : (a, b) = (a, UORA.unit) • (UORA.unit, b)

theorem Iris.Prod.mk_op_fst {α : Type u_1} {β : Type u_2} [UORA α] [UORA β] (a a' : α) : (a • a', UORA.unit) = (a, UORA.unit) • (a', UORA.unit)

theorem Iris.Prod.mk_op_snd {α : Type u_1} {β : Type u_2} [UORA α] [UORA β] (b b' : β) : (UORA.unit, b • b') = (UORA.unit, b) • (UORA.unit, b')

theorem Iris.Option.some_mk_ordN {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ₒ{n} some (a₂, b₂)) : some a₁ ≼ₒ{n} some a₂ ∧ some b₁ ≼ₒ{n} some b₂

theorem Iris.Option.some_mk_ordN_left {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ₒ{n} some (a₂, b₂)) : some a₁ ≼ₒ{n} some a₂

theorem Iris.Option.some_mk_ordN_right {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ₒ{n} some (a₂, b₂)) : some b₁ ≼ₒ{n} some b₂

theorem Iris.Option.some_mk_ord {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ₒ some (a₂, b₂)) : some a₁ ≼ₒ some a₂ ∧ some b₁ ≼ₒ some b₂

theorem Iris.Option.some_mk_ord_left {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ₒ some (a₂, b₂)) : some a₁ ≼ₒ some a₂

theorem Iris.Option.some_mk_ord_right {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ₒ some (a₂, b₂)) : some b₁ ≼ₒ some b₂

theorem Iris.Option.some_op_ordN_snd {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {n : Nat} {x y : α × β} {c : Option (α × β)} (h : some x • c ≼ₒ{n} some y) : some x.snd • Option.map Prod.snd c ≼ₒ{n} some y.snd

theorem Iris.Option.some_mk_incN {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼{n} some (a₂, b₂)) : some a₁ ≼{n} some a₂ ∧ some b₁ ≼{n} some b₂

theorem Iris.Option.some_mk_incN_left {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼{n} some (a₂, b₂)) : some a₁ ≼{n} some a₂

theorem Iris.Option.some_mk_incN_right {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼{n} some (a₂, b₂)) : some b₁ ≼{n} some b₂

theorem Iris.Option.some_mk_incN_total_fst {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [IsTotal α] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼{n} some (a₂, b₂)) : a₁ ≼{n} a₂ ∧ some b₁ ≼{n} some b₂

theorem Iris.Option.some_mk_incN_total_snd {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] [IsTotal β] {n : Nat} {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼{n} some (a₂, b₂)) : some a₁ ≼{n} some a₂ ∧ b₁ ≼{n} b₂

theorem Iris.Option.some_mk_inc {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ some (a₂, b₂)) : some a₁ ≼ some a₂ ∧ some b₁ ≼ some b₂

theorem Iris.Option.some_mk_inc_left {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ some (a₂, b₂)) : some a₁ ≼ some a₂

theorem Iris.Option.some_mk_inc_right {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ some (a₂, b₂)) : some b₁ ≼ some b₂

theorem Iris.Option.some_mk_inc_total_fst {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] [IsTotal α] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ some (a₂, b₂)) : a₁ ≼ a₂ ∧ some b₁ ≼ some b₂

theorem Iris.Option.some_mk_inc_total_snd {α : Type u_2} {β : Type u_1} [ORA α] [ORA β] [IsTotal β] {a₁ a₂ : α} {b₁ b₂ : β} (h : some (a₁, b₁) ≼ some (a₂, b₂)) : some a₁ ≼ some a₂ ∧ b₁ ≼ b₂

def Iris.Option.mapC {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] (f : α -C> β) : Option α -C> Option β

Lift a resource morphism to optional resources.

Equations

• Iris.Option.mapC f = { toHom := Iris.optionMap f.toHom, validN := ⋯, pcore := ⋯, op := ⋯, monoN_ord := ⋯, mono_ord := ⋯, increasing := ⋯ }

def Iris.Prod.mapC {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [ORA A] [ORA A'] [ORA B] [ORA B'] (f : A -C> A') (g : B -C> B') : A × B -C> A' × B'

The product of two ordered resource algebra morphisms.

Equations

• Iris.Prod.mapC f g = { f := Prod.map f.f g.f, ne := ⋯, validN := ⋯, pcore := ⋯, op := ⋯, monoN_ord := ⋯, mono_ord := ⋯, increasing := ⋯ }

@[instance_reducible]

instance Iris.instRFunctorProdOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4} [RFunctor F1] [RFunctor F2] : RFunctor (ProdOF F1 F2)

Equations

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

instance Iris.instRFunctorAffineProdOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4} [RFunctor F1] [RFunctor F2] [RFunctorAffine F1] [RFunctorAffine F2] : RFunctorAffine (ProdOF F1 F2)

@[instance_reducible]

instance Iris.instRFunctorContractiveProdOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4} [RFunctorContractive F1] [RFunctorContractive F2] : RFunctorContractive (ProdOF F1 F2)

Equations

• Iris.instRFunctorContractiveProdOF = { toRFunctor := Iris.instRFunctorProdOF, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.instURFunctorProdOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4} [URFunctor F1] [URFunctor F2] : URFunctor (ProdOF F1 F2)

Equations

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

@[instance_reducible]

instance Iris.instURFunctorContractiveProdOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4} [URFunctorContractive F1] [URFunctorContractive F2] : URFunctorContractive (ProdOF F1 F2)

Equations

• Iris.instURFunctorContractiveProdOF = { toURFunctor := Iris.instURFunctorProdOF, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.urFunctorOptionOF {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [RFunctor F] : URFunctor (OptionOF F)

Equations

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

instance Iris.instRFunctorAffineOptionOF {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [RFunctor F] [RFunctorAffine F] : RFunctorAffine (OptionOF F)

@[instance_reducible]

instance Iris.urFunctorContractiveOptionOF {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [RFunctorContractive F] : URFunctorContractive (OptionOF F)

Equations

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