# implementations.NType_naturals

Require

stdlib_binary_integers theory.integers orders.semirings.

Require Import

Setoid NSig NSigNAxioms NArith ZArith Program Morphisms

abstract_algebra interfaces.naturals interfaces.integers

interfaces.orders interfaces.additional_operations.

Module NType_Integers (Import anyN: NType).

Module axioms := NTypeIsNAxioms anyN.

Instance NType_equiv : Equiv t := eq.

Instance NType_plus : RingPlus t := add.

Instance NType_0 : RingZero t := zero.

Instance NType_1 : RingOne t := one.

Instance NType_mult : RingMult t := mul.

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, NType_equiv, eq in *.

Lemma NType_semiring_theory: semi_ring_theory zero one add mul eq.

Instance: SemiRing t | 10 := rings.from_stdlib_semiring_theory NType_semiring_theory.

Instance inject_NType_N: Coerce t N := to_N.

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

Instance: SemiRing_Morphism to_N.

Instance inject_N_NType: Coerce N t := of_N.

Instance: Inverse to_N := of_N.

Instance: Surjective to_N.

Instance: Injective to_N.

Instance: Bijective to_N := {}.

Instance: Inverse of_N := to_N.

Instance: Bijective of_N.

Instance: SemiRing_Morphism of_N.

Instance: NaturalsToSemiRing t := naturals.retract_is_nat_to_sr of_N.

Instance: Naturals t := naturals.retract_is_nat of_N.

Instance inject_NType_Z: Coerce t Z := to_Z.

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

Instance: SemiRing_Morphism to_Z.

Instance NType_le: Le t := le.

Instance NType_lt: Lt t := lt.

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

Instance: OrderEmbedding to_Z.

Instance: PartialOrder NType_le.

Instance: SemiRingOrder NType_le.

Instance: TotalRelation NType_le.

Instance: FullPseudoSemiRingOrder NType_le NType_lt.

Program Instance: ∀ x y: t, Decision (x ≤ y) := λ x y, match (compare x y) with

| Gt => right _

| _ => left _

end.

Lemma NType_succ_1_plus x : succ x = 1 + x.

Lemma NType_two_2 : two = 2.

Program Instance NType_pow: Pow t t := pow.

Instance: NatPowSpec t t NType_pow.

Program Instance NType_shiftl: ShiftL t t := shiftl.

Instance: ShiftLSpec t t NType_shiftl.

Program Instance: ShiftR t t := shiftr.

End NType_Integers.

stdlib_binary_integers theory.integers orders.semirings.

Require Import

Setoid NSig NSigNAxioms NArith ZArith Program Morphisms

abstract_algebra interfaces.naturals interfaces.integers

interfaces.orders interfaces.additional_operations.

Module NType_Integers (Import anyN: NType).

Module axioms := NTypeIsNAxioms anyN.

Instance NType_equiv : Equiv t := eq.

Instance NType_plus : RingPlus t := add.

Instance NType_0 : RingZero t := zero.

Instance NType_1 : RingOne t := one.

Instance NType_mult : RingMult t := mul.

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, NType_equiv, eq in *.

Lemma NType_semiring_theory: semi_ring_theory zero one add mul eq.

Instance: SemiRing t | 10 := rings.from_stdlib_semiring_theory NType_semiring_theory.

Instance inject_NType_N: Coerce t N := to_N.

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

Instance: SemiRing_Morphism to_N.

Instance inject_N_NType: Coerce N t := of_N.

Instance: Inverse to_N := of_N.

Instance: Surjective to_N.

Instance: Injective to_N.

Instance: Bijective to_N := {}.

Instance: Inverse of_N := to_N.

Instance: Bijective of_N.

Instance: SemiRing_Morphism of_N.

Instance: NaturalsToSemiRing t := naturals.retract_is_nat_to_sr of_N.

Instance: Naturals t := naturals.retract_is_nat of_N.

Instance inject_NType_Z: Coerce t Z := to_Z.

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

Instance: SemiRing_Morphism to_Z.

Instance NType_le: Le t := le.

Instance NType_lt: Lt t := lt.

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

Instance: OrderEmbedding to_Z.

Instance: PartialOrder NType_le.

Instance: SemiRingOrder NType_le.

Instance: TotalRelation NType_le.

Instance: FullPseudoSemiRingOrder NType_le NType_lt.

Program Instance: ∀ x y: t, Decision (x ≤ y) := λ x y, match (compare x y) with

| Gt => right _

| _ => left _

end.

Lemma NType_succ_1_plus x : succ x = 1 + x.

Lemma NType_two_2 : two = 2.

Program Instance NType_pow: Pow t t := pow.

Instance: NatPowSpec t t NType_pow.

Program Instance NType_shiftl: ShiftL t t := shiftl.

Instance: ShiftLSpec t t NType_shiftl.

Program Instance: ShiftR t t := shiftr.

End NType_Integers.