implementations.stdlib_rationals

Require
  stdlib_binary_integers Field QArith.Qfield theory.rationals.
Require Import
  Ring QArith_base Qabs Qpower
  abstract_algebra interfaces.rationals
  interfaces.orders interfaces.additional_operations
  field_of_fractions.

Instance Q_eq: Equiv Q := Qeq.
Instance Q_0 : RingZero Q := 0%Q.
Instance Q_1 : RingOne Q := 1%Q.
Instance Q_opp : GroupInv Q := Qopp.
Instance Q_plus : RingPlus Q := Qplus.
Instance Q_mult : RingMult Q := Qmult.
Instance Q_mult_inv : DecMultInv Q := Qinv.

Instance: Setoid Q := {}.

Instance: DecField Q.

Instance: x y: Q, Decision (x = y) := Qeq_dec.

Instance inject_Z_Q: Coerce Z Q := inject_Z.

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

Instance: SemiRing_Morphism inject_Z.

Instance: Injective inject_Z.

Program Instance Q_to_fracZ: Coerce Q (Frac Z) := λ x, frac (Qnum x) (Zpos (Qden x)) _.

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

Instance: SemiRing_Morphism Q_to_fracZ.

Instance: Injective Q_to_fracZ.

Instance: RationalsToFrac Q := rationals.alt_to_frac Q_to_fracZ.
Instance: Rationals Q := rationals.alt_Build_Rationals Q_to_fracZ inject_Z.

Instance Q_le: Le Q := Qle.
Instance Q_lt: Lt Q := Qlt.

Instance: SemiRingOrder Q_le.

Instance: TotalRelation Q_le.

Instance: FullPseudoSemiRingOrder Q_le Q_lt.

Program Instance: x y: Q, Decision (x y) := λ y x,
  match Qlt_le_dec x y with
  | left _ => right _
  | right _ => left _
  end.

Program Instance: Abs Q := Qabs.

Instance Q_pow: Pow Q Z := Qpower.

Instance: IntPowSpec Q Z Q_pow.

Instance Q_Npow: Pow Q N := λ x n, Qpower x (coerce N Z n).

Instance: NatPowSpec Q N Q_Npow.

Instance Q_shiftl: ShiftL Q Z := λ x k,
  match k with
  | Z0 => x
  | Zpos p => Qmake (Zshiftl (Qnum x) (Zpos p)) (Qden x)
  | Zneg p => Qmake (Qnum x) (shift_pos p (Qden x))
  end.

Instance: ShiftLSpec Q Z Q_shiftl.