1
$\begingroup$

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?

$\endgroup$
1

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thanks for the helpful response. I had seen the Unset Guard Checking option but was a little afraid of using it... I honestly didn't understand it entirely. I included it and am now able to accomplish what I wanted. Regarding your suggestion to restrict the domain in OCaml, could you elaborate a bit on how to do this? I looked at annotating data with invariant in hs-to-coq, but not sure how to do this for OCaml. $\endgroup$ Nov 3, 2022 at 18:54
  • $\begingroup$ My other suggestions were more hypothetical, as features that don't exist yet. Restricting the domain would mean adding an extra argument to the Coq function that says that the first argument is non-negative in a way that enables writing recursive functions. factorial : forall (z : Z), is_nonnegative z -> Z where is_nonnegative z := Acc (fun x y => 0 <= x < y) z; we have is_nonnegative z <-> 0 <= z, but Acc is more suitable for writing fixpoints. $\endgroup$
    – Li-yao Xia
    Nov 3, 2022 at 19:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.