Library Coq.Arith.EqNat
Equality on natural numbers
Open
Local
Scope
nat_scope
.
Implicit
Types
m
n
x
y
:
nat
.
Propositional equality
Fixpoint
eq_nat
n
m
{
struct
n
} :
Prop
:=
match
n
,
m
with
|
O
,
O
=>
True
|
O
,
S
_
=>
False
|
S
_
,
O
=>
False
|
S
n1
,
S
m1
=>
eq_nat
n1
m1
end
.
Theorem
eq_nat_refl
:
forall
n
,
eq_nat
n
n
.
Hint
Resolve
eq_nat_refl
:
arith
v62
.
eq
restricted to
nat
and
eq_nat
are equivalent
Lemma
eq_eq_nat
:
forall
n
m
,
n
=
m
->
eq_nat
n
m
.
Hint
Immediate
eq_eq_nat
:
arith
v62
.
Lemma
eq_nat_eq
:
forall
n
m
,
eq_nat
n
m
->
n
=
m
.
Hint
Immediate
eq_nat_eq
:
arith
v62
.
Theorem
eq_nat_is_eq
:
forall
n
m
,
eq_nat
n
m
<->
n
=
m
.
Theorem
eq_nat_elim
:
forall
n
(
P
:nat ->
Prop
),
P
n
->
forall
m
,
eq_nat
n
m
->
P
m
.
Theorem
eq_nat_decide
:
forall
n
m
, {
eq_nat
n
m
} + {~
eq_nat
n
m
}.
Boolean equality on
nat
Fixpoint
beq_nat
n
m
{
struct
n
} :
bool
:=
match
n
,
m
with
|
O
,
O
=>
true
|
O
,
S
_
=>
false
|
S
_
,
O
=>
false
|
S
n1
,
S
m1
=>
beq_nat
n1
m1
end
.
Lemma
beq_nat_refl
:
forall
n
,
true
=
beq_nat
n
n
.
Definition
beq_nat_eq
:
forall
x
y
,
true
=
beq_nat
x
y
->
x
=
y
.
Lemma
beq_nat_true
:
forall
x
y
,
beq_nat
x
y
=
true
->
x
=y.
Lemma
beq_nat_false
:
forall
x
y
,
beq_nat
x
y
=
false
->
x
<>y.