Coq：证明 < 和 ≤ 之间的关系

Question

我现在正在学习 Coq，在一个更大的证明中，我被以下子证明难住了：

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.

或者，展开后：

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → S n ≤ m.

这里，"n ≤ m"归纳定义如下：

  Inductive le : nat → nat → Prop :=
  | le_n : ∀ n : nat, le n n
  | le_S : ∀ n m : nat, (le n m) → (le n (S m)).

我还没有走多远，但我的尝试是这样的：

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.
  Proof.
    unfold lt.
    intro n.
    induction n.
    - induction m.
      + intros. exfalso. contradiction.
      + admit.
    - admit.
  Admitted.

在第一个归纳步骤中（以第一个承认为标记），归纳假设如下：

1 subgoal
m : nat
IHm : 0 ≤ m → 0 ≠ m → 1 ≤ m
______________________________________(1/1)
0 ≤ S m → 0 ≠ S m → 1 ≤ S m

我不确定如何利用这个假设来证明子目标。我将不胜感激任何正确方向的指导。

Answer 1

由于 le 被定义为归纳谓词，因此对其进行归纳比 n 更有意义。 le 没有对 0 甚至 S n 进行任何引用（它确实有 S m），因此对 n 进行归纳可能不是可行的方法. m 的归纳可能 有效，但可能比必要的更难。

在开始正式证明之前，考虑一下如何非正式地证明这一点（尽管仍然使用相同的定义）通常会很有帮助。如果假设 n ≤ m，那么根据 lt 的归纳定义，这意味着 n 和 m 相同，或者 m 是后继者一些数字 m' 和 n 小于或等于 m'（你能明白为什么 lt 的定义暗示了这一点吗？）。在第一种情况下，我们必须使用附加假设 n ≠ m 来得出矛盾。在第二种情况下，我们甚至不需要它。 n ≤ m' 意味着 S n ≤ S m'，因此由于 m = S m'、S n ≤ m，即 n < m.

为了形式化，我们必须证明最后一行的假设 n ≤ m 意味着 S n ≤ S m。您应该尝试类似的非正式分析来证明这一点。除此之外，非正式证明应该很容易形式化。 H: n ≤ m的案例分析就是destruct H..

还有一件事。这不是必需的，但通常可以帮助运行。在定义归纳类型（或谓词）时，如果可以分解出在每个构造函数中以相同方式使用的参数，则可以使归纳原理更加强大。您使用 le、n 的方式是普遍量化的，并且对两个构造函数使用相同的方式。 le 的每个实例都以 le n.

开头

  Inductive le : nat → nat → Prop :=
  | le_n : ∀ n : nat, le n n
  | le_S : ∀ n m : nat, (le n m) → (le n (S m)).

这意味着我们可以将该索引分解为参数。

  Inductive le' (n: nat) : nat → Prop :=
  | le_n' : le' n n
  | le_S' : ∀ m : nat, (le' n m) → (le' n (S m)).

这里稍微给大家介绍一下simpler/better归纳原理

le'_ind
     : forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, le' n m -> P m -> P (S m)) ->
       forall n0 : nat, le' n n0 -> P n0

将此与 le_ind 进行比较。

le_ind
     : forall P : nat -> nat -> Prop,
       (forall n : nat, P n n) ->
       (forall n m : nat, le n m -> P n m -> P n (S m)) ->
       forall n n0 : nat, le n n0 -> P n n0

基本上这里发生的事情是 le_ind，你必须证明每个 n 的一切。使用 le'_ind，您只需证明您正在使用的特定 n。这有时可以简化证明，尽管这对于定理的证明不是必需的。证明这两个谓词等价是一个很好的练习。

Coq：证明 < 和 ≤ 之间的关系

Coq: Proving relation between < and ≤

coq

proof

coq-tactic