## Stream: math-comp users

### Topic: A question about finType

#### 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?

#### 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]

#### 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

#### Emilio Jesús Gallego Arias (Jul 08 2020 at 14:04):

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

#### Karl Palmskog (Jul 08 2020 at 14:05):

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

#### 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

#### Karl Palmskog (Jul 08 2020 at 14:10):

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

#### 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?

#### 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.

#### 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

#### 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).

#### 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)

#### 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"

#### 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.

#### 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.

#### 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

#### Daniel Sousa (Jul 08 2020 at 15:18):

Thanks for the clarification

#### 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)

#### Paolo Giarrusso (Jul 08 2020 at 21:48):

Nevermind, you cannot, since locking prevents conversion altogether.

#### 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.

#### 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