Error: unexpected bound variable #0

[BrunoDutertre]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following fragment causes an error related to decreasing_by omega.

The error message is

unexpected bound variable #0

def simple_foldl (f: β → α → β) (a: Array α) (i: Nat) (b: β): β :=
  if h: i < a.size then
    simple_foldl f a (i+1) (f b a[i])
  else
    b

theorem simple_fold_monotonic₁ (a: Array α) (f: β → α → β) (i: Nat) {P: α → β → Prop} {x: α}
  (base: P x b)
  (mono: ∀ x x' y, P x y → P x (f y x')): P x (simple_foldl f a i b) := by
    unfold simple_foldl
    split <;> try trivial
    apply simple_fold_monotonic₁
    . apply mono; exact base
    . exact mono
  termination_by a.size - i
  decreasing_by omega

Context

Discussed at the Lean office hour on Sept 11, 2024.

Steps to Reproduce

Run lean on the fragment.

Versions

4.11.0

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Thanks for minimizing the example so well.

The goal is a huge mess (likely at least partly due to #5038), but it shouldn’t make omega get confused.

One can get the goal into a somewhat smaller state with a bunch of clear commands:

def simple_foldl (f: β → α → β) (a: Array α) (i: Nat) (b: β): β :=
  if h: i < a.size then
    simple_foldl f a (i+1) (f b a[i])
  else
    b

theorem simple_fold_monotonic₁ (a: Array α) (f: β → α → β) (i: Nat) {P: α → β → Prop} {x: α}
  (base: P x b)
  (mono: ∀ x x' y, P x y → P x (f y x')): P x (simple_foldl f a i b) := by
    unfold simple_foldl
    split <;> try trivial
    apply simple_fold_monotonic₁
    . apply mono; exact base
    . exact mono
  termination_by a.size - i
  decreasing_by 
    exfalso
    rename_i a b
    clear a b mono base    
    rename_i a; clear a    
    clear base
    clear x
    rename_i a; clear a
    clear x
    clear P
    rename_i a; clear a
    clear P
    clear i
    rename_i a; clear a    
    clear i
    clear f
    rename_i a; clear a
    clear f
    clear a
    rename_i a; clear a
    clear a
    clear b
    omega -- unexpected bound variable #0
    rename_i a; clear a
    omega -- omega could not prove the goal:

Did not look closer at this point.