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.
#[
global]
Hint Resolve O_S:
core.
Theorem n_Sn :
forall n:
nat,
n <> S n.
#[
global]
Hint Resolve n_Sn:
core.
Addition
Standard associated names
Multiplication
Standard associated names
Truncated subtraction: m-n is 0 if n>=m
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.
Register le_n as num.nat.le_n.
#[
global]
Hint Constructors le:
core.
Definition lt (
n m:
nat) :=
S n <= m.
#[
global]
Hint Unfold lt:
core.
Infix "<" :=
lt :
nat_scope.
Definition ge (
n m:
nat) :=
m <= n.
#[
global]
Hint Unfold ge:
core.
Infix ">=" :=
ge :
nat_scope.
Definition gt (
n m:
nat) :=
m < n.
#[
global]
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.
Register le as num.nat.le.
Register lt as num.nat.lt.
Register ge as num.nat.ge.
Register gt as num.nat.gt.
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 le_0_n :
forall n, 0
<= n.
Theorem le_n_S :
forall n m,
n <= m -> S n <= S m.
Case analysis
Principle of double induction
Maximum and minimum : definitions and specifications