Stream: math-comp users

Topic: Unlock finfuns


view this post on Zulip Patrick Nicodemus (Sep 09 2022 at 02:47):

I'm having a little trouble understanding locking and unlocking. Is there a way that I can set an option so that [ffun f x => x] a reduces to f a upon simplification, so I don't have to use the command ffunE every time? Or can I mark a specific finfun as unlockable?

view this post on Zulip Patrick Nicodemus (Sep 09 2022 at 02:48):

Is this something to do with the phantoms in the first 20 or so lines of the finfun file? I am having trouble making sense of that code

view this post on Zulip abab9579 (Sep 09 2022 at 12:02):

Does unlock tactic not work?

view this post on Zulip Kazuhiko Sakaguchi (Sep 09 2022 at 12:53):

rewrite ffunE ?

view this post on Zulip Patrick Nicodemus (Sep 09 2022 at 17:36):

Both unlock and rewrite ffunE work here.

I'm looking for something where I don't have to do this manually, though. Is there a way to get ([ffun x => t] y) to simplify to t[x/y] when the simplification command /= is called?

view this post on Zulip Paolo Giarrusso (Sep 09 2022 at 18:41):

not for /=, but rewrite allows customizable "variants" of /= that are almost as short

view this post on Zulip Paolo Giarrusso (Sep 09 2022 at 18:42):

there's even syntax usable inside move

view this post on Zulip Paolo Giarrusso (Sep 09 2022 at 18:42):

(for the last, see https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/.E2.9C.94.20Concise.20way.20to.20rewrite.20without.20intro.20.26.20revert.20back.3F/near/297759606)


Last updated: Feb 08 2023 at 04:04 UTC