Core/Scales/Comparison.lean — reified degree comparison

Comparison reifies the five ways a measured value relates to a threshold — =, ≥, >, ≤, < — as data (cf. core Ordering, reified for compare). It is the shared, theory-neutral primitive behind numeral modifiers, measure phrases, and (the measure-derived case of) gradable comparatives, per the joint degree-semantic treatment of [Ken15] and [Ret14].

It interprets two ways, both bottoming out in mathlib's order API so downstream proofs reduce into Set.mem_Ici & friends rather than a bespoke lemma set:

• Comparison.rel — the order relation ([kennedy-2015]'s REL).
• Comparison.interval — the order-interval (Set.Ici/Ioi/Iic/Iio/{·}).
• Comparison.over μ n — the predication μ ⁻¹' (c.interval n): the entities whose measure lands in the interval. Bare cardinals are over .eq id, measure phrases over c μ for a MeasureFn, classifier counting over .eq (atom-count).
• Comparison.overSet μ Δ — the set-standard generalization μ ⁻¹' (c.bounds Δ): the entities whose measure bounds the whole standard set Δ. The point predication over is the singleton case (overSet_singleton); this is the order-theoretic core of [Hoe83]'s S-comparative, with the binary NP-comparative its singleton face.

Main declarations

• Core.Order.Comparison — the reified comparison.
• Comparison.isStrict — Class A (>,<) vs. non-strict (=,≥,≤).
• Comparison.over / Comparison.overSet — point- and set-standard predications.
• Comparison.boundary_mem — Class A/B as interval-endpoint membership.

inductive Core.Order.Comparison : Type

[Ken15]'s REL reified: the relation a degree modifier draws between a measured value and a threshold.

• eq : Comparison

  Exact / bare: μ x = n.

• ge : Comparison

  "At least n": μ x ≥ n.

• gt : Comparison

  "More than n": μ x > n.

• le : Comparison

  "At most n": μ x ≤ n.

• lt : Comparison

  "Fewer than n": μ x < n.

@[implicit_reducible]

instance Core.Order.instDecidableEqComparison : DecidableEq Comparison

Equations

• Core.Order.instDecidableEqComparison x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Order.instReprComparison : Repr Comparison

Equations

• Core.Order.instReprComparison = { reprPrec := Core.Order.instReprComparison.repr }

def Core.Order.instReprComparison.repr : Comparison → ℕ → Std.Format

Equations

• Core.Order.instReprComparison.repr Core.Order.Comparison.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.eq")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.ge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.ge")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.gt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.gt")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.le prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.le")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.lt")).group prec✝

@[implicit_reducible]

instance Core.Order.instInhabitedComparison : Inhabited Comparison

Equations

• Core.Order.instInhabitedComparison = { default := Core.Order.instInhabitedComparison.default }

def Core.Order.Comparison.isStrict : Comparison → Prop

Strict (Class A: >, <) vs. non-strict (bare =, Class B ≥, ≤). The modifier-level Class A/B split ([GN07], [Nou10]) is isStrict restricted to the four modified forms.

Equations

• Core.Order.Comparison.gt.isStrict = True
• Core.Order.Comparison.lt.isStrict = True
• x✝.isStrict = False

@[implicit_reducible]

instance Core.Order.instDecidablePredComparisonIsStrict : DecidablePred Comparison.isStrict

Equations

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

def Core.Order.Comparison.rel {α : Type u_1} [Preorder α] : Comparison → α → α → Prop

The order relation a Comparison stands for.

Equations

• Core.Order.Comparison.eq.rel = fun (x1 x2 : α) => x1 = x2
• Core.Order.Comparison.ge.rel = fun (x1 x2 : α) => x1 ≥ x2
• Core.Order.Comparison.gt.rel = fun (x1 x2 : α) => x1 > x2
• Core.Order.Comparison.le.rel = fun (x1 x2 : α) => x1 ≤ x2
• Core.Order.Comparison.lt.rel = fun (x1 x2 : α) => x1 < x2

def Core.Order.Comparison.interval {α : Type u_1} [Preorder α] : Comparison → α → Set α

The order-interval a comparison selects, in mathlib terms: {n} / [n,∞) / (n,∞) / (-∞,n] / (-∞,n).

Equations

