Discrete degree carriers

The finite, Fin-backed scale carriers used by RSA fragments and computational Studies [Ken07] [Hei01] [KMcN05]: Bounded max / Threshold max with their order/Fintype instances, and the threshold-comparison predicates (tall / short / not tall). The abstract theory works with plain measure functions μ : E → D into a preorder (Comparative.lean, Extent.lean); this module is its decidable discretization.

Main definitions

• Bounded max, Threshold max — discrete bounded scale types.
• deg, thr — literal constructors.
• positiveMeaning, negativeMeaning, notPositiveMeaning — the three opposition relations as decidable threshold comparisons.

Discrete bounded scales

structure Degree.Bounded (max : ℕ) : Type

A degree on a scale from 0 to max — a discretized continuous value (height, temperature, …).

• value : Fin (max + 1)

def Degree.instReprBounded.repr {max✝ : ℕ} : Bounded max✝ → ℕ → Std.Format

Equations

• Degree.instReprBounded.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

@[implicit_reducible]

instance Degree.instReprBounded {max✝ : ℕ} : Repr (Bounded max✝)

Equations

• Degree.instReprBounded = { reprPrec := Degree.instReprBounded.repr }

@[implicit_reducible]

instance Degree.instDecidableEqBounded {max✝ : ℕ} : DecidableEq (Bounded max✝)

Equations

• Degree.instDecidableEqBounded = Degree.instDecidableEqBounded.decEq

def Degree.instDecidableEqBounded.decEq {max✝ : ℕ} (x✝ x✝¹ : Bounded max✝) : Decidable (x✝ = x✝¹)

Equations

• Degree.instDecidableEqBounded.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instInhabitedBounded {n : ℕ} : Inhabited (Bounded n)

Equations

• Degree.instInhabitedBounded = { default := { value := ⟨0, ⋯⟩ } }

@[implicit_reducible]

instance Degree.instLinearOrderBounded {max : ℕ} : LinearOrder (Bounded max)

Bounded max inherits a linear order from Fin (max + 1).

Equations

• Degree.instLinearOrderBounded = LinearOrder.lift' Degree.Bounded.value ⋯

@[implicit_reducible]

instance Degree.instBoundedOrderBounded {max : ℕ} : BoundedOrder (Bounded max)

Bounded max is bounded: 0 is the minimum, max the maximum.

Equations

• Degree.instBoundedOrderBounded = { top := { value := Fin.last max }, le_top := ⋯, bot := { value := ⟨0, ⋯⟩ }, bot_le := ⋯ }

def Degree.allDegrees (max : ℕ) : List (Bounded max)

All degrees from 0 to max.

Equations

• Degree.allDegrees max = List.map (fun (x : Fin (max + 1)) => { value := x }) (List.finRange (max + 1))

def Degree.Bounded.ofNat (max n : ℕ) : Bounded max

Bounded from Nat (clamped to max).

Equations

• Degree.Bounded.ofNat max n = { value := ⟨min n max, ⋯⟩ }

def Degree.Bounded.toNat {max : ℕ} (d : Bounded max) : ℕ

The numeric value of a degree.

Equations

• d.toNat = ↑d.value

structure Degree.Threshold (max : ℕ) : Type

A threshold for a gradable adjective: x is "tall" iff degree x > threshold.

• value : Fin max

@[implicit_reducible]

instance Degree.instReprThreshold {max✝ : ℕ} : Repr (Threshold max✝)

Equations

• Degree.instReprThreshold = { reprPrec := Degree.instReprThreshold.repr }

def Degree.instReprThreshold.repr {max✝ : ℕ} : Threshold max✝ → ℕ → Std.Format

Equations

• Degree.instReprThreshold.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

def Degree.instDecidableEqThreshold.decEq {max✝ : ℕ} (x✝ x✝¹ : Threshold max✝) : Decidable (x✝ = x✝¹)

Equations

• Degree.instDecidableEqThreshold.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instDecidableEqThreshold {max✝ : ℕ} : DecidableEq (Threshold max✝)

Equations

• Degree.instDecidableEqThreshold = Degree.instDecidableEqThreshold.decEq

@[implicit_reducible]

instance Degree.instInhabitedThresholdOfNeZeroNat {n : ℕ} [NeZero n] : Inhabited (Threshold n)

Equations

• Degree.instInhabitedThresholdOfNeZeroNat = { default := { value := ⟨0, ⋯⟩ } }

@[implicit_reducible]

instance Degree.instLinearOrderThreshold {max : ℕ} : LinearOrder (Threshold max)

