Iris.Algebra.COFESolver

source

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

Nat → (α : Type u) × COFE α

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

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

Type u

Equations

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

Instances For

source

instance Iris.COFE.OFunctor.Fix.Impl.instA' {F : (α β : Type u) → [OFE α] → [OFE β] → 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 Iris.COFE.OFunctor.Fix.Impl.instA {F : (α β : Type u) → [OFE α] → [OFE β] → 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.up (F : (α β : Type u) → [OFE α] → [OFE β] → 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)

Equations

Iris.COFE.OFunctor.Fix.Impl.up F 0 = { f := fun (x : Iris.COFE.OFunctor.Fix.Impl.A F 0) => default, ne := ⋯ }
Iris.COFE.OFunctor.Fix.Impl.up F n.succ = Iris.COFE.OFunctor.map (Iris.COFE.OFunctor.Fix.Impl.down F n) (Iris.COFE.OFunctor.Fix.Impl.up F n)

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.down (F : (α β : Type u) → [OFE α] → [OFE β] → 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

Equations

Iris.COFE.OFunctor.Fix.Impl.down F 0 = { f := fun (x : Iris.COFE.OFunctor.Fix.Impl.A F (0 + 1)) => { down := () }, ne := ⋯ }
Iris.COFE.OFunctor.Fix.Impl.down F n.succ = Iris.COFE.OFunctor.map (Iris.COFE.OFunctor.Fix.Impl.up F n) (Iris.COFE.OFunctor.Fix.Impl.down F n)

Instances For

source

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

OFE.Equiv ((down F k).f ((up F k).f x)) x

source

theorem Iris.COFE.OFunctor.Fix.Impl.up_down {F : (α β : Type u) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → Type u) [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] :

Type u

val (k : Nat) : A F k
down {k : Nat} : OFE.Equiv ((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) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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 Iris.COFE.OFunctor.Fix.Impl.instCoeFunTowerForallA {F : (α β : Type u) → [OFE α] → [OFE β] → 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 Iris.COFE.OFunctor.Fix.Impl.instOFETower {F : (α β : Type u) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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)

Equations

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

Instances For

source

instance Iris.COFE.OFunctor.Fix.Impl.instTower {F : (α β : Type u) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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)

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) → [OFE α] → [OFE β] → 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

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) → [OFE α] → [OFE β] → 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} :

OFE.Equiv ((downN F i).f ((upN F i).f x)) x

source

theorem Iris.COFE.OFunctor.Fix.Impl.Tower.up {F : (α β : Type u) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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.Equiv ((downN F i).f (X.val (k + i))) (X.val k)

source

instance Iris.COFE.OFunctor.Fix.Impl.instNonExpansiveTowerAVal {F : (α β : Type u) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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

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) → [OFE α] → [OFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] {i k : Nat} (e : i = k) :

A F i -n> A F k

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) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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

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) → [OFE α] → [OFE β] → 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

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) → [OFE α] → [OFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] {k : Nat} (x : A F k) :

OFE.Equiv ((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) → [OFE α] → [OFE β] → 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 Iris.COFE.OFunctor.Fix.Impl.instInhabitedTower {F : (α β : Type u) → [OFE α] → [OFE β] → 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) → [OFE α] → [OFE β] → 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))

Equations

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

Instances For

source

def Iris.COFE.OFunctor.Fix.Impl.Tower.iso {F : (α β : Type u) → [OFE α] → [OFE β] → 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)

Equations

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

Instances For

source

@[irreducible]

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

Type u

Equations

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

Instances For

source

instance Iris.COFE.OFunctor.instInhabitedFix {F : (α β : Type u) → [OFE α] → [OFE β] → 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 = inferInstanceAs (Inhabited (Iris.COFE.OFunctor.Fix.Impl.Tower F))

source

instance Iris.COFE.OFunctor.instFix {F : (α β : Type u) → [OFE α] → [OFE β] → 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 = inferInstanceAs (Iris.COFE (Iris.COFE.OFunctor.Fix.Impl.Tower F))

source

@[irreducible]

def Iris.COFE.OFunctor.Fix.iso {F : (α β : Type u) → [OFE α] → [OFE β] → 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)

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) → [OFE α] → [OFE β] → 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

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) → [OFE α] → [OFE β] → 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)

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) → [OFE α] → [OFE β] → Type u} [OFunctorContractive F] [(α : Type u) → [inst : COFE α] → IsCOFE (F α α)] [inh : Inhabited (F (ULift Unit) (ULift Unit))] (X : Fix F) :

OFE.Equiv (fold.f (unfold.f X)) X

source

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

OFE.Equiv (unfold.f (fold.f X)) X