Equivalent to Coq's compute tactic

Stream: general

[Konstantin Weitz]

How do I fully evaluate a goal in lean, including unfolding all definitions etc.

[Henrik Böving]

You can use decide for things that are, well, decidable. If you are looking to fully reduce and then continue proving the answer is that we do not encourage this mode of proof as it leads to impossible to refector APIs and you should instead try to work with grind and simp

[Konstantin Weitz]

Yes i'd like to fully reduce and then continue the proof. Are you saying there is no way to do it?

[Konstantin Weitz]

Is there a way to mark all the definitions that I'd like to be automatically unfolded by simp?

[suhr]

dsimp, but you need to list all the definitions you want to unfold.

[Kyle Miller]

Usually people use simp with the definitions they would like to unfold.

The reduce tactic in mathlib reduces everything. Like Henrik said, this approach is really not recommended. We have reduce for exploration purposes.

Could you give a #mwe that illustrates a goal where you'd want to use the Coq compute tactic?

[Thomas Murrills]

Konstantin Weitz said:

Is there a way to mark all the definitions that I'd like to be automatically unfolded by simp?

For this, you might be looking for @[simps] (or @[simps!] if necessary) if you have access to Mathlib, which will generate a simp lemma for each (dataful) projection. But whether it’s what you really want depends on the situation.