With ssreflect rewrite I can say `rewrite lemma in H1, H2`

and it will rewrite the lemma in both of these hypotheses. but how do I tell it to rewrite in the goal *and* those hypotheses? Currently I just always repeat the rewrite but that is obviously not pretty.

the docs at https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#an-extended-rewrite-tactic don't mention `in Hyp`

at all so I don't know where else I could figure this out...

`rewrite lemma in H1, H2 |- *`

`in`

is documented as a separate tactical IIRC

Ralf Jung said:

With ssreflect rewrite I can say

`rewrite lemma in H1, H2`

and it will rewrite the lemma in both of these hypotheses. but how do I tell it to rewrite in the goalandthose hypotheses? Currently I just always repeat the rewrite but that is obviously not pretty.

the docs at https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#an-extended-rewrite-tactic don't mention`in Hyp`

at all so I don't know where else I could figure this out...

It's `rewrite lemma in H1 H2 *`

cf https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#localization

Paolo Giarrusso said:

`rewrite lemma in H1, H2 |- *`

ah, thanks! I thought I had seen something involving `|-`

but never thought to combine it with `*`

looks like both of these work

I once tried `rewrite lem in *`

and got an error which to me indicated that `*`

means *all* hypotheses

Error: assumptions should be named explicitly

and it does mean that elsewhere (e.g. `simpl in *`

). so I never even tried to use it as syntax for "goal", I guess

If you're using ssreflect `in hyps *`

is the correct syntax, **without comma** and it does not mean all hyps.

Otherwise you use coq ad-hoc `in`

(i.e. which semantics is specialized to Coq rewrite as opposed to the general ssreflect `in`

tactical), which is comma separated and then `*`

does mean all hyps and `|- *`

"in goal".

Indeed`Error: assumptions should be named explicitly`

*does not mean all hyps`, simply that you must at least mention one hypothesis otherwise this is a noop.

and there's indeed no way to do ssreflect rewrite on all hyps (except maybe via an ltac loop — never tried)

nope

IIRC `in h |- *`

is also accepted, and is a synonym of `in h *`

(which is the recommended syntax)

One of the invariants of the ssreflect tactic set is that it should not change hypotheses silently, i.e. for an hypothesis to change it should be named in the script.

Last updated: Jun 13 2024 at 19:02 UTC