simp lemma discrimination tree keys are computed with iota := false, while simp uses iota := true #6331
Description
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
When computing the discrimination tree keys for a (global) simp lemma, the configuration is set to iota := false. However, the default configuration for simp uses iota := true. Since #6053, the setting iota := false propagates to the function Lean.Meta.unfoldDefinition?, which now causes bad discrimination tree keys to be computed when the LHS of a simp lemma contains a match expression.
Context
This was reported on Zulip.
Steps to Reproduce
Consider this minimal example:
abbrev Multiseries : List Nat → Type
| [] => Nat
| _ :: _ => Int
opaque maxExp (n : Nat) (ns : List Nat) (li : List (Multiseries (n :: ns))) : Nat
@[simp]
axiom bad_simp_lemma (n : Nat) (ns : List Nat) : maxExp n ns [] = 8
theorem same_lemma (n : Nat) (ns : List Nat) : maxExp n ns [] = 8 := by
simp -- simp made no progress
theorem same_lemma' (n : Nat) (ns : List Nat) : maxExp n ns [] = 8 := by
simp -iota -- succeeds
Expected behavior:
simp should succeed, while simp -iota should not succeed.
Actual behavior:
simp fails, and simp -iota succeeds.
Versions
4.16.0-nightly-2024-12-06
Additional Information
We can manually force the lemma to have the match expression already unfolded. This gives the correct discrimination tree keys for simp:
abbrev Multiseries : List Nat → Type
| [] => Nat
| _ :: _ => Int
opaque maxExp (n : Nat) (ns : List Nat) (li : List (Multiseries (n :: ns))) : Nat
@[simp]
axiom good_simp_lemma (n : Nat) (ns : List Nat) : maxExp n ns ([] : List Int) = 8
theorem same_lemma (n : Nat) (ns : List Nat) : maxExp n ns [] = 8 := by
simp -- succeeds
theorem same_lemma' (n : Nat) (ns : List Nat) : maxExp n ns [] = 8 := by
simp -iota -- simp made no progress
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.