# Library Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms

Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig.

# The interface ZSig.ZType implies the interface ZAxiomsSig

Module ZTypeIsZAxioms (Import ZZ : ZType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_square spec_sqrt
spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min
spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd
spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2
: zsimpl.
Ltac zsimpl := autorewrite with zsimpl.
Ltac zcongruence := repeat red; intros; zsimpl; congruence.
Ltac zify := unfold eq, lt, le in *; zsimpl.
Instance eq_equiv : Equivalence eq.
Local Obligation Tactic := zcongruence.
Program Instance succ_wd : Proper (eq ==> eq) succ.
Program Instance pred_wd : Proper (eq ==> eq) pred.
Program Instance add_wd : Proper (eq ==> eq ==> eq) add.
Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
Theorem pred_succ : forall n, pred (succ n) == n.
Theorem one_succ : 1 == succ 0.
Theorem two_succ : 2 == succ 1.
Section Induction.
Variable A : ZZ.t -> Prop.
Hypothesis A_wd : Proper (eq ==> iff) A.
Hypothesis A0 : A 0.
Hypothesis AS : forall n, A n <-> A (succ n).
Let B (z : Z) := A (of_Z z).
Lemma B0 : B 0.
Lemma BS : forall z : Z, B z -> B (z + 1).
Lemma BP : forall z : Z, B z -> B (z - 1).
Lemma B_holds : forall z : Z, B z.
Theorem bi_induction : forall n, A n.
End Induction.
Theorem add_0_l : forall n, 0 + n == n.
Theorem add_succ_l : forall n m, ( succ n ) + m == succ (n + m).
Theorem sub_0_r : forall n, n - 0 == n.
Theorem sub_succ_r : forall n m, n - ( succ m ) == pred (n - m).
Theorem mul_0_l : forall n, 0 * n == 0.
Theorem mul_succ_l : forall n m, ( succ n ) * m == n * m + m.
Order
Lemma eqb_eq x y : eqb x y = true <-> x == y.
Lemma leb_le x y : leb x y = true <-> x <= y.
Lemma ltb_lt x y : ltb x y = true <-> x < y.
Lemma compare_eq_iff n m : compare n m = Eq <-> n == m.
Lemma compare_lt_iff n m : compare n m = Lt <-> n < m.
Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m.
Lemma compare_antisym n m : compare m n = CompOpp (compare n m).
Include BoolOrderFacts ZZ ZZ ZZ [no inline].
Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
Theorem lt_succ_r : forall n m, n < ( succ m ) <-> n <= m.
Theorem min_l : forall n m, n <= m -> min n m == n.
Theorem min_r : forall n m, m <= n -> min n m == m.
Theorem max_l : forall n m, m <= n -> max n m == n.
Theorem max_r : forall n m, n <= m -> max n m == m.
Part specific to integers, not natural numbers
Theorem succ_pred : forall n, succ (pred n) == n.
Opp
Program Instance opp_wd : Proper (eq ==> eq) opp.
Theorem opp_0 : - 0 == 0.
Theorem opp_succ : forall n, - ( succ n ) == pred (- n).
Abs / Sgn
Theorem abs_eq : forall n, 0 <= n -> abs n == n.
Theorem abs_neq : forall n, n <= 0 -> abs n == - n.
Theorem sgn_null : forall n, n ==0 -> sgn n == 0.
Theorem sgn_pos : forall n, 0< n -> sgn n == 1.
Theorem sgn_neg : forall n, n <0 -> sgn n == opp 1.
Power
Program Instance pow_wd : Proper (eq ==> eq ==> eq) pow.
Lemma pow_0_r : forall a, a ^0 == 1.
Lemma pow_succ_r : forall a b, 0<= b -> a ^( succ b ) == a * a ^ b.
Lemma pow_neg_r : forall a b, b <0 -> a ^ b == 0.
Lemma pow_pow_N : forall a b, 0<= b -> a ^ b == pow_N a (Z.to_N (to_Z b)).
Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p).
Square
Lemma square_spec n : square n == n * n.
Sqrt
Lemma sqrt_spec : forall n, 0<= n ->
( sqrt n )*( sqrt n ) <= n /\ n < ( succ (sqrt n))*( succ (sqrt n)).
Lemma sqrt_neg : forall n, n <0 -> sqrt n == 0.
Log2
Lemma log2_spec : forall n, 0< n ->
2^( log2 n ) <= n /\ n < 2^( succ (log2 n)).
Lemma log2_nonpos : forall n, n <=0 -> log2 n == 0.
Even / Odd
Definition Even n := exists m , n == 2* m.
Definition Odd n := exists m , n == 2* m +1.
Lemma even_spec n : even n = true <-> Even n.
Lemma odd_spec n : odd n = true <-> Odd n.
Div / Mod
Program Instance div_wd : Proper (eq ==> eq ==> eq) div.
Program Instance mod_wd : Proper (eq ==> eq ==> eq) modulo.
Theorem div_mod : forall a b, ~ b ==0 -> a == b *( div a b ) + ( modulo a b ).
Theorem mod_pos_bound :
forall a b, 0 < b -> 0 <= modulo a b /\ modulo a b < b.
Theorem mod_neg_bound :
forall a b, b < 0 -> b < modulo a b /\ modulo a b <= 0.
Definition mod_bound_pos :
forall a b, 0<= a -> 0< b -> 0 <= modulo a b /\ modulo a b < b :=
fun a b _ H => mod_pos_bound a b H.
Quot / Rem
Program Instance quot_wd : Proper (eq ==> eq ==> eq) quot.
Program Instance rem_wd : Proper (eq ==> eq ==> eq) rem.
Theorem quot_rem : forall a b, ~ b ==0 -> a == b *( quot a b ) + rem a b.
Theorem rem_bound_pos :
forall a b, 0<= a -> 0< b -> 0 <= rem a b /\ rem a b < b.
Theorem rem_opp_l : forall a b, ~ b ==0 -> rem (- a) b == -( rem a b ).
Theorem rem_opp_r : forall a b, ~ b ==0 -> rem a (- b) == rem a b.
Gcd
Definition divide n m := exists p , m == p * n.
Local Notation "( x | y )" := (divide x y) (at level 0).
Lemma spec_divide : forall n m, ( n | m ) <-> Z.divide [ n ] [ m ].
Lemma gcd_divide_l : forall n m, ( gcd n m | n ).
Lemma gcd_divide_r : forall n m, ( gcd n m | m ).
Lemma gcd_greatest : forall n m p, ( p | n ) -> ( p | m ) -> ( p | gcd n m ).
Lemma gcd_nonneg : forall n m, 0 <= gcd n m.
Bitwise operations
Program Instance testbit_wd : Proper (eq ==> eq ==> Logic.eq) testbit.
Lemma testbit_odd_0 : forall a, testbit (2* a +1) 0 = true.
Lemma testbit_even_0 : forall a, testbit (2* a) 0 = false.
Lemma testbit_odd_succ : forall a n, 0<= n ->
testbit (2* a +1) (succ n) = testbit a n.
Lemma testbit_even_succ : forall a n, 0<= n ->
testbit (2* a) (succ n) = testbit a n.
Lemma testbit_neg_r : forall a n, n <0 -> testbit a n = false.
Lemma shiftr_spec : forall a n m, 0<= m ->
testbit (shiftr a n) m = testbit a (m + n).
Lemma shiftl_spec_high : forall a n m, 0<= m -> n <= m ->
testbit (shiftl a n) m = testbit a (m - n).
Lemma shiftl_spec_low : forall a n m, m < n ->
testbit (shiftl a n) m = false.
Lemma land_spec : forall a b n,
testbit (land a b) n = testbit a n && testbit b n.
Lemma lor_spec : forall a b n,
testbit (lor a b) n = testbit a n || testbit b n.
Lemma ldiff_spec : forall a b n,
testbit (ldiff a b) n = testbit a n && negb (testbit b n).
Lemma lxor_spec : forall a b n,
testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
Lemma div2_spec : forall a, div2 a == shiftr a 1.
End ZTypeIsZAxioms.
Module ZType_ZAxioms (ZZ : ZType)
<: ZAxiomsSig <: OrderFunctions ZZ <: HasMinMax ZZ
:= ZZ <+ ZTypeIsZAxioms.