Library Coq.Numbers.Integer.Binary.ZBinary



Require Import ZAxioms ZProperties.
Require Import ZArith_base.

Local Open Scope Z_scope.

Implementation of ZAxiomsSig by BinInt.Z


Module ZBinAxiomsMod <: ZAxiomsExtSig.

Bi-directional induction.

Theorem bi_induction :
  forall A : Z -> Prop, Proper (eq ==> iff) A ->
    A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.

Basic operations.

Definition eq_equiv : Equivalence (@eq Z) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Program Instance succ_wd : Proper (eq==>eq) Zsucc.
Program Instance pred_wd : Proper (eq==>eq) Zpred.
Program Instance add_wd : Proper (eq==>eq==>eq) Zplus.
Program Instance sub_wd : Proper (eq==>eq==>eq) Zminus.
Program Instance mul_wd : Proper (eq==>eq==>eq) Zmult.

Definition pred_succ n := eq_sym (Zpred_succ n).
Definition add_0_l := Zplus_0_l.
Definition add_succ_l := Zplus_succ_l.
Definition sub_0_r := Zminus_0_r.
Definition sub_succ_r := Zminus_succ_r.
Definition mul_0_l := Zmult_0_l.
Definition mul_succ_l := Zmult_succ_l.

Order

Program Instance lt_wd : Proper (eq==>eq==>iff) Zlt.

Definition lt_eq_cases := Zle_lt_or_eq_iff.
Definition lt_irrefl := Zlt_irrefl.
Definition lt_succ_r := Zlt_succ_r.

Definition min_l := Zmin_l.
Definition min_r := Zmin_r.
Definition max_l := Zmax_l.
Definition max_r := Zmax_r.

Properties specific to integers, not natural numbers.

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

Definition succ_pred n := eq_sym (Zsucc_pred n).
Definition opp_0 := Zopp_0.
Definition opp_succ := Zopp_succ.

Absolute value and sign

Definition abs_eq := Zabs_eq.
Definition abs_neq := Zabs_non_eq.

Lemma sgn_null : forall x, x = 0 -> Zsgn x = 0.
Lemma sgn_pos : forall x, 0 < x -> Zsgn x = 1.
Lemma sgn_neg : forall x, x < 0 -> Zsgn x = -1.

The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas.

Definition t := Z.
Definition eq := (@eq Z).
Definition zero := 0.
Definition succ := Zsucc.
Definition pred := Zpred.
Definition add := Zplus.
Definition sub := Zminus.
Definition mul := Zmult.
Definition lt := Zlt.
Definition le := Zle.
Definition min := Zmin.
Definition max := Zmax.
Definition opp := Zopp.
Definition abs := Zabs.
Definition sgn := Zsgn.

End ZBinAxiomsMod.

Module Export ZBinPropMod := ZPropFunct ZBinAxiomsMod.

Z forms a ring