simpa [foo] using bar

Stream: mathlib4

[Julian Berman]

I occasionally wish that when navigating over the using from simpa [foo] using bar that Lean would show the goal state after the simp but before attempting to finish off applying bar. Is this sensical to want, and if so how feasible does implementing it sound?

[Aaron Liu]

this does not sound too hard to implement

[Jireh Loreaux]

That doesn't quite make sense, because the simp can act on both the goal and on bar.

[Julian Berman]

I guess stepping back one step then, it'd be nice to somewhere see all three things (what happened to the goal, what happened to bar, and how close the two were to each other). Right now converting a multiline have + simp into simpa using is shorter but loses the ability to see what happens in between.

[Aaron Liu]

hold on, which state do you want to show here?

[Eric Wieser]

There's a point where it simplifies both to the same state, right?

[Eric Wieser]

Or is the algorithm not "apply simp lemmas to the goal and the using term until exact solves the former with the latter"?

[Robin Arnez]

The algorithm is roughly

focus
simp (disch := disch) +options only? [thms...]
first
| done; dbg_trace "try 'simp' instead of 'simpa'"
| apply have h := term; ?_
  rotate_right
  simp (disch := disch) +options only? [thms...] at h
  first
  | done; dbg_trace "try 'simp at h' instead of 'simpa'"
  | exact h; done

i.e.

1. simplify the main goal using all of the specified options. If this closes the goal and linter.unnecessarySimpa is enabled, print a warning
2. elaborate the provided term with no expected type but postponing allowed
3. create a new goal with the same type and tag
4. introduce h as a new local declaration
5. simplify h using all of the specified options. If this closed the goal and linter.unnecessarySimpa is enabled, print a warning
6. rename h to h✝ (a hygienic identifier with name h)
7. elaborate mkIdent `h with the expected type being the goal type
8. try to synthesize all synthetic metavariables
9. check that the elaborated expression has the correct type while allowing assignments of synthetic opaque metavariables
10. print an error if there are unassigned metavariables
11. try closing the goal with the elaborated expression
12. assign the original goal with the copied goal

[Aaron Liu]

so complicated

[Aaron Liu]

docs#Lean.Elab.Tactic.Simpa.evalSimpa

[Julian Berman]

(Now I'm reminded this is in core), but for some simple example without yet understanding precisely which step in that sequence it'd go at, what I was trying to say was comparing the simpa version to a 2-line version:

example (f : Nat → Nat) (n : Nat) (hf : ∀ x, f x = x + 0 + 1) : f n + 0 = 1 + n := by
  -- Somewhere on this line, show me:
  --
  -- f : Nat → Nat
  -- n : Nat
  -- this : f n = n + 1
  -- ⊢ f n = n + 1
  simpa [Nat.add_zero, Nat.add_comm] using hf n

example (f : Nat → Nat) (n : Nat) (hf : ∀ x, f x = x + 0 + 1) : f n + 0 = 1 + n := by
  simp [Nat.add_zero, Nat.add_comm]
  exact hf n

[Jireh Loreaux]

Yeah, the key difference here is that hf n doesn't need any simplification.

My favorite way to use simpa is when I can build a slightly more complicated term (e.g., with congr()) to supply with using which, after simplifying it and the goal, matches somewhere.

[Kyle Miller]

lean4#10309 is an experiment adding intermediate tactic info in the range simpa ... using, so all the positions in this range in @Julian Berman's example show

f : Nat → Nat
n : Nat
hf : ∀ (x : Nat), f x = x + 0 + 1
⊢ f n = n + 1

("in the range" means that you see this state if your cursor is after s and before the term after using).

It doesn't show simplifications for the provided using term.

[Julian Berman]

Amazing that still sounds like a huge improvement, will try out the PR!