5

I'm new with coq and i really have difficulty in applying the induction. as long as I can use theorems from the library, or tactics such as omega, all this is "not a problem". But as soon as these do not work, I'm always stuck.

To be precise, now i try to prove

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

the case n = 0 I already have.

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

But how to make the induction step?

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
4

3 回答 3

5

证明不需要归纳，Coq 库中有足够的引理可以使用。为了找到这些引理，我使用了SeachAbout moduloand 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）。虽然归纳是一个重要的组成部分，但它并不总是正确的工具。

于 2015-03-21T23:35:58.333 回答
4

正如@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。而且，尝试得到一个对“下一个”值也有用的归纳假设。因此，我将尝试证明另一个公式(n + k * m) mod m = n mod m并对 进行归纳k，因为那时只需要代数重写来k+1证明k. 但是，在这种情况下，“其他公式”已经在库中，称为Nat.sub_add.

于 2015-03-22T06:25:50.533 回答
2

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

该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).

您仍然不使用结构归纳来证明关于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.

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

于 2015-03-24T16:12:23.193 回答