simp not unifying partial application of structure projection #1937
Description
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.
Description
In the mathlib4 port, certain simp lemmas that would apply in Lean 3 no longer apply in Lean 4 in the same case. It looks like this happens whenever we have a structure containing a field with a function, and a simp lemma is defined on the partially applied function in that field. simp has no trouble with partial application if it's on other definitions.
Steps to Reproduce
The following code contains two failing simp calls where rw succeeds. Equivalent code works fine in Lean 3.
structure BundledFunction (α β : Sort _) :=
(toFun : α → β)
namespace BundledFunction
-- `simp` doesn't seem to unify partial applications of structure projections:
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20failing.20on.20partial.20application.20of.20projections
def id (α) : BundledFunction α α := ⟨λ a => a⟩
@[simp] theorem coe_id : (id α).toFun = _root_.id := rfl
example (x : α) : (id α).toFun x = x :=
by simp only [coe_id, id_eq] -- does not simplify anything
example (x : α) : (id α).toFun x = x :=
by rw [coe_id, id_eq] -- succeeds
-- seems to be another instance of the same behaviour:
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20calls.20broken.20in.20mathlib4.23922/near/314790371
def otherProjection (f : BundledFunction α β) : α → β := f.toFun
@[simp] theorem toFun_eq_otherProjection : @toFun α β = otherProjection := rfl
@[simp] theorem id_apply : (id α).otherProjection x = x := rfl
example : (id α).toFun x = x := by simp only [toFun_eq_otherProjection, id_apply] -- does not simplify anything
example : (id α).toFun x = x := by rw [toFun_eq_otherProjection, id_apply] -- succeeds
end BundledFunction
-- `simp` is happy with partial applications in other functions:
def id2 (x : α) := x
@[simp] theorem id2_eq_id : @id2 α = id := rfl
example : id2 x = x := by simp only [id2_eq_id, id_eq] -- works fine
example : id2 x = x := by rw [id2_eq_id, id_eq] -- succeedsExpected behavior: the simp calls on both lines marked -- does not simplify anything should solve the goal
Actual behavior: simp fails to rewrite. With trace.Meta.Tactic.simp on, the first simp call gives the following trace:
[Meta.Tactic.simp.unify] @BundledFunction.coe_id:1000, failed to unify
(BundledFunction.id ?α).toFun
with
BundledFunction.toFun (BundledFunction.id α) xReproduces how often: always
Versions
You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.
$ lean --version
Lean (version 4.0.0-nightly-2022-12-09, commit 57a6aefb9240, Release)
$ uname -a
Linux vouwvervorming 6.0.10-arch2-1 #1 SMP PREEMPT_DYNAMIC Sat, 26 Nov 2022 16:51:18 +0000 x86_64 GNU/Linux