Stream: Coq users

Topic: erewrite and ssreflect


view this post on Zulip Simon Hudon (Jul 25 2021 at 20:31):

I'm slowly adopting tools from ssreflect in my proofs. One thing that I haven't found a replacement for is erewrite. Is there a syntax in ssrefect to do what erewrite does, i.e. introduce existential variables and leave them unassigned?

view this post on Zulip Paolo Giarrusso (Jul 25 2021 at 22:30):

I don't know it, and I suspect that's ssreflect's way of looking down on this wish (like for inversion)?

view this post on Zulip Simon Hudon (Jul 25 2021 at 22:58):

I see. Is there an approved ssreflect way of getting around those problems?

view this post on Zulip Paolo Giarrusso (Jul 26 2021 at 00:53):

I'm sorry, that comment wasn't entirely serious. I'm also curious; if no alternative exists, I'd stick to erewrite even with ssreflect, or just pass arguments to the rewrite lemma.

view this post on Zulip Enrico Tassi (Jul 26 2021 at 05:46):

IIRC unresolved evars of sort Prop are tolerated.
Internally, evars are supported, the under tactic is basically doing an erewrite.

Historically SSR tactics did not let you assigning pre existing evars, so they won't let you create them either. Things changed for apply (which is more or less like eapply), but not rewrite.

I'd say there is room for improving SSR tactics in the context of PL where leaving evars around is so common. A trivial one would be to shadow erewrite (as we shadow rewrite), but in general I'm not a big fan of adding to each tactic a letter to tune its behavior.

Which is your usecase, exactly?

view this post on Zulip Simon Hudon (Jul 26 2021 at 14:14):

I'm actually working on a PL proof.

view this post on Zulip Simon Hudon (Jul 26 2021 at 14:14):

What do you mean by shadow rewrite / shadow erewrite?

view this post on Zulip Enrico Tassi (Jul 26 2021 at 14:54):

Require Import ssreflect takes over rewrite, but not erewrite


Last updated: Mar 28 2024 at 19:02 UTC