The Frac CMRA

This CMRA captures the notion of fractional ownership of another resource. Traditionally the underlying set is assumed to be the half open interval $$(0,1]$$.

class Iris.Fraction (α : Type u_1) extends Add α : Type u_1

• add : α → α → α
• Proper : α → Prop

  Validity predicate on fractions. Generalizes the notion of (· ≤ 1) from rational fractions.

• add_comm (a b : α) : a + b = b + a
• add_assoc (a b c : α) : a + (b + c) = a + b + c
• add_left_cancel {a b c : α} : a + b = a + c → b = c
• add_ne {a b : α} : a ≠ b + a

  There does not exist a zero fraction.

• proper_add_mono_left {a b : α} : Proper (a + b) → Proper a

def Iris.Fraction.Fractional {α : Type u_1} [Fraction α] (a : α) : Prop

A fraction does not represent the entire resource. Generalizes the notion of (· < 1) from rational fractions.

Equations

• Iris.Fraction.Fractional a = ∃ (b : α), Iris.Fraction.Proper (a + b)

def Iris.Fraction.Whole {α : Type u_1} [Fraction α] (a : α) : Prop

A fraction that is tne entire resource. Generalizes the notion of 1 from rational fractions.

Equations

• Iris.Fraction.Whole a = (Iris.Fraction.Proper a ∧ ¬Iris.Fraction.Fractional a)

theorem Iris.Fraction.Proper.fractional_or_whole {α : Type u_1} [Fraction α] {a : α} (H : Proper a) : Fractional a ∨ Whole a

theorem Iris.Fraction.Fractional.not_whole {α : Type u_1} [Fraction α] {a : α} (H : Fractional a) : ¬Whole a

theorem Iris.Fraction.Whole.not_fractional {α : Type u_1} [Fraction α] {a : α} (H : Whole a) : ¬Fractional a

theorem Iris.Fraction.add_right_cancel {α : Type u_1} [Fraction α] {a b c : α} (H : b + a = c + a) : b = c

theorem Iris.Fraction.Fractional.proper {α : Type u_1} [Fraction α] {a : α} : Fractional a → Proper a

theorem Iris.Fraction.Fractional.of_add_left {α : Type u_1} [Fraction α] {a a' : α} (H : Fractional (a + a')) : Fractional a

theorem Iris.Fraction.Fractional.of_add_right {α : Type u_1} [Fraction α] {a a' : α} (H : Fractional (a + a')) : Fractional a'

def Iris.Frac (α : Type u_1) : Type u_1

Equations

• Iris.Frac α = Iris.LeibnizO α

instance Iris.instCoeFracOfFraction {α : Type u_1} [Fraction α] : Coe (Frac α) α

Equations

• Iris.instCoeFracOfFraction = { coe := fun (x : Iris.Frac α) => x.car }

instance Iris.instCoeFracOfFraction_1 {α : Type u_1} [Fraction α] : Coe α (Frac α)

Equations

• Iris.instCoeFracOfFraction_1 = { coe := fun (x : α) => { car := x } }

instance Iris.instCOFEFrac {α : Type u_1} : COFE (Frac α)

Equations

• Iris.instCOFEFrac = inferInstanceAs (Iris.COFE (Iris.LeibnizO α))

instance Iris.instAddFracOfFraction {α : Type u_1} [Fraction α] : Add (Frac α)

Equations

• Iris.instAddFracOfFraction = { add := fun (x y : Iris.Frac α) => { car := x.car + y.car } }

instance Iris.instLeibnizFrac {α : Type u_1} : OFE.Leibniz (Frac α)

instance Iris.Frac_CMRA {α : Type u_1} [Fraction α] : CMRA (Frac α)

Equations

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

instance Iris.instDiscreteFrac {α : Type u_1} [Fraction α] : CMRA.Discrete (Frac α)

instance Iris.instExclusiveFracOfCMRAOfWholeCar {α : Type u_1} [Fraction α] [CMRA α] {a : Frac α} (Hw : Fraction.Whole a.car) : CMRA.Exclusive a

instance Iris.instCancelableFrac {α : Type u_1} [Fraction α] {a : Frac α} : CMRA.Cancelable a

instance Iris.instIdFreeFrac {α : Type u_1} [Fraction α] {a : Frac α} : CMRA.IdFree a

class Iris.UFraction (α : Type u_1) extends Iris.Fraction α, One α : Type u_1

A type of fractions with a unique whole element.

• add : α → α → α
• Proper : α → Prop
• add_comm (a b : α) : a + b = b + a
• add_assoc (a b c : α) : a + (b + c) = a + b + c
• add_left_cancel {a b c : α} : a + b = a + c → b = c
• add_ne {a b : α} : a ≠ b + a
• proper_add_mono_left {a b : α} : Proper (a + b) → Proper a
• one : α
• one_whole : Fraction.Whole 1

class Iris.NumericFraction (α : Type u_1) extends One α, Add α, LE α, LT α : Type u_1

Generic fractional instance for types with comparison and 1 operators.

• one : α
• add : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• add_comm (a b : α) : a + b = b + a
• add_assoc (a b c : α) : a + (b + c) = a + b + c
• add_left_cancel {a b c : α} : a + b = a + c → b = c
• le_def {a b : α} : a ≤ b ↔ a = b ∨ a < b
• lt_def {a b : α} : a < b ↔ ∃ (c : α), a + c = b
• lt_irrefl {a : α} : ¬a < a

instance Iris.instOneFracOfNumericFraction {T : Type u_1} [NumericFraction T] : One (Frac T)

Equations

• Iris.instOneFracOfNumericFraction = { one := { car := One.one } }

instance Iris.instLEFracOfNumericFraction {T : Type u_1} [NumericFraction T] : LE (Frac T)

Equations

• Iris.instLEFracOfNumericFraction = { le := fun (x1 x2 : Iris.Frac T) => x1.car ≤ x2.car }

instance Iris.instLTFracOfNumericFraction {T : Type u_1} [NumericFraction T] : LT (Frac T)

Equations

• Iris.instLTFracOfNumericFraction = { lt := fun (x1 x2 : Iris.Frac T) => x1.car < x2.car }

theorem Iris.le_rfl {α : Type u_1} [NumericFraction α] {a : α} : a ≤ a

theorem Iris.lt_trans {α : Type u_1} [NumericFraction α] {a b c : α} : a < b → b < c → a < c

theorem Iris.le_trans {α : Type u_1} [NumericFraction α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c

theorem Iris.add_le_mono {α : Type u_1} [NumericFraction α] {a b c : α} : a + b ≤ c → a ≤ c

theorem Iris.lt_le {α : Type u_1} [NumericFraction α] {a b : α} : a < b → a ≤ b

theorem Iris.add_ne_self {α : Type u_1} [NumericFraction α] {a b : α} : a + b ≠ a

theorem Iris.not_add_lt_self {α : Type u_1} [NumericFraction α] {a b : α} : ¬a + b < a

theorem Iris.not_add_le_self {α : Type u_1} [NumericFraction α] {a b : α} : ¬a + b ≤ a

instance Iris.instUFraction {α : Type u_1} [NumericFraction α] : UFraction α

Equations

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

theorem Iris.Frac.inc_iff_lt {α : Type u_1} [NumericFraction α] {p q : Frac α} : p ≼ q ↔ p < q

theorem Iris.Frac.le_of_inc {α : Type u_1} [NumericFraction α] {p q : Frac α} (H : p ≼ q) : p ≤ q