simp on defs (lean4#2042)

Stream: mathlib4

[Eric Wieser]

In lean3, simp on def foo (a : Nat) : Nat := 2 * a meant "add the simp lemma foo a = 2 * a". In lean 4, it means "add the simp lemma foo = fun a => 2 * a" (lean4#2042).

Can we teach mathport to not add these simp attributes, and instead insert a TODO comment for the porter asking them to write manual equation lemmas? This is particularly notable when the function is implemented with a match, which causes it to unfold to the match statement

[Eric Wieser]

Previous thread here; that was discussing fixing the behavior in Lean. In the meantime, it would be helpful for porting for the mathport output to not pollute the simp set with these bad lemmas

[Rémi Bottinelli]

That means that there is no way to get the equational lemmas automatically?

[Eric Wieser]

I think the equation lemma is now the useless foo = fun a => 2*a one

[Reid Barton]

We could define our own attribute that implements the mathlib 3 simp behavior, right? In the case without equations it's basically a trivial version of simps

[Eric Wieser]

I think it would be beneficial to have mathport output that attribute even if doesn't exist yet

[Eric Wieser]

Because then it flags something that has to be done manually while porting

[Anne Baanen]

Eric Wieser said:

I think the equation lemma is now the useless foo = fun a => 2*a one

Could you explain what makes this form useless? Wouldn't simp after rewriting foo x reduce (fun a => 2 * a) x into 2 * x?

[Eric Wieser]

It's useless in that it's not the lemma you want, and certainly not the one we had in lean 3

[Kyle Miller]

Apparently rewriting works both ways for this foo, and it doesn't even create intermediate funs:

def foo (a : Nat) : Nat := 2 * a

example (a : Nat) : 1 + 2 * a = foo a + 1 := by
  rw [foo, Nat.add_comm]

example (a : Nat) : 1 + 2 * a = foo a + 1 := by
  rw [← foo, Nat.add_comm]

(The add_com is just to keep rw from closing the goal by refl)

[Eric Wieser]

In the absence of a fix for this, and the increasing urgency of port-status#data/matrix/basic, I've created:

• #18696, which removes all of the matrix code that relies on this feature. This will likely have lots of small annoying downstream failures to fix, but it's easier to fix these in Lean 3 than while porting.
• !4#3024, which lets override the useless equation lemmas manually using an attribute

[Eric Wieser]

#18696 is now green