我想对 Peano nats 进行归纳，但我想证明 nats 1 的属性 P ..n.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.

Answer 2

只需添加n > 0或n <> 0作为假设。 例：

Require Import Arith.
Goal forall n, n > 0 -> forall a, a = n - 1 -> a + 1 = n.
  induction n; intros H.
  - now apply Nat.nlt_0_r in H.  (* This case, 0 > 0, is simply impossible *)
  - intros a H1.
    now rewrite H1; simpl; rewrite Nat.sub_0_r, Nat.add_comm.
Qed.

Answer 3

一种可能的变体是通过对属性0 <= n的归纳直接执行证明。

Require Import Arith.
Goal forall n, 1 <= n -> forall a, a = n - 1 -> a + 1 = n.
induction 1.
(* first case being considered is P 1. *)
   now intros a a0; rewrite a0.
now simpl; intros a a_m; rewrite a_m, Nat.add_1_r, Nat.sub_0_r.
Qed.

这种行为是由_ <= _阶实际上被定义为归纳关系这一事实授予的。