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)
These hints were meant to be added to the qarith database,
but a typo prevented that. This will be fixed in 8.3.
Concerning 8.2, for maximal compatibility , we
leave them in a separate database, in order to preserve
the strength of both auto with qarith and auto with *.
(see bug 2346). *)
Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith_extra.
(** Some decidability results about orders. *)
Lemma Q_dec : forall x y, {x -q <= -p.
Proof.
intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
do 2 rewrite <- Zopp_mult_distr_l; omega.
Qed.
Hint Resolve Qopp_le_compat : qarith.
Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
Proof.
intros (x1,x2) (y1,y2); unfold Qle; simpl.
rewrite <- Zopp_mult_distr_l.
split; omega.
Qed.
Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p.
Proof.
intros (x1,x2) (y1,y2); unfold Qlt; simpl.
rewrite <- Zopp_mult_distr_l.
split; omega.
Qed.
Lemma Qplus_le_compat :
forall x y z t, x<=y -> z<=t -> x+z <= y+t.
Proof.
unfold Qplus, Qle; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2);
simpl; simpl_mult.
Open Scope Z_scope.
intros.
match goal with |- ?a <= ?b => ring_simplify a b end.
rewrite Zplus_comm.
apply Zplus_le_compat.
match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
auto with zarith.
match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
auto with zarith.
Close Scope Z_scope.
Qed.
Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
Proof.
intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
Open Scope Z_scope.
intros; simpl_mult.
replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
apply Zmult_le_compat_r; auto with zarith.
Close Scope Z_scope.
Qed.
Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y.
Proof.
intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
Open Scope Z_scope.
simpl_mult.
replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
intros; apply Zmult_le_reg_r with (c1*'c2); auto with zarith.
Close Scope Z_scope.
Qed.
Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z.
Proof.
intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
Open Scope Z_scope.
intros; simpl_mult.
replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
apply Zmult_lt_compat_r; auto with zarith.
apply Zmult_lt_0_compat.
omega.
compute; auto.
Close Scope Z_scope.
Qed.
Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b.
Proof.
intros a b Ha Hb.
unfold Qle in *.
simpl in *.
auto with *.
Qed.
Lemma Qinv_le_0_compat : forall a, 0 <= a -> 0 <= /a.
Proof.
intros [[|n|n] d] Ha; assumption.
Qed.
Lemma Qle_shift_div_l : forall a b c,
0 < c -> a*c <= b -> a <= b/c.
Proof.
intros a b c Hc H.
apply Qmult_lt_0_le_reg_r with (c).
assumption.
setoid_replace (b/c*c) with (c*(b/c)) by apply Qmult_comm.
rewrite Qmult_div_r; try assumption.
auto with *.
Qed.
Lemma Qle_shift_inv_l : forall a c,
0 < c -> a*c <= 1 -> a <= /c.
Proof.
intros a c Hc H.
setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l).
change (a <= 1/c).
apply Qle_shift_div_l; assumption.
Qed.
Lemma Qle_shift_div_r : forall a b c,
0 < b -> a <= c*b -> a/b <= c.
Proof.
intros a b c Hc H.
apply Qmult_lt_0_le_reg_r with b.
assumption.
setoid_replace (a/b*b) with (b*(a/b)) by apply Qmult_comm.
rewrite Qmult_div_r; try assumption.
auto with *.
Qed.
Lemma Qle_shift_inv_r : forall b c,
0 < b -> 1 <= c*b -> /b <= c.
Proof.
intros b c Hc H.
setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l).
change (1/b <= c).
apply Qle_shift_div_r; assumption.
Qed.
Lemma Qinv_lt_0_compat : forall a, 0 < a -> 0 < /a.
Proof.
intros [[|n|n] d] Ha; assumption.
Qed.
Lemma Qlt_shift_div_l : forall a b c,
0 < c -> a*c < b -> a < b/c.
Proof.
intros a b c Hc H.
apply Qnot_le_lt.
intros H0.
apply (Qlt_not_le _ _ H).
apply Qmult_lt_0_le_reg_r with (/c).
apply Qinv_lt_0_compat.
assumption.
setoid_replace (a*c/c) with (a) by (apply Qdiv_mult_l; auto with *).
assumption.
Qed.
Lemma Qlt_shift_inv_l : forall a c,
0 < c -> a*c < 1 -> a < /c.
Proof.
intros a c Hc H.
setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l).
change (a < 1/c).
apply Qlt_shift_div_l; assumption.
Qed.
Lemma Qlt_shift_div_r : forall a b c,
0 < b -> a < c*b -> a/b < c.
Proof.
intros a b c Hc H.
apply Qnot_le_lt.
intros H0.
apply (Qlt_not_le _ _ H).
apply Qmult_lt_0_le_reg_r with (/b).
apply Qinv_lt_0_compat.
assumption.
setoid_replace (c*b/b) with (c) by (apply Qdiv_mult_l; auto with *).
assumption.
Qed.
Lemma Qlt_shift_inv_r : forall b c,
0 < b -> 1 < c*b -> /b < c.
Proof.
intros b c Hc H.
setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l).
change (1/b < c).
apply Qlt_shift_div_r; assumption.
Qed.
(** * Rational to the n-th power *)
Definition Qpower_positive (q:Q)(p:positive) : Q :=
pow_pos Qmult q p.
Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp.
Proof.
intros x1 x2 Hx y.
unfold Qpower_positive.
induction y; simpl;
try rewrite IHy;
try rewrite Hx;
reflexivity.
Qed.
Definition Qpower (q:Q) (z:Z) :=
match z with
| Zpos p => Qpower_positive q p
| Z0 => 1
| Zneg p => /Qpower_positive q p
end.
Notation " q ^ z " := (Qpower q z) : Q_scope.
Add Morphism Qpower with signature Qeq ==> @eq _ ==> Qeq as Qpower_comp.
Proof.
intros x1 x2 Hx [|y|y]; try reflexivity;
simpl; rewrite Hx; reflexivity.
Qed.