inductive Necessity : Type

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

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

@[instance_reducible]

instance instReprNecessity : Repr Necessity

Equations

• instReprNecessity = { reprPrec := instReprNecessity.repr }

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

Equations

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

@[reducible, noinline]

def Necessity.max : Necessity → Necessity → Necessity

Equations

• always.max x✝ = always
• possibly.max never = possibly
• x✝¹.max x✝ = x✝

@[reducible, noinline]

def Necessity.min : Necessity → Necessity → Necessity

Equations

• never.min x✝ = never
• possibly.min always = possibly
• x✝¹.min x✝ = x✝

@[instance_reducible]

instance Necessity.instMax : Max Necessity

Equations

• Necessity.instMax = { max := Necessity.max }

@[instance_reducible]

instance Necessity.instMin : Min Necessity

Equations

• Necessity.instMin = { min := Necessity.min }

@[instance_reducible]

instance Necessity.instLinearOrder : LinearOrder Necessity

Equations

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

@[instance_reducible]

instance Necessity.instBoundedOrder : BoundedOrder Necessity

Equations

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

@[instance_reducible]

instance Necessity.instSemilatticeSup : SemilatticeSup Necessity

Equations

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

@[instance_reducible]

instance Necessity.instSemilatticeInf : SemilatticeInf Necessity

Equations

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

@[instance_reducible]

instance Necessity.instMonoid : Monoid Necessity

Equations

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

@[instance_reducible]

instance Necessity.instLattice : Lattice Necessity

Equations

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

@[instance_reducible]

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

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

@[instance_reducible]

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.max a never = a

@[simp]

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

@[simp]

theorem Necessity.max_idem (a : Necessity) : Max.max a 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.max a b = always ↔ a = always ∨ b = always

@[simp]

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

@[simp]

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

@[simp]

theorem Necessity.min_always (a b : Necessity) : Min.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.max (Min.min a b) (Min.min possibly (Max.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

theorem Necessity.compl_le {c : Necessity} : possibly ≤ c → c.complement ≤ possibly

theorem Necessity.le_compl {c : Necessity} : c ≤ possibly → possibly ≤ c.complement