The recursive Iris proposition model over ordered ghost resources.

Copyright (c) The Iris-Lean Contributors.

@[reducible, inline]

abbrev Iris.GType : Type

The index type for the global family of ghost-resource functors.

Equations

• Iris.GType = Nat

structure Iris.GFunctor : Type (max (max (u + 1) (v + 1)) (w + 1))

A resource functor admissible in the global ghost state: contractive, with affine algebras.

• F (α : Type u) (β : Type v) [COFE α] [COFE β] : Type w

  The underlying mixed-variance family of resource carriers.

• contractive : RFunctorContractive self.F

  Contractiveness of the resource functor action.

• affine : RFunctorAffine self.F

structure Iris.BundledGFunctors : Type (max (max (u + 1) (v + 1)) (w + 1))

A global family of admissible ghost-resource functors.

• get : GType → GFunctor

  The resource functor assigned to each ghost-resource index.

@[instance_reducible]

instance Iris.instCoeFunBundledGFunctorsForallGTypeGFunctor : CoeFun BundledGFunctors fun (x : BundledGFunctors) => GType → GFunctor

Equations

• Iris.instCoeFunBundledGFunctorsForallGTypeGFunctor = { coe := Iris.BundledGFunctors.get }

def Iris.BundledGFunctors.default : BundledGFunctors

The global family assigning the constant unit resource to every index.

Equations

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

def Iris.BundledGFunctors.set (GF : BundledGFunctors) (i : Nat) (FB : GFunctor) : BundledGFunctors

Replace the resource functor at one global index.

Equations

• GF.set i FB = { get := fun (j : Iris.GType) => if j = i then FB else GF.get j }

@[reducible, inline]

abbrev Iris.GName : Type

The natural-number names used for ghost-resource allocations.

Equations

• Iris.GName = Nat

@[reducible, inline]

abbrev Iris.IResF (GF : BundledGFunctors) (α : Type u_1) (β : Type u_2) [COFE α] [COFE β] : Type u_3

The global ghost-resource functor, built from finite-support maps.

Equations

• Iris.IResF GF = Iris.DiscreteFunOF fun (i : Iris.GType) => Iris.GenMapOF (GF.get i).F

@[instance_reducible]

instance Iris.instRFunctorContractiveFGet (GF : BundledGFunctors) (i : GType) : RFunctorContractive (GF.get i).F

Equations

• Iris.instRFunctorContractiveFGet GF i = (GF.get i).contractive

instance Iris.instRFunctorAffineGF (GF : BundledGFunctors) (i : GType) : RFunctorAffine (GF.get i).F

def Iris.IPre (GF : BundledGFunctors) : Type u

The complete recursive domain used to define Iris propositions.

Equations

• Iris.IPre GF = Iris.COFE.OFunctor.Fix (Iris.UPredOF (Iris.IResF GF))

@[instance_reducible]

instance Iris.instCOFEIPre (GF : BundledGFunctors) : COFE (IPre GF)

Equations

• Iris.instCOFEIPre GF = { Dist := Iris.instCOFEIPre._aux_1 GF, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯, compl := Iris.instCOFEIPre._aux_6 GF, conv_compl := ⋯ }

def Iris.IResUR (GF : BundledGFunctors) : Type u

The global unital ordered resource algebra over the recursive pre-propositions.

Equations

• Iris.IResUR GF = ((i : Iris.GType) → Iris.GenMap ((GF.get i).F (Iris.IPre GF) (Iris.IPre GF)))

@[instance_reducible]

instance Iris.instUORAIResUR (GF : BundledGFunctors) : UORA (IResUR GF)

Equations

• Iris.instUORAIResUR GF = Iris.ucmraDiscreteFunO fun (i : Iris.GType) => Iris.GenMap ((GF.get i).F (Iris.IPre GF) (Iris.IPre GF))

instance Iris.instIncOrdIResUR (GF : BundledGFunctors) : IncOrd (IResUR GF)

@[reducible, inline]

abbrev Iris.IProp (GF : BundledGFunctors) : Type u

Monotone step-indexed predicates over the global ghost-resource algebra.

Equations

• Iris.IProp GF = Iris.UPred (Iris.IResUR GF)

def Iris.IProp.unfold (GF : BundledGFunctors) : IProp GF -n> IPre GF

Map a proposition to its recursive pre-proposition representation.

Equations

• Iris.IProp.unfold GF = Iris.COFE.OFunctor.Fix.iso.hom

def Iris.IProp.fold (GF : BundledGFunctors) : IPre GF -n> IProp GF

Map a recursive pre-proposition back to its proposition representation.

Equations

• Iris.IProp.fold GF = Iris.COFE.OFunctor.Fix.iso.inv

theorem Iris.IProp.fold_unfold (GF : BundledGFunctors) (P : IProp GF) : (fold GF).f ((unfold GF).f P) = P

theorem Iris.IProp.unfold_fold (GF : BundledGFunctors) (P : IPre GF) : (unfold GF).f ((fold GF).f P) = P