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

Question

如果我理解正确(主要来自 applyTactic 函数的存在)，则可以为 Idris 中的定理证明器编写自定义策略。我可以用什么(或哪里)的例子来学习如何做到这一点？

Answer 1

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

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

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