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: Oct 13 2024 at 01:02 UTC