Zulip Chat Archive

Stream: general

Topic: Reduction of goal

Jasmin Blanchette (Jul 07 2020 at 15:30):

Suppose I have a goal like ((Ss_fst, Ss_snd).fst, (Ss_fst, Ss_snd).snd) ⇒ ((Ss'_fst, Ss'_snd).fst, (Ss'_fst, Ss'_snd).snd) and I just want to automatically reduce it, i.e., beta-delta-etc.-reduce it. I have the impression that Lean (and Coq) discourage that, preferring a lazy approach, but sometimes it seems useful, and in a teaching context I can see many uses for that. Going outside the goal, writing

#reduce (Ss_fst Ss_snd Ss'_fst Ss'_snd, ((Ss_fst, Ss_snd).fst, (Ss_fst, Ss_snd).snd)  ((Ss'_fst, Ss'_snd).fst, (Ss'_fst, Ss'_snd).snd))

and then doing a show with the result seems like a roundabout solution. Is there a more direct approach? If not, why not?

Johan Commelin (Jul 07 2020 at 15:31):


Jasmin Blanchette (Jul 07 2020 at 15:34):

Ah!! That's what dsimp is for! I think the simp part mislead me there. Thanks a lot. :)

Kevin Buzzard (Jul 07 2020 at 17:46):

Maybe simp only [] would work too

Last updated: Aug 03 2023 at 10:10 UTC