The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Hi everyone.

I have a tactic for proving equality modulo ACI (associativity,  
commutativity and idempotence) for regular expressions. This tactic  
take the an equality x=y (where x and y are regular expressions) and  
provides a proof of their equivallence modulo ACI. This tactic is  
similar to the one described in section 16.3.3 of Coq'art book about  
proof by reflection.

Now, I would now to build a Coq function that uses this tactic for  
producing a set equivalent modulo ACI to the set given as argument to  
this function.


Do you have any suggestion, or know about any good document that I can  
give me some clear clues on how to do this?
Thanks a lot!

David.