implementations.nonneg_semiring_elements

Require
  theory.rings.
Require Import
  Ring
  abstract_algebra interfaces.orders orders.semirings.

Section nonneg_semiring_elements.
Context `{SemiRing R} `{Apart R} `{!FullPseudoSemiRingOrder Rlt Rle}.

Add Ring R : (rings.stdlib_semiring_theory R).

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

Global Program Instance NonNeg_plus: RingPlus (R⁺) := λ x y, (x + y)↾_.

Global Program Instance NonNeg_mult: RingMult (R⁺) := λ x y, (x * y)↾_.

Global Program Instance NonNeg_0: RingZero (R⁺) := 0_.

Global Program Instance NonNeg_1: RingOne (R⁺) := 1_.

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

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

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

Global Instance: SemiRing (R⁺).

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

Global Instance: SemiRing_Morphism NonNeg_inject.

Global Instance: Injective NonNeg_inject.

Global Instance NonNeg_trivial_apart `{!TrivialApart R} : TrivialApart (R⁺).

Global Instance NonNeg_equiv_dec `{ x y : R, Decision (x = y)} : x y: R⁺, Decision (x = y)
  := λ x y, decide_rel (=) ('x) ('y).

Global Instance NonNeg_apart_dec `{ x y : R, Decision (x y)} : x y: R⁺, Decision (x y)
  := λ x y, decide_rel (⪥) ('x) ('y).

Global Instance NonNeg_le: Le (R⁺) := λ x y, 'x 'y.
Global Instance NonNeg_lt: Lt (R⁺) := λ x y, 'x < 'y.

Global Instance: Proper ((=) ==> (=) ==> iff) NonNeg_le.

Global Instance: OrderEmbedding NonNeg_inject.

Instance: PartialOrder NonNeg_le.
Global Program Instance NonNeg_le_dec `{ x y : R, Decision (x y)} : x y: R⁺, Decision (x y) := λ x y,
  match decide_rel (≤) ('x) ('y) with
  | left E => left _
  | right E => right _
  end.
End nonneg_semiring_elements.

Typeclasses Opaque NonNeg_le.
Typeclasses Opaque NonNeg_lt.