Library Coq.ZArith.BinInt



Binary Integers (Pierre Crégut, CNET, Lannion, France)

Require Export BinPos.
Require Export Pnat.
Require Import BinNat.
Require Import Plus.
Require Import Mult.


Binary integer numbers


Inductive Z : Set :=
  | Z0 : Z
  | Zpos : positive -> Z
  | Zneg : positive -> Z.

Automatically open scope positive_scope for the constructors of Z
Delimit Scope Z_scope with Z.

Subtraction of positive into Z


Definition Zdouble_plus_one (x:Z) :=
  match x with
    | Z0 => Zpos 1
    | Zpos p => Zpos p~1
    | Zneg p => Zneg (Pdouble_minus_one p)
  end.

Definition Zdouble_minus_one (x:Z) :=
  match x with
    | Z0 => Zneg 1
    | Zneg p => Zneg p~1
    | Zpos p => Zpos (Pdouble_minus_one p)
  end.

Definition Zdouble (x:Z) :=
  match x with
    | Z0 => Z0
    | Zpos p => Zpos p~0
    | Zneg p => Zneg p~0
  end.

Open Local Scope positive_scope.

Fixpoint ZPminus (x y:positive) {struct y} : Z :=
  match x, y with
    | p~1, q~1 => Zdouble (ZPminus p q)
    | p~1, q~0 => Zdouble_plus_one (ZPminus p q)
    | p~1, 1 => Zpos p~0
    | p~0, q~1 => Zdouble_minus_one (ZPminus p q)
    | p~0, q~0 => Zdouble (ZPminus p q)
    | p~0, 1 => Zpos (Pdouble_minus_one p)
    | 1, q~1 => Zneg q~0
    | 1, q~0 => Zneg (Pdouble_minus_one q)
    | 1, 1 => Z0
  end.

Close Local Scope positive_scope.

Addition on integers


Definition Zplus (x y:Z) :=
  match x, y with
    | Z0, y => y
    | Zpos x', Z0 => Zpos x'
    | Zneg x', Z0 => Zneg x'
    | Zpos x', Zpos y' => Zpos (x' + y')
    | Zpos x', Zneg y' =>
      match (x' ?= y')%positive Eq with
        | Eq => Z0
        | Lt => Zneg (y' - x')
        | Gt => Zpos (x' - y')
      end
    | Zneg x', Zpos y' =>
      match (x' ?= y')%positive Eq with
        | Eq => Z0
        | Lt => Zpos (y' - x')
        | Gt => Zneg (x' - y')
      end
    | Zneg x', Zneg y' => Zneg (x' + y')
  end.

Infix "+" := Zplus : Z_scope.

Opposite


Definition Zopp (x:Z) :=
  match x with
    | Z0 => Z0
    | Zpos x => Zneg x
    | Zneg x => Zpos x
  end.

Notation "- x" := (Zopp x) : Z_scope.

Successor on integers


Definition Zsucc (x:Z) := (x + Zpos 1)%Z.

Predecessor on integers


Definition Zpred (x:Z) := (x + Zneg 1)%Z.

Subtraction on integers


Definition Zminus (m n:Z) := (m + - n)%Z.

Infix "-" := Zminus : Z_scope.

Multiplication on integers


Definition Zmult (x y:Z) :=
  match x, y with
    | Z0, _ => Z0
    | _, Z0 => Z0
    | Zpos x', Zpos y' => Zpos (x' * y')
    | Zpos x', Zneg y' => Zneg (x' * y')
    | Zneg x', Zpos y' => Zneg (x' * y')
    | Zneg x', Zneg y' => Zpos (x' * y')
  end.

Infix "*" := Zmult : Z_scope.

Comparison of integers


Definition Zcompare (x y:Z) :=
  match x, y with
    | Z0, Z0 => Eq
    | Z0, Zpos y' => Lt
    | Z0, Zneg y' => Gt
    | Zpos x', Z0 => Gt
    | Zpos x', Zpos y' => (x' ?= y')%positive Eq
    | Zpos x', Zneg y' => Gt
    | Zneg x', Z0 => Lt
    | Zneg x', Zpos y' => Lt
    | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive Eq)
  end.

Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.

Ltac elim_compare com1 com2 :=
  case (Dcompare (com1 ?= com2)%Z);
    [ idtac | let x := fresh "H" in
      (intro x; case x; clear x) ].

Sign function


Definition Zsgn (z:Z) : Z :=
  match z with
    | Z0 => Z0
    | Zpos p => Zpos 1
    | Zneg p => Zneg 1
  end.

Direct, easier to handle variants of successor and addition


Definition Zsucc' (x:Z) :=
  match x with
    | Z0 => Zpos 1
    | Zpos x' => Zpos (Psucc x')
    | Zneg x' => ZPminus 1 x'
  end.

Definition Zpred' (x:Z) :=
  match x with
    | Z0 => Zneg 1
    | Zpos x' => ZPminus x' 1
    | Zneg x' => Zneg (Psucc x')
  end.

Definition Zplus' (x y:Z) :=
  match x, y with
    | Z0, y => y
    | x, Z0 => x
    | Zpos x', Zpos y' => Zpos (x' + y')
    | Zpos x', Zneg y' => ZPminus x' y'
    | Zneg x', Zpos y' => ZPminus y' x'
    | Zneg x', Zneg y' => Zneg (x' + y')
  end.

Open Local Scope Z_scope.

Inductive specification of Z


