simpa excluding itself

Stream: lean4

[Alex Meiburg]

A minor wish of mine for simpa:

Sometimes I know that, after simplification, the resulting goal will be equivalent to a theorem foo. I could type simp; exact foo. But I prefer to type simpa using foo.

But then, sometimes it happens that foo is a @[simp] theorem itself. So then actually what happens if I type simpa using foo is that after simplification, the conclusion is just True, and it fails. So I have to do simpa [-foo] using foo, which feels a little silly.

How hard would it be to have simpa check if the closing argument is a term whose head is a simp theorem and, if it is, exclude it from the simp set by default? Or, maybe even more usefully, just exclude it from the simp set when simplifying the RHS (but not the current goal)?

[Yaël Dillies]

This is basically #lean4 > lean#4290 Closed simp tries using the forward version of use (I had your complaint in mind when I wrote it, but thought I would raise the more obviously egregious behavior first)

[Alex Meiburg]

For a little illustrative example, I have a goal something like

<stuff>
g : MyStruct
⊢ g.nodes ⟨↑(Fin.last (f.depth + g.depth)) - f.depth, ⋯⟩ = c

I have a simp theorem reading

MyStruct.nodes_last :
  ∀ {α : Type u} {inp out : Type v} (self : MyStruct α inp out), self.nodes (Fin.last self.depth) = out

so now if I call simp, I get the goal

g.nodes ⟨g.depth, ⋯⟩ = c

which is defeq to the fact g.nodes_last, which has type g.nodes (Fin.last g.depth) = out. But simp doesn't apply g.nodes_last because it doesn't recognize that the Fin.last g.depth is the same as ⟨g.depth, ⋯⟩.

If I run simpa using g.nodes_last, then I get

type mismatch, term
  g.nodes_last
after simplification has type
  True : Prop
but is expected to have type
  g.nodes ⟨g.depth, ⋯⟩ = c : Prop

so I have to use

simpa [-MyStruct.nodes_last] using g.nodes_last

instead.

[Alex Meiburg]

Yaël Dillies said:

This is basically #lean4 > lean#4290 Closed simp tries using the forward version of use

Oh, taking a look now, thanks

[Alex Meiburg]

Mm, that seems like a similar principle, but I think the mechanics of the simp there are pretty separate (this seems like a simpa-specific behavior)

[Junyan Xu]

So I have to do simpa [-foo] using foo, which feels a little silly.

This is nice trick; it makes the following work:

import Mathlib.Data.Real.Basic
def id' := @id
example : id' (0 + 0 : ℝ) = 0 := by simpa [-eq_self] using rfl
-- avoids non-terminal simp as in
example : id' (0 + 0 : ℝ) = 0 := by simp; rfl
-- even though such non-terminal simp is practically allowed.
-- In Lean 3 `simpa` simply worked.