Library Coq.setoid_ring.ArithRing
Require
Import
Mult
.
Require
Import
BinNat
.
Require
Import
Nnat
.
Require
Export
Ring
.
Set Implicit Arguments
.
Lemma
natSRth
:
semi_ring_theory
O
(
S
O
)
plus
mult
(@
eq
nat
).
Lemma
nat_morph_N
:
semi_morph
0 1
plus
mult
(
eq
(
A
:=
nat
))
0%
N
1%
N
N.add
N.mul
N.eqb
N.to_nat
.
Ltac
natcst
t
:=
match
isnatcst
t
with
true
=>
constr
:(
N.of_nat
t
)
|
_
=>
constr
:(
InitialRing.NotConstant
)
end
.
Ltac
Ss_to_add
f
acc
:=
match
f
with
|
S
?
f1
=>
Ss_to_add
f1
(
S
acc
)
|
_
=>
constr
:((
acc
+
f
)%
nat
)
end
.
Ltac
natprering
:=
match
goal
with
|-
context
C
[
S
?
p
] =>
match
p
with
O
=>
fail
1
|
p
=>
match
isnatcst
p
with
|
true
=>
fail
1
|
false
=>
let
v
:=
Ss_to_add
p
(
S
0)
in
fold
v
;
natprering
end
end
|
_
=>
change
N.to_nat
with
protected_to_nat
end
.
Ltac
natpostring
:=
match
goal
with
| |-
context
[
N.to_nat
?
x
] =>
let
v
:=
eval
cbv
in
(
N.to_nat
x
)
in
change
(
N.to_nat
x
)
with
v
;
natpostring
|
_
=>
change
protected_to_nat
with
N.to_nat
end
.
Add
Ring
natr
:
natSRth
(
morphism
nat_morph_N
,
constants
[
natcst
],
preprocess
[
natprering
],
postprocess
[
natpostring
]).