Library Coq.ZArith.BinInt


Require Export BinNums BinPos Pnat.
Require Import BinNat Bool Plus Mult Equalities GenericMinMax
 OrdersFacts ZAxioms ZProperties.
Require BinIntDef.

Binary Integers

Initial author: Pierre Crégut, CNET, Lannion, France
The type Z and its constructors Z0 and Zpos and Zneg are now defined in BinNums.v

Local Open Scope Z_scope.

Every definitions and early properties about binary integers are placed in a module Z for qualification purpose.

Module Z
 <: ZAxiomsSig
 <: UsualOrderedTypeFull
 <: UsualDecidableTypeFull
 <: TotalOrder.

Definitions of operations, now in a separate file


Include BinIntDef.Z.

When including property functors, only inline t eq zero one two


Logic Predicates


Definition eq := @Logic.eq Z.
Definition eq_equiv := @eq_equivalence Z.

Definition lt x y := (x ?= y) = Lt.
Definition gt x y := (x ?= y) = Gt.
Definition le x y := (x ?= y) <> Gt.
Definition ge x y := (x ?= y) <> Lt.

Infix "<=" := le : Z_scope.
Infix "<" := lt : Z_scope.
Infix ">=" := ge : Z_scope.
Infix ">" := gt : 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.

Definition divide x y := exists z, y = z*x.
Notation "( x | y )" := (divide x y) (at level 0).

Definition Even a := exists b, a = 2*b.
Definition Odd a := exists b, a = 2*b+1.

Decidability of equality.


Definition eq_dec (x y : Z) : {x = y} + {x <> y}.

Properties of pos_sub

pos_sub can be written in term of positive comparison and subtraction (cf. earlier definition of addition of Z)

Lemma pos_sub_spec p q :
 pos_sub p q =
 match (p ?= q)%positive with
   | Eq => 0
   | Lt => neg (q - p)
   | Gt => pos (p - q)
 end.

Lemma pos_sub_discr p q :
  match pos_sub p q with
  | Z0 => p = q
  | pos k => p = q + k
  | neg k => q = p + k
  end%positive.

Particular cases of the previous result

Lemma pos_sub_diag p : pos_sub p p = 0.

Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = neg (q - p).

Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = pos (p - q).

The opposite of pos_sub is pos_sub with reversed arguments

Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p.

In the following module, we group results that are needed now to prove specifications of operations, but will also be provided later by the generic functor of properties.

Module Import Private_BootStrap.

Properties of addition

Zero is neutral for addition


Lemma add_0_r n : n + 0 = n.

Addition is commutative


Lemma add_comm n m : n + m = m + n.

Opposite distributes over addition


Lemma opp_add_distr n m : - (n + m) = - n + - m.

Opposite is injective


Lemma opp_inj n m : -n = -m -> n = m.

Addition is associative


Lemma pos_sub_add p q r :
  pos_sub (p + q) r = pos p + pos_sub q r.

Lemma add_assoc n m p : n + (m + p) = n + m + p.

Subtraction and successor


Lemma sub_succ_l n m : succ n - m = succ (n - m).

Opposite is inverse for addition


Lemma add_opp_diag_r n : n + - n = 0.

Lemma add_opp_diag_l n : - n + n = 0.

Commutativity of multiplication


Lemma mul_comm n m : n * m = m * n.

Associativity of multiplication


Lemma mul_assoc n m p : n * (m * p) = n * m * p.

Multiplication and constants

Lemma mul_1_l n : 1 * n = n.

Lemma mul_1_r n : n * 1 = n.

Multiplication and Opposite


Lemma mul_opp_l n m : - n * m = - (n * m).

Lemma mul_opp_r n m : n * - m = - (n * m).

Lemma mul_opp_opp n m : - n * - m = n * m.

Lemma mul_opp_comm n m : - n * m = n * - m.

Distributivity of multiplication over addition


Lemma mul_add_distr_pos (p:positive) n m :
 pos p * (n + m) = pos p * n + pos p * m.

Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p.

Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p.

Basic properties of divisibility


Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive.

Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p).

Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n).

Conversions between Z.testbit and N.testbit


Lemma testbit_of_N a n :
 testbit (of_N a) (of_N n) = N.testbit a n.

Lemma testbit_of_N´ a n : 0<=n ->
 testbit (of_N a) n = N.testbit a (to_N n).

Lemma testbit_Zpos a n : 0<=n ->
 testbit (pos a) n = N.testbit (N.pos a) (to_N n).

Lemma testbit_Zneg a n : 0<=n ->
 testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)).

End Private_BootStrap.

Proofs of specifications

Specification of constants


Lemma one_succ : 1 = succ 0.

Lemma two_succ : 2 = succ 1.

Specification of addition


Lemma add_0_l n : 0 + n = n.

Lemma add_succ_l n m : succ n + m = succ (n + m).

Specification of opposite


Lemma opp_0 : -0 = 0.

Lemma opp_succ n : -(succ n) = pred (-n).

Specification of successor and predecessor


Lemma succ_pred n : succ (pred n) = n.

Lemma pred_succ n : pred (succ n) = n.

Specification of subtraction


Lemma sub_0_r n : n - 0 = n.

Lemma sub_succ_r n m : n - succ m = pred (n - m).

Specification of multiplication


Lemma mul_0_l n : 0 * n = 0.

Lemma mul_succ_l n m : succ n * m = n * m + m.

Specification of comparisons and order


Lemma eqb_eq n m : (n =? m) = true <-> n = m.

Lemma ltb_lt n m : (n <? m) = true <-> n < m.

Lemma leb_le n m : (n <=? m) = true <-> n <= m.

Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.

Lemma compare_sub n m : (n ?= m) = (n - m ?= 0).

Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).

Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.

Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.

Some more advanced properties of comparison and orders, including compare_spec and lt_irrefl and lt_eq_cases.

Include BoolOrderFacts.

Remaining specification of lt and le

Lemma lt_succ_r n m : n < succ m <-> n<=m.

Specification of minimum and maximum


Lemma max_l n m : m<=n -> max n m = n.

Lemma max_r n m : n<=m -> max n m = m.

Lemma min_l n m : n<=m -> min n m = n.

Lemma min_r n m : m<=n -> min n m = m.

Specification of absolute value


Lemma abs_eq n : 0 <= n -> abs n = n.

Lemma abs_neq n : n <= 0 -> abs n = - n.

Specification of sign


Lemma sgn_null n : n = 0 -> sgn n = 0.

Lemma sgn_pos n : 0 < n -> sgn n = 1.

Lemma sgn_neg n : n < 0 -> sgn n = -1.

Specification of power


Lemma pow_0_r n : n^0 = 1.

Lemma pow_succ_r n m : 0<=m -> n^(succ m) = n * n^m.

Lemma pow_neg_r n m : m<0 -> n^m = 0.

For folding back a pow_pos into a pow

Lemma pow_pos_fold n p : pow_pos n p = n ^ (pos p).

Specification of square


Lemma square_spec n : square n = n * n.

Specification of square root


Lemma sqrtrem_spec n : 0<=n ->
 let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.

Lemma sqrt_spec n : 0<=n ->
 let s := sqrt n in s*s <= n < (succ s)*(succ s).

Lemma sqrt_neg n : n<0 -> sqrt n = 0.

Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.

Specification of logarithm


Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)).

Lemma log2_nonpos n : n<=0 -> log2 n = 0.

Specification of parity functions

Lemma even_spec n : even n = true <-> Even n.

Lemma odd_spec n : odd n = true <-> Odd n.

Multiplication and Doubling


Lemma double_spec n : double n = 2*n.

Lemma succ_double_spec n : succ_double n = 2*n + 1.

Lemma pred_double_spec n : pred_double n = 2*n - 1.

