implementations.stdlib_binary_integers

Require
  interfaces.naturals theory.naturals peano_naturals theory.integers.
Require Import
  BinInt Ring Arith NArith ZBinary
  abstract_algebra interfaces.integers
  natpair_integers stdlib_binary_naturals
  interfaces.additional_operations interfaces.orders
  nonneg_integers_naturals.

Instance Z_equiv: Equiv Z := eq.
Instance Z_plus: RingPlus Z := Zplus.
Instance Z_0: RingZero Z := 0%Z.
Instance Z_1: RingOne Z := 1%Z.
Instance Z_mult: RingMult Z := Zmult.
Instance Z_opp: GroupInv Z := Zopp.

Instance: Ring Z.

Instance: x y : Z, Decision (x = y) := ZArith_dec.Z_eq_dec.

Add Ring Z: (rings.stdlib_ring_theory Z).

Instance inject_N_Z: Coerce BinNat.N Z := Z_of_N.

Instance: SemiRing_Morphism Z_of_N.

Instance: Injective Z_of_N.

Definition Npair_to_Z (x : SRpair N) : Z := 'pos x - 'neg x.

Instance: Proper (=) Npair_to_Z.

Instance: SemiRing_Morphism Npair_to_Z.

Instance: Injective Npair_to_Z.

Instance Z_to_Npair: Inverse Npair_to_Z := λ x,
  match x with
  | Z0 => C 0 0
  | Zpos p => C (Npos p) 0
  | Zneg p => C 0 (Npos p)
  end.

Instance: Surjective Npair_to_Z.

Instance: Bijective Npair_to_Z := {}.

Instance: SemiRing_Morphism Z_to_Npair.

Instance: IntegersToRing Z := integers.retract_is_int_to_ring Npair_to_Z.
Instance: Integers Z := integers.retract_is_int Npair_to_Z.

Instance Z_le: Le Z := Zle.
Instance Z_lt: Lt Z := Zlt.

Instance: SemiRingOrder Z_le.

Instance: TotalRelation Z_le.

Instance: FullPseudoSemiRingOrder Z_le Z_lt.

Instance inject_nat_Z: Coerce nat Z := Z_of_nat.

Instance: SemiRing_Morphism Z_of_nat.

Program Instance: IntAbs Z nat := Zabs_nat.

Program Instance: IntAbs Z N := Zabs_N.

Program Instance Z_pow: Pow Z (Z⁺) := Z.pow.

Instance: NatPowSpec Z (Z⁺) Z_pow.

Instance Z_Npow: Pow Z N := λ x n, Z.pow x ('n).

Instance: NatPowSpec Z N Z_Npow.

Program Instance Z_shiftl: ShiftL Z (Z⁺) := Z.shiftl.

Instance: ShiftLSpec Z (Z⁺) Z_shiftl.

Instance Z_Nshiftl: ShiftL Z N := λ x n, Z.shiftl x ('n).

Instance: ShiftLSpec Z N Z_Nshiftl.

Program Instance: Abs Z := Zabs.