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) :

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.

Instances For
    def Nat.Upto.GT (p : Prop) (x : Nat.Upto p) (y : Nat.Upto p) :

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

    Instances For
      instance Nat.Upto.instLT {p : Prop} :
      • Nat.Upto.instLT = { lt := fun (x y : Nat.Upto p) => x < y }
      theorem {p : Prop} :
      (∃ (x : ), p x)WellFounded (Nat.Upto.GT p)

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

      def {p : Prop} :

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

      • = 0,
      Instances For
        def Nat.Upto.succ {p : Prop} (x : Nat.Upto p) (h : ¬p x) :

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

        • x.succ h = (x).succ,
        Instances For