Correctness proofs for Trunc division


Lemma pos_div_eucl_eq a b : 0 < b ->
  let (q, r) := pos_div_eucl a b in pos a = q * b + r.

Lemma div_eucl_eq a b : b<>0 ->
 let (q, r) := div_eucl a b in a = b * q + r.

Lemma div_mod a b : b<>0 -> a = b*(a/b) + (a mod b).

Lemma pos_div_eucl_bound a b : 0<b -> 0 <= snd (pos_div_eucl a b) < b.

Lemma mod_pos_bound a b : 0 < b -> 0 <= a mod b < b.

Definition mod_bound_pos a b (_:0<=a) := mod_pos_bound a b.

Lemma mod_neg_bound a b : b < 0 -> b < a mod b <= 0.

Correctness proofs for Floor division


Theorem quotrem_eq a b : let (q,r) := quotrem a b in a = q * b + r.

Lemma quot_rem´ a b : a = b*(a÷b) + rem a b.

Lemma quot_rem a b : b<>0 -> a = b*(a÷b) + rem a b.

Lemma rem_bound_pos a b : 0<=a -> 0<b -> 0 <= rem a b < b.

Lemma rem_opp_l´ a b : rem (-a) b = - (rem a b).

Lemma rem_opp_r´ a b : rem a (-b) = rem a b.

Lemma rem_opp_l a b : b<>0 -> rem (-a) b = - (rem a b).

Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b.

Correctness proofs for gcd


Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.

Lemma ggcd_correct_divisors a b :
  let ´(g,(aa,bb)) := ggcd a b in
  a = g*aa /\ b = g*bb.

Lemma gcd_divide_l a b : (gcd a b | a).

Lemma gcd_divide_r a b : (gcd a b | b).

Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b).

Lemma gcd_nonneg a b : 0 <= gcd a b.

ggcd and opp : an auxiliary result used in QArith

Theorem ggcd_opp a b :
  ggcd (-a) b = (let ´(g,(aa,bb)) := ggcd a b in (g,(-aa,bb))).

Proofs of specifications for bitwise operations


Lemma div2_spec a : div2 a = shiftr a 1.

Lemma testbit_0_l n : testbit 0 n = false.

Lemma testbit_neg_r a n : n<0 -> testbit a n = false.

Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.

Lemma testbit_odd_succ a n : 0<=n ->
 testbit (2*a+1) (succ n) = testbit a n.

Lemma testbit_even_succ a n : 0<=n ->
 testbit (2*a) (succ n) = testbit a n.

Correctness proofs about Z.shiftr and Z.shiftl

Lemma shiftr_spec_aux a n m : 0<=n -> 0<=m ->
 testbit (shiftr a n) m = testbit a (m+n).

Lemma shiftl_spec_low a n m : m<n ->
 testbit (shiftl a n) m = false.

Lemma shiftl_spec_high a n m : 0<=m -> n<=m ->
 testbit (shiftl a n) m = testbit a (m-n).

Lemma shiftr_spec a n m : 0<=m ->
 testbit (shiftr a n) m = testbit a (m+n).

Correctness proofs for bitwise operations

Lemma lor_spec a b n :
 testbit (lor a b) n = testbit a n || testbit b n.

Lemma land_spec a b n :
 testbit (land a b) n = testbit a n && testbit b n.

Lemma ldiff_spec a b n :
 testbit (ldiff a b) n = testbit a n && negb (testbit b n).

Lemma lxor_spec a b n :
 testbit (lxor a b) n = xorb (testbit a n) (testbit b n).

Induction principles based on successor / predecessor


Lemma peano_ind (P : Z -> Prop) :
  P 0 ->
  (forall x, P x -> P (succ x)) ->
  (forall x, P x -> P (pred x)) ->
  forall z, P z.

