implementations.natpair_integers


Require
 theory.naturals orders.naturals.
Require Import
 Ring abstract_algebra theory.categories
 interfaces.naturals interfaces.integers.
Require Export
 implementations.semiring_pairs.

Section contents.
Context `{Naturals N}.
Add Ring N : (rings.stdlib_semiring_theory N).

Notation Z := (SRpair N).

Global Instance z_to_ring: IntegersToRing Z :=
  λ _ _ _ _ _ _ z, naturals_to_semiring N _ (pos z) + - naturals_to_semiring N _ (neg z).

Ltac preservation :=
   repeat (rewrite rings.preserves_plus || rewrite rings.preserves_mult || rewrite rings.preserves_0 || rewrite rings.preserves_1).

Section for_another_ring.
  Context `{Ring R}.

  Add Ring R : (rings.stdlib_ring_theory R).

  Notation n_to_sr := (naturals_to_semiring N R).
  Notation z_to_r := (integers_to_ring Z R).

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

  Ltac derive_preservation := unfold integers_to_ring, z_to_ring; simpl; preservation; ring.

  Let preserves_plus x y: z_to_r (x + y) = z_to_r x + z_to_r y.

  Let preserves_mult x y: z_to_r (x * y) = z_to_r x * z_to_r y.

  Let preserves_1: z_to_r 1 = 1.

  Let preserves_0: z_to_r 0 = 0.

  Global Instance: SemiRing_Morphism z_to_r.

  Section for_another_morphism.
    Context (f : Z R) `{!SemiRing_Morphism f}.

    Definition g : N R := f coerce N (SRpair N).

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

    Instance: SemiRing_Morphism g := {}.

    Lemma agree_on_nat : g = n_to_sr.

    Lemma same_morphism: z_to_r = f.
  End for_another_morphism.
End for_another_ring.

Instance: Initial (rings.object Z).

Global Instance: Integers Z := {}.

Lemma NtoZ_uniq x : naturals_to_semiring N Z x = 'x.

Context `{!NatDistance N}.
Global Program Instance simpleZ_abs : IntAbs Z N := λ x, nat_distance (pos x) (neg x).

Notation n_to_sr := (naturals_to_semiring N Z).

Lemma zero_product_aux (a b : N) : n_to_sr a * n_to_sr b = 0
   n_to_sr a = 0 n_to_sr b = 0.

Global Instance: ZeroProduct Z.

End contents.