implementations.ZType_integers

Require
  stdlib_binary_integers theory.integers orders.semirings.
Require Import
  ZSig ZSigZAxioms NArith ZArith
  nonneg_integers_naturals interfaces.orders
  abstract_algebra interfaces.integers interfaces.additional_operations.

Module ZType_Integers (Import anyZ: ZType).

Module axioms := ZTypeIsZAxioms anyZ.

Instance ZType_equiv : Equiv t := eq.
Instance ZType_plus : RingPlus t := add.
Instance ZType_0 : RingZero t := zero.
Instance ZType_1 : RingOne t := one.
Instance ZType_mult : RingMult t := mul.
Instance ZType_opp: GroupInv t := opp.

Instance: Setoid t | 10 := {}.

Program Instance: x y: t, Decision (x = y) := λ x y, match (compare x y) with
  | Eq => left _
  | _ => right _
  end.

Ltac unfold_equiv := unfold equiv, ZType_equiv, eq in *.

Lemma ZType_ring_theory: ring_theory zero one add mul sub opp eq.

Instance: Ring t | 10 := rings.from_stdlib_ring_theory ZType_ring_theory.

Instance inject_ZType_Z: Coerce t Z := to_Z.

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

Instance: SemiRing_Morphism to_Z.

Instance inject_Z_ZType: Coerce Z t := of_Z.
Instance: Inverse to_Z := of_Z.

Instance: Surjective to_Z.

Instance: Injective to_Z.

Instance: Bijective to_Z := {}.

Instance: Inverse of_Z := to_Z.

Instance: Bijective of_Z.

Instance: SemiRing_Morphism of_Z.

Instance: IntegersToRing t := integers.retract_is_int_to_ring of_Z.
Instance: Integers t := integers.retract_is_int of_Z.

Instance ZType_le: Le t := le.
Instance ZType_lt: Lt t := lt.

Instance: Proper ((=) ==> (=) ==> iff) ZType_le.

Instance: OrderEmbedding to_Z.

Instance: SemiRingOrder ZType_le.

Instance: TotalRelation ZType_le.

Instance: FullPseudoSemiRingOrder ZType_le ZType_lt.

Program Instance: x y: t, Decision (x y) := λ x y, match (compare x y) with
  | Gt => right _
  | _ => left _
  end.


Program Instance: IntAbs t (t⁺) := abs.


Program Instance: Abs t := abs.

Instance ZType_div: DivEuclid t := div.
Instance ZType_mod: ModEuclid t := modulo.

Instance: EuclidSpec t ZType_div ZType_mod.

Lemma ZType_succ_1_plus x : succ x = 1 + x.

Lemma ZType_two_2 : two = 2.

Program Instance ZType_pow: Pow t (t⁺) := pow.

Instance: NatPowSpec t (t⁺) ZType_pow.

Program Instance ZType_Npow: Pow t N := pow_N.

Instance: NatPowSpec t N ZType_Npow.


Program Instance ZType_shiftl: ShiftL t (t⁺) := shiftl.

Instance: ShiftLSpec t (t⁺) ZType_shiftl.

Program Instance: ShiftR t (t⁺) := shiftr.

End ZType_Integers.