Library Coq.QArith.Qfield
Require
Export
Field
.
Require
Export
QArith_base
.
Require
Import
NArithRing
.
field and ring tactics for rational numbers
Definition
Qsrt
:
ring_theory
0 1
Qplus
Qmult
Qminus
Qopp
Qeq
.
Definition
Qsft
:
field_theory
0 1
Qplus
Qmult
Qminus
Qopp
Qdiv
Qinv
Qeq
.
Lemma
Qpower_theory
:
power_theory
1
Qmult
Qeq
Z.of_N
Qpower
.
Ltac
isQcst
t
:=
match
t
with
|
inject_Z
?
z
=>
isZcst
z
|
Qmake
?
n
?
d
=>
match
isZcst
n
with
true
=>
isPcst
d
|
_
=>
false
end
|
_
=>
false
end
.
Ltac
Qcst
t
:=
match
isQcst
t
with
true
=>
t
|
_
=>
NotConstant
end
.
Ltac
Qpow_tac
t
:=
match
t
with
|
Z0
=>
N0
|
Zpos
?
n
=>
Ncst
(
Npos
n
)
|
Z.of_N
?
n
=>
Ncst
n
|
NtoZ
?
n
=>
Ncst
n
|
_
=>
NotConstant
end
.
Add
Field
Qfield
:
Qsft
(
decidable
Qeq_bool_eq
,
completeness
Qeq_eq_bool
,
constants
[
Qcst
],
power_tac
Qpower_theory
[
Qpow_tac
]).
Exemple of use:
Section
Examples
.
Let
ex1
:
forall
x
y
z
:
Q
,
(
x
+
y
)*
z
==
(
x
*
z
)+(
y
*
z
)
.
Qed
.
Let
ex2
:
forall
x
y
:
Q
,
x
+
y
==
y
+
x
.
Qed
.
Let
ex3
:
forall
x
y
z
:
Q
,
(
x
+
y
)+
z
==
x
+(
y
+
z
)
.
Qed
.
Let
ex4
:
(
inject_Z
1
)+(
inject_Z
1
)
==(
inject_Z
2
)
.
Qed
.
Let
ex5
: 1
+
1
==
2
#
1.
Qed
.
Let
ex6
:
(
1
#
1
)+(
1
#
1
)
==
2
#
1.
Qed
.
Let
ex7
:
forall
x
:
Q
,
x
-
x
==
0.
Qed
.
Let
ex8
:
forall
x
:
Q
,
x
^
1
==
x
.
Qed
.
Let
ex9
:
forall
x
:
Q
,
x
^
0
==
1.
Qed
.
Let
ex10
:
forall
x
y
:
Q
,
~(
y
==
0
)
->
(
x
/
y
)*
y
==
x
.
Qed
.
End
Examples
.
Lemma
Qopp_plus
:
forall
a
b
,
-(
a
+
b
)
==
-
a
+
-
b
.
Lemma
Qopp_opp
:
forall
q
,
-
-
q
==
q
.