implementations.semiring_pairs

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

Inductive SRpair (SR : Type) := C { pos : SR ; neg : SR }.
Implicit Arguments C [[SR]].
Implicit Arguments pos [[SR]].
Implicit Arguments neg [[SR]].

Section semiring_pairs.
Context `{SemiRing SR} `{Apart SR}.
Context `{ z, LeftCancellation (+) z}.

Add Ring SR : (rings.stdlib_semiring_theory SR).

Global Instance SRpair_equiv : Equiv (SRpair SR) := λ x y, pos x + neg y = pos y + neg x.
Global Instance SRpair_apart `{Apart SR} : Apart (SRpair SR) := λ x y, pos x + neg y pos y + neg x.

Global Instance SRpair_trivial_apart `{!TrivialApart SR} : TrivialApart (SRpair SR).

Instance: Setoid (SRpair SR).

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

Global Instance SRpair_inject: Coerce SR (SRpair SR) := λ r, C r 0.

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

Global Instance SRpair_plus: RingPlus (SRpair SR) := λ x y, C (pos x + pos y) (neg x + neg y).
Global Instance SRpair_opp: GroupInv (SRpair SR) := λ x, C (neg x) (pos x).
Global Instance SRpair_0: RingZero (SRpair SR) := ('0 : SRpair SR).
Global Instance SRpair_mult: RingMult (SRpair SR) := λ x y, C (pos x * pos y + neg x * neg y) (pos x * neg y + neg x * pos y).
Global Instance SRpair_1: RingOne (SRpair SR) := ('1 : SRpair SR).

Ltac unfolds := unfold SRpair_opp, SRpair_plus, equiv, SRpair_equiv in *; simpl in *.
Ltac ring_on_sr := repeat intro; unfolds; try ring.

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

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

Let SRpair_mult_proper_r (x y z : SRpair SR) : x = y z * x = z * y.

Instance: Commutative SRpair_mult.

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

Global Instance: Ring (SRpair SR).

Global Instance: SemiRing_Morphism SRpair_inject.

Global Instance: Injective SRpair_inject.

Lemma SRpair_splits n m : C n m = 'n + -'m.

Global Instance SRpair_le `{Le SR} : Le (SRpair SR) := λ x y, pos x + neg y pos y + neg x.
Global Instance SRpair_lt `{Lt SR} : Lt (SRpair SR) := λ x y, pos x + neg y < pos y + neg x.
Ltac unfold_le := unfold le, SRpair_le, equiv, SRpair_equiv; simpl.
Ltac unfold_lt := unfold lt, SRpair_lt, equiv, SRpair_equiv; simpl.

Section with_semiring_order.
  Context `{!SemiRingOrder SRle}.

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

  Global Instance: OrderEmbedding SRpair_inject.

  Instance: Reflexive SRpair_le.

  Instance: Transitive SRpair_le.

  Instance: AntiSymmetric SRpair_le.

  Instance: PartialOrder SRpair_le.

  Instance: z : SRpair SR, OrderPreserving ((+) z).

  Instance: x y : SRpair SR, PropHolds (0 x) PropHolds (0 y) PropHolds (0 x * y).

  Global Instance: SemiRingOrder SRpair_le.
End with_semiring_order.

Section with_strict_semiring_order.
  Context `{!StrictSemiRingOrder SRle}.

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

  Instance: Irreflexive SRpair_lt.

  Instance: Transitive SRpair_lt.

  Instance: z : SRpair SR, StrictlyOrderPreserving ((+) z).

  Instance: StrictSetoidOrder SRpair_lt.

  Instance: x y : SRpair SR, PropHolds (0 < x) PropHolds (0 < y) PropHolds (0 < x * y).

  Global Instance: StrictSemiRingOrder SRpair_lt.
End with_strict_semiring_order.

Section with_full_pseudo_semiring_order.
  Context `{!FullPseudoSemiRingOrder SRle SRlt}.

  Instance: StrongSetoid SR := pseudo_order_setoid.

  Instance: StrongSetoid (SRpair SR).

  Instance: FullPseudoOrder SRpair_le SRpair_lt.

  Instance: z : SRpair SR, StrongSetoid_Morphism (z *.).

  Global Instance: FullPseudoSemiRingOrder SRpair_le SRpair_lt.
End with_full_pseudo_semiring_order.

Global Instance SRpair_dec `{ x y : SR, Decision (x = y)} : x y : SRpair SR, Decision (x = y)
  := λ x y, decide_rel (=) (pos x + neg y) (pos y + neg x).

Global Program Instance SRpair_le_dec `{Le SR} `{ x y: SR, Decision (x y)} : x y : SRpair SR, Decision (x y) := λ x y,
  match decide_rel (≤) (pos x + neg y) (pos y + neg x) with
  | left E => left _
  | right E => right _
  end.

End semiring_pairs.

Typeclasses Opaque SRpair_equiv.
Typeclasses Opaque SRpair_le.