Frame-preserving updates of ordered resources.

Copyright (c) The Iris-Lean Contributors.

def Iris.UpdateP {α : Type u_1} [OFE α] [Op α] [Validity α] (x : α) (P : α → Prop) : Prop

A frame-preserving update to some resource satisfying a predicate.

Equations

• (x ~~>: P) = ∀ (n : Nat) (mz : Option α), ✓{n} x •? mz → ∃ (y : α), P y ∧ ✓{n} y •? mz

def Iris.«term_~~>:_» : Lean.TrailingParserDescr

Notation for a frame-preserving update satisfying a predicate.

Equations

• Iris.«term_~~>:_» = Lean.ParserDescr.trailingNode `Iris.«term_~~>:_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~~>: ") (Lean.ParserDescr.cat `term 50))

def Iris.Update {α : Type u_1} [OFE α] [Op α] [Validity α] (x y : α) : Prop

A frame-preserving update to a specified resource.

Equations

• (x ~~> y) = ∀ (n : Nat) (mz : Option α), ✓{n} x •? mz → ✓{n} y •? mz

def Iris.«term_~~>_» : Lean.TrailingParserDescr

Notation for a frame-preserving update to a specified resource.

Equations

• Iris.«term_~~>_» = Lean.ParserDescr.trailingNode `Iris.«term_~~>_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~~> ") (Lean.ParserDescr.cat `term 50))

theorem Iris.Update.of_updateP {α : Type u_1} [OFE α] [Op α] [Validity α] {x y : α} (h : x ~~>: fun (x : α) => y = x) : x ~~> y

theorem Iris.UpdateP.of_update {α : Type u_1} [OFE α] [Op α] [Validity α] {x y : α} (h : x ~~> y) : x ~~>: fun (x : α) => y = x

theorem Iris.UpdateP.id {α : Type u_1} [OFE α] [Op α] [Validity α] {P : α → Prop} {x : α} (h : P x) : x ~~>: P

theorem Iris.Update.id {α : Type u_1} [OFE α] [Op α] [Validity α] {x : α} : x ~~> x

theorem Iris.Update.trans {α : Type u_1} [OFE α] [Op α] [Validity α] {x y z : α} (uxy : x ~~> y) (uyz : y ~~> z) : x ~~> z

theorem Iris.UpdateP.trans {α : Type u_1} [OFE α] [Op α] [Validity α] {P Q : α → Prop} {x : α} (ux : x ~~>: P) (upq : ∀ (y : α), P y → y ~~>: Q) : x ~~>: Q

theorem Iris.Update.transP {α : Type u_1} [OFE α] [Op α] [Validity α] {Q : α → Prop} {x y : α} (uxy : x ~~> y) (uyq : y ~~>: Q) : x ~~>: Q

theorem Iris.UpdateP.weaken {α : Type u_1} [OFE α] [Op α] [Validity α] {P Q : α → Prop} {x : α} (uxp : x ~~>: P) (pq : ∀ (y : α), P y → Q y) : x ~~>: Q

theorem Iris.Update.exclusive {α : Type u_1} [OFE α] [Op α] [Validity α] {x y : α} [ORA.Exclusive x] (vy : ✓ y) : x ~~> y

instance Iris.instReflUpdate {α : Type u_1} [OFE α] [Op α] [Validity α] : Std.Refl Update

@[instance_reducible]

instance Iris.instTransUpdate {α : Type u_1} [OFE α] [Op α] [Validity α] : Trans Update Update Update

Equations

• Iris.instTransUpdate = { trans := ⋯ }

@[instance_reducible]

instance Iris.instTransForallPropUpdateUpdateP {α : Type u_1} [OFE α] [Op α] [Validity α] : Trans Update UpdateP UpdateP

Equations

• Iris.instTransForallPropUpdateUpdateP = { trans := ⋯ }

theorem Iris.UpdateP.op {α : Type u_1} [OFE α] [Op α] [Validity α] {P Q R : α → Prop} {x y : α} (uxp : x ~~>: P) (uyq : y ~~>: Q) (pqr : ∀ (z w : α), P z → Q w → R (z • w)) : x • y ~~>: R

theorem Iris.UpdateP.op' {α : Type u_1} [OFE α] [Op α] [Validity α] {P Q : α → Prop} {x y : α} (uxp : x ~~>: P) (uyq : y ~~>: Q) : x • y ~~>: fun (t : α) => ∃ (z : α), ∃ (w : α), t = z • w ∧ P z ∧ Q w

theorem Iris.Update.op {α : Type u_1} [OFE α] [Op α] [Validity α] {x₁ x₂ y₁ y₂ : α} (xy₁ : x₁ ~~> y₁) (xy₂ : x₂ ~~> y₂) : x₁ • x₂ ~~> y₁ • y₂

Isomorphism

