inductive Necessity : Type

Three-valued modality tracking whether a property holds always, possibly, or never.

• possibly : Necessity
• always : Necessity
• never : Necessity

instance instReprNecessity : Repr Necessity

Equations

• instReprNecessity = { reprPrec := instReprNecessity.repr }

def instReprNecessity.repr : Necessity → ℕ → Std.Format

Equations

• instReprNecessity.repr Necessity.possibly prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Necessity.possibly")).group prec✝
• instReprNecessity.repr Necessity.always prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Necessity.always")).group prec✝
• instReprNecessity.repr Necessity.never prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Necessity.never")).group prec✝

instance Necessity.instMax : Max Necessity

Equations

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

instance Necessity.instMin : Min Necessity

Equations

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

instance Necessity.instLinearOrder : LinearOrder Necessity

Equations

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

instance Necessity.instBoundedOrder : BoundedOrder Necessity

Equations

• Necessity.instBoundedOrder = { top := Necessity.always, le_top := Necessity.instBoundedOrder._proof_1, bot := Necessity.never, bot_le := Necessity.instBoundedOrder._proof_2 }

instance Necessity.instSemilatticeSup : SemilatticeSup Necessity

Equations

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

instance Necessity.instSemilatticeInf : SemilatticeInf Necessity

Equations

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

instance Necessity.instMonoid : Monoid Necessity

Equations

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

instance Necessity.instLattice : Lattice Necessity

Equations

• Necessity.instLattice = { toSemilatticeSup := Necessity.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

instance Necessity.instDistribLattice : DistribLattice Necessity

Equations

• Necessity.instDistribLattice = { toLattice := Necessity.instLattice, le_sup_inf := Necessity.instDistribLattice._proof_1 }

def Necessity.complement : Necessity → Necessity

Flips always and never, leaving possibly unchanged.

Equations

• Necessity.always.complement = Necessity.never
• Necessity.possibly.complement = Necessity.possibly
• Necessity.never.complement = Necessity.always

instance Necessity.instComplement : Complement Necessity

Equations

• Necessity.instComplement = { complement := Necessity.complement }

@[simp]

theorem Necessity.complement_always : always.complement = never

@[simp]

theorem Necessity.complement_possibly : possibly.complement = possibly

@[simp]

theorem Necessity.complement_never : never.complement = always

@[simp]

theorem Necessity.max_never_right (a : Necessity) : max a never = a

@[simp]

theorem Necessity.max_never_left (a : Necessity) : max never a = a

@[simp]

theorem Necessity.never_le (a : Necessity) : never ≤ a

@[simp]

theorem Necessity.le_always (a : Necessity) : a ≤ always

@[simp]

theorem Necessity.max_always (a b : Necessity) : max a b = always ↔ a = always ∨ b = always

@[simp]

theorem Necessity.max_never (a b : Necessity) : max a b = never ↔ a = never ∧ b = never

@[simp]

theorem Necessity.min_never (a b : Necessity) : min a b = never ↔ a = never ∨ b = never

@[simp]

theorem Necessity.min_always (a b : Necessity) : min a b = always ↔ a = always ∧ b = always

@[simp]

theorem Necessity.complement_always_iff (a : Necessity) : a.complement = always ↔ a = never

@[simp]

theorem Necessity.complement_never_iff (a : Necessity) : a.complement = never ↔ a = always

@[reducible, inline]

abbrev Necessity.ite (sel a b : Necessity) : Necessity

Conditional selection: when sel is always returns a, when never returns b, when possibly returns a conservative value (see theorem ite_possibly and ite_possibly_cases).

Equations

• sel.ite a b = max (max (min a b) (min sel a)) (min sel.complement b)

@[simp]

theorem Necessity.ite_always (a b : Necessity) : always.ite a b = a

@[simp]

theorem Necessity.ite_never (a b : Necessity) : never.ite a b = b

@[simp]

theorem Necessity.ite_possibly (a b : Necessity) : possibly.ite a b = max (min a b) (min possibly (max a b))

@[simp]

theorem Necessity.ite_possibly_cases (a b : Necessity) : possibly.ite a b = if a = b then a else possibly

@[simp]

theorem Necessity.ite_idem (a b : Necessity) : b.ite a a = a