Stream: Coq users

Topic: Context matching with ssreflect `set`


view this post on Zulip Ralf Jung (Sep 26 2023 at 15:53):

ssrelfect rewrite has this nice feature to match not just on the term-to-rewrite, but on the context: rewrite [n in f n]comm rewrite the argument of f with comm, ignoring possible other rewrite sites that are not arguments to f.
is there any way to do the same with set? like say in the goal I have f applied to a large term, and I want to give a name to that term. I tried set x := n in f n, but sadly that doesn't seem to be accepted. the docs also don't mention anything like that. is context-matching available for anything besides rewrites?

view this post on Zulip Guillaume Melquiond (Sep 26 2023 at 16:00):

It should work. (But I think I usually use parentheses, e.g., set x := (n in f n).)

view this post on Zulip Guillaume Melquiond (Sep 26 2023 at 16:02):

And the documentation indeed seems to imply that you are supposed to use parentheses: https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#contextual-pattern-in-set-and-the-tactical

view this post on Zulip Ralf Jung (Sep 26 2023 at 17:01):

ah, I read the set docs and they don't mention this at all (as far as I can see)

view this post on Zulip Ralf Jung (Sep 26 2023 at 17:01):

yes with parentheses it works :) thanks!

view this post on Zulip Enrico Tassi (Sep 26 2023 at 19:12):

All SSR tactics taking a pattern accept the same language, rewrite has [] as delimiters, while the rest needs parentheses.

view this post on Zulip Paolo Giarrusso (Sep 26 2023 at 19:54):

@Ralf Jung the docs for which set? Ssreflect set ( https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#abbreviations-ssr ) and Coq set ( https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.set ) are entirely separate tactics. But I'm not sure if the reference for the first is complete, it's hard to tell...

view this post on Zulip Enrico Tassi (Sep 26 2023 at 20:20):

This is the missing bits of SSR's set: https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#contextual-pattern-in-set-and-the-tactical

view this post on Zulip Ralf Jung (Sep 28 2023 at 05:33):

@Paolo Giarrusso I had checked here: https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#abbreviations

view this post on Zulip Ralf Jung (Sep 28 2023 at 05:33):

and it doesnt mention this, as far as I can see


Last updated: Jun 23 2024 at 05:02 UTC