Library Coq.QArith.Qreduction
Normalisation functions for rational numbers.
Require
Export
QArith_base
.
Require
Import
Znumtheory
.
First, a function that (tries to) build a positive back from a Z.
Definition
Z2P
(
z
:
Z
) :=
match
z
with
|
Z0
=> 1%positive
|
Zpos
p
=>
p
|
Zneg
p
=>
p
end
.
Lemma
Z2P_correct
:
forall
z
:
Z
, (0 <
z
)%Z ->
Zpos
(
Z2P
z
) =
z
.
Lemma
Z2P_correct2
:
forall
z
:
Z
, 0%Z <>
z
->
Zpos
(
Z2P
z
) =
Zabs
z
.
Simplification of fractions using
Zgcd
. This version can compute within Coq.
Definition
Qred
(
q
:Q) :=
let
(
q1
,q2) :=
q
in
let
(
r1
,r2) :=
snd
(
Zggcd
q1
('
q2
))
in
r1
#(Z2
P
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
.
Add
Morphism
Qred
:
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'
:
Qplus'_comp
.
Add
Morphism
Qmult'
:
Qmult'_comp
.
Qed
.
Add
Morphism
Qminus'
:
Qminus'_comp
.
Qed
.
Lemma
Qred_opp
:
forall
q
,
Qred
(-q) = - (
Qred
q
).
Theorem
Qred_compare
:
forall
x
y
,
Qcompare
x
y
=
Qcompare
(
Qred
x
) (
Qred
y
).