simp [← mylemma]

Stream: mathlib4

[Yury G. Kudryashov]

In Lean 3, simp has a nice feature: if you have a simp lemma mylemma and you write simp [←mylemma], then simp removes mylemma from the simp set. Am I right that simp in Lean 4 doesn't have this feature?

[Gabriel Ebner]

It should have this feature, with exactly the same syntax.

[Yury G. Kudryashov]

I'll try to make an #mwe.

[Yury G. Kudryashov]

def WithTop α := Option α

namespace WithTop

def some (x : α) : WithTop α := Option.some x

instance : Coe α (WithTop α) := ⟨some⟩

instance [Add α] : Add (WithTop α) where
  add x y := x.bind fun x => y.map (x + ·)

@[simp] theorem coe_add [Add α] (x y : α) :
  some (x + y) = some x + some y := rfl

set_option maxHeartbeats 3000 in -- make it fail faster
set_option trace.Meta.Tactic.simp.rewrite true in
example [Add α] (h : ∀ x y z : α, x + y + z = x + (y + z)) (x y z : α) :
    (x + y + z : WithTop α) = x + (y + z) := by
  simp [← coe_add, h]

[Yury G. Kudryashov]

@Gabriel Ebner :up:

[Thomas Murrills]

Is the syntax - instead of ←?

[Yury G. Kudryashov]

Works: simp [-coe_add, (coe_add _ _).symm, h], doesn't work: simp [-coe_add, ← coe_add, h] and simp [← coe_add, h]

[Yury G. Kudryashov]

@Thomas Murrills The simp [← coe_add] syntax worked in Lean 3. And Gabriel says that it should work in Lean 4.

[Thomas Murrills]

Interesting...as someone who's only worked with lean 4 and not lean 3, all I can speak to is that I've seen - be used to remove theorems from simp sets, and ← be used to use the lemma backward.

No idea what's going on/should be going on otherwise...but also, even assuming only those usages, not sure why example 2 isn't working, then. Maybe it doesn't play nicely with - yet?

[Thomas Murrills]

Oh wait, looks like the following works:

simp [-coe_add, ← coe_add _ _, h]

Also works:

simp [-coe_add, ← coe_add _, h]

[Thomas Murrills]

Aside, but I'm not totally sure why it needs the _ tbh...I've noticed that sometimes theorems just need a _ or two when used like this, and I can't really anticipate when.

[Thomas Murrills]

Hang on a second. This is strange:

• works: simp [-coe_add, ← (coe_add), h]
• doesn't: simp [-coe_add, ← coe_add, h]

What's going on here?

[Thomas Murrills]

My at-a-glance guess is that idents are treated differently by resolveSimpIdTheorem? in elabSimpArgs, leading to an .ext result, but elabSimpArgs doesn't seem to take care of inv (the indicator for ← syntax) at all for .ext results.

Note that there's no problem if @[simp] is removed from coe_add: simp [← coe_add, h] works in that case (because it's no longer a simp extension/.ext result). But again, this is just a guess.

Actually I'm not sure this is the full story. The trace does show backwards rewriting; so maybe it's about how inv is handled in this case rather than it not being handled at all, or about erasure not working. I'll leave it to those who already understand simp.

[Thomas Murrills]

Hmm, what should be done in a case like this? I’m a little reluctant to open an issue on the lean4 repo given that the lean devs are already overwhelmed, but I’m pretty sure it is a simp bug…

[Floris van Doorn]

I've also noticed this: -foo erases something from a discrimination tree, and I don't think that re-inserting it removes the erasure, so it's still marked as erased. That's why ← (coe_add) and ← coe_add _ both work, because now you're adding a new expression to the discrimination tree, instead of saying that the erased term has to be reinserted (which it doesn't).
The same happens with

attribute [-instance] foo
attribute [instance] foo

The second attribute command doesn't undo the first one: foo is still (locally) marked as erased (this is mentioned in lean4#2115)

[Thomas Murrills]

Interestingly simp [-thm, thm] doesn't seem to suffer from that issue, and instead works as expected! Check out

axiom P : Type
axiom p : P
axiom q : P
axiom eq : p = q

@[simp] theorem ax : p = q := eq

example : p = q := by simp [-ax, ax] -- works

It's specifically a problem with ← used with - here. I don't think ← is taken into account properly when processing simp-extension idents.

[Thomas Murrills]

(Imo ← used on a simp extension should both erase it and insert the backwards version—that is, we should only need simp [← coe_add] instead of simp [-coe_add, ←coe_add], since no one is going to want to have both coe_add and its backwards version at once, I imagine. But that's technically a different issue.)

[Yury G. Kudryashov]

@Floris van Doorn simp [-coe_add, ← coe_add, h] enters an infinite cycle.

[Yury G. Kudryashov]

It uses both coe_add and (coe_add _ _).symm.

[Yury G. Kudryashov]

@Gabriel Ebner :up:

[Thomas Murrills]

(Btw, @Floris van Doorn, the typical reason the thing you’re talking about happens (afaik) is that foo is not actually erased from the discrimination tree per se—rather, it’s added to a list of erased things which are only ignored after being matched! The problem is then that the given attribute’s add functionality doesn’t also make sure to erase the added thing from erased (if that makes sense). This is all to say that problems like that should be a simple fix. It might be different for instances though, idk. In any case, this problem is a bit different)

[Floris van Doorn]

@Thomas Murrills I came to roughly the same conclusion indeed.
Although maybe for simp something different happens if simp [-coe_add, ← coe_add, h] is an infinite cycle..