simpLocation

Stream: lean4

[Scott Morrison]

Currently in src/Lean/Elab/Tactic/Simp.lean the definition evalSimp is doing two different types of work:

1. munging the tactic Syntax to extract arguments
2. delegating to other lower level tactics based on the form of the location argument extracted from the Syntax.

I'd prefer if these were separate, in particular so that in another tactic I can run the simplifier by specifying a location. As evalSimp is currently written, I'd either have to reproduce most of its logic, or synthesize a Syntax expression in order to actually use evalSimp.

Is it reasonable to want this separation? Perhaps I'm not yet used to "the Lean 4 way"!

https://github.com/leanprover/lean4/compare/master...semorrison:semorrison/simpLocation?expand=1 is my proposed modification, introducing a simpLocation tactic.

[Mario Carneiro]

the "lean 4 way" seems to be to construct syntax to run the tactic frontend. I'm also not particularly happy with this state of affairs

[Mario Carneiro]

similar observations also apply to most command parsers, they parse their syntax and delegate right away, so you can't really run them unless you have a syntax, it's not like lean 3 where there is a backend tactic that takes exprs and such

[Scott Morrison]

The local reason I wanted this was experimenting with porting split_ifs. Part of split_ifs delegates to simp only [if_pos, if_neg, dif_pos, dif_neg] along with a discharger.

It is set up so that that list of lemmas is obtained from an attribute. The "syntactical" simp tactic in Lean 4 implemented by evalSimp doesn't support passing lemmas by attribute. It seems like it would be quite unpleasant to synthesize a Syntax after you've done whatever work is required to assemble the list of lemmas.

[Scott Morrison]

The alternative would be to directly call the underlying tactics in src/Lean/Meta/Tactic/Simp/Main.lean but none of those are set up to deal with location already (whereas evalSimp has the logic).

[Scott Morrison]

Hence my desire to separate the code the deals with Syntax and the code the deals with location.

[Jannis Limperg]

+1. I've copy-pasted a few definitions because I don't want to bother constructing Syntax for what should be a function call. If this sort of refactoring is wanted, I'd be happy to do (some of) it.

[Scott Morrison]

This is now a PR as https://github.com/leanprover/lean4/pull/797.