Stream: Coq users

Topic: SSReflect and other libraries?


view this post on Zulip Patrick Nicodemus (May 25 2022 at 09:35):

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?

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:43):

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.

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:45):

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.

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:46):

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

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:49):

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)

view this post on Zulip Paolo Giarrusso (May 25 2022 at 09:50):

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

view this post on Zulip Ana de Almeida Borges (May 25 2022 at 10:21):

There are also some cases where apply works but apply: doesn't, I never figured out why.

view this post on Zulip Enrico Tassi (May 25 2022 at 10:30):

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

view this post on Zulip Enrico Tassi (May 25 2022 at 10:36):

@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...).

view this post on Zulip James Wood (May 25 2022 at 13:51):

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?

view this post on Zulip Paolo Giarrusso (May 25 2022 at 20:41):

that is a large part of the story, but e.g. refine is a non-ssreflect tactic that uses evarconv.

view this post on Zulip Paolo Giarrusso (May 25 2022 at 20:46):

still, that is the essence.


Last updated: Oct 13 2024 at 01:02 UTC