aesop's destructProducts can add deps on implicit variables

Stream: metaprogramming / tactics

[Geoffrey Irving]

Here's (arguably) a bug which may be difficult to fix:

import Aesop
import Mathlib.Data.Nat.Basic

variable {bad : ℕ × ℕ}

set_option trace.aesop true in  -- Shows that `destructProducts` is the culprit
lemma unused {n : ℕ} {p q : ℕ → Prop} (pq : ∀ n, p n → q n) (pn : p n) : q n := by
  aesop (config := { enableSimp := false })  -- Ban `simp` so `destructProducts` has time to fire

#check unused  -- unused {bad : ℕ × ℕ} {n : ℕ} {p q : ℕ → Prop} (pq : ∀ (n : ℕ), p n → q n) (pn : p n) : q n

I'm using aesop to close a lemma unused that makes no mention of bad, and bad doesn't occur in the final proof. However, during aesop's search, it uses destructProducts to take bad apart into components, and :boom:, now the first argument of unused is {bad : ℕ × ℕ}.

[Kevin Buzzard]

yeah, in Lean 3 we used to avoid parameters, but in Lean 4 there is an argument for avoiding variables :-(

[Geoffrey Irving]

Turns out I use that implicit variable in exactly one lemma in the original file. :embarrassed:

[Geoffrey Irving]

I probably don't need it.

[Geoffrey Irving]

But I'll file this as an aesop issue in any case.

[Geoffrey Irving]

https://github.com/leanprover-community/aesop/issues/104

[Eric Wieser]

lean4#2452 is the tracking issue for variable issues

[Jannis Limperg]

I'm afraid I can't do anything about this atm. When Aesop runs, it has no way to distinguish variables from other hyps in the context afaik.

[Geoffrey Irving]

No worries, fine to ignore and then changes to general implicit variable handling will eventually fix it.