I was looking at the reglang repo:

https://github.com/coq-community/reglang/blob/master/theories/dfa.v

In it, there is a conversion from regular expression to corresponding

dfa along with a correctness proof.

But mathcomp sets are used.

For example, the dfa type looks like:

```
(* Proof-oriented dfa *)
Record dfa : Type := {
dfa_state :> finType;
dfa_s : dfa_state;
dfa_fin : {set dfa_state};
dfa_trans : dfa_state -> char -> dfa_state
}.
```

But we could also make an equivalent dfa which uses 'normal' types to

represent sets.

```
| Cardinality | Type |
|-------------+-------------|
| 0 | void |
| 1 | unit |
| 2 | bool |
| 3 | option bool |
```

So, in that sense, we could also have had a computation friendly dfa

like:

```
(* 'Concrete' dfa *)
Record cdfa : Type := {
cdfa_state :> finType;
cdfa_s : cdfa_state;
cdfa_fin : cdfa_state_set;
cdfa_trans : cdfa_state -> char -> cdfa_state
}.
```

What could be a way to have a provably correct conversion from regex

to a 'concrete' dfa like reglang does for the proof-oriented dfa?

My understanding of refinements is that we will build up a common

structure using typeclasses for the common operations.

Then we instantiate this structure with concrete, abstract values.

But in the case of the `dfa`

type in reglang, the values are build up

from regular expressions.

If we are to use refinements, the `cdfa`

would also need to be built

up like that, right?

I don't really understand how it would work with `cdfa_state_set`

. The `dfa`

representation from RegLang is heavily adapted to MathComp's `finType`

and for easy proof, if you want more computable automata I recommend https://github.com/coq-community/atbr

Last updated: Jul 15 2024 at 20:02 UTC