lean is clever

Stream: lean4

[Kenny Lau]

I just had a "wow lean is clever" moment when it typechecked my binary search algorithm without me having to specify anything

[Kenny Lau]

it automatically figured out to use (hi, hi - lo) as the proof of termination

[Aaron Liu]

it just has a list of common termination measures that it tries

[Asei Inoue]

@Kenny Lau could you show us a code example?

[Kenny Lau]

@Asei Inoue

def binaryRecursion (lo hi : Nat) : Nat :=
  if hi ≤ lo then 0
  else if lo + 1 = hi then 1
  else
    have mi := (lo + hi) / 2
    binaryRecursion lo mi + binaryRecursion mi hi

[Asei Inoue]

Thank you

[François G. Dorais]

Or avoid reinventing the wheel: Batteries.Data.Nat.Bisect

[Kenny Lau]

@François G. Dorais thanks for the pointer,

1. for some reason the docgen doesn't work
2. that's locating something using binary search, in particular it has to return the index, it cannot do a binary recursion like the one I've posted above

[Joachim Breitner]

Kenny Lau schrieb:

it automatically figured out to use (hi, hi - lo) as the proof of termination

See https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#inferring-well-founded-recursion for more details on how Lean managed to be clever

[Kenny Lau]

Thanks!