Nat.Upto

Nat.Upto p, with p a predicate on ℕ, is a subtype of elements n : ℕ such that no value (strictly) below n satisfies p.

This type has the property that > is well-founded when ∃ i, p i, which allows us to implement searches on ℕ, starting at 0 and with an unknown upper-bound.

It is similar to the well-founded relation constructed to define Nat.find with the difference that, in Nat.Upto p, p does not need to be decidable. In fact, Nat.find could be slightly altered to factor decidability out of its well-founded relation and would then fulfill the same purpose as this file.

@[reducible, inline]

abbrev Nat.Upto (p : ℕ → Prop) : Type

The subtype of natural numbers i which have the property that no j less than i satisfies p. This is an initial segment of the natural numbers, up to and including the first value satisfying p.

We will be particularly interested in the case where there exists a value satisfying p, because in this case the > relation is well-founded.

Equations

• Nat.Upto p = { i : ℕ // ∀ (j : ℕ), j < i → ¬p j }

def Nat.Upto.GT (p : ℕ → Prop) (x y : Upto p) : Prop

Lift the "greater than" relation on natural numbers to Nat.Upto.

Equations

• Nat.Upto.GT p x y = (↑x > ↑y)

instance Nat.Upto.instLT {p : ℕ → Prop} : LT (Upto p)

Equations

• Nat.Upto.instLT = { lt := fun (x y : Nat.Upto p) => ↑x < ↑y }

theorem Nat.Upto.wf {p : ℕ → Prop} : (∃ (x : ℕ), p x) → WellFounded (Upto.GT p)

The "greater than" relation on Upto p is well founded if (and only if) there exists a value satisfying p.

def Nat.Upto.zero {p : ℕ → Prop} : Upto p

Zero is always a member of Nat.Upto p because it has no predecessors.

Equations

• Nat.Upto.zero = ⟨0, ⋯⟩

def Nat.Upto.succ {p : ℕ → Prop} (x : Upto p) (h : ¬p ↑x) : Upto p

The successor of n is in Nat.Upto p provided that n doesn't satisfy p.

Equations

• x.succ h = ⟨(↑x).succ, ⋯⟩