CODEWITHSUNDEEP
coq
Arjun Viswanathan
Arjun Viswanathan

Reputation: 319

I want to do induction on Peano nats but I want to prove a property P over nats 1 ... n. Does Coq provide a tactic/tool to do this?

I want to prove something for natural numbers not including 0. So my base case for property P would be P 1 instead of P 0.

I'm considering using n >= 0 as a hypothesis in the goal, but is there another way to do this in Coq?

Upvotes: 0

Views: 61

Answers (3)

Yves
Yves

Reputation: 4236

One possible variant is to perform directly a proof by induction on the property 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.

This behavior is granted by the fact that the order _ <= _ is actually defined as an inductive relation.

Upvotes: 0

larsr
larsr

Reputation: 5811

Just add n > 0 or n <> 0 as an assumption. Example:

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.

Upvotes: 0

Li-yao Xia
Li-yao Xia

Reputation: 33429

Consider shifting the property to become a property on all nats.

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

So forall n, n >= 1 -> P n is equivalent to forall n, P' n.

Upvotes: 5

Related Questions