Regression in equation compiler

Stream: lean4

[Bhavik Mehta]

Is this a known regression?

def f : Nat → Nat → Nat := sorry
def g : Nat → Nat → Nat := sorry

theorem ind (i j : Nat)
    (h₁ : f (i + 1) (j + 2) ≤ g (i + 1 + (j + 2) - 2) (i + 1 - 1))
    (h₂ : f (i + 2) (j + 1) ≤ g (i + 2 + (j + 1) - 2) (i + 2 - 1)) :
    f (i + 2) (j + 2) ≤ g (i + 2 + (j + 2) - 2) (i + 2 - 1) :=
  sorry

theorem test : ∀ i j : Nat, f i j ≤ g (i + j - 2) (i - 1)
  | 0, _ => sorry
  | _, 0 => sorry
  | 1, j + 1 => sorry
  | i + 1, 1 => sorry -- all these are non-recursive
  | i + 2, j + 2 => ind _ _ (test (i + 1) (j + 2)) (test (i + 2) (j + 1))

The calls to test are clearly on smaller cases, and in Lean 3 the equation compiler is happy with it, but in Lean 4 this fails.

[Bhavik Mehta]

(I'm aware that I can tell it to use some lex ordering to make it work, but I'm specifically wondering why the default behaviour is weaker)

[Alex J. Best]

termination_by test i j => i + j

is enough to convince lean, no lex required!

[Bhavik Mehta]

True, but even less is needed to convince Lean 3 :) I had termination_by test i j => (i, j) in mind instead

[Kyle Miller]

Here's a simpler example:

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

Error:

fail to show termination for
  test
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    test (i + 2) (j + 1)

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    test (i + 1) (j + 2)

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

[Kyle Miller]

Adding either termination_by _ i j => (i, j) or termination_by _ i j => i + j makes it go through.

[Kyle Miller]

Even simpler:

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

The same termination_by lines make it go through.

[Bhavik Mehta]

Wow, much shorter, thank you! Is this an intentional regression in the way things by structural recursion are compiled? Is there any reason behind it?

[Joachim Breitner]

This is becoming my turf a bit, although I’m not the expert yet hat you deserve.
Is this a regression relative to lean3 or some prior version of lean4?
How much of a pain is it for you?
“guessing lexicographic order” is something that we certainly want Lean to do. At some point. So it’s a matter of weighing this against other things that need doing :-)

[Bhavik Mehta]

It's a regression relative to lean 3 - the direct back-port to Lean 3 works fine:

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

[Bhavik Mehta]

In case it's relevant, I think the key difference is that the well-founded relation that's inferred on Σ' (i : ℕ), ℕ in Lean 3 is Lex, but in Lean 4 is induced by PSigma.fst Edit: That's not what Lean 4 is doing here

[Bhavik Mehta]

Joachim Breitner said:

How much of a pain is it for you?

It's not a huge pain, as Alex and I mentioned above a work-around isn't too bad. But I somewhat expected this to be a known issue already... I found a porting note with the same problem (actually basically the same as Kyle's: docs#Nat.multichoose), so I'm certainly not the only one to hit this

[Joachim Breitner]

Noted at https://github.com/leanprover/lean4/issues/2837, so we at least have a reference point to collect examples, real-world use cases, and generally cross-reference discussions. No promise of swift implementation implied.

[Bhavik Mehta]

I added some more examples there, it looks like this was spotted in a few porting notes already, but not collected, so I took the liberty of listing the obvious ones.

[Bhavik Mehta]

One example to highlight however is in docs#List.merge, where I would expect structural recursion to work for the definition (and it seems to in Lean 3), but the ported version takes the length of both lists and adds them.

[Scott Morrison]

The default decreasing_by tactic is relatively good at arithmetic, but doesn't attempt to backtrack and use assumptions, so tends to be terrible at lexicographic orders. Hence the changes Bhavik is observing from (i,j) to i + j.

I've found that

decreasing_by
  solve_by_elim (config := { maxDepth := 10 }) [Prod.Lex.left, Prod.Lex.right'']

is often the key, with

theorem _root_.Prod.Lex.right'' [LT α] {a₁ a₂ : α} {b₁ b₂ : β} (ha : a₁ = a₂) (hb : s b₁ b₂) :
    Prod.Lex (· < ·) s (a₁, b₁) (a₂, b₂) :=
  ha ▸ Prod.Lex.right a₁ hb

[Scott Morrison]

(This solve_by_elim assumes that you've have'd everything where needed. It needs to be souped up with a discharger that knows some arithmetic.)

[Bhavik Mehta]

Scott Morrison said:

Hence the changes Bhavik is observing from (i,j) to i + j.

Could you clarify this a little? It looks to me like (i,j) and i + j both fix the problem, and the problem is that neither is used by default. Whereas in Lean 3, (i,j) with lex is the default

[Scott Morrison]

Ah, you are right. Even to get lex ordering you need a termination_by clause.

[Scott Morrison]

(My comment was about the further need for a backtracking decreasing_by tactic even once you've got lex ordering.)

[Bhavik Mehta]

I see! So you're saying that even if it did get the right ordering, that wouldn't automatically fix all the porting notes since a decreasing_by would also need to be added? Or is it that the porting notes (and this example) would be fine, but more complicated examples would probably need a cleverer method to close the goals.