Finite-support ghost maps and their resource algebras.

Copyright (c) The Iris-Lean Contributors.

GenMap

The OFE over gmaps is equivalent to a non-dependent discrete function to an Option type with a OFE of keys, and a finite number of allocated elements.

In this setting, the ORA is always unital, and as a consequence the oFunctors do not require unitality in order to act as a URFunctor(Contractive).

GenMap is only intended to be used in the construction of the core IProp model. It is a stripped-down version of the generic heap constructions, which you should use instead.

def Iris.alter {β : Sort u_1} (f : Nat → β) (a : Nat) (b : β) : Nat → β

Replace the value of a natural-number-indexed function at one key.

Equations

• Iris.alter f a b a' = if a = a' then b else f a'

structure Iris.GenMap (β : Type u_1) : Type u_1

A GenMap is a partial map from Nat to β with finite support. The bound field witnesses that all keys ≥ some N map to none.

• car : Nat → Option β

  The optional value stored at each natural-number key.

• bound : ∃ (N : Nat), ∀ (k : Nat), N ≤ k → self.car k = none

@[instance_reducible]

instance Iris.instCoeFunGenMapForallNatOption {β : Type u_1} : CoeFun (GenMap β) fun (x : GenMap β) => Nat → Option β

Equations

• Iris.instCoeFunGenMapForallNatOption = { coe := Iris.GenMap.car }

def Iris.GenMap.alter {β : Type u_1} (g : GenMap β) (a : Nat) (b : Option β) : GenMap β

Replace one ghost-map entry while preserving bounded support.

Equations

• g.alter a b = { car := Iris.alter g.car a b, bound := ⋯ }

def Iris.GenMap.empty {β : Type u_1} : GenMap β

The ghost map with no allocated keys.

Equations

• Iris.GenMap.empty = { car := fun (x : Nat) => none, bound := ⋯ }

def Iris.GenMap.singleton {β : Type u_1} (x : Nat) (y : β) : GenMap β

The ghost map allocating one value at one key.

Equations

• Iris.GenMap.singleton x y = Iris.GenMap.empty.alter x (some y)

theorem Iris.GenMap.empty_map_lookup {β : Type u_1} (γ : Nat) : empty.car γ = none

theorem Iris.GenMap.singleton_map_in {β : Type u_1} (x : Nat) (y : β) : (singleton x y).car x = some y

theorem Iris.GenMap.singleton_map_none {β : Type u_1} {x : Nat} {y : β} {x' : Nat} (h : x' ≠ x) : (singleton x y).car x' = none

theorem Iris.GenMap.exists_fresh {β : Type u_1} (g : GenMap β) : ∃ (k : Nat), g.car k = none

Any GenMap has a fresh key (one mapping to none).

theorem Iris.GenMap.exists_fresh_sat {β : Type u_1} (g : GenMap β) {P : Nat → Prop} (hP : ∀ (N : Nat), ∃ (k : Nat), N ≤ k ∧ P k) : ∃ (k : Nat), g.car k = none ∧ P k

Given a GenMap and a predicate that is satisfied by infinitely many naturals (witnessed by: for any N, there exists k ≥ N with P k), we can find a fresh key satisfying P.

def Iris.IsFree {α : Sort u_1} {β : α → Type u_2} (f : (a : α) → Option (β a)) : α → Prop

IsFree f a means key a maps to none in f. Retained for compatibility with downstream proofs that pattern-match on this.

Equations

• Iris.IsFree f a = (f a = none)

OFE

@[instance_reducible]

instance Iris.instOFEGenMap (β : Type u_1) [OFE β] : OFE (GenMap β)

Equations

