theory.rationals

Require Import
  Ring
  abstract_algebra interfaces.integers interfaces.naturals interfaces.rationals
  field_of_fractions natpair_integers
  theory.rings theory.integers theory.dec_fields.

Program Instance slow_rat_dec `{Rationals Q} : x y: Q, Decision (x = y) | 10 := λ x y,
  match decide (rationals_to_frac Q (SRpair nat) x = rationals_to_frac Q (SRpair nat) y) with
  | left E => left _
  | right E => right _
  end.

Section another_integers.
  Context `{Rationals Q} `{Integers Z}.
  Add Ring Z : (stdlib_ring_theory Z).

  Notation ZtoQ := (integers_to_ring Z Q).
  Notation QtoFrac := (rationals_to_frac Q Z).

  Lemma rationals_decompose `{!SemiRing_Morphism (f : Z Q)} (x : Q) :
     num, den, den 0 x = f num / f den.

  Global Instance integers_to_rationals_injective `{!SemiRing_Morphism (f: Z Q)} : Injective f.

  Context `{f : Q Frac Z} `{!SemiRing_Morphism f}.

  Global Instance to_frac_inverse: Inverse f := λ x, ZtoQ (num x) / ZtoQ (den x).

  Global Instance: Surjective f.

  Instance: Bijective f := {}.

  Global Instance: Bijective (f⁻¹) := {}.

  Global Instance: SemiRing_Morphism (f⁻¹) := {}.
End another_integers.

Lemma to_frac_unique `{Rationals Q} `{Integers Z} (f g : Q Frac Z) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} :
   x, f x = g x.

Definition rationals_to_rationals Q1 Q2 `{Rationals Q1} `{Rationals Q2} : Q1 Q2
  := (rationals_to_frac Q2 (SRpair nat))⁻¹ rationals_to_frac Q1 (SRpair nat).

Section another_rationals.
  Context `{Rationals Q1} `{Rationals Q2}.

  Global Instance: SemiRing_Morphism (rationals_to_rationals Q1 Q2) := {}.
  Global Instance: Bijective (rationals_to_rationals Q1 Q2) := {}.

  Instance: Bijective (rationals_to_frac Q1 (SRpair nat)) := {}.

  Lemma to_rationals_involutive:
     x, rationals_to_rationals Q2 Q1 (rationals_to_rationals Q1 Q2 x) = x.

  Lemma to_rationals_unique (f : Q1 Q2) `{!SemiRing_Morphism f} :
     x, f x = rationals_to_rationals Q1 Q2 x.
End another_rationals.

Lemma to_rationals_unique_alt `{Rationals Q1} `{Rationals Q2} (f g : Q1 Q2) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} :
   x, f x = g x.

Lemma morphisms_involutive `{Rationals Q1} `{Rationals Q2} (f : Q1 Q2) (g : Q2 Q1) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} :
   x, f (g x) = x.

Global Instance injective_nats `{Rationals Q} `{Naturals N} `{!SemiRing_Morphism (f : N Q)} : Injective f.

Section isomorphic_image_is_rationals.
  Context `{Rationals Q} `{DecField F}.
  Context (f : Q F) `{!Inverse f} `{!Bijective f} `{!SemiRing_Morphism f}.

  Instance iso_to_frac: RationalsToFrac F := λ Z _ _ _ _ _ _ _ _, rationals_to_frac Q Z f⁻¹.

  Instance: Bijective (f⁻¹) := {}.
  Instance: SemiRing_Morphism (f⁻¹) := {}.

  Lemma iso_is_rationals: Rationals F.
End isomorphic_image_is_rationals.

Section alt_Build_Rationals.
  Context `{DecField F} `{Integers Z} (F_to_fracZ : F Frac Z) `{!SemiRing_Morphism F_to_fracZ} `{!Injective F_to_fracZ}.
  Context (Z_to_F : Z F) `{!SemiRing_Morphism Z_to_F} `{!Injective Z_to_F}.

  Program Instance alt_to_frac: RationalsToFrac F := λ B _ _ _ _ _ _ _ _ x,
    frac (integers_to_ring Z B (num (F_to_fracZ x))) (integers_to_ring Z B (den (F_to_fracZ x))) _.

  Instance: `{Integers B}, Proper ((=) ==> (=)) (rationals_to_frac F B).

  Instance: `{Integers B}, SemiRing_Morphism (rationals_to_frac F B).

  Instance: `{Integers B}, Injective (rationals_to_frac F B).

  Instance: `{Integers B}, Injective (integers_to_ring B F).

  Lemma alt_Build_Rationals: Rationals F.
End alt_Build_Rationals.