# Library Coq.Numbers.Integer.BigZ.BigZ

Require Export BigN.
Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.

# BigZ : arbitrary large efficient integers.

The following BigZ module regroups both the operations and all the abstract properties:

- ZMake.Make BigN provides the operations and basic specs w.r.t. ZArith
- ZTypeIsZAxioms shows (mainly) that these operations implement the interface ZAxioms
- ZProp adds all generic properties derived from ZAxioms
- MinMax*Properties provides properties of min and max

Delimit Scope bigZ_scope with bigZ.
Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder.
Include ZMake.Make BigN [scope abstract_scope to bigZ_scope].
Include ZTypeIsZAxioms
<+ ZProp [no inline]
<+ HasEqBool2Dec [no inline]
<+ MinMaxLogicalProperties [no inline]
<+ MinMaxDecProperties [no inline].
End BigZ.
For precision concerning the above scope handling, see comment in BigN
Notations about BigZ
Local Open Scope bigZ_scope.
Notation bigZ := BigZ.t.
Local Notation "0" := BigZ.zero : bigZ_scope.
Local Notation "1" := BigZ.one : bigZ_scope.
Local Notation "2" := BigZ.two : 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.pow : bigZ_scope.
Infix "?=" := BigZ.compare : bigZ_scope.
Infix "=?" := BigZ.eqb (at level 70, no associativity) : bigZ_scope.
Infix "<=?" := BigZ.leb (at level 70, no associativity) : bigZ_scope.
Infix "<?" := BigZ.ltb (at level 70, no associativity) : bigZ_scope.
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope.
Infix "<" := BigZ.lt : bigZ_scope.
Infix "<=" := BigZ.le : bigZ_scope.
Notation "x > y" := (y < x) (only parsing) : bigZ_scope.
Notation "x >= y" := (y <= x) (only parsing) : bigZ_scope.
Notation "x < y < z" := (x<y /\ y<z) : bigZ_scope.
Notation "x < y <= z" := (x<y /\ y<=z) : bigZ_scope.
Notation "x <= y < z" := (x<=y /\ y<z) : bigZ_scope.
Notation "x <= y <= z" := (x<=y /\ y<=z) : bigZ_scope.
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
Some additional results about BigZ
Theorem spec_to_Z: forall n : bigZ,
BigN.to_Z (BigZ.to_N n) = ((Z.sgn [n]) * [n])%Z.
Theorem spec_to_N n:
([n] = Z.sgn [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].
BigZ is a ring
Lemma BigZring :
ring_theory 0 1 BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y.
Definition BigZ_of_N n := BigZ.of_Z (Z.of_N n).
Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow.
Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _)
(fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b).
Detection of constants
Ltac isBigZcst t :=
match t with
| BigZ.Pos ?t => isBigNcst t
| BigZ.Neg ?t => isBigNcst t
| BigZ.zero => constr:true
| BigZ.one => constr:true
| BigZ.two => constr:true
| BigZ.minus_one => constr:true
| _ => constr:false
end.
Ltac BigZcst t :=
match isBigZcst t with
| true => constr:t
| false => constr:NotConstant
end.
Ltac BigZ_to_N t :=
match t with
| BigZ.Pos ?t => BigN_to_N t
| BigZ.zero => constr:0%N
| BigZ.one => constr:1%N
| BigZ.two => constr:2%N
| _ => constr:NotConstant
end.
Registration for the "ring" tactic
Add Ring BigZr : BigZring
(decidable BigZeqb_correct,
constants [BigZcst],
power_tac BigZpower [BigZ_to_N],
div BigZdiv).
Section TestRing.
Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x.
Let test' : forall x y, 1 + x*y + x^2 - 1*1 - y*x + 1*(-x)*x == 0.
End TestRing.
BigZ also benefits from an "order" tactic
Ltac bigZ_order := BigZ.order.
Section TestOrder.
Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
End TestOrder.
We can use at least a bit of (r)omega by translating to Z.
Section TestOmega.
Let test : forall x y : bigZ, x<=y -> y<=x -> x==y.
End TestOmega.
Todo: micromega