Hi!

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

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

What do you want to do exactly?

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.

It does not

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)

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.

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

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