The Coq Standard Library

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.
Require Import Logic.

Open Scope nat_scope.

Definition eq_S := f_equal S.

Hint Resolve (f_equal S): v62.
Hint Resolve (f_equal (A:=nat)): core.

Definition pred (n:nat) : nat := match n with
                                 | O => n
                                 | S u => u
                                 end.
Hint Resolve (f_equal pred): v62.

Theorem pred_Sn : forall n:nat, n = pred (S n).

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 : forall n m:nat, n <> m -> S n <> S m.
Hint Resolve not_eq_S: core.

Definition IsSucc (n:nat) : Prop :=
  match n with
  | O => False
  | S p => True
  end.

Theorem O_S : forall n:nat, 0 <> S n.
Hint Resolve O_S: core.

Theorem n_Sn : forall n:nat, n <> S n.
Hint Resolve n_Sn: core.

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

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

Hint Resolve (f_equal2 plus): v62.
Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.

Lemma plus_n_O : forall n:nat, n = n + 0.
Hint Resolve plus_n_O: core.

Lemma plus_O_n : forall n:nat, 0 + n = n.

Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
Hint Resolve plus_n_Sm: core.

Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).

Notation plus_0_r_reverse := plus_n_O (compat "8.2").
Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2").

Fixpoint mult (n m:nat) : nat :=
  match n with
  | O => 0
  | S p => m + p * m
  end

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

Hint Resolve (f_equal2 mult): core.

Lemma mult_n_O : forall n:nat, 0 = n * 0.
Hint Resolve mult_n_O: core.

Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
Hint Resolve mult_n_Sm: core.

Notation mult_0_r_reverse := mult_n_O (compat "8.2").
Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2").

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O, _ => n
  | S k, O => n
  | S k, S l => k - l
  end

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

Inductive le (n:nat) : nat -> Prop :=
| le_n : n <= n
| le_S : forall m:nat, n <= m -> n <= S m

where "n <= m" := (le n m) : nat_scope.

Hint Constructors le: core.

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

Infix "<" := lt : nat_scope.

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

Infix ">=" := ge : nat_scope.

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

Infix ">" := gt : nat_scope.

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

Theorem le_pred : forall n m, n <= m -> pred n <= pred m.

Theorem le_S_n : forall n m, S n <= S m -> n <= m.

Theorem nat_case :
forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.

Theorem nat_double_ind :
forall R:nat -> nat -> Prop,
   (forall n:nat, R 0 n) ->
   (forall n:nat, R (S n) 0) ->
   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.

Fixpoint max n m : nat :=
  match n, m with
    | O, _ => m
    | S n´, O => n
    | 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.

Theorem max_l : forall n m : nat, m <= n -> max n m = n.

Theorem max_r : forall n m : nat, n <= m -> max n m = m.

Theorem min_l : forall n m : nat, n <= m -> min n m = n.

Theorem min_r : forall n m : nat, m <= n -> min n m = m.

Fixpoint nat_iter (n:nat) {A} (f:A->A) (x:A) : A :=
  match n with
    | O => x
    | S n´ => f (nat_iter n´ f x)
  end.

Lemma nat_iter_succ_r n {A} (f:A->A) (x:A) :
  nat_iter (S n) f x = nat_iter n f (f x).

Theorem nat_iter_plus :
  forall (n m:nat) {A} (f:A -> A) (x:A),
    nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).

Library Coq.Init.Peano