implementations.fast_rationals

Require
  theory.shiftl theory.int_pow.
Require Import
  QArith BigQ
  abstract_algebra
  interfaces.integers interfaces.rationals interfaces.additional_operations
  fast_naturals fast_integers field_of_fractions stdlib_rationals.
Require Export
  QType_rationals.

Module Import BigQ_Rationals := QType_Rationals BigQ.

Instance inject_bigZ_bigQ: Coerce bigZ bigQ := BigQ.Qz.
Instance inject_bigN_bigQ: Coerce bigN bigQ := coerce bigZ bigQ coerce bigN bigZ.
Instance inject_Z_bigQ: Coerce Z bigQ := coerce bigZ bigQ coerce Z bigZ.

Instance: Proper ((=) ==> (=)) inject_bigZ_bigQ.

Instance: SemiRing_Morphism inject_bigZ_bigQ.

Instance: Proper ((=) ==> (=) ==> (=)) BigQ.Qq.

Lemma bigQ_div_bigQq (n : bigZ) (d : bigN) :
  BigQ.Qq n d = 'n / 'd.

Lemma bigQ_div_bigQq_alt (n : bigZ) (d : bigN) :
  BigQ.Qq n d = 'n / 'coerce bigN bigZ d.

Instance inject_bigQ_frac_bigZ: Coerce bigQ (Frac bigZ) := λ x,
  match x with
  | BigQ.Qz n => 'n
  | BigQ.Qq n d =>
     match decide_rel (=) ('d : bigZ) 0 with
     | left _ => 0
     | right E => frac n ('d) E
     end
  end.

Lemma inject_bigQ_frac_bigZ_correct:
 coerce bigQ (Frac bigZ) = rationals_to_frac bigQ bigZ.

Instance: Injective inject_bigQ_frac_bigZ.

Instance: SemiRing_Morphism inject_bigQ_frac_bigZ.

Instance bigQ_shiftl: ShiftL bigQ bigZ := λ x k,
  match k with
  | BigZ.Pos k =>
    match x with
    | BigQ.Qz n => '(n k)
    | BigQ.Qq n d => BigQ.Qq (n k) d
    end
  | BigZ.Neg k =>
    match x with
    | BigQ.Qz n => BigQ.Qq n (1 k)
    | BigQ.Qq n d => BigQ.Qq n (d k)
    end
  end.

Instance: ShiftLSpec bigQ bigZ _.

Instance bigQ_Zshiftl: ShiftL bigQ Z := λ x k, x 'k.

Instance: ShiftLSpec bigQ Z _.