Library Coq.ZArith.BinInt

Require Export BinNums BinPos Pnat.
Require Import BinNat Bool 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 }.

Proofs of morphisms, obvious since eq is Leibniz

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 := _.

Properties of pos_sub

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

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.

Operations and constants

Lemma add_0_r n : n + 0 = n.

Lemma mul_0_r n : n * 0 = 0.

Lemma mul_1_l n : 1 * n = 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_pos p n m : pos p + (n + m ) = pos p + n + m.

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

Opposite is inverse for addition

Lemma add_opp_diag_r n : n + - n = 0.

Multiplication and Opposite

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

Distributivity of multiplication over addition

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

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

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.

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.

We can now derive all properties of basic functions and orders, and use these properties for proving the specs of more advanced functions.

Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

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.

Extra properties about divide

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

Extra properties about 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)).

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

Generic properties of advanced functions.

Include ZExtraProp.

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 and Z.pos

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 inj_pos p q : Z.pos p = Z.pos q -> p = q.

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

Lemma neg_is_neg p : Z.neg p < 0.

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

Lemma pos_is_pos p : 0 < Z.pos p.

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

Lemma neg_le_pos p q : Zneg p <= Zpos q.

Lemma neg_lt_pos p q : Zneg p < Zpos q.

Lemma neg_le_neg p q : (q <= p)%positive -> Zneg p <= Zneg q.

Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q.

Lemma pos_le_pos p q : (p <= q)%positive -> Zpos p <= Zpos q.

Lemma pos_lt_pos p q : (p < q)%positive -> Zpos p < Zpos q.

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 pos_xO p : Z.pos p ~0 = 2 * Z.pos p.

Lemma pos_xI p : Z.pos p ~1 = 2 * Z.pos 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 add_pos_pos p q : Z.pos p + Z.pos q = Z.pos (p +q).

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

Lemma testbit_pos a n : 0<=n ->
Z.testbit (Z.pos a) n = N.testbit (N.pos 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 (only parsing).
Notation Zdouble_minus_one := Z.pred_double (only parsing).
Notation Zdouble := Z.double (compat "8.7").
Notation ZPminus := Z.pos_sub (only parsing).
Notation Zsucc' := Z.succ (compat "8.7").
Notation Zpred' := Z.pred (compat "8.7").
Notation Zplus' := Z.add (compat "8.7").
Notation Zplus := Z.add (only parsing). Notation Zopp := Z.opp (compat "8.7").
Notation Zsucc := Z.succ (compat "8.7").
Notation Zpred := Z.pred (compat "8.7").
Notation Zminus := Z.sub (only parsing).
Notation Zmult := Z.mul (only parsing).
Notation Zcompare := Z.compare (compat "8.7").
Notation Zsgn := Z.sgn (compat "8.7").
Notation Zle := Z.le (compat "8.7").
Notation Zge := Z.ge (compat "8.7").
Notation Zlt := Z.lt (compat "8.7").
Notation Zgt := Z.gt (compat "8.7").
Notation Zmax := Z.max (compat "8.7").
Notation Zmin := Z.min (compat "8.7").
Notation Zabs := Z.abs (compat "8.7").
Notation Zabs_nat := Z.abs_nat (compat "8.7").
Notation Zabs_N := Z.abs_N (compat "8.7").
Notation Z_of_nat := Z.of_nat (only parsing).
Notation Z_of_N := Z.of_N (only parsing).

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

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

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.