Library Coq.ZArith.BinInt
Require Export BinNums BinPos Pnat.
Require Import BinNat Bool Plus Mult Equalities GenericMinMax
OrdersFacts ZAxioms ZProperties.
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.
When including property functors, only inline t eq zero one two
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.
Properties of pos_sub
Lemma pos_sub_spec p q :
pos_sub p q =
match (p ?= q)%positive with
| Eq => 0
| Lt => Zneg (q - p)
| Gt => Zpos (p - q)
end.
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 = Zneg (q - p).
Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = Zpos (p - q).
The opposite of pos_sub is pos_sub with reversed arguments
Lemma opp_Zneg p : - Zneg p = Zpos p.
Lemma opp_Zpos p : - Zpos p = Zneg p.
Lemma succ_Zpos p : succ (Zpos p) = Zpos (Pos.succ p).
Lemma add_Zpos p q : Zpos p + Zpos q = Zpos (p+q).
Lemma add_Zneg p q : Zneg p + Zneg q = Zneg (p+q).
Lemma add_Zpos_Zneg p q : Zpos p + Zneg q = pos_sub p q.
Lemma add_Zneg_Zpos p q : Zneg p + Zpos q = pos_sub q p.
Lemma sub_Zpos n m : (n < m)%positive -> Zpos m - Zpos n = Zpos (m-n).
Lemma mul_Zpos (p q : positive) : Zpos p * Zpos q = Zpos (p*q).
Lemma pow_Zpos p q : (Zpos p)^(Zpos q) = Zpos (p^q).
Lemma inj_Zpos p q : Zpos p = Zpos q <-> p = q.
Lemma inj_Zneg p q : Zneg p = Zneg q <-> p = q.
Lemma pos_xI p : Zpos p~1 = 2 * Zpos p + 1.
Lemma pos_xO p : Zpos p~0 = 2 * Zpos p.
Lemma neg_xI p : Zneg p~1 = 2 * Zneg p - 1.
Lemma neg_xO p : Zneg p~0 = 2 * Zneg 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.
Lemma pos_sub_add p q r :
pos_sub (p + q) r = Zpos p + pos_sub q r.
Lemma add_assoc n m p : n + (m + p) = n + m + p.
Multiplication and constants
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.
Lemma mul_add_distr_pos (p:positive) n m :
Zpos p * (n + m) = Zpos p * n + Zpos 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.
End Private_BootStrap.
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.
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 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 Zpos 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 : (Zpos p|Zpos q) <-> (p|q)%positive.
Lemma divide_Zpos_Zneg_r n p : (n|Zpos p) <-> (n|Zneg p).
Lemma divide_Zpos_Zneg_l n p : (Zpos p|n) <-> (Zneg 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 (Zpos a) n = N.testbit (Npos a) (to_N n).
Lemma testbit_Zneg a n : 0<=n ->
testbit (Zneg 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).
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.
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 := _.
Include ZProp
<+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
Otherwise Z stays associated with abstract_scope : (TODO FIX)
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 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.
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.
Notation "( x | y )" := (Z.divide x y) (at level 0).
Infix "?=" := Z.compare (at level 70, no associativity) : 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.
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.
Compatibility Notations
Notation Zdouble_plus_one := Z.succ_double (only parsing).
Notation Zdouble_minus_one := Z.pred_double (only parsing).
Notation Zdouble := Z.double (only parsing).
Notation ZPminus := Z.pos_sub (only parsing).
Notation Zsucc' := Z.succ (only parsing).
Notation Zpred' := Z.pred (only parsing).
Notation Zplus' := Z.add (only parsing).
Notation Zplus := Z.add (only parsing). Notation Zopp := Z.opp (only parsing).
Notation Zsucc := Z.succ (only parsing).
Notation Zpred := Z.pred (only parsing).
Notation Zminus := Z.sub (only parsing).
Notation Zmult := Z.mul (only parsing).
Notation Zcompare := Z.compare (only parsing).
Notation Zsgn := Z.sgn (only parsing).
Notation Zle := Z.le (only parsing).
Notation Zge := Z.ge (only parsing).
Notation Zlt := Z.lt (only parsing).
Notation Zgt := Z.gt (only parsing).
Notation Zmax := Z.max (only parsing).
Notation Zmin := Z.min (only parsing).
Notation Zabs := Z.abs (only parsing).
Notation Zabs_nat := Z.abs_nat (only parsing).
Notation Zabs_N := Z.abs_N (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 Zopp_0 := Z.opp_0 (only parsing).
Notation Zopp_neg := Z.opp_Zneg (only parsing).
Notation Zopp_involutive := Z.opp_involutive (only parsing).
Notation Zopp_inj := Z.opp_inj (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 Zopp_succ := Z.opp_succ (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_inj := Z.succ_inj (only parsing).
Notation Zsucc'_inj := Z.succ_inj (only parsing).
Notation Zsucc'_pred' := Z.succ_pred (only parsing).
Notation Zpred'_succ' := Z.pred_succ (only parsing).
Notation Zpred'_inj := Z.pred_inj (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 := Z.pos_xI (only parsing).
Notation Zpos_xO := Z.pos_xO (only parsing).
Notation Zneg_xI := Z.neg_xI (only parsing).
Notation Zneg_xO := Z.neg_xO (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 Zpos_succ_morphism : forall p, Zpos (Psucc p) = Zsucc (Zpos p).
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 Zpos_minus_morphism : forall a b,
Pcompare a b Eq = Lt -> Zpos (b - a) = Zpos b - Zpos a.
Lemma Zeq_minus : forall n m, n = m -> n - m = 0.
Lemma Zminus_eq : forall n m, n - m = 0 -> n = m.
Lemma Zpos_mult_morphism : forall p q, Zpos (p * q) = Zpos p * Zpos q.
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 * Zsucc m.
Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Zsucc n * m.
Lemma Zpos_eq : forall p q, p = q -> Zpos p = Zpos q.
Lemma Zpos_eq_rev : forall p q, Zpos p = Zpos q -> p = q.
Lemma Zpos_eq_iff : forall p q, p = q <-> Zpos p = Zpos q.
Lemma Zpos_plus_distr : forall p q, Zpos (p + q) = Zpos p + Zpos q.
Lemma Zneg_plus_distr : forall p q, Zneg (p + q) = Zneg p + Zneg q.
Hint Immediate Zsucc_pred: zarith.
Obsolete stuff