Stream: Coq users

Topic: ssreflect rewrite: rewirte in multiple hpyotheses and goal


view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Jul 26 2023 at 17:37):

rewrite lemma in H1, H2 |- *

view this post on Zulip Paolo Giarrusso (Jul 26 2023 at 17:38):

in is documented as a separate tactical IIRC

view this post on Zulip 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 *

view this post on Zulip Cyril Cohen (Jul 26 2023 at 18:13):

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

view this post on Zulip 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 *

view this post on Zulip Ralf Jung (Jul 26 2023 at 18:25):

looks like both of these work

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

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

nope

view this post on Zulip 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)

view this post on Zulip 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: Jun 13 2024 at 19:02 UTC