The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

> We can use Extract Inductive list => list[nil cons] to bind Coq lists to
> Caml lists during extraction, but suppose I want to do the same for the
> head function? I would like head in Coq to become hd in Caml, but the
> problem is that head is defined in Coq as a total function, which
> returns Value x or error.
> 
> Is there any simple way to make the link between explicit error values
> in Coq and true errors (or imcomplete pattern matching) in Caml?

No, there is not. If you translate a Coq function returing a value in
a sum type into an incomplete pattern matching, how can you certify
that the extracted function will never be applied to one of the
non-existent case?

If you are able to prove in Coq that all your calls to head do not
return an error, then you can define another head function in Coq with
a pre-condition expressing that the list is not empty (so that in the
case analysis, you can reason by absurdum for nil) Then this function
will be extracted using an exception for the nil case (which is known
to be never raised, actually).

Best regards,
-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr