# 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.