The Coq mailing list

["St�phane Lescuyer" <lescuyer AT lri.fr>]

Hello there,

>   1. In programming languages, we are taught to program against an interface
> and not to an implementation. Can I formalize by programming against the
> finite map interface ?  Is there anything wrong in doing so ?
Indeed you can and as a matter of fact you are encouraged to do so :)
The whole point of the modular design of the finite set/map libraries
is precisely that you can set up your development in a way thats
independent of the actual implementation. In practice, a way to to so
is write your stuff as a functor taking an abstract implementation of
maps as an argument:

Module MyE := ... (* your ordered type *)

Module MyStuff (M : FMapInterface.S with Module E := MyE).
 ... (* here you can use M.t, M.add, etc ... *)
End MyStuff.

>   2. I tried to import the finite map interface  but none of the interface
> definitions are available in the CoqIde. However, if I import a particular
> implementation, all the definitions (in that particular implementation) are
> visible in the CoqIde. Is that intentional ?
If you import FMaps, you still need to access the map interface
through FMapInterface.S. Only if you import FMapInterface you get to
use S without further qualification. Then assuming you have a module M
of type FMapInterface.S, you can access the interface definitions in M
by M.t, M.empty, etc.

>  3. Are there formalizations showing usage of any of the implementations of
> finite maps ? If so, I will appreciate pointers.
I use finite maps and finite sets extensively in my development. You
can find a part of it that uses sets here:
http://www.lri.fr/~lescuyer/sat/tactic.tgz. You can also read a bit
about the formalization in
http://www.lri.fr/~lescuyer/pdf/tphols08.pdf, I dont know if it can
help. Unfortunately, I dont have anything available (ie, nicely
packaged ^^) using maps to show you but sets and maps are used in a
very similar fashion.

>  4. Is there literature on the theory behind finite maps as implemented in
> Coq libraries ? Is it similar to the following paper (HOL implementation) by
> Don Syme and Graham Collins (available at
> http://research.microsoft.com/research/pubs/view.aspx?type=Publication&id=595)?
As far as I know, finite maps and sets in Coq were developed by
following the interfaces Set and Map of Ocaml's standard library. I
havent read the paper you point thoroughly, but at first glance it
looks like it is indeed the same data structure that they are modeling
(modulo name changes, additional functions in the interface, etc).

Hope this helps,

Stéphane L.

-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06