Stream: math-comp users

Topic: `rewrite /` and $$\zeta$$-reduction


view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 11:48):

Is it expected that rewrite /name performs ζ\zeta-reduction after name has been unfolded?

view this post on Zulip Enrico Tassi (Sep 08 2022 at 11:55):

Hum, it surely needs to do some reduction, otherwise you would end up with ...(fun x y => ...) a b... whenever name is a function.
Where are the let you see expanded, actually?

view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 11:56):

All of them in the body.

view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 11:57):

Currently, I do a cbv delta[name] beta iota.

view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 11:57):

And I would have expected that rewrite /name does the same.

view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 11:57):

(Note that unfold is documented as cbv delta[name] beta iota zeta)

view this post on Zulip Enrico Tassi (Sep 08 2022 at 12:01):

The doc says

if my_def is a (local or global) defined constant, the tactic rewrite /my_def. is analogous to unfold my_def.

So, I guess it is not a bug, bat rather a behavior inherited by calling unfold behind the scenes.

view this post on Zulip Enrico Tassi (Sep 08 2022 at 12:02):

(I don't think it makes a lot of sense...)

view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 12:02):

Yes, but footnote 12 says:

image.png

view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 12:03):

But anyway, this was more by curiosity that I asked this question :)

view this post on Zulip Enrico Tassi (Sep 08 2022 at 12:05):

ROTFL

view this post on Zulip Enrico Tassi (Sep 08 2022 at 12:07):

I can only suggest to define Definition nameE a b : name a b = let _ in _ := erefl (name a b). and use that

view this post on Zulip Pierre-Yves Strub (Sep 08 2022 at 13:42):

Yes, or write some Ltac. Anywayt, thank.


Last updated: Jul 25 2024 at 16:02 UTC