Ordered families of equivalences and complete step-indexed spaces.

Copyright (c) The Iris-Lean Contributors.

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

Ordered family of equivalences

• Dist : Nat → α → α → Prop

  The equivalence relation at a specified step index.

• 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

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

Notation for equivalence at a specified step index.

Equations

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

theorem Iris.OFE.eq_dist {α : Type u_1} [self : OFE α] {x y : α} : x = y ↔ ∀ (n : Nat), Dist n x y

theorem Iris.OFE.eq_dist_1 {α : Type u_1} [self : OFE α] {x y : α} : x = y → ∀ (n : Nat), Dist n x y

theorem Iris.OFE.eq_dist_2 {α : Type u_1} [self : OFE α] {x y : α} : (∀ (n : Nat), Dist n x y) → x = y

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

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

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

@[simp]

theorem Iris.OFE.Dist.refl {α : 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 Eq.dist {α : Type u_1} {n : Nat} [Iris.OFE α] {x y : α} (h : x = y) : Iris.OFE.Dist n x y

@[instance_reducible]

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

instance Iris.OFE.const_ne {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {x : α} : NonExpansive (Function.const β x)

theorem Iris.OFE.NonExpansive.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] {g : β → γ} {f : α → β} (hg : NonExpansive g) (hf : NonExpansive f) : NonExpansive (g ∘ f)

Note: Not an instance, as any function can be decomposed as a composition in multiple ways.

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₂.ne_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] (f : α → β → γ) [NonExpansive₂ f] (a : α) : NonExpansive (f a)

Note: Not an instance, for symmetry with NonExpansive₂.ne_left, which cannot be an instance.

theorem Iris.OFE.NonExpansive₂.ne_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] (f : α → β → γ) [NonExpansive₂ f] (b : β) : NonExpansive fun (x : α) => f x b

Note: Not an instance, due to instance coherence problems.

