examining well-founded def

Stream: lean4

[Chris B]

Is there any way to either generate code using WellFounded.fix or reasonably unfold a function defined using termination_by? I have a pretty simple function that decreases based on nat subtraction; if I define it using termination_by, it unfolds into a big irreducible machine-generated term.
I'm fine with using fix and defining lemmas along the lines of div_eq, but WellFounded.fix in user code still throws an error about not generating anything executable.

[Mario Carneiro]

The way to generate code using WellFounded.fix is to have two versions of the function and connect them using implementedBy; there are a couple of examples here that were replaced by termination_by in mathlib4#136

[Mario Carneiro]

It is also possible to unfold the autogenerated fix equation. The simplest way to do it at the moment is to use simp [my_func, my_func._unary]; rw [WellFounded.fix_eq]; rfl with an appropriately stated equality lemma

[Chris B]

Thank you; it took a little bit of effort, but I think I got where I needed to be.

[Chris B]

Is there a way to use the termination_by and decreasing_by gadgets for theorems?

[Mario Carneiro]

Yes, it works exactly the same way

[Chris B]

I was using lemma instead of theorem; I think the parser for lemma needs to be extended with additional patterns for termination and decreasing. They don't seem to be part of val:declVal.

[Chris B]

There's a terminationSuffix parser in Parser/Commands.lean, but it doesn't seem to be accessible.