modulo - 模上的Coq归纳

我是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

最佳答案

证明不是必要的归纳法，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来证明重写实例似乎无法用作内置引理。这有点棘手，因为使用nat不能正常工作，只有在n >= m时才有效。 (编辑:实际上内置的引理Nat.sub_add就可以了)。

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

的确，对n的归纳根本没有推进证明，因为没有办法显示归纳假设的前提(无法从n >= m导出S n >= m)。虽然归纳是一个重要的构建块，但它并不总是正确的工具。

关于modulo - 模上的Coq归纳，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/29189073/