Lemma bi_induction (P : Z -> Prop) :
  Proper (eq ==> iff) P ->
  P 0 ->
  (forall x, P x <-> P (succ x)) ->
  forall z, P z.

Proofs of morphisms, obvious since eq is Leibniz


Local Obligation Tactic := simpl_relation.
Program Definition succ_wd : Proper (eq==>eq) succ := _.
Program Definition pred_wd : Proper (eq==>eq) pred := _.
Program Definition opp_wd : Proper (eq==>eq) opp := _.
Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.

The Bind Scope prevents Z to stay associated with abstract_scope. (TODO FIX)

Include ZProp. Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

In generic statements, the predicates lt and le have been favored, whereas gt and ge don't even exist in the abstract layers. The use of gt and ge is hence not recommended. We provide here the bare minimal results to related them with lt and le.

Lemma gt_lt_iff n m : n > m <-> m < n.

Lemma gt_lt n m : n > m -> m < n.

Lemma lt_gt n m : n < m -> m > n.

Lemma ge_le_iff n m : n >= m <-> m <= n.

Lemma ge_le n m : n >= m -> m <= n.

Lemma le_ge n m : n <= m -> m >= n.

We provide a tactic converting from one style to the other.

Ltac swap_greater := rewrite ?gt_lt_iff in *; rewrite ?ge_le_iff in *.

Similarly, the boolean comparisons ltb and leb are favored over their dual gtb and geb. We prove here the equivalence and a few minimal results.

Lemma gtb_ltb n m : (n >? m) = (m <? n).

Lemma geb_leb n m : (n >=? m) = (m <=? n).

Lemma gtb_lt n m : (n >? m) = true <-> m < n.

Lemma geb_le n m : (n >=? m) = true <-> m <= n.

Lemma gtb_spec n m : BoolSpec (m<n) (n<=m) (n >? m).

Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m).

TODO : to add in Numbers ?

Lemma add_reg_l n m p : n + m = n + p -> m = p.

Lemma mul_reg_l n m p : p <> 0 -> p * n = p * m -> n = m.

Lemma mul_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.

Lemma opp_eq_mul_m1 n : - n = n * -1.

Lemma add_diag n : n + n = 2 * n.

Comparison and opposite


Lemma compare_opp n m : (- n ?= - m) = (m ?= n).

Comparison and addition


Lemma add_compare_mono_l n m p : (n + m ?= n + p) = (m ?= p).

End Z.

Re-export Notations

Infix "+" := Z.add : Z_scope.
Notation "- x" := (Z.opp x) : Z_scope.
Infix "-" := Z.sub : Z_scope.
Infix "*" := Z.mul : Z_scope.
Infix "^" := Z.pow : Z_scope.
Infix "/" := Z.div : Z_scope.
Infix "mod" := Z.modulo (at level 40, no associativity) : Z_scope.
Infix "÷" := Z.quot (at level 40, left associativity) : Z_scope.
Infix "?=" := Z.compare (at level 70, no associativity) : Z_scope.
Infix "=?" := Z.eqb (at level 70, no associativity) : Z_scope.
Infix "<=?" := Z.leb (at level 70, no associativity) : Z_scope.
Infix "<?" := Z.ltb (at level 70, no associativity) : Z_scope.
Infix ">=?" := Z.geb (at level 70, no associativity) : Z_scope.
Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope.
Notation "( x | y )" := (Z.divide x y) (at level 0) : Z_scope.
Infix "<=" := Z.le : Z_scope.
Infix "<" := Z.lt : Z_scope.
Infix ">=" := Z.ge : Z_scope.
Infix ">" := Z.gt : 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.

Conversions from / to positive numbers

Module Pos2Z.

Lemma id p : Z.to_pos (Z.pos p) = p.

Lemma inj p q : Z.pos p = Z.pos q -> p = q.

Lemma inj_iff p q : Z.pos p = Z.pos q <-> p = q.

Lemma is_pos p : 0 < Z.pos p.

