Library Coq.Numbers.Integer.BigZ.BigZ
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
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
BigZ is a ring
Detection of constants
Registration for the "ring" tactic
BigZ also benefits from an "order" tactic
We can use at least a bit of (r)omega by translating to Z.
Todo: micromega