Strict well-orders and least-element search

Suppose a property of natural numbers is known to hold of at least one number. Then it holds of a least number: among the witnesses there is a smallest one. For a general strict well-order, this chapter uses a descent from a known witness. If some strictly smaller element is still a witness, move down to it and repeat. If not, the current element is least. Well-foundedness of the order guarantees this descent cannot continue forever, so the process stops at a least witness.

This chapter turns that argument into a theorem for any strict well-order, not just the natural numbers. Two pieces of order data carry the proof. First, a comparison of two elements has three possible outcomes, strictly below, equal, or strictly above, and representing these outcomes as explicit data lets a proof reason by cases on them; this is what shows a least witness, once found, is unique, since two least witnesses cannot be strictly below each other. Second, well-foundedness is presented as an accessibility certificate for every element, and it is these certificates, handed down step by step, that let the descent be carried out inside type theory. One genuinely classical ingredient remains in this proof: at each step the search decides whether some smaller witness still exists, and that mere-existence question is settled by excluded middle at the level where it is asked. Everything else, including the uniqueness of the result, is constructive.

The chapter first defines comparison data, then states the order laws together, then proves that being least is a proposition and that least witnesses exist. It closes by assembling the strict order on the natural numbers into an instance, so the search applies there concretely.

The carrier of the order and the order relation itself need not sit at the same universe level: a relation may be valued at a fixed level ℓₚ while its carrier lives at any level. This separation is a matter of generality, not of the mathematics of the search; the least-element argument below never compares levels.

Two mathematical notions then do the work. Well-foundedness is phrased through the accessibility predicate Acc: an element is accessible when every strictly smaller element is accessible in turn, and a relation is well founded when every element is accessible. These accessibility certificates are what license the recursive descent of the search. Trichotomy, in turn, is the comparison data that makes least witnesses unique. The natural-number order supplies both notions already, so its instance requires assembly rather than a fresh proof.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.WellOrder.Base {ℓₚ : Level} where

The search must also live with incomplete information. The hypothesis says only that the set of witnesses is merely inhabited, an inhabitant of ∥_∥₁, and at each descent step the question whether some strictly smaller witness remains is again a mere existence statement. Neither assumption hands over a chosen witness, and neither needs to: propositional truncation may be eliminated because the goal, being a least element, is a proposition, and that propositionhood is proved in this chapter. Excluded middle enters precisely to turn each such existence question into a two-way decision, a proof or a refutation.

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
open import Cubical.Data.Nat using ( ℕ )
open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
import Cubical.HITs.PropositionalTruncation as PT

This logical situation fixes the order of the proof. Before eliminating either truncation, we first show that leastness at a point is a proposition and that the total type of least witnesses is also a proposition. Trichotomy supplies the path between any two candidates, while impossible strict comparisons are discharged by their minimality. Only after that uniqueness argument is the descent allowed to consume the merely inhabited hypothesis.

open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )
open import Cubical.Relation.Nullary using ( isProp¬ ) renaming ( ¬_ to ¬ᵗ_ )
import Cubical.Data.Empty as Empty

A decision, when it exists, returns either a proof or a refutation. The two-way sum with its constructors provides exactly this shape of verdict, and it will carry the choice that excluded middle hands to the descent.

open import Cubical.Data.Sum using ( _⊎_; inl; inr )

Trichotomy, as data

Comparing two elements of a strict well-order has three possible outcomes, and later proofs need to reason by cases on which outcome occurred. We therefore represent the comparison as an inductive type with three constructors, each carrying its own evidence: a proof of the strict relation in one direction, an equality, or a proof in the other direction. Because the three alternatives are constructor tags rather than a nested sum of types, a proof can inspect the comparison directly and name the case it is in. Each of the three types may live at its own universe level, and the comparison type lands at the maximum of the three.

The three constructors lt, eq and gt correspond to the three outcomes. The equality branch carries a proof of the path a ≡ b between the carrier elements, rather than returning a bare tag that merely reports equality. For the natural-number example this type will be filled by translating the library's three-way decision on a ≟ b, constructor by constructor.

