New Lean blog post: Functional Induction

Stream: general

[David Thrane Christiansen]

My colleague @Joachim Breitner has just posted a blog post on the functional induction feature that's going to be part of the Lean 4.8 release. This makes it much easier to prove things about functions defined by well-founded recursion, as well as mutually-recursive definitions.

[Johan Commelin]

@Joachim Breitner Nice blog post! Thanks a lot!

Instead, we have to instantiate this parameter in the expression passed to with

Should that be using, instead of with?

[Joachim Breitner]

Well spotted, fixed.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I think in ".. so let us spell it out in prose:", the last two bullets need rewording: right now it reads "then two arbitrary lists (the targets xs and xy, which correspond to the varying parameters of the function) for which the property holds."

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

As far as the induction, one thing that briefly gave me pause was that the induction principle does not actually depend on what the function does; it is purely about its recursive shape. For example, if we write

def altRev {α : Type} : (xs ys : List α) → List α
  | [], ys => ys
  | x::xs, ys => altRev ys xs ++ [x]
termination_by xs ys => xs.length + ys.length

then altRev.induct ≡ alternate.induct (by proof-irrelevance), even though altRev reverses the lists. Maybe this is interesting to mention.

[Joachim Breitner]

Good observation! I have defined functions purely to get their induction principle, or used the induction principle from one function in a proof for something else.-