Bundled decidable total preorders

A TotalPreorder α bundles a relation with mathlib's unbundled relation-class laws (IsPreorder, Std.Total) and decidability. Bundled — unlike a Preorder instance — because consumers quantify over orderings of a fixed carrier: plausibility frames rank worlds ([Lew73b] comparative similarity), and metalinguistic common grounds are sets of ordering-world pairs ranking semantic interpretations ([RK24]), so orderings must be first-class data.

Main declarations

• TotalPreorder — the bundle, with lt, equiv, and ofBool (construction from a Boolean table, for finite models).
• IsMaximal, AcceptedAt — top-ranked points, and truth of a predicate throughout them (Stalnaker-style acceptance on a plausibility frame).

Implementation notes

The canonical form of an ordering-as-data is the model-theoretic one: a Language.order.Structure modeling the total-preorder theory (Core/Logic/FirstOrder/TotalPreorder.lean, where toStructure/ofModel exchange the two presentations). This bundle is that object's decidable, proof-transparent working presentation. Mathlib has no bundled order-on-a-carrier object (its Preord bundles a type with one order); among term-level presentations, a raw relation with unbundled relation classes — the founding used here — beats extends Preorder α, which would transport the Preorder API but makes lt an opaque field where consumers need the transparent le a b ∧ ¬ le b a for decide and destructuring. Same-rank equivalence is mathlib's AntisymmRel rather than a new definition.

structure Core.Order.TotalPreorder (α : Type u_1) : Type u_1

A bundled total preorder. Laws are carried as mathlib's unbundled relation classes, registered as instances; decidability is not part of the frame — it enters locally where finite models compute (decidableLE_ofBool).

• le : α → α → Prop

  The preorder relation: le a b means a is ranked no higher than b.

• isPreorder : IsPreorder α self.le

  Reflexivity and transitivity, as mathlib's unbundled relation class.

• total : Std.Total self.le

  Totality, as mathlib's unbundled relation class.

theorem Core.Order.TotalPreorder.le_refl {α : Type u_1} (ord : TotalPreorder α) (a : α) : ord.le a a

