RFC: `simp [f]` as explainable syntax; `simp [unfold f]`.

Proposal

Right now, when the user writes simp [f] where f is a defined function, it can have one of the following effects

1. It adds it to the toUnfold set, and uses the internal “unfolding” machinery when encountering applications of it.
2. It looks up its equational theorems (f.eq_1…), and treats them mostly like any other rewrite rule.
3. It does both.

The rules are intricate. It uses 1 for projection functions and reducible functions, 3 for structurally recursive functions with smart unfoldings and for non-recursive functions, and 2 else.

Following the guideline that smartness in the system can ideally be explained by less smart, more primitive features, I am wondering if it is worth coming up with syntax that exposes mechanism 1 and 2 directly.

For mechanism 1, we have that: The user can write simp [f.eq_1, f.eq_2, …] explicitly. It’s a bit annoying to have to write out the list, but that’s ok for now (and can be addressed separately if a problem).

But for mechanism 2 (and hence 3), we don’t have syntax, so I am wondering if it is worth introducing one. One proposal would be to write simp [unfold f], where unfold is a modifier similar to ↑, to mean mechanism 2. (Mechanism 3 is then just writing simp [unfold f, f.eq_1,…]).

This can be useful, for example, for functions that have equational lemmas that are too specific, and the user wants to rewrite more occurrencs, but simp [f.eq_def] is insufficient, maybe because of unfoldPartialApp or some other intricacies of simp’s bespoke unfolding machineries.

Open questions

I have not fully convinced myself yet that this is worth it.

I also want to understand better in which circumstances simp [unfold f] would work better than simp [f.eq_def] or (with #5110) simp [f.unfold]. Maybe it’s possible that we can explain every behavior of simp in terms of rewriting with various f.… lemmas.

One difference is for unfolding projection functions, which is unfolded at higher transparency setting (withReducibleAndInstances) and thus also implicitly unfolds an instance dictionary argument. Hmm.

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Review the three simp [f] mechanisms described in the proposal, then compare the proposed simp [unfold f] syntax with f.eq_def and f.unfold from #5110. Done means resolving whether the syntax is worthwhile and specifying how it should differ from those existing approaches, including projection and instance-dictionary behavior.