Library Coq.nsatz.Nsatz
Require
Import
List
.
Require
Import
Setoid
.
Require
Import
BinPos
.
Require
Import
BinList
.
Require
Import
Znumtheory
.
Require
Export
Morphisms
Setoid
Bool
.
Require
Export
Algebra_syntax
.
Require
Export
Ncring
.
Require
Export
Ncring_initial
.
Require
Export
Ncring_tac
.
Require
Export
Integral_domain
.
Require
Import
DiscrR
.
Require
Import
ZArith
.
Require
Import
Lia
.
Require
Export
NsatzTactic
.
Make use of
discrR
in
nsatz
Ltac
nsatz_internal_discrR
::=
discrR
.
Require
Import
Reals
.
Require
Import
RealField
.
Lemma
Rsth
:
Setoid_Theory
R
(@
eq
R
).
Instance
Rops
: (@
Ring_ops
R
0%
R
1%
R
Rplus
Rmult
Rminus
Ropp
(@
eq
R
)).
Defined
.
Instance
Rri
: (
Ring
(
Ro
:=
Rops
)).
Defined
.
Class
can_compute_Z
(
z
:
Z
) :=
dummy_can_compute_Z
:
True
.
Hint Extern
0 (
can_compute_Z
?
v
) =>
match
isZcst
v
with
true
=>
exact
I
end
:
typeclass_instances
.
Instance
reify_IZR
z
lvar
{
_
:
can_compute_Z
z
} :
reify
(
PEc
z
)
lvar
(
IZR
z
).
Defined
.
Lemma
R_one_zero
: 1%
R
<>
0%
R
.
Instance
Rcri
: (
Cring
(
Rr
:=
Rri
)).
Instance
Rdi
: (
Integral_domain
(
Rcr
:=
Rcri
)).
Require
Import
QArith
.
Instance
Qops
: (@
Ring_ops
Q
0%
Q
1%
Q
Qplus
Qmult
Qminus
Qopp
Qeq
).
Defined
.
Instance
Qri
: (
Ring
(
Ro
:=
Qops
)).
Defined
.
Lemma
Q_one_zero
:
not
(
Qeq
1%
Q
0%
Q
).
Instance
Qcri
: (
Cring
(
Rr
:=
Qri
)).
Instance
Qdi
: (
Integral_domain
(
Rcr
:=
Qcri
)).
Lemma
Z_one_zero
: 1%
Z
<>
0%
Z
.
Instance
Zcri
: (
Cring
(
Rr
:=
Zr
)).
Instance
Zdi
: (
Integral_domain
(
Rcr
:=
Zcri
)).