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

- best wish

Answer 1

证明中不需要归纳，因为 Coq 库中有足够的引理可以使用。 要查找这些引理，我使用了 SearchAbout 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的归纳根本没有推进证明，因为无法从S n >= m推导出归纳假设的前提条件（不能推导出n >= m）。虽然归纳是一个重要的构建块，但并不总是正确的工具。

- Atsby

Answer 2

如@Atsby所说，该库中已经有有用的引理，因此您可以执行以下操作：

Require Import NPeano.
Require Import Omega.

Lemma mod_diff : forall n m : nat, n>=m /\ m <> 0 -> (n - m) mod m = n mod m.
  intros n m [H1 H2].
  rewrite <- (Nat.mod_add _ 1); try rewrite mult_1_l, Nat.sub_add; auto.
Qed.

关于你如何用归纳法做这个问题的问题，我的通用建议是尽可能得到一个最普遍的归纳假设，即在进行归纳之前不要引入量化变量。此外，还要尽可能获得可用于“下一个”值的归纳假设。因此，我建议证明另一个公式 (n + k * m) mod m = n mod m 并对 k 进行归纳，因为只需要进行代数重写就可以从 k 证明 k+1 情况。但是，在这种情况下，“其他公式”已经在库中了，称为 Nat.sub_add。

- larsr

---

不错。不知怎么的，我错过了Nat.sub_add，毫无疑问部分原因是交换n和m对大脑非常困惑 ;) - Atsby

谢谢。我尝试了对 (n + k * m) mod m = n mod m 进行归纳，至少这个方法是可行的。 引理 mod_t: forall n m k, m > 0 -> (n + k * m) mod m = n mod m. 归纳 k; intro。 简化。重写 Nat.add_0_r。平凡。 重写 <- IHk。对称。重写 <- (Nat.mod_add _ 1)。 重写 <- plus_assoc。重写 Nat.mul_add_distr_r with(p:=m)(n:=k)(m:=1)。 重写 Nat.add_1_r。平凡。 omega。假设。 Qed. - best wish

干得好！您还可以更多地使用omega。如果您使用“replace”进行代数操作并以“omega”结束，将使证明更易于理解。像这样：引理mod_t：对于所有n，m，k，m> 0，（n + k * m）mod m = n mod m。归纳k;介绍H。自动使用Nat.add_0_r。重写<-IHk，<-（Nat.mod_add（_ + k * _）1）;替换（n + Sk * m）为（n + km + 1 * m）;简化;汽车;欧米茄。Qed. - larsr

Answer 3

你应该使用不同的归纳原理。

mod 函数遵循以下关系。

Inductive mod_rel : nat -> nat -> nat -> Prop :=
  | mod_rel_1 : forall n1 n2, n2 = 0 -> mod_rel n1 n2 0
  | mod_rel_2 : forall n1 n2, n2 > 0 -> n1 < n2 -> mod_rel n1 n2 n1
  | mod_rel_3 : forall n1 n2 n3, n2 > 0 -> n1 >= n2 -> mod_rel (n1 - n2) n2 n3 -> mod_rel n1 n2 n3.

在标准数学中，通常假定对零取模是未定义的。 事实上，在涉及到取模的所有定理中，第二个参数都有前提条件，即不为零，因此无论对零取模是否已定义都并不重要。

以下是mod函数的定义域。

Inductive mod_dom : nat -> nat -> Prop :=
  | mod_dom_1 : forall n1 n2, n2 = 0 -> mod_dom n1 n2
  | mod_dom_2 : forall n1 n2, n2 > 0 -> n1 < n2 -> mod_dom n1 n2
  | mod_dom_3 : forall n1 n2, n2 > 0 -> n1 >= n2 -> mod_dom (n1 - n2) n2 -> mod_dom n1 n2.

在Coq中只有总函数，所以任何一对自然数都在mod的定义域内。这可以通过良序归纳和情况分析来证明。

Conjecture wf_ind : forall P1, (forall n1, (forall n2, n2 < n1 -> P1 n2) -> P1 n1) -> forall n1, P1 n1.
Conjecture O_gt : forall n1, n1 = 0 \/ n1 > 0.
Conjecture lt_ge : forall n1 n2, n1 < n2 \/ n1 >= n2.

