Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Ralf Jung 
<>
 writes:

> We are using these patterns a lot as they really help making some forms
> of forward reasoning significantly more convenient.

Indeed then I guess you are setting foot on pretty uncharted territory :D

> The trouble is that we'd like to stay compatible with a stable, released
> version of Coq for the benefit of people that use the library we
> develop.  So, wholesale moving to 8.7 is not an option :/

What I was trying to say is that if you think of improvements to the
%pat feature, they will happen in 8.7, so you would need to start
supporting it. Which IMO, is feasible.

So you would have an iris-tactics-8.6.v and iris-tactics-8.7.v file and
you would select the file at compile time.

This way you could suggest improvements and try them.

>> Let me finish mentioning that a more stable called "views", which offers
>> similar (and extra) functionality is available in ssreflect.
>
> Unfortunately, ssreflect's intro patterns cannot (as far as I know) be
> reasonably made to work in custom tactics.  For Coq's patterns, we are
> using "simple_intropattern(x)" in our tactic notation; is there anything
> comparable for ssreflect?

> (The ssreflect style for achieving this would probably be to leave stuff
> on the goal stack and use the "=>" tactical for introduction.  However,
> that's not an option for us, the patterns only describe a part of what's
> going on, and the "context" has to be handled by our custom tactic. This
> in particular involves doing Ltac work before and after executing the
> patterns.  ssreflect's style does not permit us to do any work ourselves
> after the patterns are done.)

That's very interesting, thanks for the feedback. Unfortunately I have
no clue about your question, maybe people in the SSR mailing list do
know? [cc'ed]

E.