How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion?

Question

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?

Answer 1

The easiest thing to do seems to be to disable termination checking. There is a setting in coq-of-ocaml to insert Unset Guard Checking in the generated file.

---

Of course, that jeopardizes logical consistency (although a nonterminating factorial alone won't lead to a contradiction). Note that this factorial is simply not well-defined on negative numbers, so there will be no free lunch. Here are some alternative approaches that a tool could implement.

• You could rely on the technicality that int in OCaml is bounded so factorial terminates after underflowing. Implementing this logic in Coq would still be rather involved.

• You could modify factorial to actually terminate, either at the source, or during/after generation (like hs-to-coq does using edits). There are many possible strategies here. One idea I like is to restrict the domain of factorial, so you wouldn't ever reason about negative inputs, and require all callers to prove that they provide arguments in that domain. (hs-to-coq has a variant of this idea, by annotating data types with invariant.)

• You could translate factorial into a monad that explicitly features nontermination (e.g., using fuel or coinduction). This moves the burden of reasoning about termination out of the tool; this has its pros and cons.