Less than or equal for nat

Stream: new members

[Brandon Brown]

In Lean3 mathlib, less than or equal to for a nat is defined as an inductive type

inductive lte (a : ℕ) : ℕ → Prop
| refl {} : lte a
| step : Π {b}, lte b → lte (nat.succ b)

In Lean4 prelude, it is defined as a function returning a boolean (which is then mapped to a Prop by proposing an equality to true)

def Nat.ble : Nat → Nat → Bool
  | zero,   zero   => true
  | zero,   succ m => true
  | succ n, zero   => false
  | succ n, succ m => ble n m

protected def Nat.le (n m : Nat) : Prop :=
  ble n m = true

Is there any important differences between these two constructions? I tend to find the latter much more intuitive as a novice as I still haven't totally wrapped my head around what exactly is happening in the first one. I think it's creating an inductive family. Is there some other way of writing the inductive version that is more explicit about what's going on?

[Eric Rodriguez]

I'm not sure why the different definition was chosen, but I can try to explain the lean3 one. The first constructor basically says a ≤ a, and the second one says a ≤ b → a ≤ b + 1.

[Chris B]

Brandon Brown said:

Is there any important differences between these two constructions? I tend to find the latter much more intuitive as a novice as I still haven't totally wrapped my head around what exactly is happening in the first one. I think it's creating an inductive family. Is there some other way of writing the inductive version that is more explicit about what's going on?

The inductive one lets you do induction on evidence (the hitchhikers guide calls it rule induction), so you can do induction (h : a <= b). In some cases inductive relations let you nicely model things that functional ones don't necessarily. They can be strange at first since they seem backwards. There's a big section in Software Foundations 1 where they do both a functional and relational evaluator for a basic programming language, and they discuss how the relational version can more conveniently model things like potentially infinite loops and nondeterminism. They follow it up with this sort of high-level overview of the idea:

At this point you maybe wondering: which style should I use by default? In the examples we've just seen, relational definitions turned out to be more useful than functional ones. For situations like these, where the thing being defined is not easy to express as a function, or indeed where it is not a function, there is no real choice. But what about when both styles are workable?
One point in favor of relational definitions is that they can be more elegant and easier to understand.
...
On the other hand, functional definitions can often be more convenient:

    Functions are by definition deterministic and defined on all arguments; for a relation we have to prove these properties explicitly if we need them.
    With functions we can also take advantage of Coq's computation mechanism to simplify expressions during proofs.
...
Ultimately, the choice often comes down to either the specifics of a particular situation or simply a question of taste. Indeed, in large Coq developments it is common to see a definition given in both functional and relational styles, plus a lemma stating that the two coincide, allowing further proofs to switch from one point of view to the other at will.

The chapter on inductive predicates in the hitchhikers guide is Lean specific and gives a more condensed overview of the idea. There's also a section in SF where they discuss a version of reflection that lets sort of go back and forth between the two as needed, like ∀ (a b : nat), inductiveLE a b <-> (boolLe a b = tt).

[Brandon Brown]

Thanks! Is there any reason why the mathlib version is not defined like this:

inductive lte2 : ℕ → ℕ → Prop
| refl (a : ℕ) : lte2 a a
| step (a b : ℕ) : lte2 a b → lte2 a (nat.succ b)

example : lte2 1 4 :=
begin
  apply lte2.step,
  apply lte2.step,
  apply lte2.step,
  apply lte2.refl,
end

[Eric Wieser]

Because a is always passed unchanged as the first argument, so there's no point including it in the equation matching

[Chris B]

You mean with both nats on the right of the colon? There may be some mathlib specific purpose, but I think the idea of separating params and indices with the colon such that users would only have to retype the indices was a convenience experiment in Lean 3 that doesn't seem to have been ported to Lean 4, possibly because people found it more confusing than helpful.

[Chris B]

This doesn't work in 4:

inductive MyLe (a : Nat) : Nat -> Prop
| Refl : MyLe a

But this does:

inductive MyLe (a : Nat) : Nat -> Prop
| Refl : MyLe a a

And it will yell at you if you give it something other than a in the first arg position.

[Chris B]

@Eric Wieser Do you know if there's an optional way to fix arguments in lean 4?

[Kevin Buzzard]

@Branden Brown the two definitions satisfy the same theorems so as far as I'm concerned as a mathematician, the definitions are the same. Things that come for free with one definition need to be proved with the other one, but this is not hard. In the natural number game I use a third definition because my experience with mathematicians was that they found it the easiest to develop an API for, but mathematicians are not used to doing induction on things that aren't naturals

[Kevin Buzzard]

The NNG definition is $x\le y\iff\exists z, y=x+z.$