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

Ordered family of equivalences

• Equiv : α → α → Prop
• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• equiv_dist {x y : α} : Equiv x y ↔ ∀ (n : Nat), Dist n x y
• dist_lt {n : Nat} {x y : α} {m : Nat} : Dist n x y → m < n → Dist m x y

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

Equations

• Iris.«term_≡_» = Lean.ParserDescr.trailingNode `Iris.«term_≡_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 41))

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

Equations

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

theorem Iris.OFE.Dist.lt {α : Type u_1} [OFE α] {m n : Nat} {x y : α} : Dist n x y → m < n → Dist m x y

theorem Iris.OFE.Dist.le {α : Type u_1} [OFE α] {m n : Nat} {x y : α} (h : Dist n x y) (h' : m ≤ n) : Dist m x y

@[simp]

theorem Iris.OFE.Dist.rfl {α : Type u_1} [OFE α] {n : Nat} {x : α} : Dist n x x

theorem Iris.OFE.Dist.symm {α : Type u_1} {y : α} [OFE α] {n : Nat} {x : α} : Dist n x y → Dist n y x

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

theorem Iris.OFE.Dist.of_eq {α : Type u_1} {n : Nat} [OFE α] {x y : α} : x = y → Dist n x y

theorem Iris.OFE.equiv_eqv {α : Type u_1} [ofe : OFE α] : Equivalence Equiv

@[simp]

theorem Iris.OFE.Equiv.rfl {α : Type u_1} [OFE α] {x : α} : Equiv x x

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

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

theorem Iris.OFE.Equiv.dist {α : Type u_1} {y : α} {n : Nat} [OFE α] {x : α} : Equiv x y → Dist n x y

theorem Iris.OFE.Equiv.of_eq {α : Type u_1} [OFE α] {x y : α} : x = y → Equiv x y

instance Iris.OFE.instTransEquiv {α : Type u_1} [OFE α] : Trans Equiv Equiv Equiv

Equations

• Iris.OFE.instTransEquiv = { trans := ⋯ }

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

Equations

• Iris.OFE.instTransDist = { trans := ⋯ }

class Iris.OFE.NonExpansive {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) : Prop

A function f : α → β is non-expansive if it preserves n-equivalence.

• ne ⦃n : Nat⦄ ⦃x₁ x₂ : α⦄ : Dist n x₁ x₂ → Dist n (f x₁) (f x₂)

instance Iris.OFE.id_ne {α : Type u_1} [OFE α] : NonExpansive id

theorem Iris.OFE.NonExpansive.eqv {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {f : α → β} [NonExpansive f] ⦃x₁ x₂ : α⦄ (h : Equiv x₁ x₂) : Equiv (f x₁) (f x₂)

A non-expansive function preserves equivalence.

class Iris.OFE.NonExpansive₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] (f : α → β → γ) : Prop

A function f : α → β → γ is non-expansive if it preserves n-equivalence in each argument.

• ne ⦃n : Nat⦄ ⦃x₁ x₂ : α⦄ : Dist n x₁ x₂ → ∀ ⦃y₁ y₂ : β⦄, Dist n y₁ y₂ → Dist n (f x₁ y₁) (f x₂ y₂)

theorem Iris.OFE.NonExpansive₂.eqv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] {f : α → β → γ} [NonExpansive₂ f] ⦃x₁ x₂ : α⦄ (hx : Equiv x₁ x₂) ⦃y₁ y₂ : β⦄ (hy : Equiv y₁ y₂) : Equiv (f x₁ y₁) (f x₂ y₂)

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

DistLater n x y means that x and y are m-equivalent for all m < n.

Equations

• Iris.OFE.DistLater n x y = ∀ (m : Nat), m < n → Iris.OFE.Dist m x y

@[simp]

theorem Iris.OFE.DistLater.rfl {α : Type u_1} [OFE α] {n : Nat} {x : α} : DistLater n x x

theorem Iris.OFE.DistLater.symm {α : Type u_1} {y : α} [OFE α] {n : Nat} {x : α} (h : DistLater n x y) : DistLater n y x

theorem Iris.OFE.DistLater.trans {α : Type u_1} {y z : α} [OFE α] {n : Nat} {x : α} (h1 : DistLater n x y) (h2 : DistLater n y z) : DistLater n x z

theorem Iris.OFE.distLater_eqv {α : Type u_1} [OFE α] {n : Nat} : Equivalence (DistLater n)

DistLater n-equivalence is an equivalence relation.

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

n-equivalence implies DistLater n-equivalence.

theorem Iris.OFE.DistLater.dist_lt {α : Type u_1} [OFE α] {m n : Nat} {x y : α} (h : DistLater n x y) (hm : m < n) : Dist m x y

DistLater n-equivalence implies m-equivalence for all m < n.

@[simp]

theorem Iris.OFE.distLater_zero {α : Type u_1} [OFE α] {x y : α} : DistLater 0 x y

DistLater 0-equivalence is trivial.

theorem Iris.OFE.distLater_succ {α : Type u_1} [OFE α] {n : Nat} {x y : α} : DistLater n.succ x y ↔ Dist n x y

DistLater n-equivalence is equivalent to (n + 1)-equivalence.

class Iris.OFE.Contractive {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) : Prop

A function f : α → β is contractive if it sends DistLater n-equivalent inputs to n-equivalent outputs.

• distLater_dist {n : Nat} {x y : α} : DistLater n x y → Dist n (f x) (f y)

@[simp]

theorem Iris.OFE.Contractive.zero {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) [Contractive f] {x y : α} : Dist 0 (f x) (f y)

theorem Iris.OFE.Contractive.succ {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) [Contractive f] {n : Nat} {x y : α} (h : Dist n x y) : Dist n.succ (f x) (f y)

instance Iris.OFE.ne_of_contractive {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) [Contractive f] : NonExpansive f

A contractive function is non-expansive.

theorem Iris.OFE.Contractive.eqv {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) [Contractive f] ⦃x y : α⦄ (h : Equiv x y) : Equiv (f x) (f y)

A contractive function preserves equivalence.

instance Iris.OFE.instContractive {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {x : β} : Contractive fun (x_1 : α) => x

Constant functions are contractive.

def Iris.OFE.ofDiscrete {α : Type u_1} (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : OFE α

The discrete OFE obtained from an equivalence relation Equiv

Equations

• Iris.OFE.ofDiscrete Equiv equiv_eqv = { Equiv := Equiv, Dist := fun (x : Nat) => Equiv, dist_eqv := ⋯, equiv_dist := ⋯, dist_lt := ⋯ }

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

A discrete element in an OFE

• discrete {y : α} : Dist 0 x y → Equiv x y

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

A discrete OFE is one where equivalence is implied by 0-equivalence.

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

theorem Iris.OFE.Discrete.discrete {α : Type u_1} [OFE α] [Discrete α] {n : Nat} {x y : α} (h : Dist n x y) : Equiv x y

For discrete OFEs, n-equivalence implies equivalence for any n.

theorem Iris.OFE.Discrete.discrete_n {α : Type u_1} [OFE α] [Discrete α] {n : Nat} {x y : α} (h : Dist 0 x y) : Dist n x y

For discrete OFEs, n-equivalence implies equivalence for any n.

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

• eq_of_eqv {x y : α} : Equiv x y → x = y

@[simp]

theorem Iris.OFE.Leibniz.leibniz {α : Type u_1} [OFE α] [Leibniz α] {x y : α} : Equiv x y ↔ x = y

structure Iris.OFE.Hom (α : Type u_1) (β : Type u_2) [OFE α] [OFE β] : Type (max u_1 u_2)

A morphism between OFEs, written α -n> β, is defined to be a function that is non-expansive.

• f : α → β
• ne : NonExpansive self.f

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

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

def Iris.OFE.«term_-n>_» : Lean.TrailingParserDescr

A morphism between OFEs, written α -n> β, is defined to be a function that is non-expansive.

Equations

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

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

Equations

• Iris.OFE.instCoeFunHomForall = { coe := Iris.OFE.Hom.f }

instance Iris.OFE.instNonExpansiveF {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α -n> β) : NonExpansive f.f

def Iris.OFE.Hom.id {α : Type u_1} [OFE α] : α -n> α

The identity morphism on an OFE.

Equations

• Iris.OFE.Hom.id = { f := id, ne := ⋯ }

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

The composition of two morphisms between OFEs.

Equations

• g.comp f = { f := g.f ∘ f.f, ne := ⋯ }

@[simp]

theorem Iris.OFE.Hom.id_apply {α : Type u_1} [OFE α] {x : α} : Hom.id.f x = x

@[simp]

theorem Iris.OFE.Hom.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] {g : β -n> γ} {f : α -n> β} {x : α} : (g.comp f).f x = g.f (f.f x)

@[simp]

theorem Iris.OFE.Hom.id_comp {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {f : α -n> β} : Hom.id.comp f = f

@[simp]

theorem Iris.OFE.Hom.comp_id {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {f : α -n> β} : f.comp Hom.id = f

theorem Iris.OFE.Hom.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [OFE α] [OFE β] [OFE γ] [OFE δ] (h : γ -n> δ) (g : β -n> γ) (f : α -n> β) : (h.comp g).comp f = h.comp (g.comp f)

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

• f : α → β
• ne : NonExpansive self.f
• contractive : Contractive self.f

theorem Iris.OFE.ContractiveHom.ext_iff {α : Type u_1} {β : Type u_2} {inst✝ : OFE α} {inst✝¹ : OFE β} {x y : α -c> β} : x = y ↔ x.f = y.f

theorem Iris.OFE.ContractiveHom.ext {α : Type u_1} {β : Type u_2} {inst✝ : OFE α} {inst✝¹ : OFE β} {x y : α -c> β} (f : x.f = y.f) : x = y

def Iris.OFE.«term_-c>_» : Lean.TrailingParserDescr

Equations

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

instance Iris.OFE.instCoeFunContractiveHomForall {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : CoeFun (α -c> β) fun (x : α -c> β) => α → β

Equations

• Iris.OFE.instCoeFunContractiveHomForall = { coe := fun (x : α -c> β) => x.f }

instance Iris.OFE.instContractiveF {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α -c> β) : Contractive f.f

theorem Iris.OFE.InvImage.equivalence {α : Sort u} {β : Sort v} {r : β → β → Prop} {f : α → β} (H : Equivalence r) : Equivalence (InvImage r f)

instance Iris.OFE.instUnit : OFE Unit

Equations

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

instance Iris.OFE.instULift {α : Type u_1} [OFE α] : OFE (ULift α)

Equations

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

def Iris.OFE.uliftUpHom {α : Type u_1} [OFE α] : α -n> ULift α

Equations

• Iris.OFE.uliftUpHom = { f := ULift.up, ne := ⋯ }

def Iris.OFE.uliftDownHom {α : Type u_1} [OFE α] : ULift α -n> α

Equations

• Iris.OFE.uliftDownHom = { f := ULift.down, ne := ⋯ }

def Option.Forall₂ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) : Option α → Option β → Prop

Equations

• Option.Forall₂ R none none = True
• Option.Forall₂ R (some a) (some b) = R a b
• Option.Forall₂ R x✝¹ x✝ = False

theorem Option.Forall₂.equivalence {α : Type u_1} {R : α → α → Prop} (H : Equivalence R) : Equivalence (Forall₂ R)

instance Iris.OFE.instOption {α : Type u_1} [OFE α] : OFE (Option α)

Equations

• Iris.OFE.instOption = { Equiv := Option.Forall₂ Iris.OFE.Equiv, Dist := fun (n : Nat) => Option.Forall₂ (Iris.OFE.Dist n), dist_eqv := ⋯, equiv_dist := ⋯, dist_lt := ⋯ }

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

@[simp]

theorem Iris.OFE.some_eqv_some {α : Type u_1} [OFE α] {x y : α} : Equiv (some x) (some y) ↔ Equiv x y

@[simp]

theorem Iris.OFE.not_some_eqv_none {α : Type u_1} [OFE α] {x : α} : ¬Equiv (some x) none

@[simp]

theorem Iris.OFE.not_none_eqv_some {α : Type u_1} [OFE α] {x : α} : ¬Equiv none (some x)

@[simp]

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

@[simp]

theorem Iris.OFE.not_some_dist_none {α : Type u_1} [OFE α] {n : Nat} {x : α} : ¬Dist n (some x) none

@[simp]

theorem Iris.OFE.not_none_dist_some {α : Type u_1} [OFE α] {n : Nat} {x : α} : ¬Dist n none (some x)

theorem Iris.OFE.equiv_some {α : Type u_1} [OFE α] {o : Option α} {y : α} (e : Equiv o (some y)) : ∃ (z : α), o = some z ∧ Equiv z y

theorem Iris.OFE.equiv_none {α : Type u_1} [OFE α] {o : Option α} : Equiv o none ↔ o = none

theorem Iris.OFE.dist_some {α : Type u_1} [OFE α] {n : Nat} {mx : Option α} {y : α} (h : Dist n mx (some y)) : ∃ (z : α), mx = some z ∧ Dist n y z

instance Iris.OFE.instLeibnizOption {α : Type u_1} [OFE α] [Leibniz α] : Leibniz (Option α)

@[reducible, inline]

abbrev Iris.OFE.OFEFun {α : Type u_1} (β : α → Type u_2) : Type (max u_1 u_2)

Equations

• Iris.OFE.OFEFun β = ((a : α) → Iris.OFE (β a))

instance Iris.OFE.instForallOfOFEFun {α : Type u_1} {β : α → Type u_2} [OFEFun β] : OFE ((x : α) → β x)

Equations

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

instance Iris.OFE.instHom {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : OFE (α -n> β)

Equations

• Iris.OFE.instHom = { Equiv := fun (f g : α -n> β) => Iris.OFE.Equiv f.f g.f, Dist := fun (n : Nat) (f g : α -n> β) => Iris.OFE.Dist n f.f g.f, dist_eqv := ⋯, equiv_dist := ⋯, dist_lt := ⋯ }

instance Iris.OFE.instContractiveHom {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : OFE (α -c> β)

Equations

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

def Iris.OFE.applyHom {α : Type u_1} {β : α → Type u_2} [OFEFun β] (x : α) : ((x : α) → β x) -n> β x

Equations

• Iris.OFE.applyHom x = { f := fun (f : (x : α) → β x) => f x, ne := ⋯ }

def Iris.OFE.mapCodHom {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} [OFEFun β₁] [OFEFun β₂] (F : (x : α) → β₁ x -n> β₂ x) : ((x : α) → β₁ x) -n> (x : α) → β₂ x

Equations

• Iris.OFE.mapCodHom F = { f := fun (f : (x : α) → β₁ x) (x : α) => (F x).f (f x), ne := ⋯ }

instance Iris.OFE.instProd {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : OFE (α × β)

Equations

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

theorem Iris.OFE.equiv_fst {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {x y : α × β} (h : Equiv x y) : Equiv x.fst y.fst

theorem Iris.OFE.equiv_snd {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {x y : α × β} (h : Equiv x y) : Equiv x.snd y.snd

theorem Iris.OFE.equiv_prod_ext {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {x₁ x₂ : α} {y₁ y₂ : β} (ex : Equiv x₁ x₂) (ey : Equiv y₁ y₂) : Equiv (x₁, y₁) (x₂, y₂)

theorem Iris.OFE.dist_fst {α : Type u_1} {β : Type u_2} {n : Nat} [OFE α] [OFE β] {x y : α × β} (h : Dist n x y) : Dist n x.fst y.fst

theorem Iris.OFE.dist_snd {α : Type u_1} {β : Type u_2} {n : Nat} [OFE α] [OFE β] {x y : α × β} (h : Dist n x y) : Dist n x.snd y.snd

theorem Iris.OFE.dist_prod_ext {α : Type u_1} {β : Type u_2} {n : Nat} [OFE α] [OFE β] {x₁ x₂ : α} {y₁ y₂ : β} (ex : Dist n x₁ x₂) (ey : Dist n y₁ y₂) : Dist n (x₁, y₁) (x₂, y₂)

structure Iris.OFE.Iso (α : Type u_1) (β : Type u_2) [OFE α] [OFE β] : Type (max u_1 u_2)

An isomorphism between two OFEs is a pair of morphisms whose composition is equivalent to the identity morphism.

• hom : α -n> β
• inv : β -n> α
• hom_inv {x : β} : Equiv (self.hom.f (self.inv.f x)) x
• inv_hom {x : α} : Equiv (self.inv.f (self.hom.f x)) x

theorem Iris.OFE.Iso.ext {α : Type u_1} {β : Type u_2} {inst✝ : OFE α} {inst✝¹ : OFE β} {x y : Iso α β} (hom : x.hom = y.hom) (inv : x.inv = y.inv) : x = y

theorem Iris.OFE.Iso.ext_iff {α : Type u_1} {β : Type u_2} {inst✝ : OFE α} {inst✝¹ : OFE β} {x y : Iso α β} : x = y ↔ x.hom = y.hom ∧ x.inv = y.inv

instance Iris.OFE.instCoeFunIsoHom {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : CoeFun (Iso α β) fun (x : Iso α β) => α -n> β

Equations

• Iris.OFE.instCoeFunIsoHom = { coe := Iris.OFE.Iso.hom }

instance Iris.OFE.instNonExpansiveFHom {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) : NonExpansive iso.hom.f

instance Iris.OFE.instNonExpansiveFInv {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) : NonExpansive iso.inv.f

@[simp]

theorem Iris.OFE.Iso.hom_inv_dist {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) {n : Nat} {x : β} : Dist n (iso.hom.f (iso.inv.f x)) x

@[simp]

theorem Iris.OFE.Iso.inv_hom_dist {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) {n : Nat} {x : α} : Dist n (iso.inv.f (iso.hom.f x)) x

theorem Iris.OFE.Iso.hom_eqv {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) ⦃x y : α⦄ : Equiv x y ↔ Equiv (iso.hom.f x) (iso.hom.f y)

OFE isomorphisms preserve equivalence.

theorem Iris.OFE.Iso.inv_eqv {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) ⦃x y : β⦄ : Equiv x y ↔ Equiv (iso.inv.f x) (iso.inv.f y)

The inverse of an OFE isomorphism preserves equivalence.

theorem Iris.OFE.Iso.hom_dist {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) {n : Nat} ⦃x y : α⦄ : Dist n x y ↔ Dist n (iso.hom.f x) (iso.hom.f y)

OFE isomorphisms preserve n-equivalence.

theorem Iris.OFE.Iso.inv_dist {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) {n : Nat} ⦃x y : β⦄ : Dist n x y ↔ Dist n (iso.inv.f x) (iso.inv.f y)

The inverse of an OFE isomorphism preserves n-equivalence.

def Iris.OFE.Iso.id {α : Type u_1} [OFE α] : Iso α α

The identity OFE isomorphism

Equations

• Iris.OFE.Iso.id = { hom := Iris.OFE.Hom.id, inv := Iris.OFE.Hom.id, hom_inv := ⋯, inv_hom := ⋯ }

@[simp]

theorem Iris.OFE.Iso.id_apply {α : Type u_1} [OFE α] {x : α} : id.hom.f x = x

def Iris.OFE.Iso.symm {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (iso : Iso α β) : Iso β α

The inverse of an OFE isomorphism

Equations

• iso.symm = { hom := iso.inv, inv := iso.hom, hom_inv := ⋯, inv_hom := ⋯ }

def Iris.OFE.Iso.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] (iso1 : Iso β γ) (iso2 : Iso α β) : Iso α γ

Composition of OFE isomorphisms

Equations

• iso1.comp iso2 = { hom := iso1.hom.comp iso2.hom, inv := iso2.inv.comp iso1.inv, hom_inv := ⋯, inv_hom := ⋯ }

structure Iris.Chain (α : Type u_1) [OFE α] : Type u_1

A chain in an OFE is a Nat-indexed sequence of elements that is upward-closed in terms of n-equivalence.

• chain : Nat → α
• cauchy {n i : Nat} : n ≤ i → OFE.Dist n (self.chain i) (self.chain n)

instance Iris.instCoeFunChainForallNat {α : Type u_1} [OFE α] : CoeFun (Chain α) fun (x : Chain α) => Nat → α

Equations

• Iris.instCoeFunChainForallNat = { coe := Iris.Chain.chain }

def Iris.Chain.const {α : Type u_1} [OFE α] (a : α) : Chain α

The constant chain.

Equations

• Iris.Chain.const a = { chain := fun (x : Nat) => a, cauchy := ⋯ }

@[simp]

theorem Iris.Chain.const_apply {α : Type u_1} [OFE α] {a : α} {n : Nat} : (const a).chain n = a

def Iris.Chain.map {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α -n> β) (c : Chain α) : Chain β

Mapping a chain through a non-expansive function.

Equations

• Iris.Chain.map f c = { chain := fun (n : Nat) => f.f (c.chain n), cauchy := ⋯ }

@[simp]

theorem Iris.Chain.map_apply {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {f : α -n> β} {c : Chain α} {n : Nat} : (map f c).chain n = f.f (c.chain n)

@[simp]

theorem Iris.Chain.map_id {α : Type u_1} [OFE α] {c : Chain α} : map OFE.Hom.id c = c

theorem Iris.Chain.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] {f : α -n> β} {g : β -n> γ} {c : Chain α} : map (g.comp f) c = map g (map f c)

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

Complete ordered family of equivalences

• compl : Chain α → α
• conv_compl {n : Nat} {c : Chain α} : OFE.Dist n (compl c) (c.chain n)

class Iris.COFE (α : Type u_1) extends Iris.OFE α, Iris.IsCOFE α : Type u_1

Complete ordered family of equivalences

• Equiv : α → α → Prop
• Dist : Nat → α → α → Prop
• dist_eqv {n : Nat} : Equivalence (Dist n)
• equiv_dist {x y : α} : Equiv x y ↔ ∀ (n : Nat), Dist n x y
• dist_lt {n : Nat} {x y : α} {m : Nat} : Dist n x y → m < n → Dist m x y
• compl : Chain α → α
• conv_compl {n : Nat} {c : Chain α} : OFE.Dist n (compl c) (c.chain n)

theorem Iris.COFE.conv_compl' {α : Type u_1} [COFE α] {c : Chain α} {n i : Nat} (h : n ≤ i) : OFE.Dist n (compl c) (c.chain i)

theorem Iris.COFE.compl_map {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] (f : α -n> β) (c : Chain α) : OFE.Equiv (compl (Chain.map f c)) (f.f (compl c))

Chain maps commute with completion.

@[simp]

theorem Iris.COFE.compl_const {α : Type u_1} [COFE α] (a : α) : OFE.Equiv (compl (Chain.const a)) a

Constant chains complete to their constant value

@[simp]

theorem Iris.COFE.discrete_cofe_compl {α : Type u_1} [COFE α] [OFE.Discrete α] (c : Chain α) : OFE.Equiv (compl c) (c.chain 0)

Completion of discrete COFEs is the constant value.

def Iris.COFE.ofDiscrete {α : Type u_1} (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : COFE α

The discrete COFE obtained from an equivalence relation Equiv

Equations

• Iris.COFE.ofDiscrete Equiv equiv_eqv = { toOFE := Iris.OFE.ofDiscrete Equiv equiv_eqv, compl := fun (c : Iris.Chain α) => c.chain 0, conv_compl := ⋯ }

instance Iris.COFE.instULift {α : Type u_1} [COFE α] : COFE (ULift α)

Equations

• Iris.COFE.instULift = { toOFE := Iris.OFE.instULift, compl := fun (c : Iris.Chain (ULift α)) => { down := Iris.IsCOFE.compl (Iris.Chain.map Iris.OFE.uliftDownHom c) }, conv_compl := ⋯ }

instance Iris.COFE.instUnit : COFE Unit

Equations

• Iris.COFE.instUnit = { toOFE := Iris.OFE.instUnit, compl := fun (x : Iris.Chain Unit) => (), conv_compl := ⋯ }

@[reducible, inline]

abbrev Iris.COFE.IsCOFEFun {α : Type u_1} (β : α → Type u_2) [OFE.OFEFun β] : Type (max u_1 u_2)

Equations

• Iris.COFE.IsCOFEFun β = ((x : α) → Iris.IsCOFE (β x))

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

Equations

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

@[reducible, inline]

abbrev Iris.COFE.OFunctorPre : Type (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1))

Equations

• Iris.COFE.OFunctorPre = ((α : Type ?u.8) → (β : Type ?u.7) → [Iris.OFE α] → [Iris.OFE β] → Type ?u.6)

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

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

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

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

@[reducible, inline]

abbrev Iris.COFE.constOF (B : Type) : OFunctorPre

Equations

• Iris.COFE.constOF B x✝³ x✝² = B

instance Iris.COFE.oFunctorConstOF {B : Type} [OFE B] : OFunctor (constOF B)

Equations

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

instance Iris.COFE.OFunctor.constOF_contractive {B : Type} [OFE B] : OFunctorContractive (constOF B)

Equations

• Iris.COFE.OFunctor.constOF_contractive = { toOFunctor := Iris.COFE.oFunctorConstOF, map_contractive := ⋯ }

structure Iris.LeibnizO (α : Type u_1) : Type u_1

• car : α

theorem Iris.LeibnizO.ext_iff {α : Type u_1} {x y : LeibnizO α} : x = y ↔ x.car = y.car

theorem Iris.LeibnizO.ext {α : Type u_1} {x y : LeibnizO α} (car : x.car = y.car) : x = y

theorem Iris.Eq_Equivalence {α : Type u_1} : Equivalence Eq

instance Iris.instCOFELeibnizO {α : Type u_1} : COFE (LeibnizO α)

Equations

• Iris.instCOFELeibnizO = Iris.COFE.ofDiscrete Eq ⋯

instance Iris.instLeibnizLeibnizO {α : Type u_1} : OFE.Leibniz (LeibnizO α)

instance Iris.instDiscreteLeibnizO {α : Type u_1} : OFE.Discrete (LeibnizO α)

instance Iris.instLeibnizLeibnizO_1 {α : Type u_1} : OFE.Leibniz (LeibnizO α)

theorem Iris.LeibnizO.eqv_inj {α : Type u_1} {x y : α} (H : OFE.Equiv { car := x } { car := y }) : x = y

theorem Iris.LeibnizO.dist_inj {α : Type u_1} {x y : α} {n : Nat} (H : OFE.Dist n { car := x } { car := y }) : x = y

@[reducible, inline]

abbrev Iris.DiscreteFunOF {C : Type u_1} (F : C → COFE.OFunctorPre) : COFE.OFunctorPre

Equations

• Iris.DiscreteFunOF F A B = ((c : C) → F c A B)

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

Equations

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

def Iris.optionChain {α : Type u_1} [OFE α] (c : Chain (Option α)) (x : α) : Chain α

Equations

• Iris.optionChain c x = { chain := fun (n : Nat) => (c.chain n).getD x, cauchy := ⋯ }

instance Iris.isCOFE_option {α : Type u_1} [OFE α] [IsCOFE α] : IsCOFE (Option α)

Equations

• Iris.isCOFE_option = { compl := fun (c : Iris.Chain (Option α)) => Option.map (fun (x : α) => Iris.IsCOFE.compl (Iris.optionChain c x)) (c.chain 0), conv_compl := ⋯ }

def Iris.optionMap {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α -n> β) : Option α -n> Option β

Equations

• Iris.optionMap f = { f := Option.map f.f, ne := ⋯ }

@[reducible, inline]

abbrev Iris.OptionOF (F : COFE.OFunctorPre) : COFE.OFunctorPre

Equations

• Iris.OptionOF F A B = Option (F A B)

instance Iris.oFunctorOption (F : COFE.OFunctorPre) [COFE.OFunctor F] : COFE.OFunctor (OptionOF F)

Equations

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

instance Iris.instOFunctorContractiveOptionOF (F : COFE.OFunctorPre) [COFE.OFunctorContractive F] : COFE.OFunctorContractive (OptionOF F)

Equations

• Iris.instOFunctorContractiveOptionOF F = { toOFunctor := Iris.oFunctorOption F, map_contractive := ⋯ }

def Iris.LimitPreserving {α : Type u_1} [COFE α] (P : α → Prop) : Prop

Equations

• Iris.LimitPreserving P = ∀ (c : Iris.Chain α), (∀ (n : Nat), P (c.chain n)) → P (Iris.IsCOFE.compl c)

theorem Iris.LimitPreserving.const {α : Type u_1} [COFE α] {P : Prop} : LimitPreserving fun (x : α) => P

theorem Iris.LimitPreserving.discrete {α : Type u_1} [COFE α] {P : α → Prop} : (∀ {x y : α}, OFE.Dist 0 x y → P x → P y) → LimitPreserving P

theorem Iris.LimitPreserving.and {α : Type u_1} [COFE α] {P Q : α → Prop} (HP : LimitPreserving P) (HQ : LimitPreserving Q) : LimitPreserving fun (a : α) => P a ∧ Q a

theorem Iris.LimitPreserving.forall {α : Type u_1} {β : Sort u_2} [COFE α] (P : β → α → Prop) (Hlim : ∀ (y : β), LimitPreserving (P y)) : LimitPreserving fun (x : α) => ∀ (y : β), P y x

theorem Iris.LimitPreserving.impl {α : Type u_1} [COFE α] (P1 P2 : α → Prop) (HP1 : ∀ {x y : α}, OFE.Dist 0 x y → P1 x → P1 y) (Hcompl : LimitPreserving P2) : LimitPreserving fun (x : α) => P1 x → P2 x

theorem Iris.LimitPreserving.equiv {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] (f g : α -n> β) : LimitPreserving fun (x : α) => OFE.Equiv (f.f x) (g.f x)

def Iris.Fixpoint.chain {α : Type u_1} [OFE α] [Inhabited α] (f : α → α) [OFE.Contractive f] : Chain α

Equations

• Iris.Fixpoint.chain f = { chain := fun (n : Nat) => Nat.repeat f (n + 1) default, cauchy := ⋯ }

def Iris.fixpoint {α : Type u_1} [COFE α] [Inhabited α] (f : α → α) [OFE.Contractive f] : α

Fixpoints inside of a COFE

Equations

• Iris.fixpoint f = Iris.IsCOFE.compl (Iris.Fixpoint.chain f)

@[reducible, inline]

abbrev Iris.OFE.ContractiveHom.fixpoint {α : Type u_1} [COFE α] [Inhabited α] (f : α -c> α) : α

Equations

• f.fixpoint = Iris.fixpoint f.f

theorem Iris.fixpoint_unfold {α : Type u_1} [COFE α] [Inhabited α] (f : α -c> α) : OFE.Equiv (fixpoint f.f) (f.f (fixpoint f.f))

theorem Iris.fixpoint_unique {α : Type u_1} [COFE α] [Inhabited α] {f : α -c> α} {x : α} (H : OFE.Equiv x (f.f x)) : OFE.Equiv x (fixpoint f.f)

instance Iris.OFE.ContractiveHom.fixpoint_ne {α : Type u_1} [COFE α] [Inhabited α] : NonExpansive fixpoint

theorem Iris.OFE.ContractiveHom.fixpoint_ind {α : Type u_1} [COFE α] [Inhabited α] (f : α -c> α) (P : α → Prop) (HProper : ∀ (A B : α), Equiv A B → P A → P B) (x : α) (Hbase : P x) (Hind : ∀ (x : α), P x → P (f.f x)) (Hlim : LimitPreserving P) : P f.fixpoint

structure Iris.Later (A : Type u) : Type (u + 1)

• next :: (
• car : A
• )

instance Iris.isOFE_later {A : Type u_1} [OFE A] : OFE (Later A)

Equations

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

instance Iris.NextContractive {A : Type} [OFE A] : OFE.Contractive Later.next

def Iris.laterChain {A : Type u_1} [OFE A] (c : Chain (Later A)) : Chain A

Equations

• Iris.laterChain c = { chain := fun (n : Nat) => (c.chain n.succ).car, cauchy := ⋯ }

instance Iris.isCOFE_later {A : Type u_1} [OFE A] [IsCOFE A] : IsCOFE (Later A)

Equations

• Iris.isCOFE_later = { compl := fun (c : Iris.Chain (Iris.Later A)) => { car := Iris.IsCOFE.compl (Iris.laterChain c) }, conv_compl := ⋯ }

def Iris.laterMap {A : Type u_1} {B : Type u_2} [OFE A] [OFE B] (f : A -n> B) : Later A -n> Later B

Equations

• Iris.laterMap f = { f := fun (x : Iris.Later A) => { car := f.f x.car }, ne := ⋯ }

@[reducible, inline]

abbrev Iris.LaterOF (F : COFE.OFunctorPre) : COFE.OFunctorPre

Equations

• Iris.LaterOF F A B = Iris.Later (F A B)

instance Iris.oFunctorLater (F : COFE.OFunctorPre) [COFE.OFunctor F] : COFE.OFunctor (LaterOF F)

Equations

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

instance Iris.instOFunctorContractiveLaterOF (F : COFE.OFunctorPre) [COFE.OFunctorContractive F] : COFE.OFunctorContractive (LaterOF F)

Equations

• Iris.instOFunctorContractiveLaterOF F = { toOFunctor := Iris.oFunctorLater F, map_contractive := ⋯ }