# 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.

Require Import LogicUtil.
Require Export ZArith.

Open Local Scope Z_scope.

simplification

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

Proof.
intro. destruct x; refl.
Qed.

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

Proof.
intro. destruct x; refl.
Qed.

inequalities

Lemma pos_lt : x y : Z, 0 y-x-1 → x < y.

Proof.
intros. omega.
Qed.

Lemma pos_le : x y : Z, 0 y-xx y.

Proof.
intros. omega.
Qed.

power

Fixpoint power (x : Z) (n : nat) {struct n} : Z :=
match n with
| O ⇒ 1
| S n'x × power x n'
end.

Infix "^" := power.

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

Proof.
induction n1; intros; simpl. apply zeqr. rewrite IHn1. ring.
Qed.

Lemma power_one : n, power 1 n = 1.

Proof.
induction n; simpl. refl. rewrite IHn. refl.
Qed.

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

Proof.
refl.
Qed.

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

Proof.
induction n1; induction n2; intros. refl. rewrite power_one. refl.
rewrite mult_0_r. refl. rewrite power_succ. rewrite <- IHn2.
rewrite <- mult_n_Sm. simpl. repeat rewrite power_plus. simpl. ring.
Qed.

Lemma pos_power : x n, 0 x → 0 power x n.

Proof.
induction n; intros; simpl. omega. apply Zmult_le_0_compat. assumption.
apply IHn. assumption.
Qed.

Lemma spos_power : x n, 0 < x → 0 < power x n.

Proof.
induction n; intros; simpl. omega. apply Zmult_lt_O_compat. assumption.
apply IHn. assumption.
Qed.

Lemma power_le_compat : x y n, 0xxypower x n power y n.

Proof.
induction n; intros; simpl. omega. apply Zmult_le_compat. assumption.
apply IHn; assumption. assumption. apply pos_power. assumption.
Qed.

positive integers

Definition is_pos z :=
match z with
| Zpos _true
| _false
end.

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.

Proof.
simpl. omega.
Qed.

Notation D0 := (inj Zero_in_D).

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

Proof.
intros. destruct x. apply pos_power. assumption.
Qed.

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

Require Import RelUtil.

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

Require Import Zwf.
Require Import Wellfounded.

Lemma Dlt_well_founded : well_founded Dlt.

Proof.
unfold Dlt. apply wf_incl with (R2 := (fun x y : DZwf 0 (val x) (val y))).
unfold inclusion, Zwf. intros (x,Hx) (y,Hy). simpl. intuition omega.
apply (wf_inverse_image D Z (Zwf 0) val). apply Zwf_well_founded.
Qed.

Require Import SN.

Lemma WF_Dgt : WF Dgt.

Proof.
apply wf_transp_WF. apply Dlt_well_founded.
Qed.

Lemma power_Dlt_compat : x y n,
Dlt x yDlt (inj (pos_power_val x (S n))) (inj (pos_power_val y (S n))).

Proof.
intros x y. destruct x. destruct y. unfold Dlt. simpl.
induction n; simpl; intros. omega. ded (IHn H).
apply Zle_lt_trans with (m := x × (x0 × power x0 n)). apply Zmult_le_compat_l.
omega. assumption. apply Zmult_gt_0_lt_compat_r. apply Zlt_gt.
apply Zmult_lt_O_compat. omega. apply spos_power. omega. assumption.
Qed.

max

Lemma Zmax_gub : m n k, m kn kZmax m n k.

Proof.
intros. apply Zmax_case; assumption.
Qed.

Lemma elim_Zmax_l : x y z, x yx Zmax y z.

Proof.
intros. eapply Zle_trans. apply H. apply Zle_max_l.
Qed.

Lemma elim_lt_Zmax_l : x y z, x < yx < Zmax y z.

Proof.
intros. eapply Zlt_le_trans. eexact H. apply Zle_max_l.
Qed.

Lemma elim_Zmax_r : x y z, x zx Zmax y z.

Proof.
intros. eapply Zle_trans. apply H. apply Zle_max_r.
Qed.

Lemma elim_lt_Zmax_r : x y z, x < zx < Zmax y z.

Proof.
intros. rewrite Zmax_comm. apply elim_lt_Zmax_l. assumption.
Qed.

Lemma Zmax_l : x y, x yZmax x y = x.

Proof.
intros. unfold Zmax.
destruct (Dcompare_inf (x ?= y)) as [[xy | xy] | xy]; rewrite xy; try refl.
assert (x < y). assumption. omega.
Qed.

Lemma Zmax_r : x y, y xZmax x y = y.

Proof.
intros. rewrite Zmax_comm. apply Zmax_l. assumption.
Qed.

Lemma Zmax_ge_compat : x y x' y',
x x'y y'Zmax x y Zmax x' y'.

Proof.
intros. destruct (Zmax_irreducible_inf x' y') as [H1|H1] ; rewrite H1; unfold ge.
rewrite Zmax_comm. apply Zle_ge. apply elim_Zmax_r. omega.
apply Zle_ge. apply elim_Zmax_r. omega.
Qed.

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

Proof.
intros. destruct (Z_ge_dec x y); destruct (Z_ge_dec x' y');
do 2 first
[ rewrite Zmax_r; [idtac | omega]
| rewrite Zmax_l; [idtac | omega]
| idtac
];
omega.
Qed.

orders

Lemma Zge_refl : k, k k.

Proof.
intros. omega.
Qed.