theory.integers

Require Export
 interfaces.integers.
Require
 theory.naturals theory.nat_distance.
Require Import
 RelationClasses Ring
 interfaces.naturals abstract_algebra natpair_integers.

Lemma to_ring_involutive `{Integers Int} Int2 `{Integers Int2} x :
  integers_to_ring Int2 Int (integers_to_ring Int Int2 x) = x.

Lemma to_ring_unique `{Integers Int} `{Ring R} (f: Int R) {h: SemiRing_Morphism f} x :
  f x = integers_to_ring Int R x.

Lemma to_ring_unique_alt `{Integers Int} `{Ring R} (f g: Int R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x :
  f x = g x.

Lemma morphisms_involutive `{Integers N} `{Integers N2} (f: N N2) (g: N2 N)
  `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x : f (g x) = x.

Lemma to_ring_twice `{Integers N} `{Ring R1} `{Ring R2} (f : R1 R2) (g : N R1) (h : N R2)
     `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} `{!SemiRing_Morphism h} x :
  f (g x) = h x.

Lemma to_ring_self `{Integers N} (f : N N) `{!SemiRing_Morphism f} x : f x = x.

Lemma to_ring_injective `{Integers Int} `{Ring R} (f: R Int) (g: Int R) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g}:
  Injective g.

Instance integers_to_integers_injective `{Integers Int} `{Integers Int2} (f: Int Int2) `{!SemiRing_Morphism f}:
  Injective f.

Instance naturals_to_integers_injective `{Integers Int} `{Naturals N} (f: N Int) `{!SemiRing_Morphism f} :
  Injective f.

Section retract_is_int.
  Context `{Integers Int} `{Ring Int2}.
  Context (f : Int Int2) `{!Inverse f} `{!Surjective f} `{!SemiRing_Morphism f} `{!SemiRing_Morphism (f⁻¹)}.

  Definition retract_is_int_to_ring : IntegersToRing Int2 := λ R _ _ _ _ _, integers_to_ring Int R f⁻¹.

  Section for_another_ring.
    Context `{Ring R}.

    Instance: SemiRing_Morphism (integers_to_ring Int R f⁻¹) := {}.
    Context (h : Int2 R) `{!SemiRing_Morphism h}.

    Lemma same_morphism: integers_to_ring Int R f⁻¹ = h.
  End for_another_ring.

  Program Definition retract_is_int: Integers Int2 (U:=retract_is_int_to_ring).
End retract_is_int.

Section contents.
Context `{Integers Int}.

Global Program Instance: x y: Int, Decision (x = y) | 10 := λ x y,
  match decide (integers_to_ring Int (SRpair nat) x = integers_to_ring Int (SRpair nat) y) with
  | left E => left _
  | right E => right _
  end.

Instance: PropHolds ((1:Int) 0).

Global Instance zero_product: ZeroProduct Int.

Global Instance: IntegralDomain Int := {}.
End contents.