The Coq mailing list

[gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)]

"John Wiegley" 
<johnw AT newartisans.com>
 writes:

> Another benefit of this approach is that I was able to make all use of 
> vector
> and fin disappear from the extracted Haskell code, where it now reduces down
> to Int and [a], so cheers all around.
>
> Emilio's suggestion about using ssreflect tuples is a great one -- since I'm
> trying to use ssreflect more; I will investigate that avenue next.

tuples in ssr are a pair of a list plus a proof of its size, it may work
well wrt to extraction (I have never extracted ssr code).

IMVHO, programming in this explicit-proof style does requires a bit of
discipline following the conventions and the proper interfaces (subType,
etc...), but when so, everything works very well.

Indeed, my previous code didn't respect quite a few ssr proof and naming
conventions, for instance, the right way to prove vnth_replace_neq is to
use the tnth_tset_nth lemma, not the hack I did. More correct code is
attached.

Best regards,
Emilio.

Attachment: tset_nth.v
Description: Binary data