coq - 可变数量的战术

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）；我不认为它可以给你一个你可以以编程方式迭代的列表。