Lemma is_nonneg p : 0 <= Z.pos p.

Lemma inj_1 : Z.pos 1 = 1.

Lemma inj_xO p : Z.pos p~0 = 2 * Z.pos p.

Lemma inj_xI p : Z.pos p~1 = 2 * Z.pos p + 1.

Lemma inj_succ p : Z.pos (Pos.succ p) = Z.succ (Z.pos p).

Lemma inj_add p q : Z.pos (p+q) = Z.pos p + Z.pos q.

Lemma inj_sub p q : (p < q)%positive ->
 Z.pos (q-p) = Z.pos q - Z.pos p.

Lemma inj_sub_max p q : Z.pos (p - q) = Z.max 1 (Z.pos p - Z.pos q).

Lemma inj_pred p : p <> 1%positive ->
 Z.pos (Pos.pred p) = Z.pred (Z.pos p).

Lemma inj_mul p q : Z.pos (p*q) = Z.pos p * Z.pos q.

Lemma inj_pow_pos p q : Z.pos (p^q) = Z.pow_pos (Z.pos p) q.

Lemma inj_pow p q : Z.pos (p^q) = (Z.pos p)^(Z.pos q).

Lemma inj_square p : Z.pos (Pos.square p) = Z.square (Z.pos p).

Lemma inj_compare p q : (p ?= q)%positive = (Z.pos p ?= Z.pos q).

Lemma inj_leb p q : (p <=? q)%positive = (Z.pos p <=? Z.pos q).

Lemma inj_ltb p q : (p <? q)%positive = (Z.pos p <? Z.pos q).

Lemma inj_eqb p q : (p =? q)%positive = (Z.pos p =? Z.pos q).

Lemma inj_max p q : Z.pos (Pos.max p q) = Z.max (Z.pos p) (Z.pos q).

Lemma inj_min p q : Z.pos (Pos.min p q) = Z.min (Z.pos p) (Z.pos q).

Lemma inj_sqrt p : Z.pos (Pos.sqrt p) = Z.sqrt (Z.pos p).

Lemma inj_gcd p q : Z.pos (Pos.gcd p q) = Z.gcd (Z.pos p) (Z.pos q).

Definition inj_divide p q : (Z.pos p|Z.pos q) <-> (p|q)%positive.

Lemma inj_testbit a n : 0<=n ->
 Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).

Some results concerning Z.neg

Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q.

Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q.

Lemma neg_is_neg p : Z.neg p < 0.

Lemma neg_is_nonpos p : Z.neg p <= 0.

Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p.

Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1.

Lemma opp_neg p : - Z.neg p = Z.pos p.

Lemma opp_pos p : - Z.pos p = Z.neg p.

Lemma add_neg_neg p q : Z.neg p + Z.neg q = Z.neg (p+q).

Lemma add_pos_neg p q : Z.pos p + Z.neg q = Z.pos_sub p q.

Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p.

Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p).

Lemma divide_pos_neg_l n p : (Z.pos p|n) <-> (Z.neg p|n).

Lemma testbit_neg a n : 0<=n ->
 Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)).

End Pos2Z.

Module Z2Pos.

Lemma id x : 0 < x -> Z.pos (Z.to_pos x) = x.

Lemma inj x y : 0 < x -> 0 < y -> Z.to_pos x = Z.to_pos y -> x = y.

Lemma inj_iff x y : 0 < x -> 0 < y -> (Z.to_pos x = Z.to_pos y <-> x = y).

Lemma to_pos_nonpos x : x <= 0 -> Z.to_pos x = 1%positive.

Lemma inj_1 : Z.to_pos 1 = 1%positive.

Lemma inj_double x : 0 < x ->
 Z.to_pos (Z.double x) = (Z.to_pos x)~0%positive.

Lemma inj_succ_double x : 0 < x ->
 Z.to_pos (Z.succ_double x) = (Z.to_pos x)~1%positive.