Reflexivity (mathlib's Std.Refl, field-style).

theorem Core.Order.TotalPreorder.le_trans {α : Type u_1} (ord : TotalPreorder α) (a b c : α) : ord.le a b → ord.le b c → ord.le a c

Transitivity (mathlib's IsTrans, field-style).

theorem Core.Order.TotalPreorder.le_total {α : Type u_1} (ord : TotalPreorder α) (a b : α) : ord.le a b ∨ ord.le b a

Totality (mathlib's Std.Total, field-style).

def Core.Order.TotalPreorder.lt {α : Type u_1} (ord : TotalPreorder α) (a b : α) : Prop

Strict ordering: a is ranked strictly below b.

Equations

• ord.lt a b = (ord.le a b ∧ ¬ord.le b a)

@[implicit_reducible]

instance Core.Order.TotalPreorder.decRelLt {α : Type u_1} (ord : TotalPreorder α) [DecidableRel ord.le] : DecidableRel ord.lt

Equations

• ord.decRelLt x✝¹ x✝ = Core.Order.TotalPreorder.decRelLt._aux_1 ord x✝¹ x✝

theorem Core.Order.TotalPreorder.lt_of_le_of_lt {α : Type u_1} (ord : TotalPreorder α) {a b c : α} (h : ord.le a b) (h' : ord.lt b c) : ord.lt a c

theorem Core.Order.TotalPreorder.lt_of_lt_of_le {α : Type u_1} (ord : TotalPreorder α) {a b c : α} (h : ord.lt a b) (h' : ord.le b c) : ord.lt a c

theorem Core.Order.TotalPreorder.lt_irrefl {α : Type u_1} (ord : TotalPreorder α) (a : α) : ¬ord.lt a a

theorem Core.Order.TotalPreorder.exists_le_max {α : Type u_1} (ord : TotalPreorder α) (S : Finset α) (hS : S.Nonempty) : ∃ m ∈ S, ∀ s ∈ S, ord.le s m

Every nonempty finset has a greatest element under a total preorder.

@[reducible, inline]

abbrev Core.Order.TotalPreorder.equiv {α : Type u_1} (ord : TotalPreorder α) (a b : α) : Prop

Equivalence: a and b are ranked at the same level — mathlib's AntisymmRel (whose AntisymmRel.setoid is the level-quotient).

Equations

• ord.equiv a b = AntisymmRel ord.le a b

@[implicit_reducible]

instance Core.Order.TotalPreorder.decRelEquiv {α : Type u_1} (ord : TotalPreorder α) [DecidableRel ord.le] : DecidableRel ord.equiv

Equations

• ord.decRelEquiv x✝¹ x✝ = Core.Order.TotalPreorder.decRelEquiv._aux_1 ord x✝¹ x✝

theorem Core.Order.TotalPreorder.le_of_not_lt {α : Type u_1} (ord : TotalPreorder α) {a b : α} (h : ¬ord.lt a b) : ord.le b a

¬(a < b) → b ≤ a (by totality).

def Core.Order.TotalPreorder.ofBool {α : Type u_2} (f : α → α → Bool) (h_refl : ∀ (a : α), f a a = true) (h_trans : ∀ (a b c : α), f a b = true → f b c = true → f a c = true) (h_total : ∀ (a b : α), f a b = true ∨ f b a = true) : TotalPreorder α

Construct a TotalPreorder from a Bool-valued table — the convenient form for concrete finite models defined by pattern matching.

Equations

• Core.Order.TotalPreorder.ofBool f h_refl h_trans h_total = { le := fun (a b : α) => f a b = true, isPreorder := ⋯, total := ⋯ }

@[implicit_reducible]

instance Core.Order.TotalPreorder.decidableLE_ofBool {α : Type u_2} (f : α → α → Bool) (h₁ : ∀ (a : α), f a a = true) (h₂ : ∀ (a b c : α), f a b = true → f b c = true → f a c = true) (h₃ : ∀ (a b : α), f a b = true ∨ f b a = true) : DecidableRel (ofBool f h₁ h₂ h₃).le

Table-built orderings are decidable — the local decidability finite models recover in one instance.

Equations

• Core.Order.TotalPreorder.decidableLE_ofBool f h₁ h₂ h₃ x✝¹ x✝ = Core.Order.TotalPreorder.decidableLE_ofBool._aux_1 f h₁ h₂ h₃ x✝¹ x✝

def Core.Order.TotalPreorder.IsMaximal {α : Type u_1} (ord : TotalPreorder α) (x : α) : Prop

A top-ranked point: no point is ranked strictly above it.

Equations

• ord.IsMaximal x = ∀ (y : α), ¬ord.lt x y

@[implicit_reducible]

instance Core.Order.TotalPreorder.instDecidableIsMaximalOfFintypeOfDecidableRelLe {α : Type u_1} (ord : TotalPreorder α) [Fintype α] [DecidableRel ord.le] (x : α) : Decidable (ord.IsMaximal x)

Equations

• ord.instDecidableIsMaximalOfFintypeOfDecidableRelLe x = id inferInstance

def Core.Order.TotalPreorder.AcceptedAt {α : Type u_1} (ord : TotalPreorder α) (A : α → Prop) : Prop

Acceptance: a predicate holds throughout the top-ranked points.

Equations

• ord.AcceptedAt A = ∀ (x : α), ord.IsMaximal x → A x

@[implicit_reducible]

instance Core.Order.TotalPreorder.instDecidableAcceptedAtOfFintypeOfDecidableRelLeOfDecidablePred {α : Type u_1} (ord : TotalPreorder α) [Fintype α] [DecidableRel ord.le] (A : α → Prop) [DecidablePred A] : Decidable (ord.AcceptedAt A)

Equations

• ord.instDecidableAcceptedAtOfFintypeOfDecidableRelLeOfDecidablePred A = id inferInstance