Grip.Modality: the three-valued modality

never < possibly < always, the truth values of the grip parser grade algebra. Batteries-only: no mathlib. Join and meet are the core Max/Min classes (max/min); grip deliberately does not declare Sup/Inf, so grip-props can import mathlib (which declares those) without a duplicate-declaration clash.

inductive Modality : Type

Three-valued modality tracking whether a property holds always, possibly, or never. The order is never ≤ possibly ≤ always.

• never : Modality
• possibly : Modality
• always : Modality

@[instance_reducible]

instance instDecidableEqModality : DecidableEq Modality

Equations

• instDecidableEqModality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprModality.repr : Modality → Nat → Std.Format

Equations

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

@[instance_reducible]

instance instReprModality : Repr Modality

Equations

• instReprModality = { reprPrec := instReprModality.repr }

@[reducible]

def Modality.sup : Modality → Modality → Modality

Supremum on Modality: the join in never < possibly < always. max a b = a when a is the greater element.

Reducible so that a grade product of named grades (conditional * conditional, ...) still reduces under instances transparency, which is what dsimp/rw type-check goals at since Lean v4.31.

Equations

• always.sup x✝ = always
• x✝.sup always = always
• possibly.sup x✝ = possibly
• x✝.sup possibly = possibly
• never.sup never = never

def Modality.inf : Modality → Modality → Modality

Infimum on Modality: the meet in never < possibly < always.

Equations

• never.inf x✝ = never
• x✝.inf never = never
• possibly.inf x✝ = possibly
• x✝.inf possibly = possibly
• always.inf always = always

@[instance_reducible]

instance Modality.instMax : Max Modality

Equations

• Modality.instMax = { max := Modality.sup }

@[instance_reducible]

instance Modality.instMin : Min Modality

Equations

• Modality.instMin = { min := Modality.inf }

def Modality.le : Modality → Modality → Prop

Order relation: never ≤ possibly ≤ always.

Equations

• never.le x✝ = True
• x✝.le always = True
• possibly.le possibly = True
• x✝¹.le x✝ = False

@[instance_reducible]

instance Modality.instLE : LE Modality

Equations

• Modality.instLE = { le := Modality.le }

@[instance_reducible]

instance Modality.instLT : LT Modality

Equations

• Modality.instLT = { lt := fun (a b : Modality) => a ≤ b ∧ ¬b ≤ a }

@[instance_reducible]

instance Modality.instDecidableLe (a b : Modality) : Decidable (a ≤ b)

Decidability of ≤ on Modality.

Equations

• never.instDecidableLe never = isTrue True.intro
• never.instDecidableLe possibly = isTrue True.intro
• never.instDecidableLe always = isTrue True.intro
• possibly.instDecidableLe never = isFalse Modality.instDecidableLe._proof_1
• possibly.instDecidableLe possibly = isTrue True.intro
• possibly.instDecidableLe always = isTrue True.intro
• always.instDecidableLe never = isFalse Modality.instDecidableLe._proof_2
• always.instDecidableLe possibly = isFalse Modality.instDecidableLe._proof_3
• always.instDecidableLe always = isTrue True.intro

def Modality.ite (sel a b : Modality) : Modality

Conditional selection driven by sel : Modality.

• always.ite a b = a (first branch wins)
• never.ite a b = b (second branch wins)
• possibly.ite a b = a when a = b, otherwise possibly (conservative)

Equations

• always.ite a b = a
• never.ite a b = b
• possibly.ite a b = if a = b then a else possibly

@[simp]

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

@[simp]

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

@[simp]

theorem Modality.ite_possibly_eq (a : Modality) : possibly.ite a a = a

@[simp]

theorem Modality.ite_possibly (a b : Modality) : possibly.ite a b = if a = b then a else possibly

@[simp]

theorem Modality.sup_never_left (a : Modality) : max never a = a

never is the left identity for join.

@[simp]

theorem Modality.sup_never_right (a : Modality) : max a never = a

never is the right identity for join.

@[simp]

theorem Modality.sup_always_left (a : Modality) : max always a = always

always absorbs on the left for join.

@[simp]

theorem Modality.sup_always_right (a : Modality) : max a always = always

always absorbs on the right for join.

@[simp]

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

A join equals always iff at least one operand is always.

@[simp]

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

A join equals never iff both operands are never.

@[simp]

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

A meet equals never iff at least one operand is never.

@[simp]

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

A meet equals always iff both operands are always.

theorem Modality.sup_comm (a b : Modality) : max a b = max b a

Join is commutative.

theorem Modality.le_possibly_of_ne_always {a : Modality} (h : a ≠ always) : a ≤ possibly

If a ≠ always then a ≤ possibly.

theorem Modality.possibly_le_of_ne_never {a : Modality} (h : a ≠ never) : possibly ≤ a

If a ≠ never then possibly ≤ a.