structure Iris.Agree (α : Type u) : Type u

• car : List α
• not_nil : self.car ≠ []

theorem Iris.Agree.ext_iff {α : Type u} {x y : Agree α} : x = y ↔ x.car = y.car

theorem Iris.Agree.ext {α : Type u} {x y : Agree α} (car : x.car = y.car) : x = y

def Iris.toAgree {α : Type u} (a : α) : Agree α

Equations

• Iris.toAgree a = { car := [a], not_nil := ⋯ }

theorem Iris.mem_of_agree {α : Type u} (x : Agree α) : ∃ (a : α), a ∈ x.car

def Iris.Agree.dist {α : Type u} [OFE α] (n : Nat) (x y : Agree α) : Prop

Equations

• Iris.Agree.dist n x y = ((∀ (a : α), a ∈ x.car → ∃ (b : α), b ∈ y.car ∧ Iris.OFE.Dist n a b) ∧ ∀ (b : α), b ∈ y.car → ∃ (a : α), a ∈ x.car ∧ Iris.OFE.Dist n a b)

theorem Iris.Agree.dist_equiv {α : Type u} [OFE α] {n : Nat} : Equivalence (dist n)

instance Iris.instOFEAgree {α : Type u} [OFE α] : OFE (Agree α)

Equations

• Iris.instOFEAgree = { Equiv := fun (x y : Iris.Agree α) => ∀ (n : Nat), Iris.Agree.dist n x y, Dist := Iris.Agree.dist, dist_eqv := ⋯, equiv_dist := ⋯, dist_lt := ⋯ }

theorem Iris.Agree.equiv_def {α : Type u} [OFE α] {x y : Agree α} : OFE.Equiv x y ↔ ∀ (n : Nat), dist n x y

theorem Iris.Agree.dist_def {α : Type u} [OFE α] {n : Nat} {x y : Agree α} : OFE.Dist n x y ↔ dist n x y

def Iris.Agree.validN {α : Type u} [OFE α] (n : Nat) (x : Agree α) : Prop

Equations

• Iris.Agree.validN n x = match x.car with | [head] => True | x_1 => ∀ (a : α), a ∈ x.car → ∀ (b : α), b ∈ x.car → Iris.OFE.Dist n a b

theorem Iris.Agree.validN_iff {α : Type u} [OFE α] {n : Nat} {x : Agree α} : validN n x ↔ ∀ (a : α), a ∈ x.car → ∀ (b : α), b ∈ x.car → OFE.Dist n a b

def Iris.Agree.valid {α : Type u} [OFE α] (x : Agree α) : Prop

Equations

• x.valid = ∀ (n : Nat), Iris.Agree.validN n x

def Iris.Agree.op {α : Type u} (x y : Agree α) : Agree α

Equations

• x.op y = { car := x.car ++ y.car, not_nil := ⋯ }

theorem Iris.Agree.op_comm {α : Type u} [OFE α] {x y : Agree α} : OFE.Equiv (x.op y) (y.op x)

theorem Iris.Agree.op_commN {α : Type u} [OFE α] {n : Nat} {x y : Agree α} : OFE.Dist n (x.op y) (y.op x)

theorem Iris.Agree.op_assoc {α : Type u} [OFE α] {x y z : Agree α} : OFE.Equiv (x.op (y.op z)) ((x.op y).op z)

theorem Iris.Agree.idemp {α : Type u} [OFE α] {x : Agree α} : OFE.Equiv (x.op x) x

theorem Iris.Agree.validN_ne {α : Type u} [OFE α] {n : Nat} {x y : Agree α} : OFE.Dist n x y → validN n x → validN n y

theorem Iris.Agree.op_ne {α : Type u} [OFE α] {x : Agree α} : OFE.NonExpansive x.op

theorem Iris.Agree.op_ne₂ {α : Type u} [OFE α] : OFE.NonExpansive₂ op

theorem Iris.Agree.op_invN {α : Type u} [OFE α] {n : Nat} {x y : Agree α} : validN n (x.op y) → OFE.Dist n x y

theorem Iris.Agree.op_inv {α : Type u} [OFE α] {x y : Agree α} : (x.op y).valid → OFE.Equiv x y

instance Iris.instCMRAAgree {α : Type u} [OFE α] : CMRA (Agree α)

Equations

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

theorem Iris.Agree.op_def {α : Type u} [OFE α] {x y : Agree α} : x • y = x.op y

