Well-founded recursion: Lean could guess the lexicographic order

[nomeata]

This definition

def test : ∀ i j : Nat, Nat
  | 0, _ => 1
  | _, 0 => 1
  | i + 1, j + 1 => test i (j + 1) + test (i + 1) j

needs

termination_by _ i j => (i, j)

or

termination_by _ i j => i + j

to go through. It didn’t need that in Lean3 (and our friendly competitors don't need that annotation either, I believe).

It would be nice if Lean4 would be up to that.

Previous discussion:

• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20equation.20compiler/near/400582161 by Bhavik Mehta

[b-mehta]

The original version in the Zulip thread showed up in porting the Exponential Ramsey project, in which I hit this when trying to define the Ramsey numbers! It also appears in mathlib:

1. in Mathlib/Data/Nat/Choose/Basic: the definition of multichoose and the theorem multichoose_eq both gained a termination_by fix which weren't needed in Lean 3.
2. twice in Archive/Wiedijk100Theorems/BallotProblem
3. four times in Mathlib/Computability/Ackermann
4. once in Mathlib/Computability/PartrecCode
5. twice in Mathlib/Data/List/Infix
6. at least once in Mathlib/Data/List/Sort: it's hard to tell which ones in here are new. But the definition of merge is one where I would expect structural recursion to succeed.
7. once in Mathlib/Data/Nat/Hyperoperation
8. once in Mathlib/Data/Sym/Card
9. once in Mathlib/RingTheory/Multiplicity
10. four times in Mathlib/SetTheory/Game/Basic: mathlib3 gave the decreasing_by tactic, but the relation was seemingly inferred correctly
11. seemingly around 20 more times in Mathlib/SetTheory overall

[hargoniX]

We could look into implementing what Isabelle did here: https://www21.in.tum.de/~krauss/papers/lexicographic-orders.pdf

[b-mehta]

That would be nice, but a simpler approach might just be to restore the old behaviour: build a PSigma of the arguments in the order they're given, and do lex on that.

[nomeata]

Probably doing one and later the other is best.