Timeline for Defining a terminating `ripple`, with arguments swapping places
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 2, 2023 at 17:05 | comment | added | David Thrane Christiansen |
I'm short on time, and will be for the next month or so, but here's a sketch. The type class WellFoundedRelation is used to find a default well-founded relation for the type to the right of the => in the termination_by clause. The tactic decreasing_tactic is used to actually show that the relation holds for the recursive call in question, unless this tactic is overridden by a separate decreasing_by clause. Lean tactics are extensible with extra fallback cases. You can read more at leanprover.github.io/theorem_proving_in_lean4/…
|
|
| Sep 1, 2023 at 15:53 | comment | added | James Wood |
Interesting! Can we make sense of the generated code? I imagine that it has to find a well founded relation > on natural numbers, together with its well-foundedness proof, and then do some algebra to show that (1 + m) + n > n + m, but I can't see much evidence of the last step. And, not knowing the library definitions, I don't know which relation it is finding.
|
|
| S Sep 1, 2023 at 15:43 | review | First answers | |||
| Sep 1, 2023 at 18:47 | |||||
| S Sep 1, 2023 at 15:43 | history | answered | David Thrane Christiansen | CC BY-SA 4.0 |