• Core.Order.Comparison.eq.interval = fun (n : α) => {n}
• Core.Order.Comparison.ge.interval = Set.Ici
• Core.Order.Comparison.gt.interval = Set.Ioi
• Core.Order.Comparison.le.interval = Set.Iic
• Core.Order.Comparison.lt.interval = Set.Iio

def Core.Order.Comparison.over {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (n : α) : Set E

The unifying predication: the entities whose measure μ lands in the comparison's interval. The measure varies — id for bare cardinals, a dimensional MeasureFn for measure phrases, an atom-count for classifiers.

Equations

• c.over μ n = μ ⁻¹' c.interval n

@[simp]

theorem Core.Order.Comparison.mem_interval {α : Type u_1} [Preorder α] (c : Comparison) (a n : α) : a ∈ c.interval n ↔ c.rel a n

@[simp]

theorem Core.Order.Comparison.mem_over {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (n : α) (x : E) : x ∈ c.over μ n ↔ c.rel (μ x) n

@[implicit_reducible]

instance Core.Order.Comparison.relDecidable {α : Type u_1} [Preorder α] [DecidableEq α] [DecidableLE α] [DecidableLT α] (c : Comparison) (a n : α) : Decidable (c.rel a n)

Equations

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

@[implicit_reducible]

instance Core.Order.Comparison.overDecidable {E : Type u_1} {α : Type u_2} [Preorder α] [DecidableEq α] [DecidableLE α] [DecidableLT α] (c : Comparison) (μ : E → α) (n : α) (x : E) : Decidable (x ∈ c.over μ n)

Equations

• c.overDecidable μ n x = decidable_of_iff (c.rel (μ x) n) ⋯

@[simp]

theorem Core.Order.Comparison.boundary_mem {α : Type u_1} [Preorder α] (c : Comparison) (n : α) : n ∈ c.interval n ↔ ¬c.isStrict

Class A/B is interval-endpoint membership. A non-strict comparison (bare =, Class B ≥/≤) keeps the boundary n; a strict one (Class A >/<) drops it — the whole Class A/B distinction ([GN07], [Nou10]) in one lemma.

Set-standard comparison

The than-clause of a comparative supplies not a point but a set of degrees. Comparison.bounds lifts Comparison.interval from a point n to a standard set Δ — the (strict) upper/lower bounds matching the comparison's relation — and Comparison.overSet is the corresponding measure-pullback predication. The point predication over is exactly the singleton case (overSet_singleton).

def Core.Order.Comparison.bounds {α : Type u_1} [Preorder α] : Comparison → Set α → Set α

The standard-set a comparison imposes: the bounds of Δ matching the comparison's relation (upperBounds/strictUpperBounds/… per case). Generalizes Comparison.interval from a point n (≡ {n}) to a standard set Δ.

Equations

• Core.Order.Comparison.eq.bounds = fun (Δ : Set α) => {x : α | ∀ a ∈ Δ, x = a}
• Core.Order.Comparison.ge.bounds = upperBounds
• Core.Order.Comparison.gt.bounds = strictUpperBounds
• Core.Order.Comparison.le.bounds = lowerBounds
• Core.Order.Comparison.lt.bounds = strictLowerBounds

def Core.Order.Comparison.overSet {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (Δ : Set α) : Set E

Set-standard predication: the entities whose measure bounds the whole standard set Δ. The set-standard generalization of Comparison.over and the order-theoretic core of [Hoe83]'s S-comparative; the binary NP-comparative is the singleton case (overSet_singleton).

Equations

• c.overSet μ Δ = μ ⁻¹' c.bounds Δ

theorem Core.Order.Comparison.bounds_singleton {α : Type u_1} [Preorder α] (c : Comparison) (n : α) : c.bounds {n} = c.interval n

bounds at a singleton standard collapses to the point interval.

@[simp]

theorem Core.Order.Comparison.mem_overSet {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (Δ : Set α) (x : E) : x ∈ c.overSet μ Δ ↔ μ x ∈ c.bounds Δ

@[simp]

theorem Core.Order.Comparison.overSet_singleton {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (n : α) : c.overSet μ {n} = c.over μ n

The NP ⊂ S bridge: the set-standard predication at a singleton standard is the point predication. Makes [Hoe83]'s NP↔S equivalence definitional.