LeanPool.IrisAlgebra.Algebra.COFESolver

A guarded recursive domain equation solver.

def Iris.COFE.OFunctor.Fix.Impl.A' (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] :

Nat → (α : Type u) × COFE α

The approximation carriers bundled with their complete space structures.

Equations

Iris.COFE.OFunctor.Fix.Impl.A' F 0 = ⟨ULift Unit, inferInstance ⟩
Iris.COFE.OFunctor.Fix.Impl.A' F n.succ = match Iris.COFE.OFunctor.Fix.Impl.A' F n with | ⟨A, snd⟩ => ⟨F A A, inferInstance ⟩

Instances For

source

@[implicit_reducible]

def Iris.COFE.OFunctor.Fix.Impl.A (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] (n : Nat) :

Type u

The carrier at one level of the recursive-domain approximation.

Equations

Iris.COFE.OFunctor.Fix.Impl.A F n = (Iris.COFE.OFunctor.Fix.Impl.A' F n).fst

Instances For

source

@[instance_reducible]

instance Iris.COFE.OFunctor.Fix.Impl.instA' {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] (n : Nat) :

COFE (A' F n).fst

Equations

Iris.COFE.OFunctor.Fix.Impl.instA' n = (Iris.COFE.OFunctor.Fix.Impl.A' F n).snd

source

@[instance_reducible]

instance Iris.COFE.OFunctor.Fix.Impl.instA {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] (n : Nat) :

COFE (A F n)

Equations

Iris.COFE.OFunctor.Fix.Impl.instA n = (Iris.COFE.OFunctor.Fix.Impl.A' F n).snd

source

def Iris.COFE.OFunctor.Fix.Impl.updown (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (k : Nat) :

(A F k -n> A F (k + 1)) × (A F (k + 1) -n> A F k)

The section/retraction pair at every level, computed by a single recursion so that evaluating either component at level k costs O(k) (the naive mutual recursion recomputes both branches at every level, which is 2^k).

Equations

One or more equations did not get rendered due to their size.
Iris.COFE.OFunctor.Fix.Impl.updown F n.succ = match Iris.COFE.OFunctor.Fix.Impl.updown F n with | (u, d) => (Iris.COFE.OFunctor.map d u, Iris.COFE.OFunctor.map u d)

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.up (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (k : Nat) :

A F k -n> A F (k + 1)

The section from one approximation level to its successor.

Equations

Iris.COFE.OFunctor.Fix.Impl.up F k = (Iris.COFE.OFunctor.Fix.Impl.updown F k).fst

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.down (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (k : Nat) :

A F (k + 1) -n> A F k

The retraction from a successor approximation to its predecessor.

Equations

Iris.COFE.OFunctor.Fix.Impl.down F k = (Iris.COFE.OFunctor.Fix.Impl.updown F k).snd

Instances For

source

theorem Iris.COFE.OFunctor.Fix.Impl.down_up {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (x : A F k) :

(down F k).f ((up F k).f x) = x

source

theorem Iris.COFE.OFunctor.Fix.Impl.up_down {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (x : A F (k + 1 + 1)) :

OFE.Dist k ((up F (k + 1)).f ((down F (k + 1)).f x)) x

source

structure Iris.COFE.OFunctor.Fix.Impl.Tower (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

Type u

A family of approximations compatible with all one-step retractions.

val (k : Nat) : A F k
The approximation at each tower level.
down {k : Nat} : (down F k).f (self.val (k + 1)) = self.val k

Instances For

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.ext {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} {inst✝ : OFunctorContractive F} {inst✝¹ : (α : Type u) → [inst : COFE α] → IsCOFE (F α α)} {inh : Inhabited (F (ULift Unit) (ULift Unit))} {x y : Tower F} (val : x.val = y.val) :

x = y

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.ext_iff {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} {inst✝ : OFunctorContractive F} {inst✝¹ : (α : Type u) → [inst : COFE α] → IsCOFE (F α α)} {inh : Inhabited (F (ULift Unit) (ULift Unit))} {x y : Tower F} :

x = y ↔ x.val = y.val

source

@[instance_reducible]

instance Iris.COFE.OFunctor.Fix.Impl.instCoeFunTowerForallA {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

CoeFun (Tower F) fun (x : Tower F) => (k : Nat) → A F k

Equations

Iris.COFE.OFunctor.Fix.Impl.instCoeFunTowerForallA = { coe := Iris.COFE.OFunctor.Fix.Impl.Tower.val }

source

@[instance_reducible]

instance Iris.COFE.OFunctor.Fix.Impl.instOFETower {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

OFE (Tower F)

Equations

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

source

def Iris.COFE.OFunctor.Fix.Impl.towerChain {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (c : Chain (Tower F)) (k : Nat) :

Chain (A F k)

Evaluate a chain of coherent towers at one level.

Equations

Iris.COFE.OFunctor.Fix.Impl.towerChain c k = { chain := fun (i : Nat) => (c.chain i).val k, cauchy := ⋯ }

Instances For

source

@[instance_reducible]

instance Iris.COFE.OFunctor.Fix.Impl.instTower {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

COFE (Tower F)

Equations

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

source

def Iris.COFE.OFunctor.Fix.Impl.upN (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (n : Nat) :

A F k -n> A F (k + n)

Compose the sections through a specified number of approximation levels.

Equations

Iris.COFE.OFunctor.Fix.Impl.upN F 0 = Iris.OFE.Hom.id
Iris.COFE.OFunctor.Fix.Impl.upN F n.succ = (Iris.COFE.OFunctor.Fix.Impl.up F (k + n)).comp (Iris.COFE.OFunctor.Fix.Impl.upN F n)

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.downN (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (n : Nat) :

A F (k + n) -n> A F k

Compose the retractions through a specified number of approximation levels.

Equations

Iris.COFE.OFunctor.Fix.Impl.downN F 0 = Iris.OFE.Hom.id
Iris.COFE.OFunctor.Fix.Impl.downN F n.succ = (Iris.COFE.OFunctor.Fix.Impl.downN F n).comp (Iris.COFE.OFunctor.Fix.Impl.down F (k + n))

Instances For

source

theorem Iris.COFE.OFunctor.Fix.Impl.downN_upN {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (x : A F k) {i : Nat} :

(downN F i).f ((upN F i).f x) = x

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.up {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (X : Tower F) :

OFE.Dist k ((up F (k + 1)).f (X.val (k + 1))) (X.val (k + 2))

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.upN {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (X : Tower F) (i : Nat) :

OFE.Dist k ((upN F i).f (X.val (k + 1))) (X.val (k + 1 + i))

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.downN {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (X : Tower F) (i : Nat) :

(downN F i).f (X.val (k + i)) = X.val k

source

instance Iris.COFE.OFunctor.Fix.Impl.instNonExpansiveTowerAVal {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (k : Nat) :

OFE.NonExpansive fun (X : Tower F) => X.val k

source

def Iris.COFE.OFunctor.Fix.Impl.Tower.proj {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (k : Nat) :

Tower F -n> A F k

Project a coherent tower to one approximation level.

Equations

Iris.COFE.OFunctor.Fix.Impl.Tower.proj k = { f := fun (x : Iris.COFE.OFunctor.Fix.Impl.Tower F) => x.val k, ne := ⋯ }

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.eqToHom {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] {i k : Nat} (e : i = k) :

A F i -n> A F k

Transport an approximation along an equality of its level indices.

Equations

Iris.COFE.OFunctor.Fix.Impl.eqToHom e = e ▸ Iris.OFE.Hom.id

Instances For

source

theorem Iris.COFE.OFunctor.Fix.Impl.eqToHom_up {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k k' : Nat} {x : A F k} (e : k = k') :

(eqToHom ⋯).f ((up F k).f x) = (up F k').f ((eqToHom e).f x)

source

theorem Iris.COFE.OFunctor.Fix.Impl.down_eqToHom {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k k' : Nat} {x : A F (k + 1)} (e : k = k') :

(down F k').f ((eqToHom ⋯).f x) = (eqToHom e).f ((down F k).f x)

source

def Iris.COFE.OFunctor.Fix.Impl.embed {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k i : Nat} :

A F k -n> A F i

Embed or retract between any two approximation levels.

Equations

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

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.Tower.embed {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (k : Nat) :

A F k -n> Tower F

Extend one approximation to a coherent tower.

Equations

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

Instances For

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.embed_up {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (x : A F k) :

(Tower.embed (k + 1)).f ((up F k).f x) = (Tower.embed k).f x

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.embed_self {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (X : Tower F) :

OFE.Dist k ((Tower.embed (k + 1)).f (X.val (k + 1))) X

source

@[instance_reducible]

instance Iris.COFE.OFunctor.Fix.Impl.instInhabitedTower {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

Inhabited (Tower F)

Equations

Iris.COFE.OFunctor.Fix.Impl.instInhabitedTower = { default := (Iris.COFE.OFunctor.Fix.Impl.Tower.embed 0).f { down := () } }

source

def Iris.COFE.OFunctor.Fix.Impl.unfoldChain {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (X : Tower F) :

Chain (F (Tower F) (Tower F))

The Cauchy chain of functor images used to unfold a coherent tower.

Equations

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

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.Tower.isoAux {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

OFE.Iso (F (Tower F) (Tower F)) (Tower F)

The explicit isomorphism between a coherent tower and its functor image.

Equations

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

Instances For

source

@[irreducible]

def Iris.COFE.OFunctor.Fix.Impl.Tower.iso {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

OFE.Iso (F (Tower F) (Tower F)) (Tower F)

The tower isomorphism, kept irreducible during elaboration.

Equations

Iris.COFE.OFunctor.Fix.Impl.Tower.iso = Iris.COFE.OFunctor.Fix.Impl.Tower.isoAux

Instances For

source

@[irreducible]

def Iris.COFE.OFunctor.Fix (F : (α β : Type u) → [COFE α] → [COFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

Type u

The recursive domain constructed as a tower of finite approximations.

Equations

Iris.COFE.OFunctor.Fix F = Iris.COFE.OFunctor.Fix.Impl.Tower F

Instances For

source

@[instance_reducible]

instance Iris.COFE.OFunctor.instInhabitedFix {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

Inhabited (Fix F)

Equations

Iris.COFE.OFunctor.instInhabitedFix = { default := Iris.COFE.OFunctor.instInhabitedFix._aux_1 }

source

@[instance_reducible]

instance Iris.COFE.OFunctor.instFix {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

COFE (Fix F)

Equations

Iris.COFE.OFunctor.instFix = { Dist := Iris.COFE.OFunctor.instFix._aux_1, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯, compl := Iris.COFE.OFunctor.instFix._aux_6, conv_compl := ⋯ }

source

@[irreducible]

def Iris.COFE.OFunctor.Fix.iso {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

OFE.Iso (F (Fix F) (Fix F)) (Fix F)

The isomorphism from the functor image to the constructed recursive domain.

Equations

Iris.COFE.OFunctor.Fix.iso = Iris.COFE.OFunctor.Fix.Impl.Tower.iso

Instances For

source

@[irreducible]

def Iris.COFE.OFunctor.Fix.fold {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

F (Fix F) (Fix F) -n> Fix F

Fold a functor value into the constructed recursive domain.

Equations

Iris.COFE.OFunctor.Fix.fold = Iris.COFE.OFunctor.Fix.iso.hom

Instances For

source

@[irreducible]

def Iris.COFE.OFunctor.Fix.unfold {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

Fix F -n> F (Fix F) (Fix F)

Unfold a recursive-domain value into its functor image.

Equations

Iris.COFE.OFunctor.Fix.unfold = Iris.COFE.OFunctor.Fix.iso.inv

Instances For

source

theorem Iris.COFE.OFunctor.Fix.fold_unfold {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (X : Fix F) :

fold.f (unfold.f X) = X

source

theorem Iris.COFE.OFunctor.Fix.unfold_fold {F : (α β : Type u) → [COFE α] → [COFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (X : F (Fix F) (Fix F)) :

unfold.f (fold.f X) = X