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
- NPropSig adds all generic properties derived from NAxioms
- NDivPropFunct provides generic properties of div and mod.
- MinMax*Properties provides properties of min and max.
Notations about BigN
Notation bigN :=
BigN.t.
Delimit Scope bigN_scope with bigN.
Local Notation "0" :=
BigN.zero :
bigN_scope.
Local Notation "1" :=
BigN.one :
bigN_scope.
Infix "+" :=
BigN.add :
bigN_scope.
Infix "-" :=
BigN.sub :
bigN_scope.
Infix "*" :=
BigN.mul :
bigN_scope.
Infix "/" :=
BigN.div :
bigN_scope.
Infix "^" :=
BigN.power :
bigN_scope.
Infix "?=" :=
BigN.compare :
bigN_scope.
Infix "==" :=
BigN.eq (
at level 70,
no associativity) :
bigN_scope.
Notation "x != y" := (
~x==y)%
bigN (
at level 70,
no associativity) :
bigN_scope.
Infix "<" :=
BigN.lt :
bigN_scope.
Infix "<=" :=
BigN.le :
bigN_scope.
Notation "x > y" := (
BigN.lt y x)(
only parsing) :
bigN_scope.
Notation "x >= y" := (
BigN.le y x)(
only parsing) :
bigN_scope.
Notation "x < y < z" := (
x<y /\ y<z)%
bigN :
bigN_scope.
Notation "x < y <= z" := (
x<y /\ y<=z)%
bigN :
bigN_scope.
Notation "x <= y < z" := (
x<=y /\ y<z)%
bigN :
bigN_scope.
Notation "x <= y <= z" := (
x<=y /\ y<=z)%
bigN :
bigN_scope.
Notation "[ i ]" := (
BigN.to_Z i) :
bigN_scope.
Infix "mod" :=
BigN.modulo (
at level 40,
no associativity) :
bigN_scope.
Local Open Scope bigN_scope.
Example of reasoning about BigN
BigN is a semi-ring
Detection of constants
Ltac isStaticWordCst t :=
match t with
|
W0 =>
constr:
true
|
WW ?
t1 ?
t2 =>
match isStaticWordCst t1 with
|
false =>
constr:
false
|
true =>
isStaticWordCst t2
end
|
_ =>
isInt31cst t
end.
Ltac isBigNcst t :=
match t with
|
BigN.N0 ?
t =>
isStaticWordCst t
|
BigN.N1 ?
t =>
isStaticWordCst t
|
BigN.N2 ?
t =>
isStaticWordCst t
|
BigN.N3 ?
t =>
isStaticWordCst t
|
BigN.N4 ?
t =>
isStaticWordCst t
|
BigN.N5 ?
t =>
isStaticWordCst t
|
BigN.N6 ?
t =>
isStaticWordCst t
|
BigN.Nn ?
n ?
t =>
match isnatcst n with
|
true =>
isStaticWordCst t
|
false =>
constr:
false
end
|
BigN.zero =>
constr:
true
|
BigN.one =>
constr:
true
|
_ =>
constr:
false
end.
Ltac BigNcst t :=
match isBigNcst t with
|
true =>
constr:
t
|
false =>
constr:
NotConstant
end.
Ltac Ncst t :=
match isNcst t with
|
true =>
constr:
t
|
false =>
constr:
NotConstant
end.
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