具有可变数量的策略

Question

假设我想要一种策略来一次清除多个假设，做类似clear_multiple H1, H2, H3.. 我尝试使用对来做到这一点，如下所示：

Ltac clear_multiple arg :=
match arg with
| (?f, ?s) => clear s; clear_multiple f
| ?f => clear f
end.

但是，问题是我必须放置括号才能有一个Prod：

Variable A: Prop.

Goal A -> A -> A -> True.
intros.
clear_multiple (H, H0, H1).

我的问题是，如何在不使用Prods 的情况下做到这一点？

---

我检查了这个问题，但这不是我想要的，因为我想要的参数数量未知。

Answer 1

您可能想知道该clear策略可以采用多个参数，因此您不需要定义新策略：您只需编写clear H H0 H1.

当然，您可能想为其他任务定义这样的 n 元策略。Coq 有一个支持此类定义的策略符号机制。不幸的是，它们并不是太强大：您只能将某种类型的参数列表传递给需要多个参数的策略（例如clear）；我认为它不能为您提供一个可以以编程方式迭代的列表。