I am learning Coq and I'd like to use it to formalize Regular languages theory, specially finite automata. Let's say I have a structure for an automata as follows:
Record automata : Type := {
dfa_set_states : list state;
init_state : state;
end_state : state;
dfa_func: state -> terminal -> state;
}.
Where state is an inductive type as:
Inductive state:Type :=
S.
And the type terminal terminal is
Inductive terminal:Type :=
a | b.
I am trying to define it so later I'll be able to generalize the definition for any regular language. For now, I'd want to construct an automata which recognizes the language (a * b *), which is all words over the {a,b} alphabet. Does anyone have an idea on how to build some kind of fixpoint function that will run the word (which I see as a list of terminal) and tell me if that automata recgonizes that word or not? Any idea/help will be greatly apreciated.
Thanks in advance, Erick.