# Library CoLoR.Util.Integer.ZUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-04-20
• Frederic Blanqui, 2005-02-25
useful definitions and lemmas about integers

Set Implicit Arguments.

decidability of equality

Local Open Scope positive_scope.

Fixpoint beq_pos x y :=
match x, y with
| xI x', xI y' => beq_pos x' y'
| xO x', xO y' => beq_pos x' y'
| xH, xH => true
| _, _ => false
end.

Lemma beq_pos_ok : forall x y, beq_pos x y = true <-> x = y.

Local Open Scope Z_scope.

Fixpoint beq_Z x y :=
match x, y with
| Z0, Z0 => true
| Zpos x', Zpos y' => beq_pos x' y'
| Zneg x', Zneg y' => beq_pos x' y'
| _, _ => false
end.

Lemma beq_Z_ok : forall x y, beq_Z x y = true <-> x = y.

simplification

Lemma zeql : forall x,
match x with
| Z0 => 0
| Zpos y' => Zpos y'
| Zneg y' => Zneg y'
end = x.

Lemma zeqr : forall x,
x = match x with
| Z0 => 0
| Zpos y' => Zpos y'
| Zneg y' => Zneg y'
end.

inequalities

Lemma pos_lt : forall x y : Z, 0 <= y-x-1 -> x < y.

Lemma pos_le : forall x y : Z, 0 <= y-x -> x <= y.

power

Fixpoint power (x : Z) (n : nat) : Z :=
match n with
| O => 1
| S n' => x * power x n'
end.

Infix "^" := power.

Lemma power_plus : forall x n1 n2, power x (n1+n2) = power x n1 * power x n2.

Lemma power_one : forall n, power 1 n = 1.

Lemma power_succ : forall x n, power x (S n) = x * power x n.

Lemma power_mult : forall x n1 n2, power x (n1*n2) = power (power x n1) n2.

Lemma pos_power : forall x n, 0 <= x -> 0 <= power x n.

Lemma spos_power : forall x n, 0 < x -> 0 < power x n.

Lemma power_le_compat : forall x y n, 0<=x -> x<=y -> power x n <= power y n.

positive integers

Definition is_pos z :=
match z with
| Zpos _ => true
| _ => false
end.

Lemma is_pos_ok : forall z, is_pos z = true <-> z > 0.

non-negative integers

Definition is_not_neg z :=
match z with
| Zneg _ => false
| _ => true
end.

Lemma is_not_neg_ok : forall z, is_not_neg z = true <-> 0 <= z.

Notation pos := (fun z => 0 <= z).
Notation D := (sig pos).
Notation val := (@proj1_sig Z pos).
Notation inj := (@exist Z pos _).

Lemma Zero_in_D : pos 0.

Notation D0 := (inj Zero_in_D).

Lemma pos_power_val : forall x n, pos (power (val x) n).

Definition Dlt x y := Zlt (val x) (val y).
Definition Dle x y := Zle (val x) (val y).

Definition Dgt := transp Dlt.
Definition Dge := transp Dle.

Lemma well_founded_Dlt : well_founded Dlt.

Lemma WF_Dgt : WF Dgt.

Lemma power_Dlt_compat : forall x y n,
Dlt x y -> Dlt (inj (pos_power_val x (S n))) (inj (pos_power_val y (S n))).

Lemma trans_Dgt : transitive Dgt.

Lemma trans_Dge : transitive Dge.

Lemma refl_Dge : reflexive Dge.

max

Lemma Zmax_gub : forall m n k, m >= k -> n >= k -> Zmax m n >= k.

Lemma elim_Zmax_l : forall x y z, x <= y -> x <= Zmax y z.

Lemma elim_lt_Zmax_l : forall x y z, x < y -> x < Zmax y z.

Lemma elim_Zmax_r : forall x y z, x <= z -> x <= Zmax y z.

Lemma elim_lt_Zmax_r : forall x y z, x < z -> x < Zmax y z.

Lemma Zmax_l : forall x y, x >= y -> Zmax x y = x.

Lemma Zmax_r : forall x y, y >= x -> Zmax x y = y.

Lemma Zmax_ge_compat : forall x y x' y',
x >= x' -> y >= y' -> Zmax x y >= Zmax x' y'.

Lemma Zmax_gt_compat : forall x y x' y',
x > x' -> y > y' -> Zmax x y > Zmax x' y'.

orders

Lemma Zge_refl : forall k, k >= k.