Stream: math-comp users

Topic: A question about finType


view this post on Zulip Daniel Sousa (Jul 08 2020 at 14:03):

I am a bit of a newbie with mathcomp and I have another question.

I'm trying to define finite automata. The Sigma and Q (the alphabet and states) are defined to be of an arbitrary finType. Everything was working well until I tried to define the "size" of the automaton. This requires knowing #|Q| and #|Sigma|, which apparently is also locked? Do you have any suggestions of another way of doing this? Should I just give up on "generality" and define them as being ssrnat?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 08 2020 at 14:03):

Hi @Daniel Sousa , indeed that's a kind of a FAQ for math-comp [I dunno if any of the doc resources already explain this]

view this post on Zulip Emilio Jesús Gallego Arias (Jul 08 2020 at 14:04):

The best way to proceed is indeed to define a rewriting lemma #|Q| = some_q which helps you to rewrite to a computable expression

view this post on Zulip Emilio Jesús Gallego Arias (Jul 08 2020 at 14:04):

You may have a look at the existing libs for automaton to

view this post on Zulip Karl Palmskog (Jul 08 2020 at 14:05):

@Daniel Sousa if you want a reference solution, see https://github.com/coq-community/reglang

view this post on Zulip Daniel Sousa (Jul 08 2020 at 14:09):

I've looked into that for inspiration, but they also define them as finType, but then don't try to define a notion of size

view this post on Zulip Karl Palmskog (Jul 08 2020 at 14:10):

so for precision you want to actually compute the sizes of specific FAs?

view this post on Zulip Cyril Cohen (Jul 08 2020 at 14:10):

Hi @Daniel Sousa I am not sure why you need to unlock card is it for computation purposes?

view this post on Zulip Daniel Sousa (Jul 08 2020 at 14:14):

Yes, exactly. I think it will be a bit of a pain to have to prove everything and not have the ability to write a concrete automaton (and other stuff) to test if the definitions are making sense.

view this post on Zulip Karl Palmskog (Jul 08 2020 at 14:20):

Cyril can probably explain better than I can, but MathComp in general (and RegLang) is highly optimized for proving and computation inside proofs, not computation of functions by Eval, etc. One approach to get computable definitions is to define separate functions working on separate representations that are shown equivalent to MathComp's. This can be facilitated by CoqEAL, for example. See this thread for some examples: https://github.com/coq-community/reglang/issues/4

view this post on Zulip Daniel Sousa (Jul 08 2020 at 14:26):

Probably that would be a bit of an overkill. I don't really require computation.

The computation was mostly to test what I'm writing to make sure that I'm using the correct definition (unsurprisingly, I was not).

view this post on Zulip Karl Palmskog (Jul 08 2020 at 14:28):

the "standard approach" for validation in MathComp is to prove small lemmas about your definition (which would allow using repeated rewrites and the like to get computation-like behavior)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 08 2020 at 14:34):

There should definitively be a guide for the question "how do I compute with math-comp stuff"

view this post on Zulip Christian Doczkal (Jul 08 2020 at 14:41):

Daniel Sousa said:

I've looked into that for inspiration, but they also define them as finType, but then don't try to define a notion of size

What would be your notion of size? For me, the main developer of reglang, #|Q| (i.e., the number of states of some automaton Q) has always been sufficient as the "size of the automaton". We even provide verified translations between automata with verified bounds on the increase in the number of states.

view this post on Zulip Daniel Sousa (Jul 08 2020 at 15:09):

Oh, hi!
My definition is not just that, but for the purposes of the question we can assume it's #|Q| wlog.

For proofs it'll probably be enough to use #|_| as a black box. It's what you do, right?
It's just that I was trying to compute stuff, but I'll do as has been suggested.

Thank you all very much for your patience.

view this post on Zulip Cyril Cohen (Jul 08 2020 at 15:14):

Daniel Sousa said:

Oh, hi!
My definition is not just that, but for the purposes of the question we can assume it's #|Q| wlog.

For proofs it'll probably be enough to use #|_| as a black box. It's what you do, right?
It's just that I was trying to compute stuff, but I'll do as has been suggested.

Thank you all very much for your patience.

opaque \neq blackbox.
There are many card lemmas and whenever you create a new fintype you should prove cardinal equalities.
e.g. https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fintype.v#L2249-L2254

view this post on Zulip Daniel Sousa (Jul 08 2020 at 15:18):

Thanks for the clarification

view this post on Zulip Paolo Giarrusso (Jul 08 2020 at 21:43):

Can you just compute with vm_compute, since it ignores Opaque? (That’s brainstorming, but it is sometimes recommended for stdpp... e.g. see https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/gmap.v#L4)

view this post on Zulip Paolo Giarrusso (Jul 08 2020 at 21:48):

Nevermind, you cannot, since locking prevents conversion altogether.

view this post on Zulip Enrico Tassi (Jul 09 2020 at 06:40):

There is "opaque" and "Qed opaque". The Opaque/Transparent directive for tactics is surely ignored by vm_compute, but not the "Qed opaque" status of a constant, that makes it akin an axiom.

view this post on Zulip Enrico Tassi (Jul 09 2020 at 06:41):

FTR in MathComp "opaque" really means Qed opaque, since the other directive is very "volatile" in the Coq code base.


Last updated: Feb 08 2023 at 04:04 UTC