theory.abs

Require Import
  Setoid Morphisms Ring
  abstract_algebra interfaces.orders orders.rings.

Section contents.
Context `{Ring R} `{Apart R} `{!TrivialApart R} `{!FullPseudoSemiRingOrder Rle Rlt} `{ x y, Decision (x = y)} `{a : !Abs R}.

Add Ring R : (rings.stdlib_ring_theory R).

Global Instance abs_proper: Proper ((=) ==> (=)) abs.

Lemma abs_nonneg (x : R) : 0 x abs x = x.

Lemma abs_nonpos (x : R) : x 0 abs x = -x.

Lemma abs_nonneg_plus (x y : R) :
  0 x 0 y abs (x + y) = abs x + abs y.

Lemma abs_nonpos_plus (x y : R) :
  x 0 y 0 abs (x + y) = abs x + abs y.

Lemma abs_0 : abs 0 = 0.

Lemma abs_mult (x y : R) : abs (x * y) = abs x * abs y.

Lemma abs_1 : abs 1 = 1.

Lemma abs_opp (x : R) : abs (-x) = abs x.
End contents.

Program Instance default_abs `{Ring R} `{!SemiRingOrder Rle} `{ x y, Decision (x y)} : Abs R | 20
  := λ x, if decide_rel (≤) 0 x then x else (-x).

Section order_preserving.
  Context `{Ring A} `{oA : Le A} `{!SemiRingOrder oA} `{!TotalRelation oA} `{!Abs A}
    `{Ring B} `{oB : Le B} `{!SemiRingOrder oB} `{!TotalRelation oB} `{!Abs B}
    {f : A B} `{!OrderPreserving f} `{!SemiRing_Morphism f}.

  Lemma preserves_abs x : f (abs x) = abs (f x).
End order_preserving.