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不好

Answer 1

这个问题需要归纳。归纳法需要一些谓词 P : nat -> Prop 才能使用。像 (fun n => ~good 0) 这样的原始（常量）谓词不会给你太多：你将无法证明 1 的基本情况（对应于构造函数 g1），因为谓词 "forgets" 它的论点。

因此您需要证明一些逻辑上等价（或更强）的陈述，这些陈述很容易为您提供必要的谓词。这种等价陈述的一个例子是 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。

Answer 2

确实，g3 在试图反驳 good 0 时可以被应用无限次。这就是为什么我们可以认为这个证明需要 induction（并且我们可以看到@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.

CoQ 中有根据的归纳

Wellfounded induction in CoQ

coq

induction