Stream: Coq users

Topic: fset automation


view this post on Zulip Philipp G. Haselwarter (Nov 08 2021 at 10:18):

I do have a question for here rather than the issue tracker though -- what's a reasonable way to go about automating these simple minded fset proofs?

view this post on Zulip Karl Palmskog (Nov 08 2021 at 10:19):

hmm, isn't fset MathComp stuff? Then I would look into ssrAC: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v

view this post on Zulip Théo Winterhalter (Nov 08 2021 at 10:23):

Here it is the fset from extructures. And ssrAC does not provide any automation does it?

view this post on Zulip Théo Winterhalter (Nov 08 2021 at 10:23):

Can be interesting nonetheless indeed.

view this post on Zulip Karl Palmskog (Nov 08 2021 at 10:24):

my understanding of ssrAC is that you get rewriting modulo AC with the regular SSR rewrite, but I could be wrong

view this post on Zulip Théo Winterhalter (Nov 08 2021 at 10:30):

The file you gave says:

Rewriting with AC (not modulo AC), using a small scale command.

view this post on Zulip Philipp G. Haselwarter (Nov 08 2021 at 10:43):

thanks for the pointer!


Last updated: Feb 08 2023 at 22:03 UTC