# Library Coq.ZArith.Zabs

Binary Integers (Pierre Crégut (CNET, Lannion, France)
Require Import Arith_base.
Require Import BinPos.
Require Import BinInt.
Require Import Zorder.
Require Import Zmax.
Require Import Znat.
Require Import ZArith_dec.
Open Local Scope Z_scope.

# Properties of absolute value

Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n.
Lemma Zabs_non_eq : forall n:Z, n <= 0 -> Zabs n = - n.
Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n.

# Proving a property of the absolute value by cases

Lemma Zabs_ind :
forall (P:Z -> Prop) (n:Z),
(n >= 0 -> P n) -> (n <= 0 -> P (- n)) -> P (Zabs n).
Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Zabs n).
Definition Zabs_dec : forall x:Z, { x = Zabs x } + { x = - Zabs x }.
Lemma Zabs_pos : forall n:Z, 0 <= Zabs n.
Lemma Zabs_involutive : forall x:Z, Zabs (Zabs x) = Zabs x.
Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m.
Lemma Zabs_spec : forall x:Z,
0 <= x /\ Zabs x = x \/
0 > x /\ Zabs x = - x.

# Triangular inequality

Hint Local Resolve Zle_neg_pos: zarith.
Theorem Zabs_triangle : forall n m:Z, Zabs (n + m) <= Zabs n + Zabs m.

# Absolute value and multiplication

Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n.
Lemma Zabs_Zsgn : forall n:Z, Zabs n * Zsgn n = n.
Theorem Zabs_Zmult : forall n m:Z, Zabs (n * m) = Zabs n * Zabs m.
Theorem Zabs_square : forall a, Zabs a * Zabs a = a * a.

# Results about absolute value in nat.

Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n * m) = (Zabs_nat n * Zabs_nat m)%nat.
Lemma Zabs_nat_Zsucc:
forall p, 0 <= p -> Zabs_nat (Zsucc p) = S (Zabs_nat p).
Lemma Zabs_nat_Zplus:
forall x y, 0<= x -> 0<= y -> Zabs_nat (x + y) = (Zabs_nat x + Zabs_nat y)%nat.
Lemma Zabs_nat_Zminus:
forall x y, 0 <= x <= y -> Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat.
Lemma Zabs_nat_le :
forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
Lemma Zabs_nat_lt :
forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.

# Some results about the sign function.

Lemma Zsgn_Zmult : forall a b, Zsgn (a * b) = Zsgn a * Zsgn b.
Lemma Zsgn_Zopp : forall a, Zsgn (- a) = - Zsgn a.
A characterization of the sign function:
Lemma Zsgn_spec : forall x:Z,
0 < x /\ Zsgn x = 1 \/
0 = x /\ Zsgn x = 0 \/
0 > x /\ Zsgn x = -1.
Lemma Zsgn_pos : forall x:Z, Zsgn x = 1 <-> 0 < x.
Lemma Zsgn_neg : forall x:Z, Zsgn x = -1 <-> x < 0.
Lemma Zsgn_null : forall x:Z, Zsgn x = 0 <-> x = 0.