As far as I understand it, SSReflect is just a tactic language, there should be nothing left of SSReflect at the level of the Coq files underneath, right?

If I import some mathcomp library files and theorems and use those, I can use the standard Coq tactics to write my own theorems about them, right?

Conversely if someone else has written Coq theorems in the usual Ltac, I can still import them and write SSReflect-based tactic stuff to reason about them.

How far would it be reasonable to take this? Is it realistic to have a library where some files are written in ordinary Ltac and some are written in SSReflect based on the preference of the individual developers collaborating on this?

ssreflect is mostly a set of ltac1 tactics, and they mostly use disjoint names from standard ones, so you can mix them with normal ltac1 tactics.

however, there are also some Coq libraries that come with the tactics, and the two are not fully separated. ssreflect also changes the meaning of some existing constructs, including `if`

(can be disabled), the `rewrite`

tactic (their version is usually better, and `rewrite ->`

and `rewrite <-`

use the standard tactic), and more.

OTOH, using normal tactics on math-comp is likely to run into issues.

more specifically, ssreflect `apply:`

and normal `apply`

use different strategies to infer missing information, and AFAICT `apply`

sometimes has problems with theorems using canonical structures (I don't understand the root causes here, but this is visible and documented in Iris)

apart from that, it is realistic to mix and match tactics.

There are also some cases where `apply`

works but `apply:`

doesn't, I never figured out why.

`apply`

does many things more, and many things less, than `apply:`

.

For example `apply foo`

for `foo : A * B`

may mean `apply (fst foo)`

(or `snd`

) while `apply: foo`

only works if your goal is `A * B`

.

Similarly for `IFF`

(even if `apply/foo`

would work in that case).

@Patrick Nicodemus the main warning when using vanilla tactics together with MC theorems is that vanilla tactics do sometimes use the legacy unification algorithm (it is the case for `apply`

for example) and that is known to be a bit buggy w.r.t. CS inference. Things got better, but it may be the case that a thm does not apply simply because you are using the legacy unifier (not because you are using the wrong theorem).

For `rewrite`

, you should really prefer the SSR one (even on non MC theorems) since it is way more permissive w.r.t. implicit arguments (they are hidden in the goal, inferred in your theorem, and compared by the tactic... SSR quotients more, and since you don't see them nor write them...).

Enrico Tassi said:

Patrick Nicodemus the main warning when using vanilla tactics together with MC theorems is that vanilla tactics do sometimes use the legacy unification algorithm (it is the case for

`apply`

for example) and that is known to be a bit buggy w.r.t. CS inference. Things got better, but it may be the case that a thm does not apply simply because you are using the legacy unifier (not because you are using the wrong theorem).

Does this remark imply an answer to my StackExchange question: Tactic unification vs evarconv in Coq?

that is a large part of the story, but e.g. `refine`

is a non-ssreflect tactic that uses `evarconv`

.

still, that is the essence.

Last updated: Jun 25 2024 at 15:02 UTC