coq 中“小于”关系的证据归纳

Question

我工作在以下定理的证明Sn_le_Sm__n_le_m中IndProp.v的软件基础（第1卷：逻辑基础）。

Theorem Sn_le_Sm__n_le_m : ?n m,
  S n ? S m ? n ? m.
Proof.
  intros n m HS.
  induction HS as [ | m' Hm' IHm'].
  - (* le_n *) (* Failed Here *)
  - (* le_S *) apply IHSm'.
Admitted.

其中，的定义le (i.e., ?)是：

Inductive le : nat ? nat ? Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : le n (S m).
Notation "m ? n" := (le m n).

之前induction HS，上下文和目标如下：

n, m : nat
HS : S n <= S m
______________________________________(1/1)
n <= m

在第一个子弹点-，上下文和目标是：

n, m : nat
______________________________________(1/1)
n <= m

我们必须在n <= m没有任何上下文的情况下证明，这显然是不可能的。

为什么它不为 中的案例生成S n = S m（然后n = m）？le_ninduction HS

Answer 1

我认为这里的主要问题是不可能使用归纳法来证明该定理，HS因为无法仅用n假设来说明某些内容S n，因为没有一个构造函数le不会改变 的值n。但无论如何，在第一个项目符号之后没有假设的原因-是因为调用induction具有用与每个构造函数对应的值替换所有出现的属性参数的效果，并且在这种情况下没有帮助，因为被替换的术语S n是没有任何地方提到。有一些技巧可以避免这种情况。例如，您可以将 n 替换为pred(S n)如下。

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  assert(Hn: n=pred (S n)). reflexivity. rewrite Hn.
  assert(Hm: m=pred (S m)). reflexivity. rewrite Hm.
  induction HS.
  - (* le_n *) apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

但正如我上面提到的，不可能再进一步了。另一种方法是使用inversion更聪明的方法，但在某些情况下它可能没有帮助，因为归纳假设是必要的。但值得了解一下。

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  inversion HS.
  - (* le_n *) apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

解决该问题的最佳方法是使用remember如下策略。

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n m HS.
  remember (S n) as Sn.
  remember (S m) as Sm.
  induction HS as [ n' | n' m' H IH].
  - (* le_n *)
    rewrite HeqSn in HeqSm. injection HeqSm as Heq.
    rewrite <- Heq. apply le_n.
  - (* le_S *) (* Stucks! *) Abort.

根据软件基础（第 1 卷：逻辑基础）

该策略remember e as x使 Coq (1) 将所有出现的表达式 e 替换为变量 x，并且 (2) 将方程 x = e 添加到上下文中。

不管怎样，虽然不可能用HS-imo-上的归纳来证明这个事实，但对-上进行归纳m就可以解决这个问题。（注意使用inversion。）

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros n.
  induction m as [|m' IHm'].
  - intros H. inversion H as [Hn | n' contra Hn'].
    + apply le_n.
    + inversion contra.
  - intros H. inversion H as [HnSm' | n' HSnSm' Heq].
    + apply le_n.
    + apply le_S. apply IHm'. apply HSnSm'.
Qed.