对关系的归纳

Question

我正在尝试证明以下关于自然数排序的玩具定理：

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

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

我应该如何进行？

Answer 1

这是由于 Coq 的限制，当使用 induction 时不仅仅由变量组成。通过归纳，Coq 忘记了第一个参数是某些 n.

的 S 这一事实

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

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

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

Answer 2

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

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

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

Answer 3

这是因为 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。以下是相关摘录：

When Coq performs a case analysis, it first abstracts over all indices. You may have seen this manifest as a loss of information when using destruct on predicates

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

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.

对关系的归纳

Induction over relations

coq

coq-tactic