关于模数的Coq归纳

Question

我是新的coq,我真的很难应用感应.只要我可以使用图书馆的定理,或者像欧米茄这样的策略,这一切都"不是问题".但是一旦这些不起作用,我就会被困住.

确切地说,现在我试图证明

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用于证明重写的实例似乎不是可用的内置引理.这有点棘手,因为使用nat它一般不起作用,但仅限于n >= m.(编辑:实际上内置的引理Nat.sub_add会工作).

因此,证明中的想法是首先证明一个允许你"加回"的引理m,因为这似乎是一个好主意,有一个单独的引理.但是,我想它也可以作为单一的证据来完成.

事实上,归纳于n不前进的证据可言,因为没有办法显示归纳假设(不能推导的前提条件n >= m从S n >= m).虽然归纳是一个重要的构建块,但它并不总是正确的工具.