Zulip Chat Archive

Stream: general

Topic: Well-founded recursion / quick sort

Gihan Marasingha (Jun 28 2021 at 14:32):

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 (Jun 28 2021 at 14:44):

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

Horatiu Cheval (Jun 28 2021 at 15:01):

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

Yakov Pechersky (Jun 28 2021 at 15:11):

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

Horatiu Cheval (Jun 28 2021 at 15:13):

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 (Jun 28 2021 at 15:53):

@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 (Jun 28 2021 at 15:57):

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 (Jun 28 2021 at 18:57):

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

Jeremy Avigad (Jun 28 2021 at 18:59):

@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 (Jun 28 2021 at 19:54):

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 (Jun 28 2021 at 20:06):

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

Last updated: Aug 03 2023 at 10:10 UTC