Stream: Coq users

Topic: Stdpp analogue for by []


view this post on Zulip Karl Palmskog (Mar 24 2022 at 08:03):

In SSReflect, by [] is preferred over running the equivalent done by itself. This enables having all proof scripts subgoals end in by ....

Stdpp provides a standalone analogue to done, but seemingly it's not possible to do by [] using only Stdpp. Is the Stdpp idiom to only write done when one wants to run done by itself?

view this post on Zulip Paolo Giarrusso (Mar 24 2022 at 08:27):

In stdpp, that's correct

view this post on Zulip Paolo Giarrusso (Mar 24 2022 at 08:29):

And as you imply, loading ssreflect lets you "fix" that, but some tweaks are "recommended"

view this post on Zulip Paolo Giarrusso (Mar 24 2022 at 08:33):

https://gitlab.mpi-sws.org/iris/iris/-/blob/d7eae97aa4fad623c63c3c8d4cf4f607c7d689ad/iris/prelude/prelude.v#L1-L6

view this post on Zulip Paolo Giarrusso (Mar 24 2022 at 08:35):

Stdpp also has a notation for by tactic, but not the brace variant:

https://gitlab.mpi-sws.org/iris/stdpp/-/blob/2c67e51782ca27b4d6edbc0766650d8a2dad8f13/theories/tactics.v#L70

view this post on Zulip Karl Palmskog (Mar 24 2022 at 08:44):

right, so I guess I have to define the brace variant by myself then (I'd like to avoid mixing Stdpp and SSR)

view this post on Zulip Paolo Giarrusso (Mar 24 2022 at 10:20):

All of iris uses that mix of course, but YMMV. I'd guess you can define this shortcut easily, but you probably can't define by [tac1 | tac2] and variants without a plugin.


Last updated: Feb 01 2023 at 11:04 UTC