class Iris.OFE.NonExpansive₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [OFE α] [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₂ → ∀ ⦃z₁ z₂ : γ⦄, Dist n z₁ z₂ → Dist n (f x₁ y₁ z₁) (f x₂ y₂ z₂)

class Iris.OFE.NonExpansive₄ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} [OFE α] [OFE β] [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₂ → ∀ ⦃z₁ z₂ : γ⦄, Dist n z₁ z₂ → ∀ ⦃w₁ w₂ : δ⦄, Dist n w₁ w₂ → Dist n (f x₁ y₁ z₁ w₁) (f x₂ y₂ z₂ w₂)

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

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

@[simp]

theorem Iris.OFE.DistLater.refl {α : 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 + 1)-equivalence is equivalent to n-equivalence.

theorem Iris.OFE.distLater_soundness {α : Type u_1} [OFE α] {x y : α} (H : ∀ (n : Nat), DistLater n x y → Dist n x y) : x = y

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.ne_dist_later {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) [NonExpansive f] {n : Nat} {x y : α} (h : DistLater n x y) : DistLater n (f x) (f y)

Pre-composing a non-expansive function preserves DistLater.

theorem Iris.OFE.dist_pointwise_lt {β : Type u_1} {α : Sort u_2} [OFE β] {n m : Nat} {f g : α → β} (hlt : m < n) (hp : ∀ (a : α), DistLater n (f a) (g a)) (a : α) : Dist m (f a) (g a)

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

Constant functions are contractive.

@[reducible]

def Iris.OFE.ofDiscrete (α : Type u_1) : OFE α

The discrete OFE obtained from an equality relation Eq

Equations

• Iris.OFE.ofDiscrete α = { Dist := fun (x : Nat) => Eq, dist_eqv := ⋯, eq_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 → x = y

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

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

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

theorem Iris.OFE.discreteE_eq {α : Type u_1} [OFE α] {x y : α} (h : x = y) : DiscreteE x ↔ DiscreteE y

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

For discrete OFEs, n-equivalence implies equality.

instance Iris.OFE.Discrete.toDiscreteE {α : Type u_1} [OFE α] [Discrete α] (x : α) : DiscreteE x

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, 0-equivalence implies equivalence for any n.

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

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

@[reducible]

def Iris.OFE.ofQuotient {X : Type u} {s : Setoid X} (dist : Nat → X → X → Prop) (heqv : ∀ {n : Nat}, Equivalence (dist n)) (hlt : ∀ {n m : Nat} {x y : X}, dist n x y → m < n → dist m x y) (hs : ∀ (x y : X), Setoid.r x y ↔ ∀ (n : Nat), dist n x y) : OFE (Quotient s)

Build a Leibniz OFE on Quotient s from a step-indexed distance dist on the carrier, given that the setoid relation coincides with the OFE equivalence fun x y => ∀ n, dist n x y (hypothesis hs). Quotienting forces the resulting OFE equality to be Leibniz, while Quotient.sound/Quotient.exact keep speaking about the domain relation s.r. See https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean/topic/Evaluating.20a.20specialization.20to.20Leibnize.20OFE.27s/with/606745235

Equations

• Iris.OFE.ofQuotient dist heqv hlt hs = { Dist := fun (n : Nat) => Quotient.lift₂ (dist n) ⋯, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

theorem Iris.OFE.ofQuotient.dist_mk {X : Type u} {s : Setoid X} {dist : Nat → X → X → Prop} {heqv : ∀ {n : Nat}, Equivalence (dist n)} {hlt : ∀ {n m : Nat} {x y : X}, dist n x y → m < n → dist m x y} {hs : ∀ (x y : X), Setoid.r x y ↔ ∀ (n : Nat), dist n x y} {n : Nat} {x y : X} : Dist n (Quotient.mk s x) (Quotient.mk s y) ↔ dist n 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 : α → β

  The underlying function of a non-expansive morphism.

• 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_reducible]

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)

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

The constant non-expansive morphism with a specified value.

Equations

• Iris.OFE.Hom.const x = { f := Function.const α x, ne := ⋯ }

@[simp]

theorem Iris.OFE.Hom.const_apply {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {x : β} {a : α} : (Hom.const x).f a = x

def Iris.OFE.Hom.ofSubtype {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : { f : α → β // NonExpansive f }) : α -n> β

Construct a Hom from a subtype bundling a function with its nonexpansiveness proof.

Equations

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

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

A bundled contractive function between ordered equivalence spaces.

• 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

Notation for a bundled contractive map.

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_reducible]

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

def Function.toContractiveHom {α : Type u_1} {β : Type u_2} (f : α → β) [Iris.OFE α] [Iris.OFE β] [ι : Iris.OFE.Contractive f] : α -c> β

Bundle a function with its available contractiveness instance.

Equations

• Function.toContractiveHom f = { f := f, ne := ⋯, contractive := ι }

@[simp]

theorem Function.toContractiveHom_apply {α : Type u_1} {β : Type u_2} {f : α → β} [Iris.OFE α] [Iris.OFE β] [ι : Iris.OFE.Contractive f] {x : α} : (toContractiveHom f).f x = f x

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

@[instance_reducible]

instance Iris.OFE.unitOFE : OFE Unit

Equations

• Iris.OFE.unitOFE = { Dist := fun (x : Nat) (x_1 x_2 : Unit) => True, dist_eqv := @Iris.OFE.unitOFE._proof_2, eq_dist' := @Iris.OFE.unitOFE._proof_1, dist_lt := ⋯ }

instance Iris.OFE.instDiscreteEUnitUnit : DiscreteE ()

@[instance_reducible]

instance Iris.OFE.instEmpty : OFE Empty

Equations

• Iris.OFE.instEmpty = { Dist := fun (x : Nat) (x_1 x_2 : Empty) => True, dist_eqv := @Iris.OFE.instEmpty._proof_1, eq_dist' := @Iris.OFE.instEmpty._proof_2, dist_lt := ⋯ }

@[instance_reducible]

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

Equations

• Iris.OFE.instULift = { Dist := fun (n : Nat) (x y : ULift α) => Iris.OFE.Dist n x.down y.down, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

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

The non-expansive injection into a universe lift.

Equations

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

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

The non-expansive projection from a universe lift.

Equations

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

@[instance_reducible]

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

Equations

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

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

@[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.dist_none {α : Type u_1} {n : Nat} [OFE α] {o : Option α} : Dist n 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

def Iris.OFE.distSome {α : Type u_1} [OFE α] {n : Nat} {mx : Option α} {y : α} (h : Dist n mx (some y)) : (z : α) ×' mx = some z ∧ Dist n y z

Data-valued form of dist_some, for building the witnesses of ORA.extend.

Equations

• Iris.OFE.distSome h_2 = ⟨val, ⋯⟩
• Iris.OFE.distSome h_2 = False.elim h_2

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

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

theorem Iris.OFE.dist_some_inv_l' {α : Type u_1} [OFE α] {n : Nat} {my : Option α} {x : α} (h : Dist n (some x) my) : ∃ (x' : α), some x' = my ∧ Dist n x x'

theorem Iris.OFE.fmap_some_dist {β : Type u_1} {α : Type u_2} [OFE β] (f : α → β) {mx : Option α} {y : β} {n : Nat} : Dist n (Option.map f mx) (some y) ↔ ∃ (x : α), mx = some x ∧ Dist n y (f x)

instance Iris.OFE.Option.some.ne {α : Type u_1} [OFE α] : NonExpansive some

instance Iris.OFE.Option.some_is_discrete {α : Type u_1} [OFE α] {e : α} [DiscreteE e] : DiscreteE (some e)

theorem Iris.OFE.Option.ne_match {α : Type u_1} [OFE α] {B : Type u_2} [OFE B] (f : α → B) (hf : NonExpansive f) (g : B) : NonExpansive fun (x : Option α) => match x with | some a => f a | none => g

Note: Not an instance, due to instance coherence problems.

instance Iris.OFE.Option.none_is_discrete {α : Type u_1} [OFE α] : DiscreteE none

instance Iris.OFE.Option.merge_ne {α : Type u_1} [OFE α] {op : α → α → α} [NonExpansive₂ op] : NonExpansive₂ (Option.merge op)

instance Iris.OFE.Option.bind_fun_ne {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → Option β) [NonExpansive f] : NonExpansive (flip Option.bind f)

theorem Iris.OFE.Option.bind_dist {β : Type u_1} {α : Type u_2} {n : Nat} [OFE β] {x : Option α} {f g : α → Option β} (H : ∀ (x : α), Dist n (f x) (g x)) : Dist n (x.bind f) (x.bind g)

@[reducible, inline]

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

A pointwise family of ordered equivalence structures.

Equations

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

@[instance_reducible]

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

Equations

• Iris.OFE.instForallOfOFEFun = { Dist := fun (n : Nat) (f g : (x : α) → β x) => ∀ (x : α), Iris.OFE.Dist n (f x) (g x), dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

@[instance_reducible]

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

Equations

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

instance Iris.OFE.ofe_mor_car_ne {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive₂ fun (f : α -n> β) (x : α) => f.f x

@[instance_reducible]

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

Equations

• Iris.OFE.instInhabitedHom = { default := { f := Function.const α default, ne := ⋯ } }

@[instance_reducible]

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

Equations

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

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

Evaluate a dependent function at a specified argument.

Equations

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

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

Evaluate a bundled non-expansive morphism at a specified argument.

Equations

• Iris.OFE.applyNe x = { f := fun (f : α -n> β) => f.f x, ne := ⋯ }

instance Iris.OFE.instNonExpansiveHomApplyNe {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive applyNe

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

Apply a family of non-expansive maps pointwise to dependent functions.

Equations

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

theorem Iris.OFE.mapCodHom_id {α : Type u_1} {β : α → Type u_2} [OFEFun β] (g : (x : α) → β x) : (mapCodHom fun (x : α) => Hom.id).f g = g

theorem Iris.OFE.mapCodHom_compose {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} {β₃ : α → Type u_4} [OFEFun β₁] [OFEFun β₂] [OFEFun β₃] (f₁ : (x : α) → β₁ x -n> β₂ x) (f₂ : (x : α) → β₂ x -n> β₃ x) (g : (x : α) → β₁ x) : (mapCodHom fun (x : α) => (f₂ x).comp (f₁ x)).f g = (mapCodHom f₂).f ((mapCodHom f₁).f g)

instance Iris.OFE.mapCod_lookup_discrete {α : Type u_1} {β : α → Type u_2} [OFEFun β] (f : (x : α) → β x) (x : α) [hf : DiscreteE f] : DiscreteE (f x)

@[instance_reducible]

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

Equations

• Iris.OFE.instProd = { Dist := fun (n : Nat) (a b : α × β) => Iris.OFE.Dist n a.fst b.fst ∧ Iris.OFE.Dist n a.snd b.snd, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

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₂)

instance Iris.OFE.Prod.mk_ne {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive₂ Prod.mk

theorem Iris.OFE.prod_mk_ne_left {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (b : β) : NonExpansive fun (x : α) => (x, b)

Note: Not an instance, due to instance coherence problems.

theorem Iris.OFE.prod_mk_ne_right {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (a : α) : NonExpansive fun (x : β) => (a, x)

Note: Not an instance, due to instance coherence problems.

instance Iris.OFE.instNonExpansiveProdFst {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive Prod.fst

instance Iris.OFE.instNonExpansiveProdSnd {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive Prod.snd

theorem Iris.OFE.NonExpansive₂.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] {f : α → β → γ} (hf : NonExpansive₂ f) : NonExpansive (Function.uncurry f)

Note: Not an instance, due to instance coherence problems.

theorem Iris.OFE.NonExpansive.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] {f : α × β → γ} (hf : NonExpansive f) : NonExpansive₂ (Function.curry f)

Note: Not an instance, due to instance coherence problems.

theorem Iris.OFE.NonExpansive.curry₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [OFE α] [OFE β] [OFE γ] [OFE δ] {f : α × β × γ → δ} (hf : NonExpansive f) : NonExpansive₃ fun (a : α) (b : β) (c : γ) => f (a, b, c)

Note: Not an instance, due to instance coherence problems.

theorem Iris.OFE.NonExpansive₃.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [OFE α] [OFE β] [OFE γ] [OFE δ] {f : α → β → γ → δ} (hf : NonExpansive₃ f) : NonExpansive fun (p : α × β × γ) => f p.fst p.snd.fst p.snd.snd

Note: Not an instance, due to instance coherence problems.

theorem Iris.OFE.NonExpansive.curry₄ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} [OFE α] [OFE β] [OFE γ] [OFE δ] [OFE ε] {f : α × β × γ × δ → ε} (hf : NonExpansive f) : NonExpansive₄ fun (a : α) (b : β) (c : γ) (d : δ) => f (a, b, c, d)

Note: Not an instance, due to instance coherence problems.

theorem Iris.OFE.NonExpansive₄.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} [OFE α] [OFE β] [OFE γ] [OFE δ] [OFE ε] {f : α → β → γ → δ → ε} (hf : NonExpansive₄ f) : NonExpansive fun (p : α × β × γ × δ) => f p.fst p.snd.fst p.snd.snd.fst p.snd.snd.snd

Note: Not an instance, due to instance coherence problems.

instance Iris.OFE.prod.is_discrete {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {a : α} {b : β} [DiscreteE a] [DiscreteE b] : DiscreteE (a, b)

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

@[instance_reducible]

instance Iris.OFE.instSum {α : 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.dist_inl {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {n : Nat} {x y : α} (h : Dist n x y) : Dist n (Sum.inl x) (Sum.inl y)

theorem Iris.OFE.dist_inr {α : Type u_2} {β : Type u_1} [OFE α] [OFE β] {n : Nat} {x y : β} (h : Dist n x y) : Dist n (Sum.inr x) (Sum.inr y)

theorem Iris.OFE.dist_ext_left {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {n : Nat} {x y : α} (h : Dist n (Sum.inl x) (Sum.inl y)) : Dist n x y

theorem Iris.OFE.dist_ext_right {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {n : Nat} {x y : β} (h : Dist n (Sum.inr x) (Sum.inr y)) : Dist n x y

instance Iris.OFE.instNonExpansiveInl {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive Sum.inl

instance Iris.OFE.instNonExpansiveInr {α : Type u_2} {β : Type u_1} [OFE α] [OFE β] : NonExpansive Sum.inr

instance Iris.OFE.instNonExpansiveElim {α : Type u_2} {β : Type u_3} [OFE α] [OFE β] {γ : Type u_1} [OFE γ] {f₁ : α → γ} {f₂ : β → γ} [NonExpansive f₁] [NonExpansive f₂] : NonExpansive (Sum.elim f₁ f₂)

theorem Iris.OFE.discreteE_inl {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {a : α} (Ha : DiscreteE a) : DiscreteE (Sum.inl a)

theorem Iris.OFE.discreteE_inr {α : Type u_2} {β : Type u_1} [OFE α] [OFE β] {a : β} (Ha : DiscreteE a) : DiscreteE (Sum.inr a)

instance Iris.OFE.instDiscreteSum {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] [Discrete α] [Discrete β] : Discrete (α ⊕ β)

@[instance_reducible]

instance Iris.OFE.instSubtype {α : Type u_1} [OFE α] (P : α → Prop) : OFE (Subtype P)

Equations

• Iris.OFE.instSubtype P = { Dist := fun (n : Nat) (x y : Subtype P) => Iris.OFE.Dist n x.val y.val, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

instance Iris.OFE.instDiscreteESubtypeOfVal {α : Type u_1} [OFE α] (P : α → Prop) (x : Subtype P) [DiscreteE x.val] : DiscreteE x

instance Iris.OFE.instDiscreteSubtype {α : Type u_1} [OFE α] [Discrete α] (P : α → Prop) : Discrete (Subtype P)

theorem Iris.OFE.exist_ne {α : Type u_1} [OFE α] {P : α → Prop} {n : Nat} {a1 a2 : α} (H1 : P a1) (H2 : P a2) (h : Dist n a1 a2) : Dist n ⟨a1, H1⟩ ⟨a2, H2⟩

instance Iris.OFE.instNonExpansiveSubtypeVal {α : Type u_1} [OFE α] (P : α → Prop) : NonExpansive Subtype.val

instance Iris.OFE.Hom.ofSubtype_ne {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive ofSubtype

def Iris.OFE.Hom.toSubtype {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α -n> β) : { f : α → β // NonExpansive f }

Extract the underlying subtype from a Hom.

Equations

• f.toSubtype = ⟨f.f, ⋯⟩

instance Iris.OFE.Hom.toSubtype_ne {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] : NonExpansive toSubtype

@[instance_reducible]

instance Iris.OFE.instOFESigma {α : Type u_1} (P : α → Type u_2) [(x : α) → OFE (P x)] : OFE (Sigma P)

Equations

• Iris.OFE.instOFESigma P = { Dist := fun (n : Nat) (x y : Sigma P) => ∃ (heq : x.fst = y.fst), Iris.OFE.Dist n (heq ▸ x.snd) y.snd, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

instance Iris.OFE.instDiscreteESigma {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] {x : Sigma P} [inst : DiscreteE x.snd] : DiscreteE x

instance Iris.OFE.instDiscreteSigma {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] [∀ (x : α), Discrete (P x)] : Discrete (Sigma P)

theorem Iris.OFE.Sigma.dist_eq {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] {n : Nat} {x1 x2 : Sigma P} : Dist n x1 x2 ↔ ∃ (heq : x1.fst = x2.fst), Dist n (heq ▸ x1.snd) x2.snd

instance Iris.OFE.Sigma.fst_ne {α : Type u_1} {P : α → Type u_2} [OFE α] [(x : α) → OFE (P x)] : NonExpansive Sigma.fst

theorem Iris.OFE.Sigma.dist_fst {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] {n : Nat} {x y : Sigma P} (h : Dist n x y) : x.fst = y.fst

The first components of n-equivalent dependent pairs are equal.

Split out of Sigma.dist_snd so that the projection happens in a body rather than in a statement: in a statement the OFE (Sigma P) instance argument is still an unsolved metavariable, so h's type cannot be reduced to the ∃ heq, .. of instOFESigma to project out of.

theorem Iris.OFE.Sigma.dist_snd {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] {n : Nat} {x y : Sigma P} (h : Dist n x y) : Dist n (⋯ ▸ x.snd) y.snd

theorem Iris.OFE.Sigma.mk_dist {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] {n : Nat} {i1 i2 : α} {v1 : P i1} {v2 : P i2} (heq : i1 = i2) (h : Dist n (heq ▸ v1) v2) : Dist n ⟨i1, v1⟩ ⟨i2, v2⟩

instance Iris.OFE.Sigma.mk_ne {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] (a : α) : NonExpansive (Sigma.mk a)

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> β

  The forward non-expansive map of an isomorphism.

• inv : β -n> α

  The inverse non-expansive map of an isomorphism.

• hom_inv {x : β} : self.hom.f (self.inv.f x) = x
• inv_hom {x : α} : self.inv.f (self.hom.f x) = x

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

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

@[instance_reducible]

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

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

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 : α⦄ : x = y ↔ 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 : β⦄ : x = y ↔ 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 → α

  The approximation at each natural-number index.

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

@[instance_reducible]

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)

theorem Iris.Chain.chain_none_const {V : Type u_1} {n : Nat} [OFE V] {c : Chain (Option V)} (H : c.chain n = none) : c = const none

If a chain of Option is ever none, is the constant none chain.

theorem Iris.Chain.chain_option_some {V : Type u_1} {n : Nat} {v : V} [OFE V] {c : Chain (Option V)} (H : c.chain n = some v) : ∃ (c' : Chain V), c = map { f := some, ne := ⋯ } c'

If a chain of Option is ever some, it is the lift a chain by some.

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

Complete ordered family of equivalences

• compl : Chain α → α

  Complete a Cauchy chain in the ordered equivalence space.

• 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

• 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
• compl : Chain α → α
• conv_compl {n : Nat} {c : Chain α} : OFE.Dist n (compl c) (c.chain n)

@[instance_reducible]

instance Iris.instCOFEOfIsCOFE {α : Type u_1} [OFE α] [IsCOFE α] : COFE α

Equations

• Iris.instCOFEOfIsCOFE = { toOFE := inst✝¹, toIsCOFE := inst✝ }

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 α) : 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 : α) : 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 α) : compl c = c.chain 0

Completion of discrete COFEs is the constant value.

@[reducible]

def Iris.COFE.ofDiscrete (α : Type u_1) : COFE α

The discrete COFE obtained from an equality relation Eq

Equations

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

@[instance_reducible]

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.instDiscreteUnit : OFE.Discrete Unit

@[instance_reducible]

instance Iris.COFE.instUnit : COFE Unit

Equations

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

instance Iris.COFE.instDiscreteEmpty : OFE.Discrete Empty

@[instance_reducible]

instance Iris.COFE.instEmpty : COFE Empty

Equations

• Iris.COFE.instEmpty = { toOFE := Iris.OFE.instEmpty, compl := fun (c : Iris.Chain Empty) => (c.chain 0).elim, conv_compl := @Iris.COFE.instEmpty._proof_1 }

@[reducible, inline]

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

Pointwise completeness of a family of ordered equivalence spaces.

Equations

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

@[instance_reducible]

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.

@[instance_reducible]

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

Equations

• Iris.COFE.instIsCOFEHom = { compl := fun (c : Iris.Chain (α -n> β)) => { f := fun (x : α) => Iris.IsCOFE.compl (Iris.Chain.map (Iris.OFE.applyNe x) c), ne := ⋯ }, conv_compl := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Iris.COFE.instIsCOFESum {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] [IsCOFE α] [IsCOFE β] : IsCOFE (α ⊕ β)

Equations

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

theorem Iris.COFE.Sigma.chain_const_proj1 {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] (c : Chain (Sigma P)) (n : Nat) : (c.chain n).fst = (c.chain 0).fst

def Iris.COFE.Sigma.chainMapSnd {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] (c : Chain (Sigma P)) : Chain (P (c.chain 0).fst)

Transport a dependent-pair chain into the fiber of its constant first component.

Equations

• Iris.COFE.Sigma.chainMapSnd c = { chain := fun (n : Nat) => ⋯ ▸ (c.chain n).snd, cauchy := ⋯ }

@[instance_reducible]

instance Iris.COFE.instIsCOFESigma {α : Type u_1} {P : α → Type u_2} [(x : α) → OFE (P x)] [(x : α) → IsCOFE (P x)] : IsCOFE (Sigma P)

Equations

• Iris.COFE.instIsCOFESigma = { compl := fun (c : Iris.Chain (Sigma P)) => ⟨(c.chain 0).fst, Iris.IsCOFE.compl (Iris.COFE.Sigma.chainMapSnd c)⟩, conv_compl := ⋯ }

class Iris.COFE.OFunctor (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 equivalence spaces with a non-expansive action.

• ofe {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : OFE (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -n> 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.COFE.OFunctorContractive (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) extends Iris.COFE.OFunctor F : Type (max (max (u_1 + 1) (u_2 + 1)) u_3)

A mixed-variance space functor whose action on morphisms is contractive.

• ofe {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : OFE (F α β)
• map {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} [COFE α₁] [COFE α₂] [COFE β₁] [COFE β₂] : (α₂ -n> α₁) → (β₁ -n> β₂) → F α₁ β₁ -n> 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 OFunctor.map)

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

A type equipped with equality as its step-indexed equivalence.

• car : α

  The underlying element of a discrete ordered equivalence space.

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

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

@[instance_reducible]

instance Iris.instCOFEDiscreteO {α : Type u_1} : COFE (DiscreteO α)

Equations

• Iris.instCOFEDiscreteO = Iris.COFE.ofDiscrete (Iris.DiscreteO α)

instance Iris.instDiscreteDiscreteO {α : Type u_1} : OFE.Discrete (DiscreteO α)

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

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

@[reducible, inline]

abbrev Iris.ComposeOF (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₂ α β)] (α β : Type u_3) [COFE α] [COFE β] : Type u_2

The composition of two functors, F₁ applied to F₂.

Equations

• Iris.ComposeOF F₁ F₂ α β = F₁ (F₂ β α) (F₂ α β)

theorem Iris.COFE.OFunctor.map_id_eq {α : Type u_1} {β : Type u_2} {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [OFunctor F] [COFE α] [COFE β] : map OFE.Hom.id OFE.Hom.id = OFE.Hom.id

theorem Iris.COFE.OFunctor.map_comp_eq {α₁ α₂ α₃ : Type u_1} {β₁ β₂ β₃ : Type u_2} {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [OFunctor F] [COFE α₁] [COFE α₂] [COFE α₃] [COFE β₁] [COFE β₂] [COFE β₃] (f : α₂ -n> α₁) (g : α₃ -n> α₂) (f' : β₁ -n> β₂) (g' : β₂ -n> β₃) : map (f.comp g) (g'.comp f') = (map g g').comp (map f f')

theorem Iris.COFE.OFunctorContractive.map_distLater {α₁ α₂ : Type u_1} {β₁ β₂ : Type u_2} {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [OFunctorContractive 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 ((OFunctor.map f₁ g₁).f x) ((OFunctor.map f₂ g₂).f x)

@[instance_reducible]

instance Iris.oFunctorComposeOF {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₂ α β)] [COFE.OFunctor F₁] : COFE.OFunctor (ComposeOF F₁ F₂)

Equations

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

@[instance_reducible]

instance Iris.oFunctorComposeOFContractiveLeft {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₂ α β)] [COFE.OFunctorContractive F₁] : COFE.OFunctorContractive (ComposeOF F₁ F₂)

Equations

• Iris.oFunctorComposeOFContractiveLeft = { toOFunctor := Iris.oFunctorComposeOF, map_contractive := ⋯ }

@[instance_reducible]

instance Iris.oFunctorComposeOFContractiveRight {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₂ α β)] [COFE.OFunctor F₁] : COFE.OFunctorContractive (ComposeOF F₁ F₂)

Equations

• Iris.oFunctorComposeOFContractiveRight = { toOFunctor := Iris.oFunctorComposeOF, map_contractive := ⋯ }

@[reducible, inline]

abbrev Iris.DiscreteFunOF {C : Type u_1} (F : C → (α : Type u_2) → (β : Type u_3) → [COFE α] → [COFE β] → Type u_4) (α : Type u_2) (β : Type u_3) [COFE α] [COFE β] : Type (max u_1 u_4)

The pointwise product of an indexed family of space functors.

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Iris.oFunctorDiscreteFunOFContractive F = { toOFunctor := Iris.oFunctorDiscreteFunOF F, map_contractive := ⋯ }

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

Extract a chain of values from an optional chain, using a fallback for absence.

Equations

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

@[instance_reducible]

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

Equations

• Iris.isCOFEOption = { 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 β

Lift a non-expansive map to optional values.

Equations

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

theorem Iris.Option.map_ne {α : Type u_2} [OFE α] {β : Type u_1} [OFE β] {f g : α → β} {x y : Option α} {n : Nat} : (∀ (x y : α), OFE.Dist n x y → OFE.Dist n (f x) (g y)) → OFE.Dist n x y → OFE.Dist n (Option.map f x) (Option.map g y)

instance Iris.optionMap_ne {α : Type u_2} [OFE α] {β : Type u_1} [OFE β] : OFE.NonExpansive optionMap

theorem Iris.Option.bind_ne {α : Type u_2} [OFE α] {β : Type u_1} [OFE β] {f g : α → Option β} {x y : Option α} {n : Nat} (hf : ∀ (x y : α), OFE.Dist n x y → OFE.Dist n (f x) (g y)) (hxy : OFE.Dist n x y) : OFE.Dist n (x.bind f) (y.bind g)

theorem Iris.Option.join_ne {α : Type u_1} [OFE α] {x y : Option (Option α)} {n : Nat} (hxy : OFE.Dist n x y) : OFE.Dist n x.join y.join

theorem Iris.Option.elim_ne {α : Type u_2} [OFE α] {β : Type u_1} (R : β → β → Prop) {f g : α → β} {d d' : β} {x y : Option α} {n : Nat} (hf : ∀ (x y : α), OFE.Dist n x y → R (f x) (g y)) (hd : R d d') (hxy : OFE.Dist n x y) : R (x.elim d f) (y.elim d' g)

@[reducible, inline]

abbrev Iris.OptionOF (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) (α : Type u_1) (β : Type u_2) [COFE α] [COFE β] : Type u_3

Lift a space functor to optional values.

Equations

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

@[instance_reducible]

instance Iris.oFunctorOption (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [COFE.OFunctor F] : COFE.OFunctor (OptionOF F)

Equations

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

@[instance_reducible]

instance Iris.instOFunctorContractiveOptionOF (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [COFE.OFunctorContractive F] : COFE.OFunctorContractive (OptionOF F)

Equations

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

instance Iris.instNonExpansiveProdMap {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [OFE A] [OFE A'] [OFE B] [OFE B'] (f : A → A') (g : B → B') [OFE.NonExpansive f] [OFE.NonExpansive g] : OFE.NonExpansive (Prod.map f g)

theorem Iris.Prod.map_ext {A : Type u_1} {A' : Type u_3} {B : Type u_2} {B' : Type u_4} {x : A × B} {f f' : A → A'} {g g' : B → B'} (Hf : ∀ (a : A), f a = f' a) (Hg : ∀ (a : B), g a = g' a) : Prod.map f g x = Prod.map f' g' x

theorem Iris.Prod.map_ne {A : Type u_1} {A' : Type u_3} {B : Type u_2} {B' : Type u_4} [OFE A'] [OFE B'] {n : Nat} {x : A × B} {f f' : A → A'} {g g' : B → B'} (Hf : ∀ (a : A), OFE.Dist n (f a) (f' a)) (Hg : ∀ (a : B), OFE.Dist n (g a) (g' a)) : OFE.Dist n (Prod.map f g x) (Prod.map f' g' x)

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

The product of two non-expansive maps.

Equations

• Iris.Prod.mapO f g = { f := Prod.map f.f g.f, ne := ⋯ }

instance Iris.Prod.mapO_ne {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [OFE A] [OFE A'] [OFE B] [OFE B'] : OFE.NonExpansive₂ mapO

@[reducible, inline]

abbrev Iris.ProdOF (F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) (F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4) (α : Type u_1) (β : Type u_2) [COFE α] [COFE β] : Type (max u_4 u_3)

The pointwise product of two mixed-variance space functors.

Equations

• Iris.ProdOF F1 F2 A B = (F1 A B × F2 A B)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• Iris.instOFunctorContractiveProdOF = { toOFunctor := Iris.instOFunctorProdOF, map_contractive := ⋯ }

instance Iris.instNonExpansiveSumMap {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [OFE A] [OFE A'] [OFE B] [OFE B'] (f : A → A') (g : B → B') [OFE.NonExpansive f] [OFE.NonExpansive g] : OFE.NonExpansive (Sum.map f g)

theorem Iris.Sum.map_ext {A : Type u_1} {A' : Type u_3} {B : Type u_2} {B' : Type u_4} {x : A ⊕ B} {f f' : A → A'} {g g' : B → B'} (Hf : ∀ (a : A), f a = f' a) (Hg : ∀ (a : B), g a = g' a) : Sum.map f g x = Sum.map f' g' x

theorem Iris.Sum.map_ne {A : Type u_1} {A' : Type u_3} {B : Type u_2} {B' : Type u_4} [OFE A'] [OFE B'] {n : Nat} {x : A ⊕ B} {f f' : A → A'} {g g' : B → B'} (Hf : ∀ (a : A), OFE.Dist n (f a) (f' a)) (Hg : ∀ (a : B), OFE.Dist n (g a) (g' a)) : OFE.Dist n (Sum.map f g x) (Sum.map f' g' x)

def Iris.Sum.mapO {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [OFE A] [OFE A'] [OFE B] [OFE B'] (f : A -n> A') (g : B -n> B') : A ⊕ B -n> A' ⊕ B'

The sum of two non-expansive maps.

Equations

• Iris.Sum.mapO f g = { f := Sum.map f.f g.f, ne := ⋯ }

instance Iris.Sum.mapO_ne {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [OFE A] [OFE A'] [OFE B] [OFE B'] : OFE.NonExpansive₂ mapO

@[reducible, inline]

abbrev Iris.SumOF (F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) (F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4) (α : Type u_1) (β : Type u_2) [COFE α] [COFE β] : Type (max u_4 u_3)

The pointwise sum of two mixed-variance space functors.

Equations

• Iris.SumOF F1 F2 A B = (F1 A B ⊕ F2 A B)

@[instance_reducible]

instance Iris.instOFunctorSumOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4} [COFE.OFunctor F1] [COFE.OFunctor F2] : COFE.OFunctor (SumOF F1 F2)

Equations

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

@[instance_reducible]

instance Iris.instOFunctorContractiveSumOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_4} [COFE.OFunctorContractive F1] [COFE.OFunctorContractive F2] : COFE.OFunctorContractive (SumOF F1 F2)

Equations

• Iris.instOFunctorContractiveSumOF = { toOFunctor := Iris.instOFunctorSumOF, map_contractive := ⋯ }

def Iris.Sigma.mapO {A : Type u_1} {P1 : A → Type u_2} {P2 : A → Type u_3} [(x : A) → OFE (P1 x)] [(x : A) → OFE (P2 x)] : ((a : A) → P1 a -n> P2 a) -n> Sigma P1 -n> Sigma P2

Map non-expansive fiber maps over dependent pairs.

Equations

• Iris.Sigma.mapO = { f := fun (g : (a : A) → P1 a -n> P2 a) => { f := fun (x : Sigma P1) => ⟨x.fst, (g x.fst).f x.snd⟩, ne := ⋯ }, ne := ⋯ }

@[reducible, inline]

abbrev Iris.SigmaOF {A : Type u_1} (F : A → (α : Type u_2) → (β : Type u_3) → [COFE α] → [COFE β] → Type u_4) (α : Type u_2) (β : Type u_3) [COFE α] [COFE β] : Type (max u_4 u_1)

The dependent sum of an indexed family of space functors.

Equations

• Iris.SigmaOF F B C = ((a : A) × F a B C)

@[instance_reducible]

instance Iris.instOFunctorSigmaOF {A : Type u_1} {F : A → (α : Type u_2) → (β : Type u_3) → [COFE α] → [COFE β] → Type u_4} [(a : A) → COFE.OFunctor (F a)] : COFE.OFunctor (SigmaOF F)

Equations

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

@[instance_reducible]

instance Iris.instOFunctorContractiveSigmaOF {A✝ : Type u_1} {F : A✝ → (α : Type u_2) → (β : Type u_3) → [COFE α] → [COFE β] → Type u_4} [(a : A✝) → COFE.OFunctorContractive (F a)] : COFE.OFunctorContractive (SigmaOF F)

Equations

• Iris.instOFunctorContractiveSigmaOF = { toOFunctor := Iris.instOFunctorSigmaOF, map_contractive := ⋯ }

def Iris.termConstOF : Lean.ParserDescr

The constant mixed-variance space family.

Equations

• Iris.termConstOF = Lean.ParserDescr.node `Iris.termConstOF 1024 (Lean.ParserDescr.symbol "constOF")

@[instance_reducible]

instance Iris.oFunctorConstOF {B : Type u_1} [OFE B] : COFE.OFunctor ((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.constOFContractive {B : Type u_1} [OFE B] : COFE.OFunctorContractive ((fun (B : Type u_1) (A : Type u_2) (C : Type u_3) [COFE A] [COFE C] => B) B)

Equations

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

def Iris.termIdOF : Lean.ParserDescr

The space family selecting its covariant argument.

Equations

• Iris.termIdOF = Lean.ParserDescr.node `Iris.termIdOF 1024 (Lean.ParserDescr.symbol "IdOF")

@[instance_reducible]

instance Iris.instOFunctor : COFE.OFunctor fun (A : Type u_1) (B : Type u_2) [COFE A] [COFE B] => B

Equations

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

def Iris.Hom.map {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [OFE A] [OFE A'] [OFE B] [OFE B'] (pre : A' -n> A) (post : B -n> B') : (A -n> B) -n> A' -n> B'

Precompose and postcompose a non-expansive map.

Equations

• Iris.Hom.map pre post = { f := fun (h : A -n> B) => post.comp (h.comp pre), ne := ⋯ }

instance Iris.instNonExpansive₂HomMap {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [OFE A] [OFE A'] [OFE B] [OFE B'] : OFE.NonExpansive₂ Hom.map

@[reducible, inline]

abbrev Iris.HomOF (F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) (F2 : (α : Type u_2) → (β : Type u_1) → [COFE α] → [COFE β] → Type u_4) [COFE.OFunctor F1] [COFE.OFunctor F2] (α : Type u_2) (β : Type u_1) [COFE α] [COFE β] : Type (max u_4 u_3)

The mixed-variance family of non-expansive maps between two space functors.

Equations

• Iris.HomOF F1 F2 A B = (F1 B A -n> F2 A B)

@[instance_reducible]

instance Iris.instOFunctorHomOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_2) → (β : Type u_1) → [COFE α] → [COFE β] → Type u_4} [COFE.OFunctor F1] [COFE.OFunctor F2] : COFE.OFunctor (HomOF F1 F2)

Equations

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

@[instance_reducible]

instance Iris.instOFunctorContractiveHomOF {F1 : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} {F2 : (α : Type u_2) → (β : Type u_1) → [COFE α] → [COFE β] → Type u_4} [COFE.OFunctorContractive F1] [COFE.OFunctorContractive F2] : COFE.OFunctorContractive (HomOF F1 F2)

Equations

• Iris.instOFunctorContractiveHomOF = { toOFunctor := Iris.instOFunctorHomOF, map_contractive := ⋯ }

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

A predicate closed under completion of Cauchy approximation chains.

• compl (c : Chain α) : (∀ (n : Nat), P (c.chain n)) → P (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} (hdisc : ∀ {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.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 α] [OFE β] (f g : α -n> β) : LimitPreserving fun (x : α) => f.f x = g.f x

theorem Iris.LimitPreserving.ext {α : Type u_1} [COFE α] {P Q : α → Prop} (he : ∀ {x : α}, P x ↔ Q x) (hp : LimitPreserving P) : LimitPreserving Q

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

The Cauchy chain obtained by iterating a contractive endomorphism.

Equations

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

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

The chain construction of the Banach fixpoint. fixpointP packages it, together with its unfolding equation, in an irreducible definition.

Equations

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

theorem Iris.fixpointAux_unfold {α : Type u_1} [COFE α] [Inhabited α] (f : α -c> α) : fixpointAux f.f = f.f (fixpointAux f.f)

@[irreducible]

def Iris.fixpointP {α : Type u_1} [COFE α] [Inhabited α] (f : α → α) [OFE.Contractive f] : { x : α // x = f x }

The Banach fixed point together with its unfolding equation. Irreducibility keeps elaboration from unfolding the approximation chain implicitly.

Equations

• Iris.fixpointP f = ⟨Iris.fixpointAux f, ⋯⟩

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

Fixpoints inside of a COFE

Equations

• Iris.fixpoint f = (Iris.fixpointP f).val

@[reducible, inline]

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

The fixed point of a bundled contractive endomorphism.

Equations

• f.fixpoint = Iris.fixpoint f.f

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

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

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

theorem Iris.fixpoint_dist {α : Type u_1} [COFE α] [Inhabited α] {f g : α → α} [OFE.Contractive f] [OFE.Contractive g] {n : Nat} (H : ∀ (z : α), OFE.Dist n (f z) (g z)) : OFE.Dist n (fixpoint f) (fixpoint g)

theorem Iris.fixpoint_proper {α : Type u_1} [COFE α] [Inhabited α] {f g : α → α} [OFE.Contractive f] [OFE.Contractive g] (H : ∀ (x : α), f x = g x) : fixpoint f = fixpoint g

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

theorem Iris.repeat_dist {α : Type u_1} [OFE α] (f g : α → α) [OFE.NonExpansive f] {n : Nat} (Hfg : ∀ (z : α), OFE.Dist n (f z) (g z)) (k : Nat) (z : α) : OFE.Dist n (Nat.repeat f k z) (Nat.repeat g k z)

def Iris.fixpointK {α : Type u_1} [COFE α] [Inhabited α] (k : Nat) (f : α → α) [OFE.Contractive (Nat.repeat f k)] : α

The fixed point obtained when a specified iterate is contractive.

Equations

• Iris.fixpointK k f = Iris.fixpoint (Nat.repeat f k)

theorem Iris.fixpointK_unfold {α : Type u_1} [COFE α] [Inhabited α] (k : Nat) (f : α → α) [OFE.Contractive (Nat.repeat f k)] : fixpointK k f = f (fixpointK k f)

theorem Iris.fixpointK_unique {α : Type u_1} [COFE α] [Inhabited α] (k : Nat) (f : α → α) [OFE.Contractive (Nat.repeat f k)] {x : α} (H : x = f x) : x = fixpointK k f

theorem Iris.fixpointK_ne {α : Type u_1} [COFE α] [Inhabited α] (k : Nat) (f g : α → α) [OFE.Contractive (Nat.repeat f k)] [OFE.Contractive (Nat.repeat g k)] [OFE.NonExpansive f] {n : Nat} (Hfg : ∀ (z : α), OFE.Dist n (f z) (g z)) : OFE.Dist n (fixpointK k f) (fixpointK k g)

theorem Iris.fixpointK_proper {α : Type u_1} [COFE α] [Inhabited α] (k : Nat) (f g : α → α) [OFE.Contractive (Nat.repeat f k)] [OFE.Contractive (Nat.repeat g k)] (Hfg : ∀ (z : α), f z = g z) : fixpointK k f = fixpointK k g

theorem Iris.fixpointK_ind {α : Type u_1} [COFE α] [Inhabited α] (k : Nat) (f : α → α) [OFE.Contractive (Nat.repeat f k)] (P : α → Prop) (x : α) (Hbase : P x) (Hind : ∀ (x : α), P x → P (f x)) (Hlim : LimitPreserving P) : P (fixpointK k f)

@[instance_reducible]

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

Equations

• Iris.instCoeFunContractiveHomHomForallForall = { coe := fun (f : α -c> β -n> γ) (x : α) => (f.f x).f }

@[instance_reducible]

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

Equations

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

instance Iris.ne₂_of_contractive_ne {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] (fA : α -c> β -n> γ) : OFE.NonExpansive₂ fun (x : α) => (fA.f x).f

A Contractive function with NonExpansive function codomain is NonExpansive₂.

instance Iris.ne₂_of_contractive {α : Type u_1} {β : Type u_2} {γ : Type u_3} [OFE α] [OFE β] [OFE γ] (fB : α -c> β -c> γ) : OFE.NonExpansive₂ fun (x : α) => (fB.f x).f

A Contractive function with Contractive function codomain is NonExpansive₂.

def Iris.fixpointAB {α : Type u_1} {β : Type u_2} [OFE α] [COFE β] [Inhabited β] (fB : α -c> β -c> β) (x : α) : β

The fixed point in the second variable for a given first argument.

Equations

• Iris.fixpointAB fB x = { f := (fun (x : α) => (fB.f x).f) x, ne := ⋯, contractive := ⋯ }.fixpoint

theorem Iris.fixpointAB_contractive {α : Type u_1} {β : Type u_2} [OFE α] [COFE β] [Inhabited β] (fB : α -c> β -c> β) : OFE.Contractive (fixpointAB fB)

def Iris.fixpointAA {α : Type u_1} {β : Type u_2} [OFE α] [COFE β] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) (x : α) : α

Substitute the second-variable fixed point into the first component.

Equations

• Iris.fixpointAA fA fB x = (fun (x : α) => (fA.f x).f) x (Iris.fixpointAB fB x)

theorem Iris.fixpointAA_contractive {α : Type u_1} {β : Type u_2} [OFE α] [COFE β] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : OFE.Contractive (fixpointAA fA fB)

def Iris.fixpointA {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : α

The first component of a simultaneous guarded fixed point.

Equations

• Iris.fixpointA fA fB = { f := Iris.fixpointAA fA fB, ne := ⋯, contractive := ⋯ }.fixpoint

def Iris.fixpointB {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : β

The second component of a simultaneous guarded fixed point.

Equations

• Iris.fixpointB fA fB = Iris.fixpointAB fB (Iris.fixpointA fA fB)

theorem Iris.fixpointA_unfold {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : (fun (x : α) => (fA.f x).f) (fixpointA fA fB) (fixpointB fA fB) = fixpointA fA fB

theorem Iris.fixpointB_unfold {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) : (fun (x : α) => (fB.f x).f) (fixpointA fA fB) (fixpointB fA fB) = fixpointB fA fB

theorem Iris.fixpointA_unique {α : Type u_1} {β : Type u_2} {p : α} {q : β} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) (Hp : (fun (x : α) => (fA.f x).f) p q = p) (Hq : (fun (x : α) => (fB.f x).f) p q = q) : p = fixpointA fA fB

theorem Iris.fixpointB_unique {α : Type u_1} {β : Type u_2} {p : α} {q : β} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α) (fB : α -c> β -c> β) (Hp : (fun (x : α) => (fA.f x).f) p q = p) (Hq : (fun (x : α) => (fB.f x).f) p q = q) : q = fixpointB fA fB

instance Iris.fixpointA_ne {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] : OFE.NonExpansive₂ fixpointA

instance Iris.fixpointB_ne {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] : OFE.NonExpansive₂ fixpointB

theorem Iris.fixpointA_proper {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA fA' : α -c> β -n> α) (fB fB' : α -c> β -c> β) (HA : ∀ (x : α) (y : β), (fun (x : α) => (fA.f x).f) x y = (fun (x : α) => (fA'.f x).f) x y) (HB : ∀ (x : α) (y : β), (fun (x : α) => (fB.f x).f) x y = (fun (x : α) => (fB'.f x).f) x y) : fixpointA fA fB = fixpointA fA' fB'

theorem Iris.fixpointB_proper {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA fA' : α -c> β -n> α) (fB fB' : α -c> β -c> β) (HA : ∀ (x : α) (y : β), (fun (x : α) => (fA.f x).f) x y = (fun (x : α) => (fA'.f x).f) x y) (HB : ∀ (x : α) (y : β), (fun (x : α) => (fB.f x).f) x y = (fun (x : α) => (fB'.f x).f) x y) : fixpointB fA fB = fixpointB fA' fB'

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

Delay equivalence by one step index.

• next :: (
• car : A

  The underlying value of a delayed equivalence space.

• )

@[instance_reducible]

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

Equations

• Iris.isOFELater = { Dist := fun (n : Nat) (x y : Iris.Later A) => Iris.OFE.DistLater n x.car y.car, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

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

theorem Iris.Later.uninj {A : Type u_1} (x : Later A) : ∃ (a : A), x = { car := a }

theorem Iris.contractive_alt {A : Type u_1} {B : Type u_2} [OFE A] [OFE B] (f : A → B) : OFE.Contractive f ↔ ∃ (g : Later A → B), OFE.NonExpansive g ∧ ∀ (x : A), f x = g { car := x }

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

Remove the delay from a chain by advancing every index.

Equations

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

@[instance_reducible]

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

Equations

• Iris.isCOFELater = { 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

Lift a non-expansive map through the one-step delay.

Equations

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

@[simp]

theorem Iris.laterMap_next {A : Type u_1} {B : Type u_2} [OFE A] [OFE B] (f : A -n> B) (x : A) : (laterMap f).f { car := x } = { car := f.f x }

theorem Iris.laterMap_id {A : Type u_1} [OFE A] (x : Later A) : (laterMap OFE.Hom.id).f x = x

theorem Iris.laterMap_compose {A : Type u_1} {B : Type u_2} {C : Type u_3} [OFE A] [OFE B] [OFE C] (f : A -n> B) (g : B -n> C) (x : Later A) : (laterMap (g.comp f)).f x = (laterMap g).f ((laterMap f).f x)

theorem Iris.laterMap_ext {A : Type u_1} {B : Type u_2} [OFE A] [OFE B] {f g : A -n> B} (x : Later A) (h : ∀ (a : A), f.f a = g.f a) : (laterMap f).f x = (laterMap g).f x

instance Iris.laterMap_contractive {A : Type u_1} {B : Type u_2} [OFE A] [OFE B] : OFE.Contractive laterMap

@[reducible, inline]

abbrev Iris.LaterOF (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) (α : Type u_1) (β : Type u_2) [COFE α] [COFE β] : Type u_3

Apply one-step delay to a mixed-variance space functor.

Equations

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

@[instance_reducible]

instance Iris.instOFunctorLater (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [COFE.OFunctor F] : COFE.OFunctor (LaterOF F)

Equations

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

@[instance_reducible]

instance Iris.instOFunctorContractiveLater (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [COFE.OFunctor F] : COFE.OFunctorContractive (LaterOF F)

Equations

• Iris.instOFunctorContractiveLater F = { toOFunctor := Iris.instOFunctorLater F, map_contractive := ⋯ }

@[reducible]

def Iris.isoCofeSubtype {α : Type u_1} {β : Type u_2} [COFE α] [OFE β] (P : α → Prop) (f : (x : α) → P x → β) (g : β -n> α) (g_dist : ∀ (n : Nat) (y1 y2 : β), OFE.Dist n y1 y2 ↔ OFE.Dist n (g.f y1) (g.f y2)) (gf : ∀ (x : α) (Hx : P x), g.f (f x Hx) = x) (Hlimit : ∀ (c : Chain β), P (IsCOFE.compl (Chain.map g c))) : IsCOFE β

Transport completeness through a map onto a completion-closed subtype.

Equations

• Iris.isoCofeSubtype P f g g_dist gf Hlimit = { compl := fun (c : Iris.Chain β) => f (Iris.IsCOFE.compl (Iris.Chain.map g c)) ⋯, conv_compl := ⋯ }

@[reducible]

def Iris.isoCofeSubtype' {α : Type u_1} {β : Type u_2} [COFE α] [OFE β] (P : α → Prop) (f : (x : α) → P x → β) (g : β -n> α) (Pg : ∀ (y : β), P (g.f y)) (g_dist : ∀ (n : Nat) (y1 y2 : β), OFE.Dist n y1 y2 ↔ OFE.Dist n (g.f y1) (g.f y2)) (gf : ∀ (x : α) (Hx : P x), g.f (f x Hx) = x) (Hlimit : LimitPreserving P) : IsCOFE β

Transport completeness using a limit-preserving predicate on the source.

Equations

• Iris.isoCofeSubtype' P f g Pg g_dist gf Hlimit = Iris.isoCofeSubtype P f g g_dist gf ⋯

@[reducible]

def Iris.isoCofe {α : Type u_1} {β : Type u_2} [COFE α] [OFE β] (f : α → β) (g : β -n> α) (g_dist : ∀ (n : Nat) (y1 y2 : β), OFE.Dist n y1 y2 ↔ OFE.Dist n (g.f y1) (g.f y2)) (gf : ∀ (x : α), g.f (f x) = x) : IsCOFE β

Transport completeness along an isomorphism of ordered equivalence spaces.

Equations

• Iris.isoCofe f g g_dist gf = Iris.isoCofeSubtype (fun (x : α) => True) (fun (x : α) (x_1 : True) => f x) g g_dist ⋯ ⋯

@[reducible]

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

Completeness of a subtype defined by a limit-preserving predicate.

Equations

• Iris.sigCofe H = Iris.isoCofeSubtype' P (fun (x : α) (h : P x) => ⟨x, h⟩) { f := Subtype.val, ne := ⋯ } ⋯ ⋯ ⋯ H

@[instance_reducible]

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

Equations

• Iris.instOFEIso = { Dist := fun (n : Nat) (I1 I2 : Iris.OFE.Iso α β) => Iris.OFE.Dist n I1.hom I2.hom ∧ Iris.OFE.Dist n I1.inv I2.inv, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

@[instance_reducible]

instance Iris.ofeIsoCofe {α : Type u_1} {β : Type u_2} [COFE α] [COFE β] : IsCOFE (OFE.Iso α β)

Equations

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

def Iris.isoOfeCong (F : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2) [COFE.OFunctor F] {A B : Type u_1} [COFE A] [COFE B] (I : OFE.Iso A B) : OFE.Iso (F A A) (F B B)

Lift an isomorphism through both arguments of a mixed-variance space functor.

Equations

• Iris.isoOfeCong F I = { hom := Iris.COFE.OFunctor.map I.inv I.hom, inv := Iris.COFE.OFunctor.map I.hom I.inv, hom_inv := ⋯, inv_hom := ⋯ }

instance Iris.isoOfeCong_ne (F : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2) [COFE.OFunctor F] {A B : Type u_1} [COFE A] [COFE B] : OFE.NonExpansive (isoOfeCong F)

instance Iris.isoOfeCong_contractive (F : (α β : Type u_1) → [COFE α] → [COFE β] → Type u_2) [COFE.OFunctorContractive F] {A B : Type u_1} [COFE A] [COFE B] : OFE.Contractive (isoOfeCong F)

theorem Iris.OFE.cast_dist {α β : Type u_1} {n : Nat} [Iα : OFE α] [Iβ : OFE β] {x y : α} (Ht : α = β) (HIt : Iα = ⋯ ▸ Iβ) (H : Dist n x y) : Dist n (Ht ▸ x) (Ht ▸ y)