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 inject_Z (
x :
Z) :=
Qmake x 1.
Notation QDen p := (
Zpos (
Qden p)).
Notation " 0 " := (0
#1) :
Q_scope.
Notation " 1 " := (1
#1) :
Q_scope.
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.
Rational to the n-th power