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

Question

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

---

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

Answer 1

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

但是，有可能在 ocaml 级别或用一种较新的策略语言（如ltac2or ）编写这样的策略mtac。