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.
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
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
<- "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.
@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?
Since 8.12 Search is not sadowed either, by default. In theory the vanilla one
should be strictly more expressive.
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?
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