我想对Peano螺帽进行归纳，但我想证明螺帽1 ... n上的性质P。Coq是否提供策略/工具来做到这一点？

Question

我想证明不包含0的自然数。因此，我对属性P的基本情况应为P 1而不是P 0。

我正在考虑使用n> = 0作为目标假设，但是在Coq中还有另一种方法可以做到这一点吗？

Answer 1

考虑将属性转变为所有上nat的属性。

Definition P' (n : nat) := P (S n).

所以forall n, n >= 1 -> P n等于forall n, P' n。