Я хочу сделать индукцию на Peano nats, но я хочу доказать свойство P над nats 1 ... 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

Одним из возможных вариантов является прямое индуктивное доказательство свойства 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.

Такое поведение обеспечивается тем фактом, что порядок _ <= _ фактически определяется как индуктивное отношение..

Answer 3

Просто добавьте 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.