Library Coq.QArith.QArith_base


Require Export ZArith_base.
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 of_decimal (d:Decimal.decimal) : Q :=
  let '(i, f, e) :=
    match d with
    | Decimal.Decimal i f => (i, f, Decimal.Pos Decimal.Nil)
    | Decimal.DecimalExp i f e => (i, f, e)
    end in
  let num := Z.of_int (Decimal.app_int i f) in
  let e := Z.sub (Z.of_int e) (Z.of_nat (Decimal.nb_digits f)) in
  match e with
  | Z0 => Qmake num 1
  | Zpos e => Qmake (Pos.iter (Z.mul 10) num e) 1
  | Zneg e => Qmake num (Pos.iter (Pos.mul 10) 1%positive e)
  end.

Definition to_decimal (q:Q) : option Decimal.decimal :=
  
  let choose_exponent i ne :=
    let i := match i with Decimal.Pos i | Decimal.Neg i => i end in
    let li := Decimal.nb_digits i in
    let le := Decimal.nb_digits (Nat.to_uint ne) in
    Nat.ltb (Nat.add li le) ne in
  
  let decimal_exponent i ne :=
      let e := Z.to_int (Z.opp (Z.of_nat ne)) in
      Decimal.DecimalExp i Decimal.Nil e in
  
  let decimal_dot i ne :=
    let ai := match i with Decimal.Pos i | Decimal.Neg i => i end in
    let ni := Decimal.nb_digits ai in
    if Nat.ltb ne ni then
      let i := Decimal.del_tail_int ne i in
      let f := Decimal.del_head (Nat.sub ni ne) ai in
      Decimal.Decimal i f
    else
      let z := match i with
        | Decimal.Pos _ => Decimal.Pos (Decimal.zero)
        | Decimal.Neg _ => Decimal.Neg (Decimal.zero) end in
      Decimal.Decimal z (Nat.iter (Nat.sub ne ni) Decimal.D0 ai) in
  let num := Z.to_int (Qnum q) in
  let (den, e_den) := Decimal.nztail (Pos.to_uint (Qden q)) in
  match den with
  | Decimal.D1 Decimal.Nil =>
    match e_den with
    | O => Some (Decimal.Decimal num Decimal.Nil)
    | ne =>
      if choose_exponent num ne then Some (decimal_exponent num ne)
      else Some (decimal_dot num ne)
    end
  | _ => None
  end.

Definition of_hexadecimal (d:Hexadecimal.hexadecimal) : Q :=
  let '(i, f, e) :=
    match d with
    | Hexadecimal.Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil)
    | Hexadecimal.HexadecimalExp i f e => (i, f, e)
    end in
  let num := Z.of_hex_int (Hexadecimal.app_int i f) in
  let e := Z.sub (Z.of_int e) (Z.mul 4 (Z.of_nat (Hexadecimal.nb_digits f))) in
  match e with
  | Z0 => Qmake num 1
  | Zpos e => Qmake (Pos.iter (Z.mul 2) num e) 1
  | Zneg e => Qmake num (Pos.iter (Pos.mul 2) 1%positive e)
  end.

Definition to_hexadecimal (q:Q) : option Hexadecimal.hexadecimal :=
  let mk_exp i e :=
    Hexadecimal.HexadecimalExp i Hexadecimal.Nil (Z.to_int (Z.opp e)) in
  let num := Z.to_hex_int (Qnum q) in
  let (den, e_den) := Hexadecimal.nztail (Pos.to_hex_uint (Qden q)) in
  let e := Z.of_nat e_den in
  match den with
  | Hexadecimal.D1 Hexadecimal.Nil =>
    match e_den with
    | O => Some (Hexadecimal.Hexadecimal num Hexadecimal.Nil)
    | _ => Some (mk_exp num (4 * e)%Z)
    end
  | Hexadecimal.D2 Hexadecimal.Nil => Some (mk_exp num (1 + 4 * e)%Z)
  | Hexadecimal.D4 Hexadecimal.Nil => Some (mk_exp num (2 + 4 * e)%Z)
  | Hexadecimal.D8 Hexadecimal.Nil => Some (mk_exp num (3 + 4 * e)%Z)
  | _ => None
  end.

Definition of_numeral (d:Numeral.numeral) : option Q :=
  match d with
  | Numeral.Dec d => Some (of_decimal d)
  | Numeral.Hex d => Some (of_hexadecimal d)
  end.

Definition to_numeral (q:Q) : option Numeral.numeral :=
  match to_decimal q with
  | None => None
  | Some q => Some (Numeral.Dec q)
  end.


Definition inject_Z (x : Z) := Qmake x 1.

Notation QDen p := (Zpos (Qden p)).

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.

Lemma Qeq_bool_comm x y: Qeq_bool x y = Qeq_bool y x.

Lemma Qeq_bool_refl x: Qeq_bool x x = true.

Lemma Qeq_bool_sym x y: Qeq_bool x y = true -> Qeq_bool y x = true.

Lemma Qeq_bool_trans x y z: Qeq_bool x y = true -> Qeq_bool y z = true -> Qeq_bool x z = true.

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

Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos 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.

Lemma Qinv_plus_distr : forall a b c, ((a # c) + (b # c) == (a+b) # c)%Q.

Lemma Qinv_minus_distr : forall a b c, (a # c) + - (b # c) == (a-b) # c.

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 x y : ~ x < y -> y <= x.

Lemma Qnot_le_lt x y : ~ x <= y -> y < x.

Lemma Qlt_not_le x y : x < y -> ~ y <= x.

Lemma Qle_not_lt 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}.

Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }.

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.

Lemma Qinv_lt_contravar : forall a b : Q,
    0 < a -> 0 < b -> (a < b <-> /b < /a).

Rational to the n-th power


Definition Qpower_positive : Q -> positive -> Q :=
 pow_pos Qmult.

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.