Stream: math-comp users

Topic: SSreflect case


view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Mar 31 2022 at 19:23):

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

view this post on Zulip Enrico Tassi (Mar 31 2022 at 19:27):

What do you want to do exactly?

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 01 2022 at 15:16):

It does not

view this post on Zulip Enrico Tassi (Apr 01 2022 at 15:19):

The main differences are:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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