Coq 模数归纳法

Question

我是 coq 的新手，我真的很难应用归纳法。只要能用到图书馆的定理，或者omega之类的战术，这都是"not a problem"。但是一旦这些不起作用，我总是被卡住。

准确的说，现在我尝试证明

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 会起作用）。

所以证明中的想法是首先证明一个引理，它允许你 "add back" m，因为这似乎是一个单独的引理的好主意。但是，我想它也可以作为一个单一的证明来完成。

的确，对n的归纳根本没有推进证明，因为无法证明归纳假设的前提条件（无法从S n >= m推导出n >= m） .虽然归纳是一个重要的组成部分，但它并不总是正确的工具。

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.

关于你关于如何使用归纳法进行归纳的问题，我的一般建议是获得一个尽可能通用的归纳假设，即在你这样做之前不要引入量化变量 induction。而且，尝试获得对 "the next" 值也有用的归纳假设。因此，我会尝试证明另一个公式 (n + k * m) mod m = n mod m 并对 k 进行归纳，因为这样只需要代数重写就可以证明 k 的 k+1 情况。但是，在这种情况下，'other formula' 已经在库中，称为 Nat.sub_add。

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.

在标准数学中，通常假设 modulo by zero 是未定义的。事实上，所有涉及 modulo 的定理都以第二个参数不为零为前提，因此是否定义 modulo by zero 并不重要。

以下是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.

的事情时，结构归纳法只能让你走到这一步

虽然不是每个证明都应该用归纳来解决。你需要问问自己，为什么你相信某件事是真的，并将其转化为严格的证据。如果您不确定为什么它是真的，您需要了解或发现它为什么是或不是。

但是除法和modulo可以通过结构递归间接定义。在下面的函数中，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).

关于div和mod的事情，你还是不用结构归纳法来证明。你用它来证明关于div_mod的事情。这些函数对应于以下（结构归纳）定理。

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.

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

Coq 模数归纳法

Coq induction on modulo

modulo

coq

induction