Well-founded recursion / quick sort

Stream: general

[Gihan Marasingha]

I've spent the past few days trying (hopefully successfully) to understand well-founded recursion and have written an exlean blog post on it, with exercises. In the post, I:

1. Discuss the (informal) notion of a well-founded relation.

2. Show how to use well-founded relations (initially just with the < relation on ℕ) to define recursive functions and prove theorems

   • using the equation compiler and
   • by writing proof terms.

3. Explain why rfl proofs don’t work for functions defined by well-founded recursion.

4. Employ sneaky equation compiler tricks to simplify function writing.

5. Explain how to use the using_well_founded command

   • to work with custom relations via rel_tac and
   • to create decreasing proofs via dec_tac.

While writing the post, I wrote a proof (not in the post) that quicksort sorts a list (ableit with different definitions of qsort and sorted to those in mathlib). If it's worth having these in mathlib (I note @Jeremy Avigad did similar proofs for merge_sort and insertion_sort), let me know!

[Huỳnh Trần Khanh]

thanks for the article! this is something I struggled to understand for a long time! many thanks 🥰🥰😊

[Horatiu Cheval]

That's a great material! I always wished for something like this

[Yakov Pechersky]

I wonder if you'd also like to provide a version of lg using docs#nat.binary_rec

[Horatiu Cheval]

Does anyone know how well founded recursion will be done in lean4? Sure, the fundamentals will most likely be the same, but will the dec_tac, rel_tac structure be preserved?

[Gihan Marasingha]

@Yakov Pechersky oh neat, I hadn't seen that before. Something like

def lg_bin : ℕ → ℕ := nat.binary_rec 0 (λ b x y, 1 + y)

?

[Yakov Pechersky]

Yes, and there are helper lemmas docs#nat.binary_rec_zero, docs#nat.binary_rec_eq. An example of using it can be found in src#nat.bin_cast_eq

[Brandon Brown]

Glad to know there's another blog about learning Lean besides the Xena blog

[Jeremy Avigad]

@Gihan Marasingha , the exposition is really great. I wrote merge_sort and insertion_sort a long time ago, before the equation compiler could handle well-founded recursion (in Lean 2, I think?). I recently had to write two well-founded recursions by hand in Lean 4. It's a little scary at first but not so bad in the end, and even when we can get Lean to fill in the details automatically, it is nice to understand what is going on under the hood.

[Gihan Marasingha]

Thanks. I haven't even tried wf recursion in Lean 4. Does the Lean 4 equation compiler handle wf recursion? That isn't clear from the manual.

[Brandon Brown]

Well-founded recursion isn't implemented in Lean4 yet, and it says so in the error message anytime a function is unable to be verified as structurally terminating by the termination checker