Library Stdlib.ZArith.BinInt
Require Export BinNums BinPos Pnat.
Require Import BinNat Bool Equalities GenericMinMax
OrdersFacts ZAxioms ZProperties DecidableClass.
Require BinIntDef.
Binary Integers
Local Open Scope Z_scope.
Every definitions and early properties about binary integers
are placed in a module Z for qualification purpose.
Include BinIntDef.Z.
Register add as num.Z.add.
Register opp as num.Z.opp.
Register succ as num.Z.succ.
Register pred as num.Z.pred.
Register sub as num.Z.sub.
Register mul as num.Z.mul.
Register pow as num.Z.pow.
Register of_nat as num.Z.of_nat.
When including property functors, only inline t eq zero one two
Definition eq := @Logic.eq Z.
Definition eq_equiv := @eq_equivalence Z.
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.
Register le as num.Z.le.
Register lt as num.Z.lt.
Register ge as num.Z.ge.
Register gt as num.Z.gt.
Register leb as num.Z.leb.
Register ltb as num.Z.ltb.
Register geb as num.Z.geb.
Register gtb as num.Z.gtb.
Register eqb as num.Z.eqb.
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 := _.
Properties of pos_sub
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
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.
Lemma pos_sub_add p q r :
pos_sub (p + q) r = pos p + pos_sub q r.
Local Arguments add !x !y.
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.
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.
Local Arguments pos_sub : simpl nomatch.
Lemma succ_pred n : succ (pred n) = n.
Lemma pred_succ n : pred (succ n) = n.
Lemma eqb_eq n m : (n =? m) = true <-> n = m.
#[global]
Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
Decidable_spec := Z.eqb_eq x y
}.
Lemma ltb_lt n m : (n <? m) = true <-> n < m.
#[global]
Instance Decidable_lt_Z : forall (x y : Z), DecidableClass.Decidable (x < y)%Z := {
Decidable_spec := Z.ltb_lt x y
}.
Lemma leb_le n m : (n <=? m) = true <-> n <= m.
#[global]
Instance Decidable_le_Z : forall (x y : Z), DecidableClass.Decidable (x <= y)%Z := {
Decidable_spec := Z.leb_le x y
}.
Lemma gtb_gt n m : (n >? m) = true <-> n > m.
#[global]
Instance Decidable_gt_Z : forall (x y : Z), DecidableClass.Decidable (x > y)%Z := {
Decidable_spec := Z.gtb_gt x y
}.
Lemma geb_ge n m : (n >=? m) = true <-> n >= m.
#[global]
Instance Decidable_ge_Z : forall (x y : Z), DecidableClass.Decidable (x >= y)%Z := {
Decidable_spec := Z.geb_ge x y
}.
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.
Remaining specification of lt and le
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.
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.
Register eq_decidable as num.Z.eq_decidable.
Register le_decidable as num.Z.le_decidable.
Register lt_decidable as num.Z.lt_decidable.
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.
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 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.
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 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.
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.
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.
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).
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
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)).
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.
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.
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 opp_eq_mul_m1 n : - n = n * -1.
Lemma add_diag n : n + n = 2 * n.
Lemma testbit_mod_pow2 a n i (H : 0 <= n)
: testbit (a mod 2 ^ n) i = ((i <? n) && testbit a i)%bool.
Lemma testbit_ones n i (H : 0 <= n)
: testbit (ones n) i = ((0 <=? i) && (i <? n))%bool.
Lemma testbit_ones_nonneg n i (Hn : 0 <= n) (Hi: 0 <= i)
: testbit (ones n) i = (i <? n).
End Z.
Bind Scope Z_scope with Z.t Z.
Re-export Notations
Number Notation Z Z.of_num_int Z.to_num_int : Z_scope.
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).
Lemma 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 ZPminus := Z.pos_sub (only parsing).
Notation Zplus := Z.add (only parsing). Notation Zminus := Z.sub (only parsing).
Notation Zmult := Z.mul (only parsing).
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 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 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'_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.
#[global]
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.
Re-export the notation for those who just Import BinInt
Number Notation Z Z.of_num_int Z.to_num_hex_int : hex_Z_scope.
Number Notation Z Z.of_num_int Z.to_num_int : Z_scope.
Number Notation Z Z.of_num_int Z.to_num_int : Z_scope.