[CoqPL'24] Mastering Well-Founded Recursion for Reliable Formal Proofs 🔍

[CoqPL'24] Well-founded recursion done right Xavier Leroy Several Coq libraries and extensions support the definition of non-structural recursive functions using well-founded orderings for termination. After pointing out some drawbacks of these existing approaches, we advocate going back to the basics and defining recursive functions by explicit structural induction on a proof of accessibility of the principal recursive argument.