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?
I don't know it, and I suspect that's ssreflect's way of looking down on this wish (like for inversion)?
I see. Is there an approved ssreflect way of getting around those problems?
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.
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?
I'm actually working on a PL proof.
What do you mean by shadow rewrite / shadow erewrite?
Require Import ssreflect takes over
rewrite, but not
Last updated: Jan 28 2023 at 06:30 UTC