Zulip Chat Archive

Stream: general

Topic: simplify type of term in goal


Winston Yin (Jul 20 2022 at 06:47):

My goal contains an expression like g ≫ f. If I hover over f and g in VSCode, I see that g : X ⟶ Y and f : Y ⟶ really_complicated_stuff. I know that really_complicated_stuff = simple_stuff. I even have a simp lemma for that. What I want to do is do a rewrite using a lemma g ≫ f = ..., which is stated for f : Y ⟶ simple_stuff. However, when I try that, Lean complains that it can't find g ≫ f in the goal, even when the pretty printer literally prints g ≫ f. What can I do?

If I do set f' := f with h, Lean even can't rw ←h because of type check difficulties. Please advise.

Eric Wieser (Jul 20 2022 at 06:51):

Can you make a #mwe?

Johan Commelin (Jul 20 2022 at 06:51):

Hmm, your example doesn't seem to typecheck. Do you want f : Y \hom simple_stuff? You are talking about f : simple_stuff halfway through your message.
I think it is hard to debug this without more details.

Eric Wieser (Jul 20 2022 at 06:53):

even when the pretty printer literally prints g ≫ f. What can I do?

You can use set_option pp.all true to check a little more thoroughly whether they're really the same

Winston Yin (Jul 20 2022 at 06:55):

Fixed typo in question

Andrew Yang (Jul 20 2022 at 06:55):

Though I do not have a #mwe as well, I can confirm this occurs on me from time to time, where I would like to dsimp on the type of the terms. And it is quite annoying to fix, usually resulting in some ugly change or erw.

Andrew Yang (Jul 20 2022 at 06:56):

(Hopefully the really_complicated_stuff = simple_stuff is defeq. It's evil to talk about equality of objects otherwise.)

Winston Yin (Jul 20 2022 at 20:50):

Yes they are defeq. The equality is a simp lemma proved with rfl. I managed to circumvent the problem by making f start out as Y ⟶ simple_stuff rather than Y ⟶ complicated_stuff


Last updated: Dec 20 2023 at 11:08 UTC