Zulip Chat Archive

Stream: new members

Topic: help with dsimp


King Crawford (Nov 14 2022 at 17:47):

I have this goal:
⊢ (λ (i : ℕ), ∃! (H : i ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f i) c
I want to beta reduce it to
⊢ ∃! (H : c ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f c
dsimp gives me the following which isn't quite what I'm looking for
⊢ ∃! (H : c ∈ finset.range n), (finset.range n).sum f = f c
Is there a way to do this?

Johan Commelin (Nov 14 2022 at 17:51):

You could show <your desired expression>

Johan Commelin (Nov 14 2022 at 17:51):

Or maybe dsimp only is slightly less aggressive?

King Crawford (Nov 14 2022 at 17:53):

dsimp only does the same thing unfortunately, but show worked. I didn't know about show. Thanks!

Martin Dvořák (Nov 14 2022 at 17:54):

Johan Commelin said:

You could show <your desired expression>

What is the difference between change and show for these purposes?

Martin Dvořák (Nov 14 2022 at 17:56):

King Crawford said:

I have this goal:
⊢ (λ (i : ℕ), ∃! (H : i ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f i) c
I want to beta reduce it to
⊢ ∃! (H : c ∈ finset.range n), ∑ (j : ℕ) in finset.range n, f j = f c
dsimp gives me the following which isn't quite what I'm looking for
⊢ ∃! (H : c ∈ finset.range n), (finset.range n).sum f = f c
Is there a way to do this?

I have had similar issues. I wish there was a command (or a rw lemma) that specifically performs the beta reduction.

Johan Commelin (Nov 14 2022 at 17:56):

@Martin Dvořák None. But change is more flexible. You can do change <foobar> at my_hyp,

Martin Dvořák (Nov 14 2022 at 17:58):

I have been using change on both the goal and hypotheses. I am glad that change exists but it is PITA to use it more than once per day.

Yaël Dillies (Nov 14 2022 at 17:59):

In fact, you can configure dsimp to perform whichever reduction you like.

Martin Dvořák (Nov 14 2022 at 18:00):

Can I keep dsimp as it is and create a new command bsimp for beta reductions only?


Last updated: Dec 20 2023 at 11:08 UTC