对关系的归纳答案

【问题标题】：Induction over relations对关系的归纳
【发布时间】：2024-01-10 00:19:01
【问题描述】：

我试图证明以下关于自然排序的玩具定理：

Inductive Le: nat -> nat -> Prop :=
  | le_n: forall n, Le n n
  | le_S: forall n m, Le n m -> Le n (S m).

Theorem le_Sn_m: forall n m,
  Le (S n) m -> Le n m.

在纸面上，这是对Le (S n) m 的简单归纳。特别是 le_n 的基本情况是微不足道的。

不过，在 Coq 中，以归纳法开始我的证明给了我以下信息：

Proof.
  intros n m H. induction H.

1 subgoal
n, n0 : nat
______________________________________(1/1)
Le n n0

...在这种情况下我被阻止了。

我应该如何继续？

【问题讨论】：

恕我直言，这个例子可以作为 Coq 归纳类型和索引的练习；但是，如果您打算将<= 关系形式化，这完全是矫枉过正，会给您带来很多麻烦。我确实建议您将您的关系定义为函数nat -> nat -> bool。

标签： coq coq-tactic

【解决方案1】：

发生这种情况是因为 Coq 对 indices 和 parameters 的处理方式不同（请参阅this question 的已接受答案以获得非常好的解释）。您的 Le 关系仅使用索引，而标准定义使第一个参数成为参数：

Inductive le (n : nat) : nat -> Prop :=
| le_n : n <= n
| le_S : forall m : nat, n <= m -> n <= S m

我可以推荐阅读 James Wilcox 的 this blog post。以下是相关摘录：

当 Coq 执行案例分析时，它首先对所有索引进行抽象。在谓词上使用 destruct 时，您可能已经将此表现为信息丢失

因此，您可以 (1) 更改您的 Le 关系，使其使用参数，或 (2) 使用 @Zimm i48 建议的 remember 策略，或 (3) 使用 dependent induction @Vinz 提到的策略：

Require Import Coq.Program.Equality.   (* for `dependent induction` *)

Inductive Le: nat -> nat -> Prop :=
  | le_n: forall n, Le n n
  | le_S: forall n m, Le n m -> Le n (S m).
Hint Constructors Le.                  (* so `auto` will work *)

Theorem le_Sn_m: forall n m,
  Le (S n) m -> Le n m.
Proof. intros n m H. dependent induction H; auto. Qed.

【讨论】：

【解决方案2】：

这是由于 Coq 的限制，当使用 induction 时，术语不仅仅由变量组成。通过进行归纳，Coq 忘记了第一个参数是 S 和一些 n 的事实。

您可以改为执行以下操作：

Theorem le_Sn_m_: forall X m,
  Le X m -> forall n, X = S n -> Le n m.

我认为有一个 dependent induction 可以为您节省这个中间引理，但我不记得在哪里。

【讨论】：

@Vinz，如果您使用 emacs 和 Proof General，请考虑研究 company-coq 模式。当您开始输入命令时，它会弹出一个带有补全的弹出窗口，您可以选择一个，按 ctrl-h 并获取技术参考手册中的文档。因此，在这种情况下，只需键入“depe”并向下箭头到“依赖感应标识”，然后按 ctrl-h。文档会告诉你包含 Coq.Program.Equality。至少可以节省您访问网络浏览器和心理上下文切换的时间......
很高兴知道！谢谢@larsr

【解决方案3】：

类似于@Vinz 的建议，但不改变您要证明的陈述：

Proof.
  intros n m H.
  remember (S n) as p.
  induction H.

使用remember 策略将在您的上下文中引入相等性，从而避免丢失此关键信息。

【讨论】：