theorem Iris.UpdateP.iso {α : Type u_1} {β : Type u_2} [OFE α] [Op α] [Validity α] [OFE β] [Op β] [Validity β] (f : α → β) (g : β → α) {y : β} {P : β → Prop} {Q : α → Prop} (gf : ∀ (x : α), g (f x) = x) (g_op : ∀ (y1 y2 : β), g (y1 • y2) = g y1 • g y2) (g_validN : ∀ (n : Nat) (y : β), ✓{n} g y ↔ ✓{n} y) (uyp : y ~~>: P) (pq : ∀ (y' : β), P y' → Q (g y')) : g y ~~>: Q

theorem Iris.UpdateP.iso' {α : Type u_1} {β : Type u_2} [OFE α] [Op α] [Validity α] [OFE β] [Op β] [Validity β] (f : α → β) (g : β → α) {y : β} {P : β → Prop} (gf : ∀ (x : α), g (f x) = x) (g_op : ∀ (y1 y2 : β), g (y1 • y2) = g y1 • g y2) (g_validN : ∀ (n : Nat) (y : β), ✓{n} g y ↔ ✓{n} y) (uyp : y ~~>: P) : g y ~~>: fun (x : α) => ∃ (y : β), x = g y ∧ P y

Lift

theorem Iris.Update.lift_updateP {α : Type u_2} {β : Type u_1} [OFE α] [Op α] [Validity α] [OFE β] [Op β] [Validity β] (g : β → α) (x y : β) (H : ∀ (P : β → Prop), x ~~>: P → g x ~~>: fun (a' : α) => ∃ (b' : β), a' = g b' ∧ P b') (uxy : x ~~> y) : g x ~~> g y

theorem Iris.Update.op_l {α : Type u_1} [ORA α] {x y : α} : x • y ~~> x

theorem Iris.Update.op_r {α : Type u_1} [ORA α] {x y : α} : x • y ~~> y

theorem Iris.Update.ord {α : Type u_1} [ORA α] {x y : α} (h : x ≼ₒ y) : y ~~> x

theorem Iris.Update.included {α : Type u_1} [ORA α] {x y : α} : x ≼ y → y ~~> x

theorem Iris.Update.valid0 {α : Type u_1} [ORA α] {x y : α} : (✓{0} x → x ~~> y) → x ~~> y

Frame preserving updates for total and discrete CMRAs

theorem Iris.UpdateP.total {α : Type u_1} [ORA α] {x : α} {P : α → Prop} [IsTotal α] : x ~~>: P ↔ ∀ (n : Nat) (z : α), ✓{n} x • z → ∃ (y : α), P y ∧ ✓{n} y • z

theorem Iris.Update.total {α : Type u_1} [ORA α] {x y : α} [IsTotal α] : x ~~> y ↔ ∀ (n : Nat) (z : α), ✓{n} x • z → ✓{n} y • z

theorem Iris.UpdateP.discrete {α : Type u_1} [ORA α] {x : α} {P : α → Prop} [ORA.Discrete α] : x ~~>: P ↔ ∀ (mz : Option α), ✓ x •? mz → ∃ (y : α), P y ∧ ✓ y •? mz

theorem Iris.Update.discrete {α : Type u_1} [ORA α] [ORA.Discrete α] {x y : α} : x ~~> y ↔ ∀ (mz : Option α), ✓ x •? mz → ✓ y •? mz

theorem Iris.UpdateP.discrete_total {α : Type u_1} [ORA α] {x : α} {P : α → Prop} [ORA.Discrete α] [IsTotal α] : x ~~>: P ↔ ∀ (z : α), ✓ x • z → ∃ (y : α), P y ∧ ✓ y • z

theorem Iris.Update.discrete_total {α : Type u_1} [ORA α] {x y : α} [ORA.Discrete α] [IsTotal α] : x ~~> y ↔ ∀ (z : α), ✓ x • z → ✓ y • z

Product

theorem Iris.UpdateP.prod {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {P : α → Prop} {Q : β → Prop} {R : α × β → Prop} {x : α × β} (uxp : x.fst ~~>: P) (uxq : x.snd ~~>: Q) (pq : ∀ (a : α) (b : β), P a → Q b → R (a, b)) : x ~~>: R

theorem Iris.UpdateP.prod' {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] (P : α → Prop) (Q : β → Prop) (x : α × β) (uxp : x.fst ~~>: P) (uxq : x.snd ~~>: Q) : x ~~>: fun (y : α × β) => P y.fst ∧ Q y.snd

theorem Iris.Update.prod {α : Type u_1} {β : Type u_2} [ORA α] [ORA β] {y : α × β} (x : α × β) (uxy₁ : x.fst ~~> y.fst) (uxy₂ : x.snd ~~> y.snd) : x ~~> y

Option

theorem Iris.UpdateP.option {α : Type u_1} [ORA α] {P : α → Prop} {Q : Option α → Prop} {x : α} (uxp : x ~~>: P) (pq : ∀ (y : α), P y → Q (some y)) : some x ~~>: Q

theorem Iris.UpdateP.option' {α : Type u_1} [ORA α] (P : α → Prop) (x : α) (uxp : x ~~>: P) : some x ~~>: fun (t : Option α) => Option.rec False P t

theorem Iris.Update.option {α : Type u_1} [ORA α] (x y : α) (uxy : x ~~> y) : some x ~~> some y