theorem-proving - Idris 中的自定义证明者策略

Question

如果我理解正确（主要是从applyTactic函数的存在），可以为 Idris 中的定理证明器编写自定义策略。我可以使用哪些（或在哪里）示例来学习如何做到这一点？

Answer 1

在 Idris 中有两种编写自定义策略的机制：高级和低级反射。

使用高级反射，您编写了一个在语法上而不是在评估数据上运行的函数——它不会减少它的参数。这些函数返回一个新策略，使用 Idris 中预先存在的策略定义。如果你想直接返回一个证明项，你总是可以使用Exact. 可以在效果库中找到这种反射的示例。byReflection使用证明模式调用高级反射策略。

在低级反思中，您直接使用 Idris 核心类型理论中引用的术语。策略就是一个函数，TT -> List (TTName, TT) -> Tactic其中第一个参数是目标类型，第二个参数是本地证明上下文，返回结果与高级反射相同。这就是上面提到的笑声。这些是applyTactic在证明模式下调用的。