我想对Peano nats进行归纳，但我想证明属性P超过nats 1 ... n。 Coq是否提供了这样做的策略/工具？

Posted 2021-04-10

我想证明自然数不包括0的东西。所以我的属性P的基本情况是P 1而不是P 0。

我正在考虑使用n> = 0作为目标中的假设，但是在Coq中有另一种方法吗？

答案

只需添加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.

另一答案

考虑将财产转移到所有nats上的财产。

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

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

另一答案

一种可能的变体是通过对属性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.

_ <= _顺序实际上被定义为归纳关系这一事实赋予了这种行为。