How to get data from an inductive type Coq

0
votes

I'm a little bit new to Coq, and I'm trying to do some formalization on regular grammars within Coq. Let's say I have an inductive type as follows:

Inductive rules : non_terminal -> list(non_terminal + terminal) -> Type :=
  rule1 : rules S [inr a; inl S] 
| rule2 : rules S [inr b;inl S] 
| rule3 : rules S [].

Which represents the (a* b*) grammar's derivation rules. Let's say I want to extract them for some later use. Is there any way I could do this and store it in a list of lists? e.g., I'd like a procedure that would return me [[S [inr a; inl S];S [inr b;inl S];[]]. Any other idea will be appreciated.

Thanks in advance.

1
coqtheorem-provinglanguage-theory
Why not to store them as a list in the first place? Programming in Coq is a bit problematic as in without having a very good understanding of future use of data, it is hard to know the best representation in advance. - ejgallego
I've considered it too, guess i'll have to store them in a list that looks like that return. The main idea in here is to get those rules and then convert it to a regular automata function. - Erick Grilo
Writing a compiler then could be an option. - ejgallego

1 Answers

0
votes

You could try using Ltac2, which can programmatically get information about inductive types? You can also use the template-coq package/plugin. These are probably not actually what you want to be doing here, though, since it's a bit convoluted.