Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig.

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.

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.

Theorem succ_pred : forall n, succ (pred n) == n.

Program Instance opp_wd : Proper (eq ==> eq) opp.

Theorem opp_0 : - 0 == 0.

Theorem opp_succ : forall n, - (succ n) == pred (- n).

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.

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

Lemma square_spec n : square n == n * n.

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.

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.

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.

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.

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.

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.

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.