coq - coq 中 "less than"关系的证据归纳

Question

我正在研究以下定理的证明 Sn_le_Sm__n_le_m在 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案例在 induction 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.

根据 Software Foundations (Vol 1: Logical Foundations)

The tactic remember e as x causes Coq to (1) replace all occurrences of the expression e by the variable x, and (2) add an equation x = e to the context.

无论如何，虽然不可能在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.