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 `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.

@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