data Tri {ℓ₁ ℓ₂ ℓ₃ : Level} (A : Type ℓ₁) (B : Type ℓ₂) (C : Type ℓ₃)
       : Type (ℓ-max ℓ₁ (ℓ-max ℓ₂ ℓ₃)) where
  lt : A → Tri A B C
  eq : B → Tri A B C
  gt : C → Tri A B C

The bundle

A strict well-order is not just a relation: it is a relation together with the laws that make least-element search work. We gather the relation, trichotomy, irreflexivity, transitivity and well-foundedness into a single record SWO over a carrier A. Naming this interface keeps all later constructions independent of how any particular order happens to be built; the natural-number order given later in this chapter and any other instance supply the same five fields. The carrier and the relation may sit at different universe levels: A lives at level ℓc, while the relation takes values in Type ℓₚ. Since the type of such relation values itself lies one universe higher, the record lives at ℓ-max ℓc (ℓ-suc ℓₚ).

The first two fields are the relation and its trichotomy. For any two elements a and b, tri∙ returns comparison data: either a <∙ b, a path a ≡ b, or b <∙ a. Trichotomy is what makes least elements unique later, since two candidates cannot be strictly below each other.

record SWO {ℓc : Level} (A : Type ℓc) : Type (ℓ-max ℓc (ℓ-suc ℓₚ)) where
  field
    _<∙_   : A → A → Type ℓₚ
    tri∙   : (a b : A) → Tri (a <∙ b) (a ≡ b) (b <∙ a)
    irr∙   : (a : A) → ¬ᵗ a <∙ a

The remaining three fields are the order laws. irr∙ says no element is below itself, trans∙ is transitivity, and wf∙ asserts that every element of A is accessible for the relation. Accessibility is the inductive principle behind well-founded recursion: given acc rs at a, the function rs produces accessibility data for every smaller element. It is precisely this supply, handed down step by step, that makes the descent in the search terminate.

    trans∙ : (a b c : A) → a <∙ b → b <∙ c → a <∙ c
    wf∙    : WellFounded _<∙_

Least elements

Fix a strict well-order w on A. For a predicate P valued in propositions, an element a is least for P when it satisfies P and no element satisfying P is strictly below it. Being least is a proposition, and so is the type of least elements as a whole: given two, trichotomy excludes both strict cases and forces equality. These two propositionhood facts are the hinge of the chapter, because a proposition-valued goal may absorb propositional truncation. That is what will let the search below turn a merely inhabited subset into an actual least element.

The definition takes P as a family of hProp: each fiber is packaged with a certificate that it is a proposition. ⟨ P a ⟩ projects the underlying type, so IsLeast P a is the pair of a witness that a satisfies P and a function sending every other witness b, together with its certificate ⟨ P b ⟩, to a refutation of b <∙ a. Note that the leastness bound is required only of elements that actually satisfy the predicate; elements outside the subset may lie anywhere.

module _ {ℓc : Level} {A : Type ℓc} (w : SWO {ℓc} A) where
  open SWO w

  IsLeast : {ℓ'' : Level} → (A → hProp ℓ'') → A → Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
  IsLeast P a = ⟨ P a ⟩ × ((b : A) → ⟨ P b ⟩ → ¬ᵗ b <∙ a)

  isPropIsLeast : {ℓ'' : Level} (P : A → hProp ℓ'') (a : A) → isProp (IsLeast P a)

