A systematic approach to "Well-founded recursion done right"
summary
Systematic pattern for well-founded recursion: add an auxiliary accessibility argument so Coq/Rocq accepts definitions as structural, generate the two small proof obligations for recursive calls, discharge them with a reusable inversion lemma put into a hint DB, and derive well-foundedness via WF_inverse_image on list length. Demonstrated on quicksort and tree algorithms, uses program/refine for obligations, yields clean extraction (prop argument erases) and straightforward proofs by well-founded induction; the approach is practical and reproducible.
AI-written summary · about
chapters (7)
- 0:00Well-founded recursion intro
- 1:27Defining recursive functions
- 3:39Accessibility proofs
- 5:50Proving well-foundedness
- 7:15Proving properties with well-founded induction
- 9:01Advantages and patterns
- 10:49Q&A
related talks
21mWell-founded recursion done right
56mAn introduction to recursion schemes
21mIntrinsically Correct Algorithms and Recursive Coalgebras
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
25mRecursive Program Synthesis using Paramorphisms
16mA Hoare-Logic Style Refinement Types Formalisation
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...