theorem Iris.Agree.validN_def {α : Type u} [OFE α] {n : Nat} {x : Agree α} : ✓{n} x ↔ validN n x

theorem Iris.Agree.valid_def {α : Type u} [OFE α] {x : Agree α} : ✓ x ↔ x.valid

instance Iris.instIsTotalAgree {α : Type u} [OFE α] : CMRA.IsTotal (Agree α)

instance Iris.instDiscreteAgreeOfDiscrete {α : Type u} [OFE α] [OFE.Discrete α] : CMRA.Discrete (Agree α)

instance Iris.instNonExpansiveAgreeToAgree {α : Type u} [OFE α] : OFE.NonExpansive toAgree

theorem Iris.Agree.toAgree_injN {α : Type u} [OFE α] {n : Nat} {a b : α} : OFE.Dist n (toAgree a) (toAgree b) → OFE.Dist n a b

theorem Iris.Agree.toAgree_inj {α : Type u} [OFE α] {a b : α} : OFE.Equiv (toAgree a) (toAgree b) → OFE.Equiv a b

theorem Iris.Agree.toAgree_uninjN {α : Type u} [OFE α] {n : Nat} {x : Agree α} : ✓{n} x → ∃ (a : α), OFE.Dist n (toAgree a) x

theorem Iris.Agree.toAgree_uninj {α : Type u} [OFE α] {x : Agree α} : ✓ x → ∃ (a : α), OFE.Equiv (toAgree a) x

theorem Iris.Agree.includedN {α : Type u} [OFE α] {n : Nat} {x y : Agree α} : x ≼{n} y ↔ OFE.Dist n y (y • x)

theorem Iris.Agree.included {α : Type u} [OFE α] {x y : Agree α} : x ≼ y ↔ OFE.Equiv y (y • x)

theorem Iris.Agree.valid_includedN {α : Type u} [OFE α] {n : Nat} {x y : Agree α} : ✓{n} y → x ≼{n} y → OFE.Dist n x y

theorem Iris.Agree.valid_included {α : Type u} [OFE α] {x y : Agree α} : ✓ y → x ≼ y → OFE.Equiv x y

@[simp]

theorem Iris.Agree.toAgree_includedN {α : Type u} [OFE α] {n : Nat} {a b : α} : toAgree a ≼{n} toAgree b ↔ OFE.Dist n a b

@[simp]

theorem Iris.Agree.toAgree_included {α : Type u} [OFE α] {a b : α} : toAgree a ≼ toAgree b ↔ OFE.Equiv a b

@[simp]

theorem Iris.Agree.toAgree_included_L {α : Type u} [OFE α] [OFE.Leibniz α] {a b : α} : toAgree a ≼ toAgree b ↔ a = b

instance Iris.instCancelableAgree {α : Type u} [OFE α] {x : Agree α} : CMRA.Cancelable x

theorem Iris.Agree.toAgree_op_validN_iff_dist {α : Type u} [OFE α] {n : Nat} {a b : α} : ✓{n} toAgree a • toAgree b ↔ OFE.Dist n a b

theorem Iris.Agree.toAgree_op_valid_iff_equiv {α : Type u} [OFE α] {b a : α} : ✓ toAgree a • toAgree b ↔ OFE.Equiv a b

theorem Iris.toAgree_op_valid_iff_eq {α : Type u} [OFE α] {b : α} [OFE.Leibniz α] {a : α} : ✓ toAgree a • toAgree b ↔ a = b

def Iris.Agree.map' {α : Type u_1} {β : Type u_2} (f : α → β) (a : Agree α) : Agree β

Equations

• Iris.Agree.map' f a = { car := List.map f a.car, not_nil := ⋯ }

theorem Iris.instNonExpansiveAgreeMap' {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {f : α → β} [hne : OFE.NonExpansive f] : OFE.NonExpansive (Agree.map' f)

def Iris.Agree.map {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] (f : α → β) [hne : OFE.NonExpansive f] : Agree α -C> Agree β

Equations

• Iris.Agree.map f = { f := Iris.Agree.map' f, ne := ⋯, validN := ⋯, pcore := ⋯, op := ⋯ }

theorem Iris.Agree.agree_map_ext {α : Type u_1} {β : Type u_2} [OFE α] [OFE β] {f : α → β} [hne : OFE.NonExpansive f] {x : Agree α} {g : α → β} [OFE.NonExpansive g] (heq : ∀ (a : α), OFE.Equiv (f a) (g a)) : OFE.Equiv ((map f).f x) ((map g).f x)