Lemma inj_succ x : 0 < x -> Z.to_pos (Z.succ x) = Pos.succ (Z.to_pos x).

Lemma inj_add x y : 0 < x -> 0 < y ->
 Z.to_pos (x+y) = (Z.to_pos x + Z.to_pos y)%positive.

Lemma inj_sub x y : 0 < x < y ->
 Z.to_pos (y-x) = (Z.to_pos y - Z.to_pos x)%positive.

Lemma inj_pred x : 1 < x -> Z.to_pos (Z.pred x) = Pos.pred (Z.to_pos x).

Lemma inj_mul x y : 0 < x -> 0 < y ->
 Z.to_pos (x*y) = (Z.to_pos x * Z.to_pos y)%positive.

Lemma inj_pow x y : 0 < x -> 0 < y ->
 Z.to_pos (x^y) = (Z.to_pos x ^ Z.to_pos y)%positive.

Lemma inj_pow_pos x p : 0 < x ->
 Z.to_pos (Z.pow_pos x p) = ((Z.to_pos x)^p)%positive.

Lemma inj_compare x y : 0 < x -> 0 < y ->
 (x ?= y) = (Z.to_pos x ?= Z.to_pos y)%positive.

Lemma inj_leb x y : 0 < x -> 0 < y ->
 (x <=? y) = (Z.to_pos x <=? Z.to_pos y)%positive.

Lemma inj_ltb x y : 0 < x -> 0 < y ->
 (x <? y) = (Z.to_pos x <? Z.to_pos y)%positive.

Lemma inj_eqb x y : 0 < x -> 0 < y ->
 (x =? y) = (Z.to_pos x =? Z.to_pos y)%positive.

Lemma inj_max x y :
 Z.to_pos (Z.max x y) = Pos.max (Z.to_pos x) (Z.to_pos y).

Lemma inj_min x y :
 Z.to_pos (Z.min x y) = Pos.min (Z.to_pos x) (Z.to_pos y).

Lemma inj_sqrt x : Z.to_pos (Z.sqrt x) = Pos.sqrt (Z.to_pos x).

Lemma inj_gcd x y : 0 < x -> 0 < y ->
 Z.to_pos (Z.gcd x y) = Pos.gcd (Z.to_pos x) (Z.to_pos y).

End Z2Pos.

Compatibility Notations

Notation Zdouble_plus_one := Z.succ_double (compat "8.3").
Notation Zdouble_minus_one := Z.pred_double (compat "8.3").
Notation Zdouble := Z.double (compat "8.3").
Notation ZPminus := Z.pos_sub (compat "8.3").
Notation Zsucc´ := Z.succ (compat "8.3").
Notation Zpred´ := Z.pred (compat "8.3").
Notation Zplus´ := Z.add (compat "8.3").
Notation Zplus := Z.add (compat "8.3"). Notation Zopp := Z.opp (compat "8.3").
Notation Zsucc := Z.succ (compat "8.3").
Notation Zpred := Z.pred (compat "8.3").
Notation Zminus := Z.sub (compat "8.3").
Notation Zmult := Z.mul (compat "8.3").
Notation Zcompare := Z.compare (compat "8.3").
Notation Zsgn := Z.sgn (compat "8.3").
Notation Zle := Z.le (compat "8.3").
Notation Zge := Z.ge (compat "8.3").
Notation Zlt := Z.lt (compat "8.3").
Notation Zgt := Z.gt (compat "8.3").
Notation Zmax := Z.max (compat "8.3").
Notation Zmin := Z.min (compat "8.3").
Notation Zabs := Z.abs (compat "8.3").
Notation Zabs_nat := Z.abs_nat (compat "8.3").
Notation Zabs_N := Z.abs_N (compat "8.3").
Notation Z_of_nat := Z.of_nat (compat "8.3").
Notation Z_of_N := Z.of_N (compat "8.3").