Conjecture mod_total : forall n1 n2, mod_dom n1 n2.

与 mod 域相关的归纳原理是：

Check mod_dom_ind : forall P1 : nat -> nat -> Prop,
  (forall n1 n2, n2 = 0 -> P1 n1 n2) ->
  (forall n1 n2, n2 > 0 -> n1 < n2 -> P1 n1 n2) ->
  (forall n1 n2, n2 > 0 -> n1 >= n2 -> mod_dom (n1 - n2) n2 -> P1 (n1 - n2) n2 -> P1 n1 n2) ->
  forall n1 n2, mod_dom n1 n2 -> P1 n1 n2.

但由于mod是总的，因此可以将其简化为

Conjecture mod_ind : forall P1 : nat -> nat -> Prop,
  (forall n1 n2, n2 = 0 -> P1 n1 n2) ->
  (forall n1 n2, n2 > 0 -> n1 < n2 -> P1 n1 n2) ->
  (forall n1 n2, n2 > 0 -> n1 >= n2 -> P1 (n1 - n2) n2 -> P1 n1 n2) ->
  forall n1 n2, P1 n1 n2.

这个归纳原则适用于任何一对自然数。它更适合证明与“mod”有关的事实，因为它遵循“mod”的定义结构。“mod”不能直接使用结构递归来定义，因此在证明与“mod”有关的内容时，结构归纳只能帮助你到一定程度。

但并不是所有的证明都应该采用归纳法。你需要问自己为什么相信某些事情是真实的，并将其转化为严谨的证明。如果你不确定它为什么是真的，你需要学习或发现为什么它是或不是真的。

但是，除法和模运算可以通过结构递归间接地进行定义。在以下函数中，“n3”和“n4”作为中间商和余数。你通过减小被除数并增加余数来定义它，直到余数达到除数为止，在这一点上，你增加商并重置余数并继续。当被除数达到零时，你就得到了真正的商和余数（假设你没有除以零）。

Conjecture ltb : nat -> nat -> bool.

Fixpoint div_mod (n1 n2 n3 n4 : nat) : nat * nat :=
  match n1 with
  | 0 => (n3, n4)
  | S n1 => if ltb (S n4) n2
    then div_mod n1 n2 n3 (S n4)
    else div_mod n1 n2 (S n3) 0
  end.

Definition div (n1 n2 : nat) : nat := fst (div_mod n1 n2 0 0).

Definition mod (n1 n2 : nat) : nat := snd (div_mod n1 n2 0 0).

你仍然没有使用结构归纳来证明关于

和的事情。你使用它来证明关于的事情。 这些函数对应于以下（结构归纳）定理。

Theorem augmented_division_algorithm : forall n1 n2 n3 n4, n4 < n2 ->
  exists n5 n6, n1 + n3 * n2 + n4 = n5 * n2 + n6 /\ n6 < n2.
Proof.
induction n1.
firstorder.
exists n3.
exists n4.
firstorder.
firstorder.
destruct (lt_ge (S n4) n2).
specialize (IHn1 n2 n3 (S n4) H0).
firstorder.
exists x.
exists x0.
firstorder.
admit. (* H1 implies the conclusion. *)
Conjecture C2 : forall n1 n2, n1 < n2 -> 0 < n2.
pose proof (C2 _ _ H).
specialize (IHn1 n2 (S n3) 0).
firstorder.
exists x.
exists x0.
firstorder.
Conjecture C3 : forall n1 n2, n1 < n2 -> S n1 >= n2 -> S n1 = n2.
pose proof (C3 _ _ H H0).
subst.
cbn in *.
admit. (* H2 implies the conclusion. *)
Qed.

通常的除法算法可以通过将 n3 和 n4 设置为零来推导出。

Conjecture division_algorithm : forall n1 n2, 0 < n2 -> exists n5 n6,
  n1 = n5 * n2 + n6 /\ n6 < n2.

免责声明：猜测和简单类型函数。

- Partial