In many parts of the standard library, there are a bunch of OCaml-native functions with no Coq counterpart. I implemented a Coq version of some of them (with added proofs to show that the Coq versions behave as I think they ought to), but now how do I check that this actually matches the OCaml version's behavior?
The easiest / most "obvious" way I can think of would be to take a test input x, compute f x in Coq, and extract a comparison f x = [[f x]] (where [[…]] marks evaluation in Coq), then repeat for some number of test cases. Unfortunately, I can't find a way to force evaluation in Coq.
Is there a trick to make this possible? Or is there some other standard way for testing behavior across extraction? (Manually going Compute (f x). and plugging the resulting terms as literals back into the sanity checks would be an ugly fallback… Unfortunately, those won't update automatically when the function is changed, and it would also be a lot of manual work that doesn't exactly encourage exhaustive tests…)
Minimal sample:
Definition foo (b : bool) : bool :=
match b with | true => false | false => true end.
Extract Inlined Constant foo => "not".
Extract Inlined Constant bool_eq => "(=)".
Definition foo_true := foo true.
Definition foo_false := foo false.
Definition foo_test : bool :=
andb (bool_eq (foo true) foo_true) (bool_eq (foo false) foo_false).
Recursive Extraction foo_test.
results in
(** val foo_true : bool **)
let foo_true = not true
(** val foo_false : bool **)
let foo_false = not false
(** val foo_test : bool **)
let foo_test = (&&) ((=) (not true) foo_true) ((=) (not false) foo_false)
which is unhelpful. All the ways I could think of to change the definition of foo_true/foo_false to try and have them pre-evaluated didn't work. I can't find any flag in the extraction mechanism to force evaluation… Both the reference manual's attribute index and the flags/options/tables index didn't contain anything that looks useful. Is there anything that I missed?
Starting a definition with Eval compute in evaluates it before registering the definition.
Definition foo_true := Eval compute in foo true.
Definition foo_false := Eval compute in foo false.
Definition foo_test : bool :=
andb (bool_eq (foo true) foo_true) (bool_eq (foo false) foo_false).
Recursive Extraction foo_test.