implementations.QType_rationals

Require
  theory.fields stdlib_rationals theory.int_pow.
Require Import
  QArith QSig
  abstract_algebra interfaces.orders
  interfaces.integers interfaces.rationals interfaces.additional_operations
  theory.rings theory.rationals.

Module QType_Rationals (Import anyQ: QType).

Module Import props := QProperties anyQ.

Instance QType_equiv: Equiv t := eq.
Instance QType_plus: RingPlus t := add.
Instance QType_0: RingZero t := zero.
Instance QType_1: RingOne t := one.
Instance QType_mult: RingMult t := mul.
Instance QType_opp: GroupInv t := opp.
Instance QType_dec_mult_inv: DecMultInv t := inv.

Instance: Setoid t := {}.

Instance: x y: t, Decision (x = y) := λ x y,
  (match anyQ.eq_bool x y as p return p Qeq_bool (to_Q x) (to_Q y) Decision (x = y) with
  | true => λ e, left _
  | false => λ e, right _
  end) (anyQ.spec_eq_bool x y).



Ltac unfold_equiv := unfold equiv, QType_equiv, eq.

Add Ring Q : Qsrt.
Lemma anyQ_field_theory: field_theory zero one add mul sub opp div inv eq.

Instance: DecField t.

Instance inject_QType_Q: Coerce t Q := to_Q.

Instance: Setoid_Morphism to_Q.

Instance: SemiRing_Morphism to_Q.

Instance inject_Q_QType: Coerce Q t := of_Q.
Instance: Inverse to_Q := of_Q.

Instance: Surjective to_Q.

Instance: Injective to_Q.

Instance: Bijective to_Q := {}.

Instance: Inverse of_Q := to_Q.

Instance: Bijective of_Q.

Instance: SemiRing_Morphism of_Q.

Instance: RationalsToFrac t := iso_to_frac of_Q.
Instance: Rationals t := iso_is_rationals of_Q.

Instance QType_le: Le t := le.
Instance QType_lt: Lt t := lt.

Instance: Proper ((=) ==> (=) ==> iff) QType_le.

Instance: OrderEmbedding to_Q.

Instance: SemiRingOrder QType_le.

Instance: TotalRelation QType_le.

Instance: FullPseudoSemiRingOrder QType_le QType_lt.

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


Program Instance QType_Zpow: Pow t Z := power.

Instance: IntPowSpec t Z QType_Zpow.

Program Instance QType_Npow: Pow t N := λ x n, power x (Z_of_N n).

Instance: NatPowSpec t N QType_Npow.

End QType_Rationals.