2

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

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

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

我应该如何继续？

4

3 回答 3

4

发生这种情况是因为 Coq 处理不同的索引和参数（请参阅这个问题的公认答案以获得非常好的解释）。您的Le关系仅使用索引，而标准定义使第一个参数成为参数：

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

我可以推荐阅读James Wilcox 的这篇博文。这是一个相关的摘录：

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

所以你可以（1）改变你的Le关系，让它使用一个参数，或者（2）使用remember@Zimm i48建议的策略，或者（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.
于 2017-05-17T12:42:47.497 回答
3

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

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

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

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

于 2017-05-17T12:37:02.833 回答
3

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

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

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

于 2017-05-17T12:40:30.550 回答