Simon Hudon (Jul 25 2021 at 20:31): 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?
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)?
Simon Hudon (Jul 25 2021 at 22:58):I see. Is there an approved ssreflect way of getting around those problems?
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.
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?
Simon Hudon (Jul 26 2021 at 14:14):I'm actually working on a PL proof.
Simon Hudon (Jul 26 2021 at 14:14):What do you mean by shadow rewrite / shadow erewrite?
Enrico Tassi (Jul 26 2021 at 14:54):Require Import ssreflect takes over rewrite, but not erewrite
Last updated: Oct 13 2024 at 01:02 UTC