A `termination_by` puzzle

Stream: lean4

[François G. Dorais]

Why doesn't fooSS work? Obviously it's because of termination_by but I don't understand exactly why. How does termination_by change the inductive definition?

def foo : Nat → Nat → Nat
| 0, 0 => 0
| 0, n+1 => foo 0 n
| m+1, n => foo m n
termination_by foo m n => m + n

theorem foo00 : foo 0 0 = 0 := rfl -- works

theorem foo0S : foo 0 (n+1) = foo 0 n := rfl -- works

theorem fooS0 : foo (m+1) 0 = foo m 0 := rfl -- works

theorem fooSS : foo (m+1) (n+1) = foo m (n+1) := rfl -- fails!?

[François G. Dorais]

PS: To avoid confusion, foo is identically zero, so fooSS is definitely true.

[Mario Carneiro]

by rw [foo] works

[Mario Carneiro]

the answer to your question is that when you use termination_by it uses well-founded recursion instead of structural recursion to define the function, and WF definitions generally don't have many definitional equalities, you have to use the defining equations directly

[François G. Dorais]

Thanks Mario. I've figured out that I can access what I wanted to know using the option trace.Elab.definition.wf (the wf is what I couldn't figure out before Mario's hint).

[František Silváši 🦉]

[deleted]