Library Coq.QArith.QArith_base



Require Export ZArith.
Require Export ZArithRing.
Require Export 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 := 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.

Properties of equality.


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.

Add Relation Q Qeq
  reflexivity proved by Qeq_refl
  symmetry proved by Qeq_sym
  transitivity proved by Qeq_trans
as Q_Setoid.

Hint Resolve Qeq_refl : qarith.
Hint Resolve Qeq_sym : qarith.
Hint Resolve Qeq_trans : qarith.

Theorem Qnot_eq_sym : forall 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 : 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

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.

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.

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.

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)

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.

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.