Library Coq.QArith.QArith_base
Rationals are pairs of Z and positive numbers.
Record Q : Set := Qmake {Qnum : Z; Qden : positive}.
Delimit Scope Q_scope with Q.
Open Scope Q_scope.
Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
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:
Theorem Qeq_dec : forall x y, {x==y} + {~ x==y}.
Definition Qeq_bool x y :=
(Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
Definition Qle_bool x y :=
(Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
Lemma Qeq_bool_iff : forall x y, Qeq_bool x y = true <-> x == y.
Lemma Qeq_bool_eq : forall x y, Qeq_bool x y = true -> x == y.
Lemma Qeq_eq_bool : forall x y, x == y -> Qeq_bool x y = true.
Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y.
Lemma Qle_bool_iff : forall x y, Qle_bool x y = true <-> x <= y.
Lemma Qle_bool_imp_le : forall x y, Qle_bool x y = true -> x <= y.
We now consider Q seen as a setoid.
Definition Q_Setoid : Setoid_Theory Q Qeq.
Add Setoid Q Qeq Q_Setoid as Qsetoid.
Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
Hint Resolve Qnot_eq_sym : qarith.
The addition, multiplication and opposite are defined
in the straightforward way:
Definition Qplus (x y : Q) :=
(Qnum x * QDen y + Qnum y * QDen x) # (Qden x * Qden y).
Definition Qmult (x y : Q) := (Qnum x * Qnum y) # (Qden x * Qden y).
Definition Qopp (x : Q) := (- Qnum x) # (Qden x).
Definition Qminus (x y : Q) := Qplus x (Qopp y).
Definition Qinv (x : Q) :=
match Qnum x with
| Z0 => 0
| Zpos p => (QDen x)#p
| Zneg p => (Zneg (Qden x))#p
end.
Definition Qdiv (x y : Q) := Qmult x (Qinv y).
Infix "+" := Qplus : Q_scope.
Notation "- x" := (Qopp x) : Q_scope.
Infix "-" := Qminus : Q_scope.
Infix "*" := Qmult : Q_scope.
Notation "/ x" := (Qinv x) : Q_scope.
Infix "/" := Qdiv : Q_scope.
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).
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
Theorem Qmult_plus_distr_r : forall x y z, x*(y+z)==(x*y)+(x*z).
Theorem Qmult_plus_distr_l : forall x y z, (x+y)*z==(x*z)+(y*z).
Integrality
Theorem Qmult_integral : forall x y, x*y==0 -> x==0 \/ y==0.
Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0.
Lemma Qinv_involutive : forall q, (/ / q) == q.
Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.
Lemma Qinv_mult_distr : forall p q, / (p * q) == /p * /q.
Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x.
Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x.
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)
Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x.
Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x.
Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x.
Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x.
Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.
Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih.
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 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.
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.
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.