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?

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]

The best way to proceed is indeed to define a rewriting lemma `#|Q| = some_q`

which helps you to rewrite to a computable expression

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

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

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

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

Hi @Daniel Sousa I am not sure why you need to unlock `card`

is it for computation purposes?

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.

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

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

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)

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

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.

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.

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

Thanks for the clarification

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)

Nevermind, you cannot, since locking prevents conversion altogether.

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.

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