implementations.peano_naturals

Require
  ua_homomorphisms.
Require Import
  Morphisms Ring Arith_base
  abstract_algebra interfaces.naturals theory.categories
  interfaces.additional_operations interfaces.orders orders.semirings.

Instance nat_equiv: Equiv nat := eq.
Instance nat_plus: RingPlus nat := plus.
Instance nat_0: RingZero nat := 0%nat.
Instance nat_1: RingOne nat := 1%nat.
Instance nat_mult: RingMult nat := mult.

Instance: SemiRing nat.

Global Instance nat_dec: x y: nat, Decision (x = y) := eq_nat_dec.

Add Ring nat: (rings.stdlib_semiring_theory nat).

Close Scope nat_scope.

Instance: NaturalsToSemiRing nat :=
  λ _ _ _ _ _, fix f (n: nat) := match n with 0%nat => 0 | S n' => f n' + 1 end.

Section for_another_semiring.
  Context `{SemiRing R}.

  Notation toR := (naturals_to_semiring nat R).

  Add Ring R: (rings.stdlib_semiring_theory R).

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

  Let f_preserves_0: toR 0 = 0.

  Let f_preserves_1: toR 1 = 1.

  Let f_preserves_plus a a': toR (a + a') = toR a + toR a'.

  Let f_preserves_mult a a': toR (a * a') = toR a * toR a'.

  Global Instance: SemiRing_Morphism (naturals_to_semiring nat R).
  Qed.
End for_another_semiring.

Lemma S_nat_plus_1 x : S x x + 1.

Lemma S_nat_1_plus x : S x 1 + x.

Instance: Initial (semirings.object nat).

Instance: Naturals nat := {}.

Instance: NoZeroDivisors nat.

Instance: z : nat, PropHolds (z 0) LeftCancellation (.*.) z.

Instance nat_le: Le nat := Peano.le.
Instance nat_lt: Lt nat := Peano.lt.

Instance: FullPseudoSemiRingOrder nat_le nat_lt.

Instance nat_le_dec: Decision (x y) := le_dec.

Instance nat_cut_minus: CutMinus nat := minus.
Instance: CutMinusSpec nat nat_cut_minus.