The Coq mailing list

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

Thank you!

In fact my question was not so clear, and your suggestion makes full  
sense :)


Best regards,

David.


On 2009/07/28, at 09:53, Yves Bertot wrote:

> David Pereira wrote:
> > 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.
> >
> >
> >
> >
> >
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.saclay.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >         http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> Your question is odd.  The input to the function satisfies your  
> verbal specification.  It may be that you want a canonical  
> representation...  In this case, the equivalent to the function  
> "flatten" from page 440 should do the trick.
>
> Yves
>
> Yves

David Pereira
MAP-i Phd Student in Computer Science
Researcher at LIACC - UP
Contacts : dpereira_at_liacc_dot_up_dot_pt
                   (+351)-220402900