Library Coq.Numbers.Integer.Abstract.ZSgnAbs

Require Import ZMulOrder.

Module GenericAbs (Import Z : ZAxiomsMiniSig´)
                  (Import ZP : ZMulOrderProp Z) <: HasAbs Z.
 Definition abs n := max n (-n).
 Lemma abs_eq : forall n, 0<=n -> abs n == n.
 Lemma abs_neq : forall n, n<=0 -> abs n == -n.
End GenericAbs.

Module Type ZDecAxiomsSig := ZAxiomsMiniSig <+ HasCompare.
Module Type ZDecAxiomsSig´ := ZAxiomsMiniSig´ <+ HasCompare.

Module Type GenericSgn (Import Z : ZDecAxiomsSig´)
                       (Import ZP : ZMulOrderProp Z) <: HasSgn Z.
 Definition sgn n :=
  match compare 0 n with Eq => 0 | Lt => 1 | Gt => -1 end.
 Lemma sgn_null : forall n, n==0 -> sgn n == 0.
 Lemma sgn_pos : forall n, 0<n -> sgn n == 1.
 Lemma sgn_neg : forall n, n<0 -> sgn n == -1.
End GenericSgn.

Module Type ZSgnAbsProp (Import Z : ZAxiomsSig´)
                        (Import ZP : ZMulOrderProp Z).

Ltac destruct_max n :=
 destruct (le_ge_cases 0 n);
  [rewrite (abs_eq n) by auto | rewrite (abs_neq n) by auto].

Instance abs_wd : Proper (eq==>eq) abs.

Lemma abs_max : forall n, abs n == max n (-n).

Lemma abs_neq´ : forall n, 0<=-n -> abs n == -n.

Lemma abs_nonneg : forall n, 0 <= abs n.

Lemma abs_eq_iff : forall n, abs n == n <-> 0<=n.

Lemma abs_neq_iff : forall n, abs n == -n <-> n<=0.

Lemma abs_opp : forall n, abs (-n) == abs n.

Lemma abs_0 : abs 0 == 0.

Lemma abs_0_iff : forall n, abs n == 0 <-> n==0.

Lemma abs_pos : forall n, 0 < abs n <-> n~=0.

Lemma abs_eq_or_opp : forall n, abs n == n \/ abs n == -n.

Lemma abs_or_opp_abs : forall n, n == abs n \/ n == - abs n.

Lemma abs_involutive : forall n, abs (abs n) == abs n.

Lemma abs_spec : forall n,
  (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n).

Lemma abs_case_strong :
  forall (P:t->Prop) n, Proper (eq==>iff) P ->
    (0<=n -> P n) -> (n<=0 -> P (-n)) -> P (abs n).

Lemma abs_case : forall (P:t->Prop) n, Proper (eq==>iff) P ->
 P n -> P (-n) -> P (abs n).

Lemma abs_eq_cases : forall n m, abs n == abs m -> n == m \/ n == - m.

Lemma abs_lt : forall a b, abs a < b <-> -b < a < b.

Lemma abs_le : forall a b, abs a <= b <-> -b <= a <= b.

Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m.

Lemma abs_sub_triangle : forall n m, abs n - abs m <= abs (n-m).

Lemma abs_mul : forall n m, abs (n * m) == abs n * abs m.

Lemma abs_square : forall n, abs n * abs n == n * n.

Ltac destruct_sgn n :=
 let LT := fresh "LT" in
 let EQ := fresh "EQ" in
 let GT := fresh "GT" in
 destruct (lt_trichotomy 0 n) as [LT|[EQ|GT]];
 [rewrite (sgn_pos n) by auto|
  rewrite (sgn_null n) by auto with relations|
  rewrite (sgn_neg n) by auto].

Instance sgn_wd : Proper (eq==>eq) sgn.

Lemma sgn_spec : forall n,
  0 < n /\ sgn n == 1 \/
  0 == n /\ sgn n == 0 \/
  0 > n /\ sgn n == -1.

Lemma sgn_0 : sgn 0 == 0.

Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n.

Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0.

Lemma sgn_neg_iff : forall n, sgn n == -1 <-> n<0.

Lemma sgn_opp : forall n, sgn (-n) == - sgn n.

Lemma sgn_nonneg : forall n, 0 <= sgn n <-> 0 <= n.

Lemma sgn_nonpos : forall n, sgn n <= 0 <-> n <= 0.

Lemma sgn_mul : forall n m, sgn (n*m) == sgn n * sgn m.

Lemma sgn_abs : forall n, n * sgn n == abs n.

Lemma abs_sgn : forall n, abs n * sgn n == n.

Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x.

End ZSgnAbsProp.