如何同时查看多个目标？答案

【问题标题】：How to look at multiple goals at the same time?如何同时查看多个目标？
【发布时间】：2018-09-17 16:40:32
【问题描述】：

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

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

【问题讨论】：

你能举一个你想“切换”目标的最小例子吗？使用destruct .. 或induction ... 之类的策略后，您通常会看到所有可用的目标，并且可以使用Focus n 将它们集中在第n 个目标上。
@nesreka 一个简单的案例是，当您在某个术语上执行dependent induction 时，归纳假设可能会生成_ = _ 条件，这几乎限制了术语应该是什么。在eapply 假设之后，如果它生成一个存在变量，则没有太多选择，而auto/eauto 不够聪明，无法解决这个问题。
all: 这样的战术可能就足够了吗？在执行dependent induction 之后，您可以运行; subst 以消除所有子目标中的等式。在coq.inria.fr/distrib/current/refman/ltac.html#sec469 中定义的all: 战术不止于此，请告诉我这是否适合您，我会将其转换为一个。
@nesreka subst 不起作用，目标选择器也不起作用，因为它不参与自动证明流程。 dependent induction 经常涉及更复杂的结构平等和 evas，这在这里不是很有帮助。人类知道要填写什么，如果证据搜索偶然以正确的顺序执行，eauto 有时可以正确填写。但这不是一个确定性的解决方案。
您能解释一下“不参与自动校样流程”是什么意思吗？

【解决方案1】：

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

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

【讨论】：