Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 12 2020 at 15:32):

dsimp only often works

view this post on Zulip Rui Liu (Dec 12 2020 at 15:36):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Dec 12 2020 at 15:40):

use dsimp [foo]

view this post on Zulip Adam Topaz (Dec 12 2020 at 15:41):

(where foo is the name of the definition)

view this post on Zulip 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