The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Mon, Jun 09, 2008 at 03:25:05PM +0100, Conor McBride wrote:
> Hi Adam
> 
> On 9 Jun 2008, at 15:12, Adam Chlipala wrote:
> 
> >Edsko de Vries wrote:
> >>I'm stuck again in trying to write some dependent code. I want to  
> >>index a
> >>vector:
> >>
> >
> >I'm sure someone else will answer your literal question, but I want  
> >to offer some advice that would lead to different (easier to  
> >discharge) goals.  I've found that vectors are _much_ easier to  
> >work with if you define them by recursion rather than with  
> >inductive types.
> 
> Let's be clear: this is a fact about Coq, not
> about vectors.

Can I ask a question about that? I'll readily admit that in Epigram or
Agda the code for vectors and the code for tuples would be equally
simple, whereas in Coq the code for vectors would be relatively
complicated. The way I understand it though is that the simple code I
write in Epigram is translated internally into something that would
probably resemble the code I write in Coq (at least conceptually). Can
this complexity always be hidden? Suppose I want to do proofs over my
functions later on, will this "hidden complexity" never come back to
bite me? 

Edsko