CoQ中的良基归纳

Question

假设我知道某些自然数是好的。我知道1是好的，如果n是好的，则3n也是好的，如果n是好的，则n + 5也是好的，这些是构造好数字的唯一方法。在Coq中，我认为这个问题的适当形式化是：

Inductive good : nat -> Prop :=
  | g1 : good 1
  | g3 : forall n, good n -> good (n * 3)
  | g5 : forall n, good n -> good (n + 5).

然而，尽管显而易见，0不好的事实似乎无法使用此定义进行证明（因为在反演时，在g3的情况下，假设只会得到相同的结果）。

现在，究竟什么是好数字并不那么明显。看起来我并不需要完全描述它们就能知道0不好。例如，我只需进行少量反演就可以知道2不好。

- Veky

Answer 1

这个问题需要归纳法。而归纳法需要一些谓词 P : nat -> Prop 来配合使用。像 (fun n => ~good 0) 这样的原始（常量）谓词并没有什么用处：你将无法证明基础情况 1 (对应构造函数 g1)，因为谓词 "忘记" 了它的参数。

所以你需要证明一些逻辑上等价（或更强）的陈述，这些陈述将很容易地给你所需的谓词。 一个这样的等价语句是 forall n, good n -> n > 0，你可以后来用它来反驳 good 0。相应的谓词 P 是 (fun n => n > 0)。

Require Import Coq.Arith.Arith.
Require Import Coq.omega.Omega.

Inductive good : nat -> Prop :=
  | g1 : good 1
  | g3 : forall n, good n -> good (n * 3)
  | g5 : forall n, good n -> good (n + 5).

Lemma good_gt_O: forall n, good n -> n > 0.
Proof.
  intros n H. induction H; omega.
Qed.

Goal ~ good 0.
  intro H. now apply good_ge_O in H.
Qed.

以下是上述等式的证明：

Lemma not_good0_gt_zero_equiv_not_good0 :
  (forall n, good n -> n > 0) <-> ~ good 0.
Proof.
  split; intros; firstorder.
  destruct n; [tauto | omega].
Qed.

很容易证明@eponier的回答中隐含的forall n, n = 0 -> ~ good n与~ good 0等价。

Lemma not_good0_eq_zero_equiv_not_good0 :
  (forall n, n = 0 -> ~ good n) <-> ~ good 0.
Proof.
  split; intros; subst; auto.
Qed.

现在，用来证明forall n, n = 0 -> ~ good n的相应谓词是fun n => n = 0 -> False。可以通过手动应用由Coq自动生成的goal_ind归纳原理来证明这一点。

Example not_good_0_manual : forall n, n = 0 -> ~ good n.
Proof.
  intros n Eq contra.
  generalize Eq.
  refine (good_ind (fun n => n = 0 -> False) _ _ _ _ _);
    try eassumption; intros; omega.
Qed.

generalize Eq.将n = 0作为当前目标的前提条件。如果没有它，要证明的目标将是False，相应的谓词将再次变成无聊的fun n => False。

- Anton Trunov

---

实际上，在我看来，“x是3的幂”的正确定义应该是存在n，n ^ 3 == x。 - ejgallego

@ejgallego说：“2的幂指的是形如2^n的数字，其中n是整数”（来自这里），因此类比可得：3^k是3的幂。n^3是n的立方。 - Anton Trunov

@Veky，如果你在纸上都不确定，那么在Coq中尝试它就没有什么意义，除非我们正在谈论某些特殊情况。 - ejgallego

确定什么？0不在闭包中？是的，尽管我不知道闭包的总体描述，但我确信_那个_。好的，假设还有另一个构造函数。我已经更新了问题。 - Veky

@AntonTrunov 非常感谢。我稍微更喜欢 eponier 的答案，因为它似乎更普遍适用。 - Veky

Answer 2

实际上，当尝试证明good 0时，可以无限次地应用g3。这就是为什么我们认为此证明需要归纳法（并且我们可以看到在@AntonTrunov的解决方案中所需的辅助引理使用了归纳法）。同样的想法在http://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html#lab428定理loop_never_stop中也被使用。

Require Import Omega.

Example not_good_0 : ~ good 0.
Proof.
  intros contra. remember 0 as n. induction contra.
  discriminate. apply IHcontra. omega. omega.
Qed.

- eponier

---

“记住0为n”是该解决方案的关键组成部分。它在某种程度上用“对于所有的n，如果n=0，那么~good n”取代了原来的语句。回答很好！ - Anton Trunov

@Veky 我找到了《软件基础》中讨论这个问题的确切段落http://www.cis.upenn.edu/~bcpierce/sf/current/MoreInd.html#lab341（归纳的概括）。 - eponier

@Veky SF，v3.2：“问题在于对于 Prop 类型的归纳只能在完全通用的 Prop 实例中正常工作，即其中所有参数都是自由变量。因此它的行为更像 destruct 而不是 inversion。当你想使用 induction 时，通常表明你需要证明更一般的东西。但在某些情况下，将任何具体的参数拆分成单独的等式就足够了，例如：∀n，n=1→¬beautiful n。还有一个叫做 remember 的策略可以从原始状态生成第二个证明状态。” - Anton Trunov

@AntonTrunov 謝謝你。所以，唯一神秘的是：在n = 1的上下文中，證明 ~ beautiful n 的方式有何具體之處（這也是 remember 要求你做的）比證明 ~ beautiful 1 更"更一般化"。 - Veky

@AntonTrunov 那正是我所指的段落，谢谢。旧版本的正确链接是http://www.cis.upenn.edu/~bcpierce/sf/sf-3.2/MoreInd.html#lab341。 - eponier