The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

David Leduc wrote:
> A few days ago, on the Agda mailing-list there was a mail by Alan
> Jeffrey "about a trick for representing lists (or any other monoid) up
> to associativity". It sounds great but unfortunately I cannot speak
> Agda. Can anyone translate this mail into Coq? TIA.
>
> https://lists.chalmers.se/pipermail/agda/2011/003420.html
>    

The motivation early in that post seems to come from the lack of a 
serious tactic language in Agda.  If all you're interested in doing is 
proving more or less traditional theorems about lists, you should find 
the traditional representation to admit more or less automatic proofs in 
Coq, with a tiny amount of tactic support (e.g., [crush] tactic from 
CPDT).  If you're interested more in dependently typed programming, the 
trick in that message might be useful; I'll leave it to some other, 
sufficiently motivated person to translate to Coq. ;)  (I have a feeling 
the use of Agda irrelevance will prevent a direct translation.)