Library Coq.QArith.QArith_base
Definition of Q and basic properties
Rationals are pairs of
Z and
positive numbers.
a#b denotes the fraction a over b.
Notation "a # b" := (
Qmake a b) (
at level 55,
no associativity) :
Q_scope.
Definition of_decimal (
d:
Decimal.decimal) :
Q :=
let '
(i, f, e) :=
match d with
|
Decimal.Decimal i f =>
(i, f, Decimal.Pos Decimal.Nil)
|
Decimal.DecimalExp i f e =>
(i, f, e)
end in
let num :=
Z.of_int (
Decimal.app_int i f)
in
let e :=
Z.sub (
Z.of_int e) (
Z.of_nat (
Decimal.nb_digits f))
in
match e with
|
Z0 =>
Qmake num 1
|
Zpos e =>
Qmake (
Pos.iter (
Z.mul 10)
num e) 1
|
Zneg e =>
Qmake num (
Pos.iter (
Pos.mul 10) 1%
positive e)
end.
Definition to_decimal (
q:
Q) :
option Decimal.decimal :=
let choose_exponent i ne :=
let i :=
match i with Decimal.Pos i |
Decimal.Neg i =>
i end in
let li :=
Decimal.nb_digits i in
let le :=
Decimal.nb_digits (
Nat.to_uint ne)
in
Nat.ltb (
Nat.add li le)
ne in
let decimal_exponent i ne :=
let e :=
Z.to_int (
Z.opp (
Z.of_nat ne))
in
Decimal.DecimalExp i Decimal.Nil e in
let decimal_dot i ne :=
let ai :=
match i with Decimal.Pos i |
Decimal.Neg i =>
i end in
let ni :=
Decimal.nb_digits ai in
if Nat.ltb ne ni then
let i :=
Decimal.del_tail_int ne i in
let f :=
Decimal.del_head (
Nat.sub ni ne)
ai in
Decimal.Decimal i f
else
let z :=
match i with
|
Decimal.Pos _ =>
Decimal.Pos (
Decimal.zero)
|
Decimal.Neg _ =>
Decimal.Neg (
Decimal.zero)
end in
Decimal.Decimal z (
Nat.iter (
Nat.sub ne ni)
Decimal.D0 ai)
in
let num :=
Z.to_int (
Qnum q)
in
let (
den,
e_den) :=
Decimal.nztail (
Pos.to_uint (
Qden q))
in
match den with
|
Decimal.D1 Decimal.Nil =>
match e_den with
|
O =>
Some (
Decimal.Decimal num Decimal.Nil)
|
ne =>
if choose_exponent num ne then Some (
decimal_exponent num ne)
else Some (
decimal_dot num ne)
end
|
_ =>
None
end.
Definition of_hexadecimal (
d:
Hexadecimal.hexadecimal) :
Q :=
let '
(i, f, e) :=
match d with
|
Hexadecimal.Hexadecimal i f =>
(i, f, Decimal.Pos Decimal.Nil)
|
Hexadecimal.HexadecimalExp i f e =>
(i, f, e)
end in
let num :=
Z.of_hex_int (
Hexadecimal.app_int i f)
in
let e :=
Z.sub (
Z.of_int e) (
Z.mul 4 (
Z.of_nat (
Hexadecimal.nb_digits f)))
in
match e with
|
Z0 =>
Qmake num 1
|
Zpos e =>
Qmake (
Pos.iter (
Z.mul 2)
num e) 1
|
Zneg e =>
Qmake num (
Pos.iter (
Pos.mul 2) 1%
positive e)
end.
Definition to_hexadecimal (
q:
Q) :
option Hexadecimal.hexadecimal :=
let mk_exp i e :=
Hexadecimal.HexadecimalExp i Hexadecimal.Nil (
Z.to_int (
Z.opp e))
in
let num :=
Z.to_hex_int (
Qnum q)
in
let (
den,
e_den) :=
Hexadecimal.nztail (
Pos.to_hex_uint (
Qden q))
in
let e :=
Z.of_nat e_den in
match den with
|
Hexadecimal.D1 Hexadecimal.Nil =>
match e_den with
|
O =>
Some (
Hexadecimal.Hexadecimal num Hexadecimal.Nil)
|
_ =>
Some (
mk_exp num (4
* e)%
Z)
end
|
Hexadecimal.D2 Hexadecimal.Nil =>
Some (
mk_exp num (1
+ 4
* e)%
Z)
|
Hexadecimal.D4 Hexadecimal.Nil =>
Some (
mk_exp num (2
+ 4
* e)%
Z)
|
Hexadecimal.D8 Hexadecimal.Nil =>
Some (
mk_exp num (3
+ 4
* e)%
Z)
|
_ =>
None
end.
Definition of_numeral (
d:
Numeral.numeral) :
option Q :=
match d with
|
Numeral.Dec d =>
Some (
of_decimal d)
|
Numeral.Hex d =>
Some (
of_hexadecimal d)
end.
Definition to_numeral (
q:
Q) :
option Numeral.numeral :=
match to_decimal q with
|
None =>
None
|
Some q =>
Some (
Numeral.Dec q)
end.
Definition inject_Z (
x :
Z) :=
Qmake x 1.
Notation QDen p := (
Zpos (
Qden p)).
Definition Qeq (
p q :
Q) := (
Qnum p * QDen q)%
Z = (
Qnum q * QDen p)%
Z.
Definition Qle (
x y :
Q) := (
Qnum x * QDen y <= Qnum y * QDen x)%
Z.
Definition Qlt (
x y :
Q) := (
Qnum x * QDen y < Qnum y * QDen x)%
Z.
Notation Qgt a b := (
Qlt b a) (
only parsing).
Notation Qge a b := (
Qle b a) (
only parsing).
Infix "==" :=
Qeq (
at level 70,
no associativity) :
Q_scope.
Infix "<" :=
Qlt :
Q_scope.
Infix "<=" :=
Qle :
Q_scope.
Notation "x > y" := (
Qlt y x)(
only parsing) :
Q_scope.
Notation "x >= y" := (
Qle y x)(
only parsing) :
Q_scope.
Notation "x <= y <= z" := (
x<=y/\y<=z) :
Q_scope.
injection from Z is injective.
Another approach : using Qcompare for defining order relations.
In a word, Qeq is a setoid equality.
Furthermore, this equality is decidable:
Addition, multiplication and opposite
The addition, multiplication and opposite are defined
in the straightforward way:
A light notation for Zpos
Setoid compatibility results
0 and 1 are apart
Properties of Qadd
Addition is associative:
0 is a neutral element for addition:
Commutativity of addition:
Injectivity of addition (uses theory about Qopp above):
Properties of Qmult
Multiplication is associative:
multiplication and zero
1 is a neutral element for multiplication:
Commutativity of multiplication
Distributivity over Qadd
Integrality
inject_Z is a ring homomorphism:
Injectivity of Qmult (requires theory about Qinv above):
Properties of order upon Q.
Large = strict or equal
x<y iff ~(y<=x)
Some decidability results about orders.
Compatibility of operations with respect to order.
Lemma Qopp_le_compat :
forall p q,
p<=q -> -q <= -p.
Hint Resolve Qopp_le_compat :
qarith.
Lemma Qle_minus_iff :
forall p q,
p <= q <-> 0
<= q+-p.
Lemma Qlt_minus_iff :
forall p q,
p < q <-> 0
< q+-p.
Lemma Qplus_le_compat :
forall x y z t,
x<=y -> z<=t -> x+z <= y+t.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qplus_lt_le_compat :
forall x y z t,
x<y -> z<=t -> x+z < y+t.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qplus_le_l (
x y z:
Q):
x + z <= y + z <-> x <= y.
Lemma Qplus_le_r (
x y z:
Q):
z + x <= z + y <-> x <= y.
Lemma Qplus_lt_l (
x y z:
Q):
x + z < y + z <-> x < y.
Lemma Qplus_lt_r (
x y z:
Q):
z + x < z + y <-> x < y.
Lemma Qmult_le_compat_r :
forall x y z,
x <= y -> 0
<= z -> x*z <= y*z.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_lt_0_le_reg_r :
forall x y z, 0
< z -> x*z <= y*z -> x <= y.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_le_r (
x y z:
Q): 0
< z -> (x*z <= y*z <-> x <= y).
Lemma Qmult_le_l (
x y z:
Q): 0
< z -> (z*x <= z*y <-> x <= y).
Lemma Qmult_lt_compat_r :
forall x y z, 0
< z -> x < y -> x*z < y*z.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_lt_r:
forall x y z, 0
< z -> (x*z < y*z <-> x < y).
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qmult_lt_l (
x y z:
Q): 0
< z -> (z*x < z*y <-> x < y).
Lemma Qmult_le_0_compat :
forall a b, 0
<= a -> 0
<= b -> 0
<= a*b.
Lemma Qinv_le_0_compat :
forall a, 0
<= a -> 0
<= /a.
Lemma Qle_shift_div_l :
forall a b c,
0
< c -> a*c <= b -> a <= b/c.
Lemma Qle_shift_inv_l :
forall a c,
0
< c -> a*c <= 1
-> a <= /c.
Lemma Qle_shift_div_r :
forall a b c,
0
< b -> a <= c*b -> a/b <= c.
Lemma Qle_shift_inv_r :
forall b c,
0
< b -> 1
<= c*b -> /b <= c.
Lemma Qinv_lt_0_compat :
forall a, 0
< a -> 0
< /a.
Lemma Qlt_shift_div_l :
forall a b c,
0
< c -> a*c < b -> a < b/c.
Lemma Qlt_shift_inv_l :
forall a c,
0
< c -> a*c < 1
-> a < /c.
Lemma Qlt_shift_div_r :
forall a b c,
0
< b -> a < c*b -> a/b < c.
Lemma Qlt_shift_inv_r :
forall b c,
0
< b -> 1
< c*b -> /b < c.
Lemma Qinv_lt_contravar :
forall a b :
Q,
0
< a -> 0
< b -> (a < b <-> /b < /a).
Rational to the n-th power