The Coq mailing list

[Erick Simas Grilo <simas_grilo AT id.uff.br>]

Hi there, I am a little bit new used to Coq and I am trying to formalize some of the regular aspects of regular languages. I already have a grammar that looks like this:

Record reg_grammar: Type:= {
    set_non_terminal : (list non_terminal);
    set_terminal : (list terminal);
    prod_rules: non_terminal -> sf -> Prop;
    start_symbol: non_terminal;
}.

which (ignoring the prod_rules type, which ends in prop,it is for other purposes) I have a list that has all the rules of the grammar that would look like this(e.g, for the regular grammar generated by (a*b*):

Definition a_b_rules: list(list(non_terminal + terminal)):= [[inl S;inr a; inl S];[inl S;inr b; inl S]].

Which one can see as S -> aS | S -> bS. where S is a non termnal and a and b are terminals (in this case, inductive types given by).

Inductive non_terminal:Type :=
S.
Inductive terminal : Type :=
a | b.

Now let's say I have an automata definition that would look like this one: 

Record dfa (S A : Type) := DFA {
  initial_state : S;
  is_final : S -> bool;
  next : S -> A -> S
}.

And a function that takes a list of elements of the type A (which will be the terminal symbols) and returns whether the list is recgonized by the automata or not.
Definition run_dfa S A (m : dfa S A) (l : list A) : bool :=
  is_final m (fold_left (next m) l (initial_state m)).

I would like to have a function that would iterate over the list of those rules and I could see one of those sublists as a possible function for the automata and store each one of them in a datatype, or just check over the list while running the word in the automata if there is any of those functions that could be used. Does anyone knows how this could be done? Any help/idea will be apreciated.

Thanks in Advance,

Erick.