batteries
batteries copied to clipboard
leanprover-community
Pattern-based unfolding tactic
This is a tactic that allows targeted unfolding of expressions in the proof state by specifying patterns and occurrences (an idea that is due to Yaël Dillies).
The file Utils.lean contains utilities that can be re-used for other pattern-based tactics.
This is coupled with a point-and-click widget (which will be in a different PR to Mathlib) for automatically generating the tactic call with the appropriate configuration from the infoview selection.
Co-authored-by: Jovan Gerbscheid [email protected]
This PR is ready for review. In a set of future PRs, we would like to introduce the following additional features:
- [ ] More general syntax for referring to locations in the proof state, including values of let hypotheses
- [ ] Modifying patterns under binders
- [ ] Recursive unfolding, including unfolding to a specified depth
- [ ] Unfolding through notation and typeclass instances
To be honest, I'm not yet convinced that the new location syntax is needed, because if you want to do something at specific locations in multiple different hypotheses, then you may as well do it with separate tactic calls.
I have code that allows these patterns to also include bound variables. Would it be better to add it to this PR or to put it in a later PR?
I also think that the code in this PR should go in 2 separate folders: one with the code related to patterns, and one with the code for the unfolding tactic (which actually is just one file). Because the code for the patterns is to be used by more future tactics, and the unfold tactic is just here as a demonstration of the usefulness of the patterns.
To be honest, I'm not yet convinced that the new location syntax is needed, because if you want to do something at specific locations in multiple different hypotheses, then you may as well do it with separate tactic calls.
I think I will remove it then. Some customisation is still necessary since there is currently no syntax to refer to the body of a let hypothesis.
I have modified the locs syntax to something simpler that targets a single location. I think I am much happier with it in this form. I have updated the checklist from my previous comment erasing the items related to the locs syntax.
The replaceLocalLetDefEq, defineAfter and replaceLocalLetDecl definitions in Pattern/Location are functions that may be of general utility, so I could also try to PR them to Lean core (say into the file Lean/Meta/Tactic/Replace.lean), if that would be better.
I have code that allows these patterns to also include bound variables. Would it be better to add it to this PR or to put it in a later PR?
I am fine either way. Perhaps the reviewers could weigh in here.
I also think that the code in this PR should go in 2 separate folders: one with the code related to patterns, and one with the code for the unfolding tactic (which actually is just one file). Because the code for the patterns is to be used by more future tactics, and the unfold tactic is just here as a demonstration of the usefulness of the patterns.
Thanks for the suggestion, I've restructured the files according to this.
Looks like this wasn't switched back to awaiting-review after the last updates. It could use another update to adapt Std -> Batteries.
I cleaned up this PR a while ago, but I didn't put it on awaiting-review, because I wasn't sure whether this should really be included into batteries. It seems to me like the recent (last week merged) mathlib PR (https://github.com/leanprover-community/mathlib4/pull/12016#event-13586997181) for rewriting things into unfolded form is an improvement over this PR.
I think so. The main observation making this PR redundant is that if you want to do a rewrite which holds definitionally, then you can do this via rw [show old = new from rfl].
That makes sense, thanks! I'm removing awaiting-review and adding duplicate. That tag is not exactly right but it's the closest fit. Anyone can ask for this tag to be removed, ping me or an active maintainer if that's the case.