Stream: math-comp users

Topic: Refining a type made with sets

Julin Shaji (Apr 19 2024 at 17:45):

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?

Karl Palmskog (Apr 30 2024 at 09:16):

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: Oct 13 2024 at 01:02 UTC