The Coq mailing list

[Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>]

Thanks Pierre for your reply. In both 

the approaches there is one problem. Suppose

I have axiomatized an Int type in Coq, lets 

call it IntInt the way you suggested. Let's assume

I would extract it to ocaml ints later on. 

Suppose having defined a FMap on these IntInt 

I later decide to write  a function on these types 

that uses arithmetic operations such as less_than.

Currently I have these functions written on Z.

Clearly I cannot use Z_lt_dec since that works on Z

and this one doesn't. I would like to enjoy the same

level of proof support in the forms of lemmas and theorems

that I get when I use ZArith. 

In my case I'd have to define my new less_than operator on 

IntInt. In this case I won't get the same level of proof support 

unless I re-develop the same by mapping it to Zs via

i2z and z2i. Am I right in thinking so? It appears that 

we have to almost re-create a new Int in Coq that I want to

see in Ocaml, or am I completely wrong?

Thanks

Ashish

Hence the most general functor in FSetAVL, named IntMake, expects
_both_ an Int (such as Z_as_Int) and a OrderedType (such as Z_as_OT).
And FSetAVL.Make is just a particular case of IntMake where the Int is
Z_as_Int, but where the OrderedType part is still to be given later.
This FSetAVL.Make is the functor aimed at casual Coq users. But if
you're interested in optimized extraction, you should use
FSetAVL.IntMap directly.

Now there are several possible ways to get ocaml int after extraction:

* For instance, you can axiomatize everything in Coq:

  Parameter int : Set.
  Parameter compare : int -> int -> comparison.
  Parameter max : int -> int -> int.
  ...
 
  then teach the extraction what to do with them

  Extract Constant int => "int".
  ...

  then create both an Int and an OrderedType based on your int
 
  Module IntInt <: Int.
  Definition int:=int.
  ...
  End.

  Module IntOrderedType <: OrderedType.
  Definition t := int.
  ...
  End.

  Then you can use IMap := FSetAVL.IntMake(IntInt)(IntOrderedType).

* Another approach is to do your whole development under a functor
  expecting both an Int module and an Orderedtype, for instance:

  Module MyDev (I:Int)(O:OrderedType with Definition O.t := I.int).
  ...
  Module IMap := FSetAVL.IntMake(I)(O).
  ...
  (*your development here. might be splitted in several file
    via repeated functors and/or use of include*)
  ...
  End.

  Then you extract this functor, and then create _in ocaml_ some
  instance of Int and OrderedType based on ocaml's int, and finally
  do the functor application in ocaml.

Hope this help...

Pierre L.