How do I use tactics to perform a reduction on goal

Stream: new members

[Rui Liu]

I want to perform reduction to a sub expression of the goal (or maybe any hypothesis in context), how do I do it?

[Rui Liu]

unfold doesn't seem to be what I want since it only unfolds definition? But I want to perform a reduction

[Mario Carneiro]

dsimp only often works

[Rui Liu]

Do I need to tag definitions as simp somehow to get it working?

[Kevin Buzzard]

do you want to unfold definitions or don't you? :-) There are several ways you can deal with definitions -- you can make them [reducible] or even abbreviations, or unfold them, and it wouldn't surprise me if you can tag them with simp as well if you want simp to do the job.

[Rui Liu]

How do I make sure unfold also does a reduction. Sometimes it seems unfold will just unfold the function, instead of applying it?

[Johan Commelin]

use dsimp [foo]

[Adam Topaz]

(where foo is the name of the definition)

[Rui Liu]

OK I seem to be able to proceed further with this