The Coq mailing list

[t x <txrev319 AT gmail.com>]

For ints,

there are:

  (1)  "nat" which consists of:

    O = 0

    S(n) = n+1

  (2) Z, which consists of:

    Zpos, Zneg, Z0; where Zpos/Zneg use binary representations (xH, xO, xI).

For arrays, texts I've read suggested representing "T arr[];" as "f: nat -> T"

However, in practice, I found it (for the sake of eval compute and proving things) easier if I represented arrays as an associative list. [Of course, you will have to do some black magic (beyond my abilities) for telling Coq to map the associative list operations to array ops rather than actual associative list ops.]

On Sat, Aug 3, 2013 at 1:24 PM, Helmut Brandl <helmut.luis.brandl AT gmail.com> wrote:

Hello all,

I am writing a verifying compiler and I use ocaml as the implementation
language. I would like to use coq to verify some critical algorithms.

I have already read some documentation on program extraction. With
inductive types I don't see any problems, because inductive types and
functions on inductive types are translated one to one (with some
lexical adaptions and proof deletion) from coq to ocaml.

However I need arrays and I need to index arrays with ints in my
program. The algorithms I am trying to verify do not use the mutability
of ocaml arrays but they use the contents.

Can anybody give me hints (or links to any documentation) on how to
represent arrays and ints in coq?

Thanks
Helmut