Induction principles from recursion: Beta testers wanted

Stream: general

[Joachim Breitner]

As part of the lean fro roadmap, I am working on a feature that can greatly simplify proving things about recursive functions.

If your function is structurally recursive, then normal induction on the decreasing parameter works fine. But if the function isn’t, things often get hairy: You often have to replicate the function’s case using splits, navigating to the recursive calls, and to get your induction hypothesis for the recursive calls you often have to recreate the full termination argument and proof (e.g. using termination_by) in every theorem.

With this feature you will get a an induction principle that exactly captures the structure of your recursive function, with one subgoal per branch of the function, and the induction hypthesis provided exactly for the arguments to the recursive calls. For example, given

def ackermann : Nat → Nat → Nat
  | 0, m => m + 1
  | n+1, 0 => ackermann n 1
  | n+1, m+1 => ackermann n (ackermann (n + 1) m)

you’ll get

ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
  (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
  (x x : Nat) : motive x x

This also works for mutual and nested recursion, for example for

inductive Tree | node : List Tree → Tree
def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ => t.rev) |>.reverse)

you’ll get

Tree.rev.induct (motive : Tree → Prop)
  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (x : Tree) : motive x

Here is an example proof using one of these induction principles (not the best example, because induction n would work here as well, but still):

theorem ackermann_pos (n m : Nat) : 0 < ackermann n m := by
  induction n, m using ackermann.induct
  all_goals simp only [ackermann] at * -- reduce function application
  case case1 m => exact Nat.zero_lt_succ m
  case case2 n IH => exact IH
  case case3 n m _IH1 IH2 => exact IH2

A larger, realistic example, including mutual recursion and a notable reduction in size and proof complexity, can be found on the Cedar repo.

Eventually, this should work out of the box (as it already does in Isabelle and others), but before I move my prototype (currently at https://github.com/nomeata/lean-wf-induct) into lean I’d like to collect more user feedback and get more testing. So if you are using well-founded recursion in your Lean work and are eager to get your hands early on this tool (or just want to help), that would be greatly appreciated.

To use this, add

require wfinduct from git
  "https://github.com/nomeata/lean-wf-induct"

to your lakefile.lean, use the command

#derive_induction foo

after you defined your function foo, and then you can use induction x, y, z using foo.induct.

Also let me know if you have trouble getting wfinduct to work with your particular version of lean.

[Kim Morrison]

@Joachim Breitner if there is interest from Mathlib users it seems reasonable we could add this as a dependency there. This project has a pretty short half-life before it is absorbs into Lean, so it's not a long-term commitment.

[Eric Wieser]

Is it a easy generalization to produce a version where motive .. : Sort u instead of Prop? Or is that an ill-defined request?

[Joachim Breitner]

Not sure about easy, and I don’t know it would reduce usefully, also and not sure how hard it will be to provide equational lemmas. But besides that it’s very likely doable. Do you have a concrete application in mind?

[Eric Wieser]

A contrived case would be a function with a return type of Fin (ackermann m n) that I want to compute via the same recursion pattern, but I indeed don't have a concrete application right now

[Eric Wieser]

Perhaps a better justification is that if such a Sort-valued function existed, it could perhaps be used in the compilation of ackermann itself.