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))
Running 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?