# Library Coq.QArith.QArith_base

Require Export ZArith.
Require Export ZArithRing.
Require Export Morphisms Setoid Bool.

# Definition of Q and basic properties

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 := 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.
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.
Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b.
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 p q : ( p == q ) <-> ( p ?= q ) = Eq.
Lemma Qlt_alt p q : ( p < q ) <-> ( p ?= q = Lt ).
Lemma Qgt_alt p q : ( p > q ) <-> ( p ?= q = Gt ).
Lemma Qle_alt p q : ( p <= q ) <-> ( p ?= q <> Gt ).
Lemma Qge_alt p q : ( p >= q ) <-> ( p ?= q <> Lt ).
Hint Unfold Qeq Qlt Qle : qarith.
Hint Extern 5 (?X1 <> ? X2) => intro; discriminate: qarith.
Lemma Qcompare_antisym x y : CompOpp (x ?= y) = ( y ?= x ).
Lemma Qcompare_spec x y : CompareSpec (x == y) (x < y) (y < x) (x ?= y).

# Properties of equality.

Theorem Qeq_refl x : x == x.
Theorem Qeq_sym x y : x == y -> y == x.
Theorem Qeq_trans x y z : x == y -> y == z -> x == z.
Hint Immediate Qeq_sym : qarith.
Hint Resolve Qeq_refl Qeq_trans : qarith.
In a word, Qeq is a setoid equality.
Instance Q_Setoid : Equivalence Qeq.
Furthermore, this equality is decidable:
Theorem Qeq_dec 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 :=
(Z.leb (Qnum x * QDen y) (Qnum y * QDen x))%Z.
Lemma Qeq_bool_iff x y : Qeq_bool x y = true <-> x == y.
Lemma Qeq_bool_eq x y : Qeq_bool x y = true -> x == y.
Lemma Qeq_eq_bool x y : x == y -> Qeq_bool x y = true.
Lemma Qeq_bool_neq x y : Qeq_bool x y = false -> ~ x == y.
Lemma Qle_bool_iff x y : Qle_bool x y = true <-> x <= y.
Lemma Qle_bool_imp_le x y : Qle_bool x y = true -> x <= y.
Theorem Qnot_eq_sym x y : ~ x == y -> ~ y == x.
Hint Resolve Qnot_eq_sym : qarith.

# Addition, multiplication and opposite

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 a b : a # b == inject_Z a / inject_Z (' b).

# Setoid compatibility results

Instance Qplus_comp : Proper (Qeq ==> Qeq ==> Qeq) Qplus.
Open Scope Z_scope.
Close Scope Z_scope.
Instance Qopp_comp : Proper (Qeq ==> Qeq) Qopp.
Open Scope Z_scope.
Close Scope Z_scope.
Instance Qminus_comp : Proper (Qeq ==> Qeq ==> Qeq) Qminus.
Instance Qmult_comp : Proper (Qeq ==> Qeq ==> Qeq) Qmult.
Open Scope Z_scope.
Close Scope Z_scope.
Instance Qinv_comp : Proper (Qeq ==> Qeq) Qinv.
Open Scope Z_scope.
Close Scope Z_scope.
Instance Qdiv_comp : Proper (Qeq ==> Qeq ==> Qeq) Qdiv.
Instance Qcompare_comp : Proper (Qeq ==> Qeq ==> eq) Qcompare.
Open Scope Z_scope.
Close Scope Z_scope.
Instance Qle_comp : Proper (Qeq ==> Qeq ==> iff) Qle.
Instance Qlt_compat : Proper (Qeq ==> Qeq ==> iff) Qlt.
Instance Qeqb_comp : Proper (Qeq ==> Qeq ==> eq) Qeq_bool.
Instance Qleb_comp : Proper (Qeq ==> Qeq ==> eq) Qle_bool.
0 and 1 are apart
Lemma Q_apart_0_1 : ~ 1 == 0.

# Properties of Qadd

Addition is associative:
Theorem Qplus_assoc : forall x y z, x +( y + z ) == ( x + y )+ z.
0 is a neutral element for addition:
Lemma Qplus_0_l : forall x, 0+ x == x.
Lemma Qplus_0_r : forall x, x +0 == x.
Commutativity of addition:
Theorem Qplus_comm : forall x y, x + y == y + x.

# Properties of Qopp

Lemma Qopp_involutive : forall q, - - q == q.
Theorem Qplus_opp_r : forall q, q +( - q ) == 0.
Injectivity of addition (uses theory about Qopp above):
Lemma Qplus_inj_r (x y z: Q):
x + z == y + z <-> x == y.
Lemma Qplus_inj_l (x y z: Q):
z + x == z + y <-> x == y.

# Properties of Qmult

Multiplication is associative:
Theorem Qmult_assoc : forall n m p, n *( m * p ) == ( n * m )* p.
multiplication and zero
Lemma Qmult_0_l : forall x , 0* x == 0.
Lemma Qmult_0_r : forall x , x *0 == 0.
1 is a neutral element for multiplication:
Lemma Qmult_1_l : forall n, 1* n == n.
Theorem Qmult_1_r : forall n, n *1== n.
Commutativity of multiplication
Theorem Qmult_comm : forall x y, x * y == y * x.
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.

# inject_Z is a ring homomorphism:

Lemma inject_Z_plus (x y: Z): inject_Z (x + y) = inject_Z x + inject_Z y.
Lemma inject_Z_mult (x y: Z): inject_Z (x * y) = inject_Z x * inject_Z y.
Lemma inject_Z_opp (x: Z): inject_Z (- x) = - inject_Z x.

# Inverse and division.

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.
Injectivity of Qmult (requires theory about Qinv above):
Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y).
Lemma Qmult_inj_l (x y z: Q): ~ z == 0 -> (z * x == z * y <-> x == y).

# Properties of order upon Q.

Lemma Qle_refl x : x <= x.
Lemma Qle_antisym 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_irrefl x : ~ x < x.
Lemma Qlt_not_eq x y : x < y -> ~ x == y.
Lemma Zle_Qle (x y: Z): (x <= y)%Z = ( inject_Z x <= inject_Z y ).
Lemma Zlt_Qlt (x y: Z): (x < y)%Z = ( inject_Z x < inject_Z y ).
Large = strict or equal
Lemma Qle_lteq x y : x <= y <-> x < y \/ x == y.
Lemma Qlt_le_weak 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: qarith.
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 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

Definition Qpower_positive (q:Q)(p:positive) : Q :=
pow_pos Qmult q p.
Instance Qpower_positive_comp : Proper (Qeq ==> eq ==> Qeq) Qpower_positive.
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.
Instance Qpower_comp : Proper (Qeq ==> eq ==> Qeq) Qpower.