Notation Zind := Z.peano_ind (compat "8.3").
Notation Zopp_0 := Z.opp_0 (compat "8.3").
Notation Zopp_involutive := Z.opp_involutive (compat "8.3").
Notation Zopp_inj := Z.opp_inj (compat "8.3").
Notation Zplus_0_l := Z.add_0_l (compat "8.3").
Notation Zplus_0_r := Z.add_0_r (compat "8.3").
Notation Zplus_comm := Z.add_comm (compat "8.3").
Notation Zopp_plus_distr := Z.opp_add_distr (compat "8.3").
Notation Zopp_succ := Z.opp_succ (compat "8.3").
Notation Zplus_opp_r := Z.add_opp_diag_r (compat "8.3").
Notation Zplus_opp_l := Z.add_opp_diag_l (compat "8.3").
Notation Zplus_assoc := Z.add_assoc (compat "8.3").
Notation Zplus_permute := Z.add_shuffle3 (compat "8.3").
Notation Zplus_reg_l := Z.add_reg_l (compat "8.3").
Notation Zplus_succ_l := Z.add_succ_l (compat "8.3").
Notation Zplus_succ_comm := Z.add_succ_comm (compat "8.3").
Notation Zsucc_discr := Z.neq_succ_diag_r (compat "8.3").
Notation Zsucc_inj := Z.succ_inj (compat "8.3").
Notation Zsucc´_inj := Z.succ_inj (compat "8.3").
Notation Zsucc´_pred´ := Z.succ_pred (compat "8.3").
Notation Zpred´_succ´ := Z.pred_succ (compat "8.3").
Notation Zpred´_inj := Z.pred_inj (compat "8.3").
Notation Zsucc´_discr := Z.neq_succ_diag_r (compat "8.3").
Notation Zminus_0_r := Z.sub_0_r (compat "8.3").
Notation Zminus_diag := Z.sub_diag (compat "8.3").
Notation Zminus_plus_distr := Z.sub_add_distr (compat "8.3").
Notation Zminus_succ_r := Z.sub_succ_r (compat "8.3").
Notation Zminus_plus := Z.add_simpl_l (compat "8.3").
Notation Zmult_0_l := Z.mul_0_l (compat "8.3").
Notation Zmult_0_r := Z.mul_0_r (compat "8.3").
Notation Zmult_1_l := Z.mul_1_l (compat "8.3").
Notation Zmult_1_r := Z.mul_1_r (compat "8.3").
Notation Zmult_comm := Z.mul_comm (compat "8.3").
Notation Zmult_assoc := Z.mul_assoc (compat "8.3").
Notation Zmult_permute := Z.mul_shuffle3 (compat "8.3").
Notation Zmult_1_inversion_l := Z.mul_eq_1 (compat "8.3").
Notation Zdouble_mult := Z.double_spec (compat "8.3").
Notation Zdouble_plus_one_mult := Z.succ_double_spec (compat "8.3").
Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (compat "8.3").
Notation Zmult_opp_opp := Z.mul_opp_opp (compat "8.3").
Notation Zmult_opp_comm := Z.mul_opp_comm (compat "8.3").
Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (compat "8.3").
Notation Zmult_plus_distr_r := Z.mul_add_distr_l (compat "8.3").
Notation Zmult_plus_distr_l := Z.mul_add_distr_r (compat "8.3").
Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (compat "8.3").
Notation Zmult_reg_l := Z.mul_reg_l (compat "8.3").
Notation Zmult_reg_r := Z.mul_reg_r (compat "8.3").
Notation Zmult_succ_l := Z.mul_succ_l (compat "8.3").
Notation Zmult_succ_r := Z.mul_succ_r (compat "8.3").

