Library Coq.Numbers.Natural.Abstract.NBase

Require Export Decidable.
Require Export NAxioms.
Require Import NZProperties.

Module NBaseProp (Import N : NAxiomsMiniSig´).

First, we import all known facts about both natural numbers and integers.

Include NZProp N.

From pred_0 and order facts, we can prove that 0 isn't a successor.

Theorem neq_succ_0 : forall n, S n ~= 0.

Theorem neq_0_succ : forall n, 0 ~= S n.

Next, we show that all numbers are nonnegative and recover regular induction from the bidirectional induction on NZ

Theorem le_0_l : forall n, 0 <= n.

Theorem induction :
forall A : N.t -> Prop, Proper (N.eq ==>iff) A ->
A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.

The theorems bi_induction, central_induction and the tactic nzinduct refer to bidirectional induction, which is not useful on natural numbers. Therefore, we define a new induction tactic for natural numbers. We do not have to call "Declare Left Step" and "Declare Right Step" commands again, since the data for stepl and stepr tactics is inherited from NZ.

Ltac induct n := induction_maker n ltac:(apply induction).

Theorem case_analysis :
forall A : N.t -> Prop, Proper (N.eq ==>iff) A ->
A 0 -> (forall n, A (S n)) -> forall n, A n.

Ltac cases n := induction_maker n ltac:(apply case_analysis).

Theorem neq_0 : ~ forall n, n == 0.

Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m.

Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m.

Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1.

Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n.

Theorem pred_inj : forall n m, n ~= 0 -> m ~= 0 -> P n == P m -> n == m.

The following induction principle is useful for reasoning about, e.g., Fibonacci numbers

Section PairInduction.

Variable A : N.t -> Prop.
Hypothesis A_wd : Proper (N.eq ==>iff) A.

Theorem pair_induction :
A 0 -> A 1 ->
(forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n.

End PairInduction.

The following is useful for reasoning about, e.g., Ackermann function

Section TwoDimensionalInduction.

Variable R : N.t -> N.t -> Prop.
Hypothesis R_wd : Proper (N.eq ==>N.eq ==>iff) R.

Theorem two_dim_induction :
   R 0 0 ->
   (forall n m, R n m -> R n (S m)) ->
   (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m.

End TwoDimensionalInduction.

Section DoubleInduction.

Variable R : N.t -> N.t -> Prop.
Hypothesis R_wd : Proper (N.eq ==>N.eq ==>iff) R.

Theorem double_induction :
   (forall m, R 0 m) ->
   (forall n, R (S n) 0) ->
   (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m.

End DoubleInduction.

Ltac double_induct n m :=
  try intros until n;
  try intros until m;
  pattern n, m; apply double_induction; clear n m;
  [solve_proper | | | ].

End NBaseProp.