Michael Soegtrop (Jul 12 2020 at 07:04): Michael Soegtrop (Jul 12 2020 at 07:04):I have some projects which use mathcomp and others which don't. Since I find it hard to switch between the tactic languages I wonder if there is a supported way to include mathcomp without changing the tactic language. I am fine with the standard tactic language - the mathcomp tactic language has for sure advantages, but for my application they are not large enough to justify switching.
Enrico Tassi (Jul 12 2020 at 08:28):Hum, at some point @Guillaume Melquiond had a similar request and we implemented the "SsrSyntax" thing. At least back then one could load MC libraries without enabling the proof language, see https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#compatibility-issues
Said that you will probably find that regular rewrite does not work well when implicit arguments contain structure instances (since it does not compare them with full unification). Similarly some P lemmas designed for begin used with case: may not work correctly with destruct, in particular the value of the indexes of inductive "spec" relations are matched as ssr's rewrite does if you use case:, it is not the case if you use destruct.
I should have probably started my message with this: note that if you Import ssreflect the only tactic that is shadowed is rewrite (and even there, one can access the vanilla one by using explicitly the -> and <- "direction flag"). All the other tactics have slightly different syntax (eg set x := t v.s. set (x := t)) hence they don't shadow the standard ones (but you may end up using them without realizing it, if you forget parentheses for example). All the known "clashes" are documented in the link above.
Michael Soegtrop (Jul 12 2020 at 16:50):@Enrico Tassi : thanks for the detailed answer - I will have a try with your answer in mind. There is one change so, which I find a bit annoying: the Search function changes quite a bit. Is what is Search in plain Coq SearchAbout when ssreflect is loaded?
Enrico Tassi (Jul 12 2020 at 17:03):Since 8.12 Search is not sadowed either, by default. In theory the vanilla one
should be strictly more expressive.
Michael Soegtrop (Jul 12 2020 at 20:19):Hmm, OK, I am still on 8.11.2 - time to switch I guess. Just to make sure: if I use mathcomp 1.11 on Coq 8.12 the Search function is not modified by ssreflect?
Enrico Tassi (Jul 13 2020 at 16:52):In 8.12 the Search originally implemented in ssreflect was deprecated in favor of the standard search (which got many improvements): https://coq.github.io/doc/v8.12/refman/changes.html#search IIRC if you want to access the Search from SSR you need to load something like ssrsearch.v, but this is not loaded by default in mathcomp.
Last updated: Jan 29 2023 at 19:02 UTC