Notation Zpos_xI := Pos2Z.inj_xI (compat "8.3").
Notation Zpos_xO := Pos2Z.inj_xO (compat "8.3").
Notation Zneg_xI := Pos2Z.neg_xI (compat "8.3").
Notation Zneg_xO := Pos2Z.neg_xO (compat "8.3").
Notation Zopp_neg := Pos2Z.opp_neg (compat "8.3").
Notation Zpos_succ_morphism := Pos2Z.inj_succ (compat "8.3").
Notation Zpos_mult_morphism := Pos2Z.inj_mul (compat "8.3").
Notation Zpos_minus_morphism := Pos2Z.inj_sub (compat "8.3").
Notation Zpos_eq_rev := Pos2Z.inj (compat "8.3").
Notation Zpos_plus_distr := Pos2Z.inj_add (compat "8.3").
Notation Zneg_plus_distr := Pos2Z.add_neg_neg (compat "8.3").

Notation Z := Z (only parsing).
Notation Z_rect := Z_rect (only parsing).
Notation Z_rec := Z_rec (only parsing).
Notation Z_ind := Z_ind (only parsing).
Notation Z0 := Z0 (only parsing).
Notation Zpos := Zpos (only parsing).
Notation Zneg := Zneg (only parsing).

Compatibility lemmas. These could be notations, but scope information would be lost.

Notation SYM1 lem := (fun n => eq_sym (lem n)).
Notation SYM2 lem := (fun n m => eq_sym (lem n m)).
Notation SYM3 lem := (fun n m p => eq_sym (lem n m p)).

Lemma Zplus_assoc_reverse : forall n m p, n+m+p = n+(m+p).
Lemma Zplus_succ_r_reverse : forall n m, Z.succ (n+m) = n+Z.succ m.
Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing).
Lemma Zplus_0_r_reverse : forall n, n = n + 0.
Lemma Zplus_eq_compat : forall n m p q, n=m -> p=q -> n+p=m+q.
Lemma Zsucc_pred : forall n, n = Z.succ (Z.pred n).
Lemma Zpred_succ : forall n, n = Z.pred (Z.succ n).
Lemma Zsucc_eq_compat : forall n m, n = m -> Z.succ n = Z.succ m.
Lemma Zminus_0_l_reverse : forall n, n = n - 0.
Lemma Zminus_diag_reverse : forall n, 0 = n-n.
Lemma Zminus_succ_l : forall n m, Z.succ (n - m) = Z.succ n - m.
Lemma Zplus_minus_eq : forall n m p, n = m + p -> p = n - m.
Lemma Zplus_minus : forall n m, n + (m - n) = m.
Lemma Zminus_plus_simpl_l : forall n m p, p + n - (p + m) = n - m.
Lemma Zminus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
Lemma Zminus_plus_simpl_r : forall n m p, n + p - (m + p) = n - m.
Lemma Zeq_minus : forall n m, n = m -> n - m = 0.
Lemma Zminus_eq : forall n m, n - m = 0 -> n = m.
Lemma Zmult_0_r_reverse : forall n, 0 = n * 0.
Lemma Zmult_assoc_reverse : forall n m p, n * m * p = n * (m * p).
Lemma Zmult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
Lemma Zmult_integral_l : forall n m, n <> 0 -> m * n = 0 -> m = 0.
Lemma Zopp_mult_distr_l : forall n m, - (n * m) = - n * m.
Lemma Zopp_mult_distr_r : forall n m, - (n * m) = n * - m.
Lemma Zmult_minus_distr_l : forall n m p, p * (n - m) = p * n - p * m.
Lemma Zmult_succ_r_reverse : forall n m, n * m + n = n * Z.succ m.
Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Z.succ n * m.
Lemma Zpos_eq : forall p q, p = q -> Z.pos p = Z.pos q.
Lemma Zpos_eq_iff : forall p q, p = q <-> Z.pos p = Z.pos q.

Hint Immediate Zsucc_pred: zarith.



Obsolete stuff

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

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

Lemma Zplus_diag_eq_mult_2 n : n + n = n * 2.

Lemma Z_eq_mult n m : m = 0 -> m * n = 0.