Library Coq.Init.Peano


The type nat of Peano natural numbers (built from O and S) is defined in Datatypes.v
This module defines the following operations on natural numbers :
  • predecessor pred
  • addition plus
  • multiplication mult
  • less or equal order le
  • less lt
  • greater or equal ge
  • greater gt
It states various lemmas and theorems about natural numbers, including Peano's axioms of arithmetic (in Coq, these are provable). Case analysis on nat and induction on nat × nat are provided too

Require Import Notations.
Require Import Datatypes.
Local Open Scope identity_scope.
Require Import Logic_Type.
Require Coq.Init.Nat.

Open Scope nat_scope.
Local Notation "0" := O.

Definition eq_S := f_equal S.

Local Definition f_equal_S := f_equal S.
Local Definition f_equal_nat := f_equal (A:=nat).
Hint Resolve f_equal_S : v62.
Hint Resolve f_equal_nat : core.

The predecessor function

Definition pred (n:nat) : nat := match n with
                                 | On
                                 | S uu
                                 end.

Theorem pred_Sn : n:nat, n = pred (S n).
Proof.
  simpl; reflexivity.
Qed.

Injectivity of successor

Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H.
Hint Immediate eq_add_S: core.

Theorem not_eq_S : n m:nat, n m S n S m.
Proof.
  red; auto.
Qed.
Hint Resolve not_eq_S: core.

Definition IsSucc (n:nat) : Type :=
  match n with
  | OFalse
  | S pTrue
  end.

Zero is not the successor of a number



addition

Fixpoint plus (n m:nat) : nat :=
  match n with
  | Om
  | S pS (p + m)
  end

where "n + m" := (plus n m) : nat_scope.

Local Definition f_equal2_plus := f_equal2 plus.
Local Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat).
Hint Resolve f_equal2_plus : v62.
Hint Resolve f_equal2_nat : core.

Lemma plus_n_O : n:nat, n = n + 0.
Proof.
  induction n; simpl; auto.
Qed.
Hint Resolve plus_n_O: core.

Lemma plus_O_n : n:nat, 0 + n = n.
Proof.
  auto.
Qed.

Lemma plus_n_Sm : n m:nat, S (n + m) = n + S m.
Proof.
  intros n m; induction n; simpl; auto.
Qed.
Hint Resolve plus_n_Sm: core.

Lemma plus_Sn_m : n m:nat, S n + m = S (n + m).
Proof.
  auto.
Qed.

Standard associated names

Notation plus_0_r_reverse := plus_n_O (only parsing).
Notation plus_succ_r_reverse := plus_n_Sm (only parsing).

Multiplication

Fixpoint mult (n m:nat) : nat :=
  match n with
  | O ⇒ 0
  | S pm + p × m
  end

where "n * m" := (mult n m) : nat_scope.

Local Definition f_equal2_mult := f_equal2 mult.
Hint Resolve f_equal2_mult : core.

Lemma mult_n_O : n:nat, 0 = n × 0.
Proof.
  induction n; simpl; auto.
Qed.
Hint Resolve mult_n_O: core.

Lemma mult_n_Sm : n m:nat, n × m + n = n × S m.
Proof.
  intros; induction n as [| p H]; simpl; auto.
  destruct H; rewrite <- plus_n_Sm; apply eq_S.
  pattern m at 1 3; elim m; simpl; auto.
Qed.
Hint Resolve mult_n_Sm: core.

Standard associated names

Notation mult_0_r_reverse := mult_n_O (only parsing).
Notation mult_succ_r_reverse := mult_n_Sm (only parsing).

Truncated subtraction: m-n is 0 if nm

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O, _n
  | S k, On
  | S k, S lk - l
  end

where "n - m" := (minus n m) : nat_scope.

Definition of the usual orders, the basic properties of le and lt can be found in files Le and Lt

Inductive le (n:nat) : nat Type :=
  | le_n : le n n
  | le_S : m:nat, le n m le n (S m).
Local Notation "n <= m" := (le n m) : nat_scope.

Hint Constructors le: core.

Definition lt (n m:nat) := S n m.
Hint Unfold lt: core.

Local Infix "<" := lt : nat_scope.

Definition ge (n m:nat) := m n.
Hint Unfold ge: core.

Local Infix ">=" := ge : nat_scope.

Definition gt (n m:nat) := m < n.
Hint Unfold gt: core.

Local Infix ">" := gt : nat_scope.

Local Notation "x <= y <= z" := (x y y z) : nat_scope.
Local Notation "x <= y < z" := (x y y < z) : nat_scope.
Local Notation "x < y < z" := (x < y y < z) : nat_scope.
Local Notation "x < y <= z" := (x < y y z) : nat_scope.

Theorem le_pred : n m, n m pred n pred m.
Proof.
induction 1; auto. destruct m; simpl; auto.
Qed.

Theorem le_S_n : n m, S n S m n m.
Proof.
intros n m. exact (le_pred (S n) (S m)).
Qed.

Case analysis

Theorem nat_case :
  (n:nat) (P:nat Type), P 0 ( m:nat, P (S m)) P n.
Proof.
  induction n; auto.
Qed.

Principle of double induction

Theorem nat_double_ind :
  R:nat nat Type,
   ( n:nat, R 0 n)
   ( n:nat, R (S n) 0)
   ( n m:nat, R n m R (S n) (S m)) n m:nat, R n m.
Proof.
  induction n; auto.
  destruct m; auto.
Qed.

Maximum and minimum : definitions and specifications

Fixpoint max n m : nat :=
  match n, m with
    | O, _m
    | S n', On
    | S n', S m'S (max n' m')
  end.

Fixpoint min n m : nat :=
  match n, m with
    | O, _ ⇒ 0
    | S n', O ⇒ 0
    | S n', S m'S (min n' m')
  end.





nth iteration of the function f

Fixpoint nat_iter (n:nat) {A} (f:AA) (x:A) : A :=
  match n with
    | Ox
    | S n'f (nat_iter n' f x)
  end.

Lemma nat_iter_succ_r n {A} (f:AA) (x:A) :
  nat_iter (S n) f x = nat_iter n f (f x).
Proof.
  induction n; intros; simpl; rewrite <- ?IHn; trivial.
Qed.

Theorem nat_iter_plus :
   (n m:nat) {A} (f:A A) (x:A),
    nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
Proof.
  induction n; intros; simpl; rewrite ?IHn; trivial.
Qed.

Preservation of invariants : if f : AA preserves the invariant Inv, then the iterates of f also preserve it.

Theorem nat_iter_invariant :
   (n:nat) {A} (f:A A) (P : A Type),
    ( x, P x P (f x))
     x, P x P (nat_iter n f x).
Proof.
  induction n; simpl; trivial.
  intros A f P Hf x Hx. apply Hf, IHn; trivial.
Qed.