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