Stream: Coq users

Topic: ssreflect rewrite: rewirte in multiple hpyotheses and goal

Ralf Jung (Jul 26 2023 at 17:30):

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

Paolo Giarrusso (Jul 26 2023 at 17:37):

rewrite lemma in H1, H2 |- *

Paolo Giarrusso (Jul 26 2023 at 17:38):

in is documented as a separate tactical IIRC

Cyril Cohen (Jul 26 2023 at 18:11):

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

It's rewrite lemma in H1 H2 *

Cyril Cohen (Jul 26 2023 at 18:13):

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

Ralf Jung (Jul 26 2023 at 18:25):

Paolo Giarrusso said:

rewrite lemma in H1, H2 |- *

ah, thanks! I thought I had seen something involving |- but never thought to combine it with *

Ralf Jung (Jul 26 2023 at 18:25):

looks like both of these work

Ralf Jung (Jul 26 2023 at 18:26):

I once tried rewrite lem in * and got an error which to me indicated that * means all hypotheses

Error: assumptions should be named explicitly

Ralf Jung (Jul 26 2023 at 18:26):

and it does mean that elsewhere (e.g. simpl in *). so I never even tried to use it as syntax for "goal", I guess

Cyril Cohen (Jul 26 2023 at 19:24):

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

IndeedError: assumptions should be named explicitly *does not mean all hyps`, simply that you must at least mention one hypothesis otherwise this is a noop.

Paolo Giarrusso (Jul 26 2023 at 20:04):

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

Enrico Tassi (Jul 26 2023 at 20:18):

nope

Enrico Tassi (Jul 26 2023 at 20:20):

IIRC in h |- * is also accepted, and is a synonym of in h * (which is the recommended syntax)

Cyril Cohen (Jul 27 2023 at 08:53):

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: Oct 13 2024 at 01:02 UTC