implementations.field_of_fractions

Require theory.fields.
Require Import Morphisms Ring abstract_algebra theory.rings.

Inductive Frac R `{ap : Equiv R} `{zero : RingZero R} : Type := frac { num: R; den: R; den_ne_0: den 0 }.
Implicit Arguments frac [[R] [ap] [zero]].
Implicit Arguments num [[R] [ap] [zero]].
Implicit Arguments den [[R] [ap] [zero]].
Implicit Arguments den_ne_0 [[R] [ap] [zero]].

Section contents.
Context `{IntegralDomain R} `{ x y, Decision (x = y)}.

Add Ring R: (stdlib_ring_theory R).

Global Instance Frac_equiv: Equiv (Frac R) := λ x y, num x * den y = num y * den x.

Instance: Setoid (Frac R).

Global Instance Frac_dec : x y: Frac R, Decision (x = y)
  := λ x y, decide_rel (=) (num x * den y) (num y * den x).

Global Program Instance Frac_inject: Coerce R (Frac R) := λ r, frac r 1 _.

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

Global Program Instance Frac_plus: RingPlus (Frac R) :=
  λ x y, frac (num x * den y + num y * den x) (den x * den y) _.

Global Instance Frac_0: RingZero (Frac R) := ('0 : Frac R).
Global Instance Frac_1: RingOne (Frac R) := ('1 : Frac R).

Global Instance Frac_opp: GroupInv (Frac R) := λ x, frac (- num x) (den x) (den_ne_0 x).

Global Program Instance Frac_mult: RingMult (Frac R) := λ x y, frac (num x * num y) (den x * den y) _.

Ltac unfolds := unfold Frac_opp, Frac_plus, equiv, Frac_equiv in *; simpl in *.
Ltac ring_on_ring := repeat intro; unfolds; try ring.

Lemma Frac_nonzero_num x : x 0 num x 0.

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

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

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

Instance: Ring (Frac R).

Global Instance Frac_dec_mult_inv: DecMultInv (Frac R) := λ x,
  match decide_rel (=) (num x) 0 with
  | left _ => 0
  | right P => frac (den x) (num x) P
  end.

Instance: Setoid_Morphism Frac_dec_mult_inv.

Global Instance: DecField (Frac R).

Lemma Frac_dec_mult_num_den x :
  x = 'num x / 'den x.

Global Instance: SemiRing_Morphism Frac_inject.

Global Instance: Injective Frac_inject.
End contents.

Typeclasses Opaque Frac_equiv.

Section morphisms.
Context `{IntegralDomain R1} `{ x y : R1, Decision (x = y)}.
Context `{IntegralDomain R2} `{ x y : R2, Decision (x = y)}.
Context `(f : R1 R2) `{!SemiRing_Morphism f} `{!Injective f}.

Program Definition Frac_lift (x : Frac R1) : Frac R2 := frac (f (num x)) (f (den x)) _.

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

Global Instance: SemiRing_Morphism Frac_lift.

Global Instance: Injective Frac_lift.
End morphisms.