Both components of IsLeast P a are propositions: the first by the certificate packed into P a, the second because a negation-valued function into propositions is propositional. Hence IsLeast P a is a proposition, by closing the pair under products of propositions. For the total type of least elements, Σ≡Prop identifies two pairs as soon as their first components agree, provided the second is propositional; that reduction is exactly what the auxiliary decide carries out.

  isPropIsLeast P a = isProp× (snd (P a)) (isPropΠ λ b → isPropΠ λ _ → isProp¬ _)

  isPropLeastOf : {ℓ'' : Level} (P : A → hProp ℓ'')
                → isProp (Σ[ a ∈ A ] IsLeast P a)
  isPropLeastOf P (m , pm , minm) (m' , pm' , minm') =
    Σ≡Prop (isPropIsLeast P) (decide (tri∙ m m'))

To compare two least elements m and m', decide inspects tri∙ m m'. If m <∙ m', then m' is least and m satisfies the predicate, so m should not be strictly below m': contradiction, via Empty.rec, which discharges any goal from an impossible case. The symmetric case is analogous. In the remaining case the comparison itself hands over the path e : m ≡ m', which is returned directly. Together with Σ≡Prop, this proves isPropLeastOf: the type of least witnesses for P is a proposition, so leastness, once it exists, is unique.

    where
    decide : Tri (m <∙ m') (m ≡ m') (m' <∙ m) → m ≡ m'
    decide (lt m<m') = Empty.rec (minm' m pm m<m')
    decide (eq e)    = e
    decide (gt m'<m) = Empty.rec (minm m' pm' m'<m)

Here is the search itself. It takes excluded middle at the level where the questions are asked, a predicate P, and a mere inhabitant of the subset of witnesses, and returns an actual pair of a least witness with its leastness data. The argument descends along the well-order: from any starting witness, ask whether some strictly smaller element still satisfies P. If yes, recurse there, which terminates because each recursion moves strictly down and accessibility is handed along. If no, the current element is least by definition. Each step needs a classical decision of a proposition built from the arbitrary predicate, and that is the only place excluded middle enters; the statement and the order laws themselves remain constructive.

The elimination of the truncation in the hypothesis is legitimate because the target Σ[ a ∈ A ] IsLeast P a was shown to be a proposition by isPropLeastOf. So from the merely inhabited subset we may extract some starting witness a₀ with its certificate, and then begin the descent go a₀ (wf∙ a₀) pa₀: the accessibility data wf∙ a₀, part of the bundle, is the fuel for the recursion. Note that the starting witness is arbitrary; the descent, not the choice of starting point, produces the least element.

  leastOf : {ℓ'' : Level} → LEM (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
          → (P : A → hProp ℓ'')
          → ∥ Σ[ a ∈ A ] ⟨ P a ⟩ ∥₁ → Σ[ a ∈ A ] IsLeast P a
  leastOf {ℓ''} lem P =
    PT.rec (isPropLeastOf P) (λ { (a₀ , pa₀) → go a₀ (wf∙ a₀) pa₀ })

The auxiliary go receives an element a, its accessibility data, and a certificate that a satisfies P; it returns a least witness. At each step it forms the proposition Smaller: whether there merely exists an element strictly below a that still satisfies P. This is an hProp because its underlying type is a propositional truncation, so excluded middle applies to it; the level bookkeeping ensures the decision is taken at exactly the level of the data involved.

    where
    go : (a : A) → Acc _<∙_ a → ⟨ P a ⟩ → Σ[ m ∈ A ] IsLeast P m
    go a (acc rs) pa = decide (lem (Smaller , squash₁))
      where
      Smaller : Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))

Applying lem to Smaller yields either a proof or a refutation, and decide turns either verdict into a least witness. In the positive case the truncated statement is again eliminated into the proposition-valued goal, handing a genuine element b strictly below a with P b; the recursion continues at b using the accessibility function rs, which is defined precisely on the elements below a. This is the descent step, and the accessibility data is what guarantees it cannot go on forever.

      Smaller = ∥ Σ[ b ∈ A ] ((b <∙ a) × ⟨ P b ⟩) ∥₁
      decide : Smaller ⊎ (Smaller → Empty.⊥) → Σ[ m ∈ A ] IsLeast P m
      decide (inl q) = PT.rec (isPropLeastOf P)
        (λ { (b , (b<a , pb)) → go b (rs b b<a) pb }) q
      decide (inr ¬q) = a , (pa , λ b pb b<a → ¬q ∣ b , (b<a , pb) ∣₁)

The natural numbers, well-ordered

The usual strict order on the natural numbers satisfies all four laws of the bundle, and its well-foundedness follows by induction on the upper number. This section assembles natOrder : SWO {ℓ-zero} ℕ; a concrete consumer, L.Choice.FiniteStageOrders, calls leastOf natOrder to pick the earliest natural-numbered finite stage witnessing a property. The library already supplies every ingredient about the usual order, so the bundle is assembled rather than proved: the relation, irreflexivity, transitivity and well-foundedness are the library's own, and the trichotomy is the library's three-way decision procedure with its answer renamed into the chapter's constructors.

One genuine step remains. The order on the natural numbers lives at the bottom universe level, while the relation of a bundle is valued at the fixed level ℓₚ; each comparison is therefore wrapped in Lift, which changes only where the type lives and nothing about its inhabitants.

liftAcc transports accessibility data from the plain order to its lifted copy. Given acc r at n, it returns acc of a function that, from m below n in the lifted order, first unwraps the lifted proof with lower and recurses at m. This is structural recursion on the accessibility argument, the same pattern that will drive leastOf. Note the two universe arguments of Lift: the source stays at zero and only the target is ℓₚ.

liftAcc : (n : ℕ) → Acc _<_ n → Acc (λ a b → Lift {ℓ-zero} {ℓₚ} (a < b)) n
liftAcc n (acc r) = acc (λ m h → liftAcc m (r m (lower h)))

natOrder : SWO {ℓ-zero} ℕ
natOrder = record
  { _<∙_   = λ a b → Lift (a < b)

With the lifted accessibility in hand, natOrder is filled in field by field. The relation sends a and b to Lift (a < b); irreflexivity unwraps its hypothesis and applies the library's ¬m<m; transitivity unwraps both proofs, composes them with the library's <-trans, and re-lifts the result; well-foundedness produces liftAcc n (<-wellfounded n) at each n. No new mathematics about the natural-number order is proved here, only the level adjustment and the renaming into the bundle's field names.

  ; tri∙   = triOf
  ; irr∙   = λ a h → ¬m<m (lower h)
  ; trans∙ = λ a b c h k → lift (<-trans (lower h) (lower k))
  ; wf∙    = λ n → liftAcc n (<-wellfounded n) }
  where

The trichotomy field is triOf, defined in the where block. The library's decision procedure a ≟ b returns a value of the library's own three-way type NatOrder.Trichotomy a b, whose constructors lt, eq and gt carry the same three kinds of evidence as the chapter's Tri. So fromNat maps constructor to constructor: a strictness proof in either direction is lifted, and an equality is passed through unchanged, since equality of natural numbers needs no level adjustment.

  triOf : (a b : ℕ) → Tri (Lift (a < b)) (a ≡ b) (Lift (b < a))
  triOf a b = fromNat (a ≟ b)
    where
    fromNat : NatOrder.Trichotomy a b → Tri (Lift (a < b)) (a ≡ b) (Lift (b < a))
    fromNat (NatOrder.lt h) = lt (lift h)

The three clauses of fromNat complete the translation. Reading them together shows why renaming suffices: the library's comparison data and the chapter's are the same shape, differing only in where the two strictness types live. With this field filled, natOrder is a fully assembled bundle, and everything from the previous sections applies to it: given excluded middle, every inhabited proposition-valued predicate on ℕ has a unique least witness.

    fromNat (NatOrder.eq h) = eq h
    fromNat (NatOrder.gt h) = gt (lift h)

Recap

Strict well-orders can now be passed around as a single structure, compared by trichotomy, and searched for least witnesses. SWO gathers the relation with its four laws, and leastOf extracts, from any merely inhabited subset, a least witness that is unique up to the path supplied by isPropLeastOf. The natural-number instance natOrder supports searches over natural-number indices, for instance when a later chapter picks the earliest finite stage of L witnessing a property. Excluded middle enters only as the decision asked at each descent step of the search; the bundle definition, its laws and the natural-number order remain constructive.