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
  • Adam Koprowski, 2008-01-30
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.