“依赖归纳”策略在 Coq 中的作用以及如何使用它

Question

您能否向我提供关于

dependent induction

/

dependent destruct

策略有哪些用例以及它们如何工作的高级解释（我将不胜感激足以让初学者理解的高级解释）。

到目前为止我发现的所有内容都极其复杂。

Answer 1

嗯，我们知道归纳数据类型通常通过索引进行索引，您可能已经看到的一个基本示例是通过类型及其大小进行索引的向量。

给出一个向量

t A (S n)

的例子，因为我们知道向量的大小大于0，所以我们知道这个向量中有一个A类型的值。 它可以简单地写为：

Theorem not_empty : forall A n, t A (S n) -> A.

但是如果您尝试使用通常的析构/归纳来证明这一点，您最终会遇到两种情况：

Theorem not_empty : forall A n, t A (S n) -> A.
intros.
destruct X.
- admit. (*here is our impossible clause*)
- exact h.
Admitted.

即使我们知道向量的大小等于/大于 1，Coq 仍然会为您提供一个与向量为空时相关的目标。我们可以通过记忆索引来滥用，并且我们可以手动捕获这些情况。

Theorem not_empty2 : forall A n, t A (S n) -> A.
intros.
remember (S n).
destruct X.
- inversion Heqn0.
- exact h.
Defined.

这很好，但如果有一种策略已经为你做到了这一点并消除了不可能的条款，那就更酷了？

Theorem not_empty3 : forall A n, t A (S n) -> A.
intros.
dependent induction X.
exact h.
Defined.