Library Coq.QArith.QArith_base
Definition of Q and basic properties
Rationals are pairs of
Z and
positive numbers.
Record Q :
Set :=
Qmake {
Qnum :
Z;
Qden :
positive}.
Declare Scope hex_Q_scope.
Delimit Scope hex_Q_scope with xQ.
Declare Scope Q_scope.
Delimit Scope Q_scope with Q.
Bind Scope Q_scope with Q.
Arguments Qmake _%
Z _%
positive.
Register Q as rat.Q.type.
Register Qmake as rat.Q.Qmake.
Open Scope Q_scope.
Ltac simpl_mult :=
rewrite ?
Pos2Z.inj_mul.
a#b denotes the fraction a over b.
Notation "a # b" := (
Qmake a b) (
at level 55,
no associativity) :
Q_scope.
Definition inject_Z (
x :
Z) :=
Qmake x 1.
Arguments inject_Z x%
Z.
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.
Notation "x <= y < z" := (
x<=y/\y<z) :
Q_scope.
Notation "x < y <= z" := (
x<y/\y<=z) :
Q_scope.
Notation "x < y < z" := (
x<y/\y<z) :
Q_scope.
Register Qeq as rat.Q.Qeq.
Register Qle as rat.Q.Qle.
Register Qlt as rat.Q.Qlt.
Qeq construction from parts.
Establishing equality by establishing equality
for numerator and denominator separately.
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:
Number notation for constants
Inductive IZ :=
|
IZpow_pos :
Z -> positive -> IZ
|
IZ0 :
IZ
|
IZpos :
positive -> IZ
|
IZneg :
positive -> IZ.
Inductive IQ :=
|
IQmake :
IZ -> positive -> IQ
|
IQmult :
IQ -> IQ -> IQ
|
IQdiv :
IQ -> IQ -> IQ.
Definition IZ_of_Z z :=
match z with
|
Z0 =>
IZ0
|
Zpos e =>
IZpos e
|
Zneg e =>
IZneg e
end.
Definition IZ_to_Z z :=
match z with
|
IZ0 =>
Some Z0
|
IZpos e =>
Some (
Zpos e)
|
IZneg e =>
Some (
Zneg e)
|
IZpow_pos _ _ =>
None
end.
Definition of_decimal (
d:
Decimal.decimal) :
IQ :=
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 den :=
Nat.iter (
Decimal.nb_digits f) (
Pos.mul 10) 1%
positive in
let q :=
IQmake (
IZ_of_Z num)
den in
let e :=
Z.of_int e in
match e with
|
Z0 =>
q
|
Zpos e =>
IQmult q (
IQmake (
IZpow_pos 10
e) 1)
|
Zneg e =>
IQdiv q (
IQmake (
IZpow_pos 10
e) 1)
end.
Definition IQmake_to_decimal num den :=
let num :=
Z.to_int num in
let (
den,
e_den) :=
Decimal.nztail (
Pos.to_uint den)
in
match den with
|
Decimal.D1 Decimal.Nil =>
match e_den with
|
O =>
Some (
Decimal.Decimal num Decimal.Nil)
|
ne =>
let ai :=
Decimal.abs num in
let ni :=
Decimal.nb_digits ai in
if Nat.ltb ne ni then
let i :=
Decimal.del_tail_int ne num in
let f :=
Decimal.del_head (
Nat.sub ni ne)
ai in
Some (
Decimal.Decimal i f)
else
let z :=
match num with
|
Decimal.Pos _ =>
Decimal.Pos (
Decimal.zero)
|
Decimal.Neg _ =>
Decimal.Neg (
Decimal.zero)
end in
Some (
Decimal.Decimal z (
Nat.iter (
Nat.sub ne ni)
Decimal.D0 ai))
end
|
_ =>
None
end.
Definition IQmake_to_decimal' num den :=
match IZ_to_Z num with
|
None =>
None
|
Some num =>
IQmake_to_decimal num den
end.
Definition to_decimal (
n :
IQ) :
option Decimal.decimal :=
match n with
|
IQmake num den =>
IQmake_to_decimal' num den
|
IQmult (
IQmake num den) (
IQmake (
IZpow_pos 10
e) 1) =>
match IQmake_to_decimal' num den with
|
Some (
Decimal.Decimal i f) =>
Some (
Decimal.DecimalExp i f (
Pos.to_int e))
|
_ =>
None
end
|
IQdiv (
IQmake num den) (
IQmake (
IZpow_pos 10
e) 1) =>
match IQmake_to_decimal' num den with
|
Some (
Decimal.Decimal i f) =>
Some (
Decimal.DecimalExp i f (
Decimal.Neg (
Pos.to_uint e)))
|
_ =>
None
end
|
_ =>
None
end.
Definition of_hexadecimal (
d:
Hexadecimal.hexadecimal) :
IQ :=
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 den :=
Nat.iter (
Hexadecimal.nb_digits f) (
Pos.mul 16) 1%
positive in
let q :=
IQmake (
IZ_of_Z num)
den in
let e :=
Z.of_int e in
match e with
|
Z0 =>
q
|
Zpos e =>
IQmult q (
IQmake (
IZpow_pos 2
e) 1)
|
Zneg e =>
IQdiv q (
IQmake (
IZpow_pos 2
e) 1)
end.
Definition IQmake_to_hexadecimal num den :=
let num :=
Z.to_hex_int num in
let (
den,
e_den) :=
Hexadecimal.nztail (
Pos.to_hex_uint den)
in
match den with
|
Hexadecimal.D1 Hexadecimal.Nil =>
match e_den with
|
O =>
Some (
Hexadecimal.Hexadecimal num Hexadecimal.Nil)
|
ne =>
let ai :=
Hexadecimal.abs num in
let ni :=
Hexadecimal.nb_digits ai in
if Nat.ltb ne ni then
let i :=
Hexadecimal.del_tail_int ne num in
let f :=
Hexadecimal.del_head (
Nat.sub ni ne)
ai in
Some (
Hexadecimal.Hexadecimal i f)
else
let z :=
match num with
|
Hexadecimal.Pos _ =>
Hexadecimal.Pos (
Hexadecimal.zero)
|
Hexadecimal.Neg _ =>
Hexadecimal.Neg (
Hexadecimal.zero)
end in
Some (
Hexadecimal.Hexadecimal z (
Nat.iter (
Nat.sub ne ni)
Hexadecimal.D0 ai))
end
|
_ =>
None
end.
Definition IQmake_to_hexadecimal' num den :=
match IZ_to_Z num with
|
None =>
None
|
Some num =>
IQmake_to_hexadecimal num den
end.
Definition to_hexadecimal (
n :
IQ) :
option Hexadecimal.hexadecimal :=
match n with
|
IQmake num den =>
IQmake_to_hexadecimal' num den
|
IQmult (
IQmake num den) (
IQmake (
IZpow_pos 2
e) 1) =>
match IQmake_to_hexadecimal' num den with
|
Some (
Hexadecimal.Hexadecimal i f) =>
Some (
Hexadecimal.HexadecimalExp i f (
Pos.to_int e))
|
_ =>
None
end
|
IQdiv (
IQmake num den) (
IQmake (
IZpow_pos 2
e) 1) =>
match IQmake_to_hexadecimal' num den with
|
Some (
Hexadecimal.Hexadecimal i f) =>
Some (
Hexadecimal.HexadecimalExp i f (
Decimal.Neg (
Pos.to_uint e)))
|
_ =>
None
end
|
_ =>
None
end.
Definition of_number (
n :
Number.number) :
IQ :=
match n with
|
Number.Decimal d =>
of_decimal d
|
Number.Hexadecimal h =>
of_hexadecimal h
end.
Definition to_number (
q:
IQ) :
option Number.number :=
match to_decimal q with
|
None =>
None
|
Some q =>
Some (
Number.Decimal q)
end.
Definition to_hex_number q :=
match to_hexadecimal q with
|
None =>
None
|
Some q =>
Some (
Number.Hexadecimal q)
end.
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):
Reduction and construction of Q
Removal/introduction of common factor in both numerator and denominator.
Construction of a new rational by multiplication with an integer or pure fraction
(or to be more precise multiplication with a rational of the form z/1 or 1/p)
Properties of order upon Q.
Large = strict or equal
Qgt and Qge are just a notations, but one might not know this and search for these lemmas
x<y iff ~(y<=x)
Some decidability results about orders.
Compatibility of addition with order
Compatibility of multiplication with order.
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 Qmult_lt_0_compat :
forall a b :
Q, 0
< a -> 0
< b -> 0
< a * b.
Lemma Qmult_le_1_compat:
forall a b :
Q, 1
<= a -> 1
<= b -> 1
<= a * b.
Lemma Qmult_lt_1_compat:
forall a b :
Q, 1
< a -> 1
< b -> 1
< a * b.
Lemma Qmult_lt_compat_nonneg:
forall x y z t :
Q, 0
<= x < y -> 0
<= z < t -> x * z < y * t.
Lemma Qmult_le_lt_compat_pos:
forall x y z t :
Q, 0
< x <= y -> 0
< z < t -> x * z < y * t.
Lemma Qmult_le_compat_nonneg:
forall x y z t :
Q, 0
<= x <= y -> 0
<= z <= t -> x * z <= y * t.
Compatibility of inversion and division with order
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