代码之家 › 专栏 › 技术社区 › best wish

模上的Coq归纳

induction coq modulo

best wish · 技术社区 · 9 年前

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

3 回复 | 直到 9 年前

Atsby 9 年前

归纳法不需要证明,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 . ( 编辑 :实际上,内置引理Natsub_add会起作用)。

因此,证明中的想法是首先证明一个引理,它允许你“加回去” m ,因为这似乎是一个有单独引理的好主意。然而,我想它也可以作为一个单一的证明。

事实上 n 根本不推进证明,因为没有办法证明归纳假设的前提条件 n>=米 从…起 S n >= m ). 虽然归纳法是一个重要的组成部分,但并不总是正确的工具。

larsr 9 年前

正如@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 .

Partial 9 年前

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

这个 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.

在标准数学中,通常假设模为零是未定义的。事实上,所有涉及模的定理都有第二个自变量不为零的前提条件,所以是否定义了零模并不重要。

以下是 摩登派青年 作用

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.

感应原理与 摩登派青年 的域为

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.

但从那时起 摩登派青年 总数,可以将其简化为

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.

这个归纳原理适用于任何一对自然数。它更适合证明以下事实 摩登派青年 因为遵循定义的结构 摩登派青年 . 摩登派青年 不能直接使用结构递归来定义,所以结构归纳只能在证明有关 摩登派青年 .

但并不是所有的证据都应该用归纳法来处理。你需要问问自己,为什么你相信某件事是真的,并将其转化为一个严格的证据。如果你不确定为什么它是真的,你需要学习或发现为什么它是或不是。

但除法和模可以通过结构递归间接定义。在以下功能中, 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 和 摩登派青年 。你用它来证明 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级 和 第4页 至零。

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

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