modulo - Coq 模数归纳

Question

我是 coq 新手，我在应用归纳法方面确实遇到困难。只要我能使用图书馆里的定理，或者诸如omega之类的策略，这一切都“不是问题”。但一旦这些不起作用，我就会陷入困境。

准确地说，现在我试图证明

Lemma mod_diff : forall n m : nat, n>=m /\ m <> 0 -> (n - m) mod m = n mod m.

我已经有了 n = 0 的情况。

Proof.
    intros. destruct H as [H1 H2 ]. induction n.
      rewrite Nat.mod_0_l by omega. rewrite Nat.mod_0_l; omega.

但是如何进行归纳步骤呢？

1 subgoal
n : nat
m : nat
H1 : S n >= m
H2 : m <> 0
IHn : n >= m -> (n - m) mod m = n mod m
______________________________________(1/1)
(S n - m) mod m = S n mod m

Answer 1

证明不需要归纳法，Coq 库中有足够的引理可以使用。为了找到这些引理，我使用了 SeachAbout modulo 和 SearchAbout plus。

然后，我做了:

Lemma mod_add_back: forall n m : nat, m <> 0 -> ((n + m) mod m) = (n mod m).
intros.
rewrite Nat.add_mod.
rewrite Nat.mod_same.
rewrite plus_0_r.
rewrite Nat.mod_mod.
reflexivity.
assumption.
assumption.
assumption.
Qed.

Lemma mod_diff: forall n m : nat, n >= m /\ m <> 0 -> (n - m) mod m = n mod m.
intros.
intuition.
rewrite <- mod_add_back.
assert ((n - m + m) = n) by omega.
rewrite H.
reflexivity.
intuition.
Qed.

请注意使用 assert ... by omega 来证明重写的实例，该实例似乎无法用作内置引理。这有点棘手，因为对于 nats，它通常不起作用，但只有在 n >= m 时才有效。 (编辑:实际上内置引理 Nat.sub_add 会起作用)。

因此，证明中的想法是首先证明一个引理，该引理允许您“加回”m，因为拥有单独的引理似乎是一个好主意。然而，我想它也可以作为一个单一的证明来完成。

事实上，对n的归纳根本不能推进证明，因为没有办法显示归纳假设的前提条件(无法推导出n >= m来自S n >= m)。虽然归纳法是一个重要的组成部分，但它并不总是正确的工具。