Library Coq.Numbers.Natural.BigN.BigN
Efficient arbitrary large natural numbers in base 2^31
Initial Author: Arnaud Spiwack
The following
BigN module regroups both the operations and
all the abstract properties:
- NMake.Make Int31Cyclic provides the operations and basic specs
w.r.t. ZArith
- NTypeIsNAxioms shows (mainly) that these operations implement
the interface NAxioms
- NProp adds all generic properties derived from NAxioms
- MinMax*Properties provides properties of min and max.
Notations about BigN
Local Open Scope bigN_scope.
Notation bigN :=
BigN.t.
Infix "+" :=
BigN.add :
bigN_scope.
Infix "-" :=
BigN.sub :
bigN_scope.
Infix "*" :=
BigN.mul :
bigN_scope.
Infix "/" :=
BigN.div :
bigN_scope.
Infix "^" :=
BigN.pow :
bigN_scope.
Infix "?=" :=
BigN.compare :
bigN_scope.
Infix "=?" :=
BigN.eqb (
at level 70,
no associativity) :
bigN_scope.
Infix "<=?" :=
BigN.leb (
at level 70,
no associativity) :
bigN_scope.
Infix "<?" :=
BigN.ltb (
at level 70,
no associativity) :
bigN_scope.
Infix "==" :=
BigN.eq (
at level 70,
no associativity) :
bigN_scope.
Notation "x != y" := (
~x==y) (
at level 70,
no associativity) :
bigN_scope.
Infix "<" :=
BigN.lt :
bigN_scope.
Infix "<=" :=
BigN.le :
bigN_scope.
Notation "x > y" := (
y < x) (
only parsing) :
bigN_scope.
Notation "x >= y" := (
y <= x) (
only parsing) :
bigN_scope.
Notation "x < y < z" := (
x<y /\ y<z) :
bigN_scope.
Notation "x < y <= z" := (
x<y /\ y<=z) :
bigN_scope.
Notation "x <= y < z" := (
x<=y /\ y<z) :
bigN_scope.
Notation "x <= y <= z" := (
x<=y /\ y<=z) :
bigN_scope.
Notation "[ i ]" := (
BigN.to_Z i) :
bigN_scope.
Infix "mod" :=
BigN.modulo (
at level 40,
no associativity) :
bigN_scope.
Example of reasoning about BigN
BigN is a semi-ring
Detection of constants
Registration for the "ring" tactic
We benefit also from an "order" tactic
We can use at least a bit of (r)omega by translating to Z.
Todo: micromega