Stream: math-comp users

Topic: SSreflect case

Raul (Mar 31 2022 at 17:38):

Hi!
Where can I find the implementation for the SSreflect case tactic? Or some paper with the specifications for the SSreflect tactics?

Karl Palmskog (Mar 31 2022 at 19:23):

https://github.com/coq/coq/blob/master/plugins/ssr/ssrelim.ml#L32

Enrico Tassi (Mar 31 2022 at 19:27):

What do you want to do exactly?

Raul (Apr 01 2022 at 13:58):

I'd like to make a diagram explaining how does case analysis work in Coq (like managing the goals) as simple as possible.
I'm not sure if SSReflect case depends on Coq's or destruct.

Enrico Tassi (Apr 01 2022 at 15:16):

It does not

Enrico Tassi (Apr 01 2022 at 15:19):

The main differences are:

• only works on the context which is explicitly mentioned (by using in or :)
• matches the values of the indexes using the matching facility all SSR is based on (keyd matching) and has syntax to pass explicit patterns for these
• does not try to infer which occurrences need to be skipped in order to make the resulting goal well typed (while Coq's one does)

Enrico Tassi (Apr 01 2022 at 15:21):

The SSR case tactic shares most of its code with elim. While the eliminator for case is standard (given by Coq), elim accepts a larger class of induction principles.

Raul (Apr 01 2022 at 18:18):

And there's some paper where its specification it's explained?
Something like this one, that explains implementation of vm_compute, https://coq.inria.fr/refman/zebibliography.html#compiledstrongreduction

Karl Palmskog (Apr 01 2022 at 18:20):

to my knowledge, SSR papers are all listed here (see "Tooling about SSReflect ..."): https://math-comp.github.io/papers.html

Last updated: Jan 29 2023 at 19:02 UTC