• Iris.instOFEGenMap β = { Dist := fun (n : Nat) (x1 x2 : Iris.GenMap β) => Iris.OFE.Dist n x1.car x2.car, dist_eqv := ⋯, eq_dist' := ⋯, dist_lt := ⋯ }

theorem Iris.GenMap.singleton_discreteE {β : Type u_1} {k : Nat} {v : β} [OFE β] [OFE.DiscreteE v] : OFE.DiscreteE (singleton k v)

theorem Iris.GenMap.empty_discreteE {β : Type u_1} [OFE β] : OFE.DiscreteE empty

theorem Iris.GenMap.ext {β : Type u_1} {a b : GenMap β} (h : a.car = b.car) : a = b

theorem Iris.GenMap.ext_iff {β : Type u_1} {a b : GenMap β} : a = b ↔ a.car = b.car

theorem Iris.GenMap.alter_of_lookup {β : Type u_1} {g : GenMap β} {x : Nat} {y : Option β} (h : g.car x = y) : g.alter x y = g

theorem Iris.GenMap.alter_alter {β : Type u_1} (g : GenMap β) (x : Nat) (y y' : Option β) : (g.alter x y).alter x y' = g.alter x y'

ORA

theorem Iris.op_bound (β : Type u_1) [ORA β] (x y : GenMap β) : ∃ (N : Nat), ∀ (k : Nat), N ≤ k → (x.car • y.car) k = none

theorem Iris.pcore_bound (β : Type u_1) [ORA β] (x : GenMap β) (cx : Nat → Option β) (hpc : PCore.pcore x.car = some cx) : ∃ (N : Nat), ∀ (k : Nat), N ≤ k → cx k = none

theorem Iris.extend_bound (β : Type u_1) [ORA β] {n : Nat} {x : GenMap β} {y1 y2 : Nat → Option β} (Hv : ✓{n} x.car) (He : OFE.Dist n x.car (y1 • y2)) : have F := fun (k : Nat) => ORA.extend ⋯ ⋯; (∃ (N : Nat), ∀ (k : Nat), N ≤ k → (fun (k : Nat) => (F k).fst) k = none) ∧ ∃ (N : Nat), ∀ (k : Nat), N ≤ k → (fun (k : Nat) => (F k).snd.fst) k = none

def Iris.pcoreGenMap (β : Type u_1) [ORA β] (x : GenMap β) : Option (GenMap β)

The total partial-core operation on finite-support ghost maps.

Equations

• Iris.pcoreGenMap β x = some { car := fun (k : Nat) => Iris.PCore.core (x.car k), bound := ⋯ }

@[reducible]

def Iris.GenMap.raOp (β : Type u_1) [ORA β] : Op (GenMap β)

Composition on finite-support ghost maps.

Equations

• Iris.GenMap.raOp β = { op := fun (x y : Iris.GenMap β) => { car := x.car • y.car, bound := ⋯ }, op_ne := ⋯, assoc := ⋯, comm := ⋯ }

@[reducible]

def Iris.GenMap.raPCore (β : Type u_1) [ORA β] : PCore (GenMap β)

The partial core on finite-support ghost maps.

Equations

• Iris.GenMap.raPCore β = { pcore := Iris.pcoreGenMap β, pcore_ne := ⋯, pcore_idem := ⋯ }

@[reducible]

def Iris.GenMap.raValid (β : Type u_1) [ORA β] : Validity (GenMap β)

Validity on finite-support ghost maps.

Equations

• Iris.GenMap.raValid β = { ValidN := fun (n : Nat) (x : Iris.GenMap β) => ✓{n} x.car, Valid := fun (x : Iris.GenMap β) => ✓ x.car, validN_ne := ⋯, valid_iff_validN := ⋯, validN_succ := ⋯ }

@[reducible]

def Iris.GenMap.raOrdered (β : Type u_1) [ORA β] : Ordered (GenMap β)

The resource order on finite-support ghost maps.

Equations

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

@[simp]

theorem Iris.GenMap.op_car (β : Type u_1) [ORA β] (x y : GenMap β) : (x • y).car = x.car • y.car

theorem Iris.GenMap.increasing_apply (β : Type u_1) [ORA β] {x : GenMap β} (h : Increasing x) (k : Nat) : Increasing (x.car k)

theorem Iris.GenMap.increasing_car (β : Type u_1) [ORA β] {x : GenMap β} (h : Increasing x) : Increasing x.car

theorem Iris.GenMap.increasing_of_car (β : Type u_1) [ORA β] {x : GenMap β} (h : Increasing x.car) : Increasing x

@[instance_reducible]

instance Iris.instORAGenMap (β : Type u_1) [ORA β] : ORA (GenMap β)

Equations

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

@[instance_reducible]

instance Iris.instUORAGenMap (β : Type u_1) [ORA β] : UORA (GenMap β)

Equations

• Iris.instUORAGenMap β = { toORA := Iris.instORAGenMap β, toOrderRefl := ⋯, unit := Iris.GenMap.empty, unit_valid := ⋯, unit_left_id := ⋯, pcore_unit := ⋯ }

instance Iris.instIsTotalGenMap (β : Type u_1) [ORA β] : IsTotal (GenMap β)

instance Iris.instIncOrdGenMap (β : Type u_1) [ORA β] [IncOrd β] : IncOrd (GenMap β)

instance Iris.instOrdIncGenMap (β : Type u_1) [ORA β] [OrdInc β] : OrdInc (GenMap β)

instance Iris.instIsIncGenMap (β : Type u_1) [ORA β] [IsInc β] : IsInc (GenMap β)

theorem Iris.GenMap.singleton_ord_mono (β : Type u_1) [ORA β] {x : Nat} {y y' : β} (h : y ≼ₒ y') : singleton x y ≼ₒ singleton x y'

theorem Iris.GenMap.alter_valid (β : Type u_1) [ORA β] {n : Nat} {b : Option β} {a : Nat} {g : GenMap β} (Hb : ✓{n} b) (Hg : ✓{n} g) : ✓{n} g.alter a b

theorem Iris.GenMap.singleton_map_op (β : Type u_1) [ORA β] (x : Nat) (y1 y2 : β) : singleton x y1 • singleton x y2 = singleton x (y1 • y2)

theorem Iris.GenMap.singleton_map_pcore (β : Type u_1) [ORA β] (x : Nat) (y : β) (γ : Nat) : ((singleton x y).car γ).bind PCore.pcore = if γ = x then PCore.pcore y else none

theorem Iris.GenMap.validN_singleton_map_in (β : Type u_1) [ORA β] (x : Nat) (y : β) (n : Nat) : ✓{n} (singleton x y).car x → ✓{n} y

theorem Iris.GenMap.op_singleton_comm (β : Type u_1) [ORA β] {mf : GenMap β} {x : Nat} (y : β) (H_free : IsFree mf.car x) : singleton x y • mf = mf.alter x (some y)

theorem Iris.GenMap.singleton_op_alter_none (β : Type u_1) [ORA β] {g : GenMap β} {x : Nat} {y : β} (h : g.car x = some y) : singleton x y • g.alter x none = g

theorem Iris.GenMap.validN_op_comm (β : Type u_1) [ORA β] {n : Nat} {m mf : GenMap β} (x : Nat) (y : β) (H : IsFree mf.car x) : ✓{n} m.alter x (some y) • mf ↔ ✓{n} (m • mf).alter x (some y)

OFunctors

@[reducible, inline]

abbrev Iris.GenMapOF (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 mixed-variance family to finite-support ghost maps.

Equations

• Iris.GenMapOF F A B = Iris.GenMap (F A B)

@[reducible, inline]

abbrev Iris.GenMap.lift {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α -n> β) : GenMap α -n> GenMap β

Map a non-expansive function over every allocated ghost-map entry.

Equations

• Iris.GenMap.lift f = { f := fun (g : Iris.GenMap α) => { car := fun (t : Nat) => Option.map f.f (g.car t), bound := ⋯ }, ne := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Iris.instURFunctorGenMapOF (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [RFunctor F] : URFunctor (GenMapOF F)

Equations

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

instance Iris.instRFunctorAffineGenMapOF (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [RFunctor F] [RFunctorAffine F] : RFunctorAffine (GenMapOF F)

@[instance_reducible]

instance Iris.instURFunctorContractiveGenMapOF (F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3) [RFunctorContractive F] : URFunctorContractive (GenMapOF F)

Equations

• Iris.instURFunctorContractiveGenMapOF F = { toURFunctor := Iris.instURFunctorGenMapOF F, map_contractive := ⋯ }