Stream: new members

Topic: How do I use tactics to perform a reduction on goal

Rui Liu (Dec 12 2020 at 15:17):

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 (Dec 12 2020 at 15:18):

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

Mario Carneiro (Dec 12 2020 at 15:32):

dsimp only often works

Rui Liu (Dec 12 2020 at 15:36):

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

Kevin Buzzard (Dec 12 2020 at 15:38):

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 (Dec 12 2020 at 15:40):

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 (Dec 12 2020 at 15:40):

use dsimp [foo]

Adam Topaz (Dec 12 2020 at 15:41):

(where foo is the name of the definition)

Rui Liu (Dec 12 2020 at 16:43):

OK I seem to be able to proceed further with this

Last updated: May 14 2021 at 05:20 UTC