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
The predecessor function
Injectivity of successor
Zero is not the successor of a number
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.
Addition
Fixpoint plus (
n m:nat) {
struct n} :
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).
Standard associated names
Multiplication
Fixpoint mult (
n m:nat) {
struct n} :
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.
Standard associated names
Truncated subtraction: m-n is 0 if n>=m
Fixpoint minus (
n m:nat) {
struct n} :
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.
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 ->
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.
Case analysis
Theorem nat_case :
forall (
n:nat) (
P:nat ->
Prop),
P 0 -> (
forall m:nat,
P (
S m)) ->
P n.
Principle of double induction
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.