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.
Automatically open scope positive_scope for the constructors of Z
Delimit Scope Z_scope with 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.
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.
Definition Zopp (x:Z) :=
match x with
| Z0 => Z0
| Zpos x => Zneg x
| Zneg x => Zpos x
end.
Notation "- x" := (Zopp x) : Z_scope.
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.
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) ].
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.
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.
opp is involutive
Injectivity of the opposite
Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n).
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.
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).
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.
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).
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.
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.
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.
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.
Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m.
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.
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).
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.
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).
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.
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.
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.
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.
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.
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.
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.