Coq/Ltac：是否可以设计一种策略，在决策程序证明目标时证明目标已被证明，而无需证明项？

Question

我正在设计一种 Coq 策略，它调用一个决策程序，该程序回答是/否，而不给出证明项。当我得到“是”时，我想说 Ltac 目标已被证明。

有办法做到这一点吗？例如，将目标更改为

True

，然后使用

exact I

？

我正在使用Ltac2，但如果它能解决问题我可以使用Ltac。

我听说过Ltac的

Tactic.change_concl

（https://coq.inria.fr/doc/V8.13.0/api/coq/Tactics/index.html），但我不知道是否可以只需将目标更改为 True；并且它在 Ltac2 中不可用。

Answer 1

你基本上不能。 Coq 的要点在于，它保证经过检查的证明，直至其自身的逻辑原理：用类型良好的归纳结构微积分语言编写的证明。这些策略只是为了帮助您建立这样的证明，因此任何接受不同程序的单词作为“oracle”的东西都超出了系统的哲学。 当然，有解决方法。例如，您可以将外部工具证明的所有结果收集到某种数据库中，然后使用 Coq 证明您的最终陈述是正确的，前提是该数据库中收集的所有事实都是正确的。 Ltac 并不是真正适合此目的的工具。

我建议查看

bigenough

和

near

在

math-comp生态系统

中的策略开发。