Coq提取前如何强制求值？或测试提取函数行为的其他方法？

OCaml标准库中有不少函数没有对应的Coq实现，我已经实现了带证明的Coq版本，现在需要验证它的行为和OCaml原生版本完全一致。我原本想的方案是选取测试输入x，在Coq中计算f x，然后生成比较式f x = [[f x]]（其中[[…]]代表Coq内求值结果），但找不到能强制Coq自动完成求值的方法。手动执行Compute (f x)再把结果作为字面量填入检查的方式太繁琐，而且没法自动更新；我尝试的最小示例提取结果也没帮助，也没找到提取机制里强制求值的相关选项。想问有没有实现技巧，或者跨提取测试行为的标准方法？

可行的实现技巧与标准方法 #

• 利用Coq高效求值命令绑定结果
  用vm_compute或native_compute直接将f x的求值结果绑定为一个定义，再生成等式进行验证。这种方式能自动更新结果，无需手动复制：

  Definition test_result := vm_compute in (f x).
  Lemma f_consistent_x : f x = test_result.
  Proof. reflexivity. Qed.
  

  当f或测试输入x修改后，重新执行定义即可自动更新test_result。

• 跨语言联动测试：Coq提取+OCaml测试框架
  将Coq实现的f提取为OCaml代码，直接在OCaml中与原生函数做对比测试。可以借助OCaml的测试库（如OUnit）批量执行用例，示例代码：

  open OUnit2
  
  let test_native_consistency test_ctxt =
    let test_cases = [1; 2; 3; 42] (* 自定义测试输入 *) in
    List.iter (fun x ->
      assert_equal (Coq_extracted.f x) (Stdlib.native_f x)
    ) test_cases
  
  let suite = "Coq vs OCaml consistency test" >::: [
    "native function match" >:: test_native_consistency
  ]
  
  let () = run_test_tt_main suite
  

  这种方法直接在目标运行环境验证，规避Coq内部求值的限制，还能复用成熟的测试工具链。

• 借助Equations库自动生成计算规则
  如果你的Coq函数是用Equations库定义的，它会自动生成函数的计算归约规则。你可以直接利用这些规则来证明函数调用的结果，无需手动触发求值。比如定义函数后，直接调用生成的f_equation引理来完成一致性验证。

• 自定义Tactic自动完成求值与等式证明
  编写简单的自定义策略，自动完成求值、结果绑定与等式证明的流程：

  Ltac auto_verify f x :=
    let computed_val := eval vm_compute in (f x) in
    assert (f x = computed_val); [ reflexivity | ].
  

  之后在验证时只需调用auto_verify f x，就能自动完成求值和一致性等式的证明。

内容的提问来源于stack exchange，提问作者nobody