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.
Another approach : using Qcompare for defining order relations.
Definition Qcompare (
p q :
Q) := (
Qnum p *
QDen q ?=
Qnum q *
QDen p)%Z.
Notation "p ?= q" := (
Qcompare p q) :
Q_scope.
Lemma Qeq_alt :
forall p q, (
p ==
q) <-> (
p ?=
q) =
Eq.
Lemma Qlt_alt :
forall p q, (
p<q) <-> (
p?=q =
Lt).
Lemma Qgt_alt :
forall p q, (
p>q) <-> (
p?=q =
Gt).
Lemma Qle_alt :
forall p q, (
p<=q) <-> (
p?=q <>
Gt).
Lemma Qge_alt :
forall p q, (
p>=q) <-> (
p?=q <>
Lt).
Hint Unfold Qeq Qlt Qle :
qarith.
Hint Extern 5 (?X1 <> ?X2) =>
intro;
discriminate:
qarith.
Theorem Qeq_refl :
forall x,
x ==
x.
Theorem Qeq_sym :
forall x y,
x ==
y ->
y ==
x.
Theorem Qeq_trans :
forall x y z,
x ==
y ->
y ==
z ->
x ==
z.
Furthermore, this equality is decidable:
We now consider Q seen as a setoid.
Addition, multiplication and opposite
The addition, multiplication and opposite are defined
in the straightforward way:
A light notation for Zpos
Notation " ' x " := (
Zpos x) (
at level 20,
no associativity) :
Z_scope.
Lemma Qmake_Qdiv :
forall a b,
a#b==inject_Z
a/inject_Z ('
b).
Setoid compatibility results
Add Morphism Qplus :
Qplus_comp.
Open Scope Z_scope.
Close Scope Z_scope.
Add Morphism Qopp :
Qopp_comp.
Open Scope Z_scope.
Close Scope Z_scope.
Add Morphism Qminus :
Qminus_comp.
Add Morphism Qmult :
Qmult_comp.
Open Scope Z_scope.
Close Scope Z_scope.
Add Morphism Qinv :
Qinv_comp.
Open Scope Z_scope.
Close Scope Z_scope.
Add Morphism Qdiv :
Qdiv_comp.
Add Morphism Qle with signature Qeq ==>
Qeq ==>
iff as Qle_comp.
Open Scope Z_scope.
Close Scope Z_scope.
Add Morphism Qlt with signature Qeq ==>
Qeq ==>
iff as Qlt_comp.
Open Scope Z_scope.
Close Scope Z_scope.
Add Morphism Qeq_bool with signature Qeq ==>
Qeq ==> (@
eq bool)
as Qeqb_comp.
Add Morphism Qle_bool with signature Qeq ==>
Qeq ==> (@
eq bool)
as Qleb_comp.
Lemma Qcompare_egal_dec:
forall n m p q :
Q,
(
n<m ->
p<q) -> (
n==m ->
p==q) -> (
n>m ->
p>q) -> ((
n?=m) = (
p?=q)).
Add Morphism Qcompare :
Qcompare_comp.
0 and 1 are apart
Addition is associative:
0 is a neutral element for addition:
Commutativity of addition:
Multiplication is associative:
multiplication and zero
1 is a neutral element for multiplication:
Commutativity of multiplication
Distributivity over Qadd
Integrality
Properties of order upon Q.
Lemma Qle_refl :
forall x,
x<=x.
Lemma Qle_antisym :
forall x y,
x<=y ->
y<=x ->
x==y.
Lemma Qle_trans :
forall x y z,
x<=y ->
y<=z ->
x<=z.
Open Scope Z_scope.
Close Scope Z_scope.
Hint Resolve Qle_trans :
qarith.
Lemma Qlt_not_eq :
forall x y,
x<y -> ~
x==y.
Large = strict or equal
Lemma Qlt_le_weak :
forall x y,
x<y ->
x<=y.
Lemma Qle_lt_trans :
forall x y z,
x<=y ->
y<z ->
x<z.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qlt_le_trans :
forall x y z,
x<y ->
y<=z ->
x<z.
Open Scope Z_scope.
Close Scope Z_scope.
Lemma Qlt_trans :
forall x y z,
x<y ->
y<z ->
x<z.
x<y iff ~(y<=x)
Some decidability results about orders.
Lemma Q_dec :
forall x y, {
x<y} + {
y<x} + {
x==y}.
Lemma Qlt_le_dec :
forall x y, {
x<y} + {
y<=x}.
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 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_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_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