Theorem Zind :
  forall P:Z -> Prop,
    P Z0 ->
    (forall x:Z, P x -> P (Zsucc' x)) ->
    (forall x:Z, P x -> P (Zpred' x)) -> forall n:Z, P n.

Misc properties about binary integer operations


Properties of opposite on binary integer numbers


Theorem Zopp_0 : Zopp Z0 = Z0.

Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.

opp is involutive

Theorem Zopp_involutive : forall n:Z, - - n = n.

Injectivity of the opposite

Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m.

Other properties of binary integer numbers


Lemma ZL0 : 2%nat = (1 + 1)%nat.

Properties of the addition on integers


Zero is left neutral for addition


Theorem Zplus_0_l : forall n:Z, Z0 + n = n.

Zero is right neutral for addition


Theorem Zplus_0_r : forall n:Z, n + Z0 = n.

Addition is commutative


Theorem Zplus_comm : forall n m:Z, n + m = m + n.

Opposite distributes over addition


Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.

Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n).

Opposite is inverse for addition


Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.

Theorem Zplus_opp_l : forall n:Z, - n + n = Z0.

Hint Local Resolve Zplus_0_l Zplus_0_r.

Addition is associative


Lemma weak_assoc :
  forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.

Hint Local Resolve weak_assoc.

Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p.

Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p).

Associativity mixed with commutativity


Theorem Zplus_permute : forall n m p:Z, n + (m + p) = m + (n + p).

Addition simplifies


Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.

Addition and successor permutes


Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).

Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m.

Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).

Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.

Misc properties, usually redundant or non natural


Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0.

Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m.

Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m.

Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q.

Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m).

Properties of successor and predecessor on binary integer numbers


Theorem Zsucc_discr : forall n:Z, n <> Zsucc n.

Theorem Zpos_succ_morphism :
  forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p).

Successor and predecessor are inverse functions


Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).

Hint Immediate Zsucc_pred: zarith.

Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).

Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m.

Properties of the direct definition of successor and predecessor


Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.

Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n.

Theorem Zsucc'_inj : forall n m:Z, Zsucc' n = Zsucc' m -> n = m.

Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n.

Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.

Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m.

Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n.

Misc properties, usually redundant or non natural

Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m.

Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m.

Properties of subtraction on binary integer numbers


minus and Z0


Lemma Zminus_0_r : forall n:Z, n - Z0 = n.

Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0.

Lemma Zminus_diag : forall n:Z, n - n = Z0.

Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n.

Relating minus with plus and Zsucc


Lemma Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p.

Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.

Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m).

Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.

Lemma Zminus_plus : forall n m:Z, n + m - n = m.

Lemma Zplus_minus : forall n m:Z, n + (m - n) = m.

Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.

Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m).

Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m.

Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt ->
  Zpos (b-a) = Zpos b - Zpos a.

Misc redundant properties


Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.

Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m.

Properties of multiplication on binary integer numbers


Theorem Zpos_mult_morphism :
  forall p q:positive, Zpos (p*q) = Zpos p * Zpos q.

One is neutral for multiplication


Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n.

Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n.

Zero property of multiplication


Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0.

Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0.

Hint Local Resolve Zmult_0_l Zmult_0_r.

Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0.

Commutativity of multiplication


Theorem Zmult_comm : forall n m:Z, n * m = m * n.

Associativity of multiplication


Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p.

Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p).

Associativity mixed with commutativity


Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p).

Z is integral


Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0.

Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0.

Lemma Zmult_1_inversion_l :
  forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1.

Multiplication and Doubling


Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z.

Lemma Zdouble_plus_one_mult : forall z,
  Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1).

Multiplication and Opposite


Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m.

Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m.

Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m).

Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m.

Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m.

Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1.

Distributivity of multiplication over addition


Lemma weak_Zmult_plus_distr_r :
  forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m.

Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p.

Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p.

Distributivity of multiplication over subtraction


Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p.

Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m.

Simplification of multiplication for non-zero integers


Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m.

Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m.

Addition and multiplication by 2


Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2.

Multiplication and successor


Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n.

Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m.

Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m.

Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m.

Misc redundant properties


Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0.

Relating binary positive numbers and binary integers


Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q.

Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q.

Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q.

Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1.

Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p.

Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1.

Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p.

Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q.

Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q.

Order relations


Definition Zlt (x y:Z) := (x ?= y) = Lt.
Definition Zgt (x y:Z) := (x ?= y) = Gt.
Definition Zle (x y:Z) := (x ?= y) <> Gt.
Definition Zge (x y:Z) := (x ?= y) <> Lt.
Definition Zne (x y:Z) := x <> y.

Infix "<=" := Zle : Z_scope.
Infix "<" := Zlt : Z_scope.
Infix ">=" := Zge : Z_scope.
Infix ">" := Zgt : Z_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.

Absolute value on integers


Definition Zabs_nat (x:Z) : nat :=
  match x with
    | Z0 => 0%nat
    | Zpos p => nat_of_P p
    | Zneg p => nat_of_P p
  end.

Definition Zabs (z:Z) : Z :=
  match z with
    | Z0 => Z0
    | Zpos p => Zpos p
    | Zneg p => Zpos p
  end.

From nat to Z


Definition Z_of_nat (x:nat) :=
  match x with
    | O => Z0
    | S y => Zpos (P_of_succ_nat y)
  end.

Require Import BinNat.

Definition Zabs_N (z:Z) :=
  match z with
    | Z0 => 0%N
    | Zpos p => Npos p
    | Zneg p => Npos p
  end.

Definition Z_of_N (x:N) :=
  match x with
    | N0 => Z0
    | Npos p => Zpos p
  end.