Monotone step-indexed predicates over ordered resources.

Copyright (c) The Iris-Lean Contributors.

structure Iris.ValidAt (M : Type u_1) [OFE M] [Validity M] (n : Nat) : Type u_1

A resource together with its validity at one step index.

• val : M

  The underlying valid resource.

• property : ✓{n} self.val

theorem Iris.ValidAt.ext {M : Type u_1} {inst✝ : OFE M} {inst✝¹ : Validity M} {n : Nat} {x y : ValidAt M n} (val : x.val = y.val) : x = y

theorem Iris.ValidAt.ext_iff {M : Type u_1} {inst✝ : OFE M} {inst✝¹ : Validity M} {n : Nat} {x y : ValidAt M n} : x = y ↔ x.val = y.val

@[instance_reducible]

instance Iris.instCoeOutValidAt {M : Type u_1} [OFE M] [Validity M] {n : Nat} : CoeOut (ValidAt M n) M

Equations

• Iris.instCoeOutValidAt = { coe := fun (x : Iris.ValidAt M n) => x.val }

def Iris.ValidAt.le {M : Type u_1} [OFE M] [Validity M] {n m : Nat} (Hle : m ≤ n) : ValidAt M n → ValidAt M m

View a valid resource at an earlier step index.

Equations

• Iris.ValidAt.le Hle v = { val := v.val, property := ⋯ }

@[simp]

theorem Iris.ValidAt.le_val {M : Type u_1} [OFE M] [Validity M] {n m : Nat} {Hle : m ≤ n} {v : ValidAt M n} : (le Hle v).val = v.val

@[simp]

theorem Iris.ValidAt.le_rfl {M : Type u_1} [OFE M] [Validity M] {n : Nat} {Hle : n ≤ n} {v : ValidAt M n} : le Hle v = v

structure Iris.UPred (M : Type u_1) [OFE M] [Validity M] [Ordered M] : Type u_1

The data of a UPred object is an indexed proposition over M (Bundled version)

• holds (n : Nat) : ValidAt M n → Prop

  The proposition asserted at a step index and valid resource.

• mono {n1 n2 : Nat} {x1 : ValidAt M n1} {x2 : ValidAt M n2} : self.holds n1 x1 → x1.val ≼ₒ{n2} x2.val → ∀ (Hle : n2 ≤ n1), self.holds n2 x2

theorem Iris.UPred.ext_iff {M : Type u_1} {inst✝ : OFE M} {inst✝¹ : Validity M} {inst✝² : Ordered M} {x y : UPred M} : x = y ↔ x.holds = y.holds

theorem Iris.UPred.ext {M : Type u_1} {inst✝ : OFE M} {inst✝¹ : Validity M} {inst✝² : Ordered M} {x y : UPred M} (holds : x.holds = y.holds) : x = y

def Iris.UPred.holdsUnpacked {M : Type u_1} [OFE M] [Validity M] [Ordered M] (P : UPred M) (n : Nat) (x : M) (Hx : ✓{n} x) : Prop

Evaluate a predicate with validity supplied as a separate proof.

Equations

• P.holdsUnpacked n x Hx = P.holds n { val := x, property := Hx }

theorem Iris.UPred.mono_unpacked {M : Type u_1} [OFE M] [Validity M] [Ordered M] (P : UPred M) {n1 n2 : Nat} {x1 x2 : M} (Hx1 : ✓{n1} x1) (Hx2 : ✓{n2} x2) (HP : P.holdsUnpacked n1 x1 Hx1) (Hxle : x1 ≼ₒ{n2} x2) (Hle : n2 ≤ n1) : P.holdsUnpacked n2 x2 Hx2

theorem Iris.uPred_alt {M : Type u_1} [OFE M] [Ordered M] [OrderRefl M] (P : Nat → M → Prop) : (∀ {n1 n2 : Nat} {x1 x2 : M}, P n1 x1 → x1 ≼ₒ{n1} x2 → n2 ≤ n1 → P n2 x2) ↔ (∀ {x : M} {n1 n2 : Nat}, n2 ≤ n1 → P n1 x → P n2 x) ∧ (∀ {n : Nat} {x1 x2 : M}, OFE.Dist n x1 x2 → ∀ (m : Nat), m ≤ n → (P m x1 ↔ P m x2)) ∧ ∀ {n : Nat} {x1 x2 : M}, x1 ≼ₒ{n} x2 → ∀ (m : Nat), m ≤ n → P m x1 → P m x2

The definition of UPred is equivalent to separately proving pointwise down-closure, non-expansivity, and monotonicity.

@[instance_reducible]

instance Iris.instInhabitedUPred {M : Type u_1} [OFE M] [Validity M] [Ordered M] : Inhabited (UPred M)

Equations

• Iris.instInhabitedUPred = { default := { holds := fun (x : Nat) (x_1 : Iris.ValidAt M x) => True, mono := ⋯ } }

@[instance_reducible]

instance Iris.instCoeFunUPredForallForallValidAtProp {M : Type u_1} [OFE M] [Validity M] [Ordered M] : CoeFun (UPred M) fun (x : UPred M) => (n : Nat) → ValidAt M n → Prop

Equations

• Iris.instCoeFunUPredForallForallValidAtProp = { coe := fun (x : Iris.UPred M) => x.holds }

@[instance_reducible]

instance Iris.instOFEUPred {M : Type u_1} [OFE M] [Validity M] [Ordered M] : OFE (UPred M)

Equations

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

theorem Iris.uPred_ne {M : Type u_1} [OFE M] [Validity M] [Ordered M] [OrderRefl M] {P : UPred M} {n : Nat} {m₁ m₂ : ValidAt M n} (H : OFE.Dist n m₁.val m₂.val) : P.holds n m₁ ↔ P.holds n m₂

theorem Iris.uPred_holds_ne {M : Type u_1} [OFE M] [Validity M] [Ordered M] [OrderRefl M] {P Q : UPred M} {n₁ n₂ : Nat} {x : M} (HPQ : OFE.Dist n₂ P Q) (Hn : n₂ ≤ n₁) (Hx : ✓{n₂} x) (Hx' : ✓{n₁} x) (HQ : Q.holds n₁ { val := x, property := Hx' }) : P.holds n₂ { val := x, property := Hx }

@[instance_reducible]

instance Iris.instIsCOFEUPredOfOrderRefl {M : Type u_1} [OFE M] [Validity M] [Ordered M] [OrderRefl M] : IsCOFE (UPred M)

Equations

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

@[reducible, inline]

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

The contravariant predicate functor induced by a unital resource functor.

Equations

• Iris.UPredOF F A B = Iris.UPred (F B A)

def Iris.uPredMap {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] (f : β -C> α) : UPred α -n> UPred β

Pull a monotone step-indexed predicate back along a resource morphism.

Equations

• Iris.uPredMap f = { f := fun (P : Iris.UPred α) => { holds := fun (n : Nat) (x : Iris.ValidAt β n) => P.holds n { val := f.f x.val, property := ⋯ }, mono := ⋯ }, ne := ⋯ }

@[instance_reducible]

instance Iris.instOFunctorUPredOF {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [URFunctor F] : COFE.OFunctor (UPredOF F)

Equations

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

@[instance_reducible]

instance Iris.instUPredOFunctorContractive {F : (α : Type u_1) → (β : Type u_2) → [COFE α] → [COFE β] → Type u_3} [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F)

Equations

• Iris.instUPredOFunctorContractive = { toOFunctor := Iris.instOFunctorUPredOF, map_contractive := ⋯ }