coq - 如何同时看待多个目标？

Question

我正在考虑编写将着眼于多个目标并基于此做出决定的策略。但是，当我使用 match goal with 时并盯着一个目标，我怎么说“请找到另一个看起来像这样的目标”？

或者更确切地说，一个更普遍的问题是，我如何在 Ltac 的目标之间切换？

Answer 1

正如我们在评论中所讨论的那样，目前在 Ltac 中不可能实现这种对当前证明目标的检查。

但是，可以在 ocaml 级别或以一种较新的战术语言(如 ltac2)编写此类策略。或 mtac .