Zulip Chat Archive
Stream: general
Topic: Wellfounded recursion / quick sort
Gihan Marasingha (Jun 28 2021 at 14:32):
I've spent the past few days trying (hopefully successfully) to understand wellfounded recursion and have written an exlean blog post on it, with exercises. In the post, I:
 Discuss the (informal) notion of a wellfounded relation.

Show how to use wellfounded relations (initially just with the < relation on ℕ) to define recursive functions and prove theorems
 using the equation compiler and
 by writing proof terms.

Explain why
rfl
proofs don’t work for functions defined by wellfounded recursion.  Employ sneaky equation compiler tricks to simplify function writing.

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
.
 to work with custom relations via
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 wellfounded recursion (in Lean 2, I think?). I recently had to write two wellfounded 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):
Wellfounded 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: Dec 20 2023 at 11:08 UTC