feature-request(coq): coq-of-ocaml support

[Alizter]

I'd like to propose a feature request for coq-of-ocaml support. See the corresponding issue: formal-land/coq-of-ocaml#219

What is coq-of-ocaml

coq-of-ocaml takes an ocaml program and translates it into a similar Coq program. This allows for properties of the OCaml program to be proven.

Proposal

I propose that we add a coq.of-ocaml stanza that takes an ocaml library stanza and creates a corresponding theory for it. Then an additional coq.theory can import the generated functions and prove things about it.

Implementation details

There are some issues with this approach:

• The generated .v files might require some post processing.
• People might want to use the generated theory directly, but it would only exist in the _build directory. This could be circumvented with a promotion mechanism but then it would be impossible to edit the files directly etc.

Example

Let's take the example from the repo as a proof of concept. They have a main.ml file:

type 'a tree =
  | Leaf of 'a
  | Node of 'a tree * 'a tree

let rec sum tree =
  match tree with
  | Leaf n -> n
  | Node (tree1, tree2) -> sum tree1 + sum tree2

we could have a dune file with something like:

(library
 (name main))

(coq.of-ocaml
 (name my_program)
 (source main))

(coq.theory
 (name my_proofs)
 (theories my_program))

Now this would produce in _build a file called Main.v in a theory called my_program.

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Inductive tree (a : Set) : Set :=
| Leaf : a -> tree a
| Node : tree a -> tree a -> tree a.

Arguments Leaf {_}.
Arguments Node {_}.

Fixpoint sum (tree : tree int) : int :=
  match tree with
  | Leaf n => n
  | Node tree1 tree2 => Z.add (sum tree1) (sum tree2)
  end.

Then in an additional coq.theory called my_proofs, we could have .v files like

Require Import Main.

(** Definition of a tree with only positive integers *)
Inductive positive : tree int -> Prop :=
| Positive_leaf : forall n, n > 0 -> positive (Leaf n)
| Positive_node : forall tree1 tree2,
  positive tree1 -> positive tree2 -> positive (Node tree1 tree2).

Require Import Coq.micromega.Lia.

Lemma positive_plus n m : n > 0 -> m > 0 -> n + m > 0.
  lia.
Qed.

(** Proof that if a tree is positive, then its sum is positive too *)
Fixpoint positive_sum (tree : tree int) (H : positive tree)
  : sum tree > 0.
  destruct tree; simpl; inversion H; trivial.
  apply positive_plus; now apply positive_sum.
Qed.

proving things about this theory.

In effect, this becomes a dual process to the extraction stanza.

I've opened this issue to discuss some of the implementation details.

[rgrinberg]

The proposal seems fine to me.

The only thing I would change is that the stanza should work at the level of sources and not libraries. I.e.

(coq.of_ocaml
 (source foo))

Should refer to a module foo. This scheme is strictly more flexible for the user and is easier for us to implement.