implementations.positive_semiring_elements

Require Import
  Ring
  abstract_algebra additional_operations
  interfaces.orders interfaces.integers
  orders.semirings theory.shiftl theory.int_pow.

Section positive_semiring_elements.
Context `{SemiRing R} `{Apart R} `{!FullPseudoSemiRingOrder Rle Rlt} `{!PropHolds (1 0)}.

Add Ring R : (rings.stdlib_semiring_theory R).

Global Instance Pos_inject: Coerce (R) R := @proj1_sig R _.

Global Program Instance Pos_plus: RingPlus (R) := λ x y, (x + y : R).

Global Program Instance Pos_mult: RingMult (R) := λ x y, (x * y : R).

Global Program Instance Pos_1: RingOne (R) := (1 : R).

Local Ltac unfold_equivs := unfold equiv, sig_equiv in *; simpl in *.

Global Instance: Proper ((=) ==> (=) ==> (=)) Pos_plus.

Global Instance: Proper ((=) ==> (=) ==> (=)) Pos_mult.

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

Global Instance: Injective Pos_inject.

Section shiftl.
  Context `{SemiRing B} `{!Biinduction B} `{!ShiftLSpec R B sl}.

  Global Program Instance Pos_shiftl: ShiftL (R) B | 5 := λ x n, (x n : R).
End shiftl.
End positive_semiring_elements.

Section int_pow.
  Context `{DecField R} `{Apart R} `{!FullPseudoSemiRingOrder Rle Rlt}
    `{!TrivialApart R} `{ x y : R, Decision (x = y)} `{Integers B} `{!IntPowSpec R B ipw}.

  Global Program Instance Pos_int_pow: Pow (R) B | 5 := λ x n, (x ^ n : R).
End int_pow.