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?

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

.)

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

ah, I read the `set`

docs and they don't mention this *at all* (as far as I can see)

yes with parentheses it works :) thanks!

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

@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...

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

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

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

Last updated: Jun 23 2024 at 05:02 UTC