ocaml - 在 OCaml 中实现 Coq 策略

Question

我想实现一个名为solve 的策略，它可以求解表示为定理的线性方程。例如:

Theorem leq :  exists x , x + 3 = 2*x - 3 .
Proof.
solve.
Qed.

我想在 Coq 源代码(在 OCaml 中)中将“解决”作为一种策略来实现。如何将目标(线性方程)传递给OCaml并在求解后返回值并完成证明？

Answer 1

请参阅以下内容 introduction to Coq plugins作为在 OCaml 中实现策略的工作示例。但是请注意，您要编写的决策程序非常重要，并且:

• 我不清楚你不能使用已经存在的 ring 或 omega
• 反射式证明方法可以让您以一种更简单、更安全的方式开发策略，方法是在 Coq 数据类型中反射(reflect)所需的方程并直接在 Coq 中实现求解过程——然后一小部分 OCaml 代码就可以用于自动化语法反射。