了解 coq 中证据的归纳

Question

我正在研究IndProp.v 的Software Foundations (Vol 1: Logical Foundations) 中的定理ev_ev__ev。

Theorem ev_ev__ev : forall n m,
  even (n+m) -> even n -> even m.
Proof.
  intros n m Enm En. induction En as [| n' Hn' IHn'].
  - (* En: ev_0 *) simpl in Enm. apply Enm.
  - (* En: ev_SS n' Hn': even n' 
              with IHn': even (n' + m) -> even m *)
    apply IHn'. simpl in Enm. inversion Enm as [| n'm H]. apply H.
Qed.

其中even 定义为：

Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

在第二个子弹-处，上下文以及目标如下：

m, n' : nat
Enm : even (S (S n') + m)
Hn' : even n'
IHn' : even (n' + m) -> even m
______________________________________(1/1)
even m

我了解上下文中的m, n', Enm, Hn' 是如何生成的。但是IHn'是怎么生成的呢？

Answer 1

归纳假设是系统地为同一类型族中的构造函数的前提创建的。因此，您可以单独查看每个构造函数。

假设您有一个类型的归纳定义，以：

Inductive arbitraryName : A -> B -> Prop :=

将创建一个称为arbitraryName_ind 的归纳原理，它从对通常称为P 且具有相同类型的任意谓词进行量化开始

forall P : A -> B -> Prop,

现在，如果你有表单的构造函数

arbitrary_constructor : forall x y, arbitraryName x y -> ...

归纳原理将为此构造函数提供一个子句，该子句以对构造函数中所有变量的相同量化、相同假设以及依赖于任意名称的前提的归纳假设开始。

forall x y, arbitraryName x y -> P x y -> ...

最后，归纳定义的每个构造函数都必须以定义的类型族的应用程序结束（在本例中为arbitraryName）。此构造函数的子句末尾将函数 P 应用于同一参数。

让我们回到arbitrary_constructor 并假设它具有以下完整类型：

arbitrary_constructor : forall x y, arbitraryName x y -> arbitraryName (g x y) (h x y)

在这种情况下，归纳原则中的子句是：

 (forall x y, arbitraryName x y -> P x y -> P (g x y) (h x y))

---

对于even，有一个构造函数ev_SS，其形状如下：

ev_SS : forall x, even x -> even (S (S x))

所以生成的子句具有以下形状：

(forall x, even x -> P x -> P (S (S x)))

归纳假设IHn'正好对应子句中的P。

全归纳原理如下图。

forall P : nat -> Prop, P 0 -> 
   (forall x, even x -> P x -> P (S (S x))) ->
   forall n, even n -> P n

当您键入induction En 时，将应用此定理。假设even n，其中n 被普遍量化，与当时目标中En 的文本相匹配。事实证明，该假设的陈述是even n（这里的n 是固定在目标中的）所以普遍量化的n 是用目标上下文中的本地n 实例化的。然后，该策略尝试在此n 出现的上下文中找到所有假设。在这种情况下，存在Enm，因此该假设用于定义将在其上实例化归纳原理的P。从某种意义上说，Enm 被放回到了目标的结论中，就像执行了revert Enm。

我们需要P n 与even (n + m) -> even m 相同。最自然的解决方案是P等于函数fun x => even (x + m) -> even m

所以在归纳证明的第二种情况下，引入一个新的n'，并将P应用于n'，给出归纳假设的内容：

(even (n' + m) -> even m)

并将P 应用于S (S n') 以给出最终目标的内容。

 even (S (S n') + m) -> even m

现在，在调用 induction 策略时，假设 Enm 在上下文中，所以声明 even (S (S n') + m)，在道德上是 Enm 的后代，被放回上下文中一样的名字。请注意，在另一个目标中已经有一个名为 Enm 的假设，但声明再次不同。

你对这个归纳假设是如何产生的有疑问是很正常的，因为实际上发生的事情涉及到几个操作。