coq - 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

确实，当试图反驳 good 0 时，g3 可以应用无数次。这就是为什么我们可以认为这个证明需要 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.