I am trying to use coq-of-ocaml to convert a simple recursive factorial function written in OCaml into Coq. I have a
testing_factorial.ml file which defines the factorial function as follows:
let rec factorial (n[@coq_cast] : int) = match n with | 0 | 1 -> 1 | n -> n * (factorial (n - 1))
coq-of-ocaml testing_factorial.ml yields a
Testing_factorial.v file with the below contents:
(** File generated by coq-of-ocaml *) Require Import CoqOfOCaml.CoqOfOCaml. Require Import CoqOfOCaml.Settings. Fixpoint factorial (n_value : int) : int := match n_value with | (0 | 1) => 1 | n_value => Z.mul n_value (factorial (Z.sub n_value 1)) end.
However, when I run this Coq program, I get the following error:
Recursive definition of factorial is ill-formed. In environment factorial : int -> int n_value : int p : positive p0 : positive Recursive call to factorial has principal argument equal to "n_value - 1" instead of a subterm of "n_value". Recursive definition is: "fun n_value : int => match n_value with | 0 => 1 | Z.pos p => match p with | 1%positive => 1 | _ => (n_value * factorial (n_value - 1))%Z end | Z.neg _ => (n_value * factorial (n_value - 1))%Z end". Not in proof mode.
I am at a lost with how to fix this. A native Coq implementation of the factorial function would use Natural numbers (Coq's nat). There is no native nat data type in OCaml. I know that it is possible to create a nat type manually in OCaml, but this would require defining from scratch all nat functions (+, -, *, etc.). This is painful to do and would likely complicate Coq proofs on the functions. For a project that I am working on, I would like to prove a number of "math-y" OCaml functions, so learning how to do this would be very helpful! Does anybody have a fix to this error, or how to avoid it in the first place with the coq-of-ocaml translation?