'unexpected occurrence of recursive application' with omega

Stream: general

[Aaron Hill]

The following code (extracted from the equational_theories project) compiles with Lean 4.18.0, but fails with 4.19.0-rc2 and above:

@[irreducible] noncomputable def g_enumerate : Option Nat := sorry

noncomputable def f_data (n: Nat): Nat := by
  match hn: n with
  | 0 => exact 0
  | a + 1 =>
    have new_vals_not_supp: g_enumerate < Option.some (f_data a) := by
      have supp_max_lt: (g_enumerate).getD 0 < (f_data a) - 1 := sorry
      match h_supp_max: (g_enumerate) with
      | Option.some max_val =>
        rw [Option.some_lt_some]
        rw [h_supp_max, Option.getD_some] at supp_max_lt
        omega
      | None => sorry
    exact 1

produces:

fail to show termination for
  f_data
with errors
failed to infer structural recursion:
Cannot use parameter n:
  unexpected occurrence of recursive application
    f_data


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal

I've had difficulty minimizing it further than this, as omega seems to be required to trigger the error (changing supp_max_lt to (g_enumerate).getD 0 < (f_data a) and using assumption will allow the proof to compile).

[Kim Morrison]

Making it clearer that the problem involves omega (specifically, probably the fact that omega is abstracting a proof into a separate declartion), this works fine:

@[irreducible] noncomputable def g_enumerate : Option Nat := sorry

theorem foo (h : x < y - 1) : x < y := by omega

noncomputable def f_data (n: Nat): Nat := by
  match hn: n with
  | 0 => exact 0
  | a + 1 =>
    have new_vals_not_supp: g_enumerate < Option.some (f_data a) := by
      have supp_max_lt: (g_enumerate).getD 0 < (f_data a) - 1 := sorry
      match h_supp_max: (g_enumerate) with
      | Option.some max_val =>
        rw [Option.some_lt_some]
        rw [h_supp_max, Option.getD_some] at supp_max_lt
        exact foo supp_max_lt
      | None => sorry
    exact 1

[Kim Morrison]

Let's ping @Joachim Breitner, who is away this week, in case no one works out a fix in the meantime. :-)

[Aaron Hill]

It looks like it's being caused by omega's usage of mkAuxTheorem (https://github.com/leanprover/lean4/pull/5998) - I can reproduce the issue by using as_aux_lemma:

def f_data (n: Nat): True := by
  match hn: n with
  | 0 => trivial
  | a + 1 =>
    have my_proof: trivial = (f_data a) := by
      as_aux_lemma => trivial
    trivial

[Aaron Hill]

replacing as_aux_lemma => trivial by trivial makes it compile

[Joachim Breitner]

Uff, this will be hard to avoid. Aux theorems abstract over all free variables, and then the call is unsaturated.

A work around sometimes is to let- or have-bind the recursive call, so that the omega proof is properly abstract in it.

[Joachim Breitner]

Workaround:

@[irreducible] noncomputable def g_enumerate : Option Nat := sorry


noncomputable def f_data (n: Nat): Nat := by
  match hn: n with
  | 0 => exact 0
  | a + 1 =>
    have fa := f_data a
    have new_vals_not_supp: g_enumerate < Option.some fa := by
      have supp_max_lt: (g_enumerate).getD 0 < fa - 1 := sorry
      match h_supp_max: (g_enumerate) with
      | Option.some max_val =>
        rw [Option.some_lt_some]
        rw [h_supp_max, Option.getD_some] at supp_max_lt
        omega
      | None => sorry
    exact 1

[Aaron Hill]

Thanks!

[Aaron Hill]

Is there any way for omega to detect that the current goal references an "outer" function, and skip creating an aux theorem?

[Aaron Hill]

It took me a while to minimize the original error, as I wasn't expecting omega to have anything to do with proving termination

[Joachim Breitner]

A more proper solution that I have been wondering about is to abstract over all calls to free variables, but I didn't complete this thought yet (what if the arguments are large and complex and contain proofs?). So it's not clear to me what the really best way is here. Or maybe the proofs should be unfolded during derecursification.