Threshold max inherits a linear order from Fin max.

Equations

• Degree.instLinearOrderThreshold = LinearOrder.lift' Degree.Threshold.value ⋯

def Degree.allThresholds (max : ℕ) : autoParam (0 < max) allThresholds._auto_1 → List (Threshold max)

All thresholds from 0 to max - 1.

Equations

• Degree.allThresholds max x✝ = List.map (fun (x : Fin max) => { value := x }) (List.finRange max)

def Degree.Threshold.toNat {max : ℕ} (t : Threshold max) : ℕ

The numeric value of a threshold.

Equations

• t.toNat = ↑t.value

@[implicit_reducible]

instance Degree.instFintypeBounded {max : ℕ} : Fintype (Bounded max)

Equations

• Degree.instFintypeBounded = Fintype.ofEquiv (Fin (max + 1)) { toFun := Degree.Bounded.mk, invFun := Degree.Bounded.value, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance Degree.instFintypeThresholdOfNeZeroNat {max : ℕ} [NeZero max] : Fintype (Threshold max)

Equations

• Degree.instFintypeThresholdOfNeZeroNat = Fintype.ofEquiv (Fin max) { toFun := Degree.Threshold.mk, invFun := Degree.Threshold.value, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance Degree.instCoeThresholdBounded {max : ℕ} : Coe (Threshold max) (Bounded max)

Coercion: a Threshold embeds into Bounded via Fin.castSucc.

Equations

• Degree.instCoeThresholdBounded = { coe := fun (t : Degree.Threshold max) => { value := t.value.castSucc } }

theorem Degree.coe_threshold_toNat {max : ℕ} (t : Threshold max) : { value := t.value.castSucc }.toNat = t.toNat

@[reducible, inline]

abbrev Degree.deg (n : ℕ) {max : ℕ} (h : n ≤ max := by omega) : Bounded max

Construct a degree by literal: deg 5 : Bounded 10.

Equations

• Degree.deg n h = { value := ⟨n, ⋯⟩ }

@[reducible, inline]

abbrev Degree.thr (n : ℕ) {max : ℕ} (h : n < max := by omega) : Threshold max

Construct a threshold by literal: thr 5 : Threshold 10.

Equations

• Degree.thr n h = { value := ⟨n, h⟩ }

Threshold-comparison meanings

General degree operations on the discrete carriers, not adjective-specific; decidability is inherited from the underlying Fin order.

def Degree.positiveMeaning {max : ℕ} (d : Bounded max) (t : Threshold max) : Prop

Positive form (tall): t < d — the strict threshold face of Core.Order.Comparison.gt.over on the discrete carrier.

Equations

• Degree.positiveMeaning d t = (d ∈ Core.Order.Comparison.gt.over id { value := t.value.castSucc })

def Degree.negativeMeaning {max : ℕ} (d : Bounded max) (t : Threshold max) : Prop

Polar antonym (short): d < t, evaluated against the antonym's own threshold (which may sit below the positive's — see Gradability.ThresholdPair).

Equations

• Degree.negativeMeaning d t = (d ∈ Core.Order.Comparison.lt.over id { value := t.value.castSucc })

def Degree.notPositiveMeaning {max : ℕ} (d : Bounded max) (t : Threshold max) : Prop

Contradictory negation (not tall): d ≤ t, the complement of positiveMeaning. Not the polar antonym — that is negativeMeaning.

Equations

• Degree.notPositiveMeaning d t = (d ∈ Core.Order.Comparison.le.over id { value := t.value.castSucc })

@[implicit_reducible]

instance Degree.instDecidablePositiveMeaning {max : ℕ} (d : Bounded max) (t : Threshold max) : Decidable (positiveMeaning d t)

Equations

• Degree.instDecidablePositiveMeaning d t = Degree.instDecidablePositiveMeaning._aux_1 d t

@[implicit_reducible]

instance Degree.instDecidableNegativeMeaning {max : ℕ} (d : Bounded max) (t : Threshold max) : Decidable (negativeMeaning d t)

Equations

• Degree.instDecidableNegativeMeaning d t = Degree.instDecidableNegativeMeaning._aux_1 d t

@[implicit_reducible]

instance Degree.instDecidableNotPositiveMeaning {max : ℕ} (d : Bounded max) (t : Threshold max) : Decidable (notPositiveMeaning d t)

Equations

• Degree.instDecidableNotPositiveMeaning d t = Degree.instDecidableNotPositiveMeaning._aux_1 d t