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.