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
- ZPropSig adds all generic properties derived from ZAxioms
- ZDivPropFunct provides generic properties of div and mod
("Floor" variant)
- MinMax*Properties provides properties of min and max
Notations about BigZ
Notation bigZ :=
BigZ.t.
Delimit Scope bigZ_scope with bigZ.
Local Notation "0" :=
BigZ.zero :
bigZ_scope.
Local Notation "1" :=
BigZ.one :
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.power :
bigZ_scope.
Infix "?=" :=
BigZ.compare :
bigZ_scope.
Infix "==" :=
BigZ.eq (
at level 70,
no associativity) :
bigZ_scope.
Notation "x != y" := (
~x==y)%
bigZ (
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 "x < y < z" := (
x<y /\ y<z)%
bigZ :
bigZ_scope.
Notation "x < y <= z" := (
x<y /\ y<=z)%
bigZ :
bigZ_scope.
Notation "x <= y < z" := (
x<=y /\ y<z)%
bigZ :
bigZ_scope.
Notation "x <= y <= z" := (
x<=y /\ y<=z)%
bigZ :
bigZ_scope.
Notation "[ i ]" := (
BigZ.to_Z i) :
bigZ_scope.
Infix "mod" :=
BigZ.modulo (
at level 40,
no associativity) :
bigN_scope.
Local Open Scope 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