Library Coq.QArith.Qreduction
Normalisation functions for rational numbers.
Require
Export
QArith_base
.
Require
Import
Znumtheory
.
Notation
Z2P
:=
Z.to_pos
(
only
parsing
).
Notation
Z2P_correct
:=
Z2Pos.id
(
only
parsing
).
Simplification of fractions using
Z.gcd
. This version can compute within Coq.
Definition
Qred
(
q
:
Q
) :=
let
(
q1
,
q2
) :=
q
in
let
(
r1
,
r2
) :=
snd
(
Z.ggcd
q1
(
Zpos
q2
))
in
r1
#(
Z.to_pos
r2
)
.
Lemma
Qred_correct
:
forall
q
,
(
Qred
q
)
==
q
.
Open
Scope
Z_scope
.
Close
Scope
Z_scope
.
Lemma
Qred_complete
:
forall
p
q
,
p
==
q
->
Qred
p
=
Qred
q
.
Open
Scope
Z_scope
.
Close
Scope
Z_scope
.
Lemma
Qred_eq_iff
q
q'
:
Qred
q
=
Qred
q'
<->
q
==
q'
.
Add
Morphism
Qred
with
signature
(
Qeq
==>
Qeq
)
as
Qred_comp
.
Definition
Qplus'
(
p
q
:
Q
) :=
Qred
(
Qplus
p
q
).
Definition
Qmult'
(
p
q
:
Q
) :=
Qred
(
Qmult
p
q
).
Definition
Qminus'
x
y
:=
Qred
(
Qminus
x
y
).
Lemma
Qplus'_correct
:
forall
p
q
:
Q
,
(
Qplus'
p
q
)==(
Qplus
p
q
)
.
Lemma
Qmult'_correct
:
forall
p
q
:
Q
,
(
Qmult'
p
q
)==(
Qmult
p
q
)
.
Lemma
Qminus'_correct
:
forall
p
q
:
Q
,
(
Qminus'
p
q
)==(
Qminus
p
q
)
.
Add
Morphism
Qplus'
with
signature
(
Qeq
==>
Qeq
==>
Qeq
)
as
Qplus'_comp
.
Add
Morphism
Qmult'
with
signature
(
Qeq
==>
Qeq
==>
Qeq
)
as
Qmult'_comp
.
Add
Morphism
Qminus'
with
signature
(
Qeq
==>
Qeq
==>
Qeq
)
as
Qminus'_comp
.
Lemma
Qred_opp
:
forall
q
,
Qred
(
-
q
)
=
-
(
Qred
q
)
.
Theorem
Qred_compare
:
forall
x
y
,
Qcompare
x
y
=
Qcompare
(
Qred
x
) (
Qred
y
).
Lemma
Qred_le
q
q'
:
Qred
q
<=
Qred
q'
<->
q
<=
q'
.
Lemma
Qred_lt
q
q'
:
Qred
q
<
Qred
q'
<->
q
<
q'
.