unfold with simp to reduce match

Stream: lean4

[Sébastien Michelland]

I'm having trouble designing definitions that unfold at the correct time with simp. My current understanding is that it unfolds definitions marked with @[simp] or mentioned explicitly; and I feel like I'm really missing the match-simplifying logic of Coq. I have some functions manipulating trees, and I keep running situations like these:

• With @[simp] on the function, everything gets expanded even when the argument is symbolic, which renders the goal unreadable and makes it hard to use high-level lemmas.
• Without it, anytime the function is used to compute with some known or partially-known argument it needs to be named manually in simp [function...], including its sometimes internal subfunctions, which is extremely cumbersome.
• This also happens with Lean definitions, so instead of unfolding my function I end up unfolding it, plus subfunctions, plus List.foldr, plus bind to expose the monad-specific bind, ...

I've played around with a simp extension to make this easier, but to fully resolve calls to my functions with known arguments it still unfolds generic definitions like bind and pure, which feels really bad.

Coq's simpl unfolds definitions when it exposes a reducible match and unfolds typeclass operators when the instance is resolved, which would solve my current problem. Is there a way to approach this behavior? Was it a particular design choice to not do this with simp? How does the Lean library usually handle the dual symbolic/computational use of its functions?

[Leonardo de Moura]

Note that simpl and simp are very different beasts. In Coq, simpl is used to reduce terms, and it preserves definitional equality.
simp is inspired by Isabelle's simp, and it is essentially a rewriting engine. The resulting term is not necessarily definitionally equal to the input term, and simp produces a proof that the input/output is equal.
That being said, I have been annoyed by the same behaviors you have described. We can add a flag to simp. It can't be the default behavior because it would create problems for the Mathlib porting efforts. It is worth discussing with other users whether the behavior above is desirable, and can be one day the default one.

[Sébastien Michelland]

Thank you for clarifying, this explains why simp can often be used instead of rw (which is really convenient IMO). A flag or even a different reduction-oriented tactic would be fine I think, without risking to break existing code.

I fear Lean's internals are still too obscure for me to attempt to write it, but I'm happy to give it a try if someone could point me in the general direction.

[Patrick Massot]

I think it makes sense to have a tactic dedicated to do careful unfolding, with a nice default behavior and a lot of options. This is useful but very different from what we expect from simp coming from Lean 3.

[Leonardo de Moura]

@Sébastien Michelland Thanks for offering. I think this feature is not a good match for new contributors. There are many details, and complications generated by Lean's simpler kernel. For example, even structurally recursive definitions are encoded using recursors in Lean.

I am impressed by your messages. If you are interested in contributing to the code base, please tell us the what kind of coding you like, and we can try to find a match.

[Sébastien Michelland]

@Leonardo de Moura I see, thanks. I'll keep the hack for now and watch for possible updates. :smile:

For context, I'm working on a research project modeling language semantics using Lean for a couple of months. I'm completely new to it so I'm not sure I can be of much help within this period, but since I'm getting help and everyone's time here it feels only right to try and contribute in return, eg. by solving my own problems.

Now that I think about it, maybe I can contribute to some documentation in the longer run. I understand the tutorials and manual for Lean 4 are still incomplete, with more experience I could probably help out there?

[Mario Carneiro]

I will echo what has been said above: this would be a useful tactic, but it's not simp. It sounds similar to the cbv tactic (also in Coq), something that does definitional reduction using smart unfolding lemmas. In lean 3 you can kind of get a similar effect using simp! (which uses all equation lemmas as simp lemmas), and over time the norm_num tactic has turned into that kind of evaluator (although it performs less well on the pure type theory stuff like reducing recursors and lambdas)

[Leonardo de Moura]

@Sébastien Michelland Thanks for sharing.

Now that I think about it, maybe I can contribute to some documentation in the longer run. I understand the tutorials and manual for Lean 4 are still incomplete, with more experience I could probably help out there?

Yes, help with the documentation is welcome :)

[Mario Carneiro]

It would probably work fairly well to build this tactic on top of the simp backend though, even if it's a different frontend. It just needs to mix bits of whnf with simp-traversal (and it should not be restricted to defeq reductions because too many functions are well-founded-recursive and would not reduce well by defeq)