证明Coq中“小于”关系的证据

Question

我正在研究Sn_le_Sm__n_le_m的IndProp.v中以下定理IndProp.v的证明。

Software Foundations (Vol 1: Logical Foundations)

其中

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_n）？

Answer 1

这里的主要问题-我认为-不可能在induction HS上使用归纳法来证明定理，因为没有关于HS的假设，仅凭n的假设就无法说些什么，因为[ C0]请勿更改S n的值。但是无论如何，在第一个项目符号le之后没有进行假设的原因是因为调用n具有用与每个构造函数相对应的值替换所有出现的property参数的作用，并且在这种情况下无济于事替换-一词在任何地方都没有提及。有一些技巧可以避免这种情况。例如，您可以将[n]替换为induction，如下所示：

S 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 -imo-上使用归纳法这一事实，但对

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.

进行归纳法将解决这种情况。 （请注意HS的使用。）

m