Library Coq.Numbers.Integer.BigZ.BigZ



Require Export BigN.
Require Import ZMulOrder.
Require Import ZSig.
Require Import ZSigZAxioms.
Require Import ZMake.

Module BigZ <: ZType := ZMake.Make BigN.

Module BigZ implements ZAxiomsSig

Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod.

Notations about BigZ

Notation bigZ := BigZ.t.

Delimit Scope bigZ_scope with bigZ.

Notation Local "0" := BigZ.zero : bigZ_scope.
Infix "+" := BigZ.add : bigZ_scope.
Infix "-" := BigZ.sub : bigZ_scope.
Notation "- x" := (BigZ.opp x) : bigZ_scope.
Infix "*" := BigZ.mul : bigZ_scope.
Infix "/" := BigZ.div : bigZ_scope.
Infix "?=" := BigZ.compare : bigZ_scope.
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
Infix "<" := BigZ.lt : bigZ_scope.
Infix "<=" := BigZ.le : bigZ_scope.
Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.

Open Scope bigZ_scope.

Some additional results about BigZ

Theorem spec_to_Z: forall n:bigZ,
  BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.

Theorem spec_to_N n:
 ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.

Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
  BigN.to_Z (BigZ.to_N n) = [n].

Lemma sub_opp : forall x y : bigZ, x - y == x + (- y).

Lemma add_opp : forall x : bigZ, x + (- x) == 0.

BigZ is a ring

Lemma BigZring :
 ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.

Add Ring BigZr : BigZring.

Todo: tactic translating from BigZ to Z + omega

Todo: micromega