# Library Coq.Numbers.Natural.BigN.BigN

# Efficient arbitrary large natural numbers in base 2^31

Initial Author: Arnaud Spiwack
Require Export Int31.
Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
NProperties GenericMinMax.
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.

Delimit Scope bigN_scope with bigN.
Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
Include NTypeIsNAxioms
<+ NProp [no inline]
<+ HasEqBool2Dec [no inline]
<+ MinMaxLogicalProperties [no inline]
<+ MinMaxDecProperties [no inline].
End BigN.
Nota concerning scopes : for the first Include, we cannot bind the scope bigN_scope to a type that doesn't exists yet. We hence need to explicitely declare the scope substitution. For the next Include, the abstract type t (in scope abstract_scope) gets substituted to concrete BigN.t (in scope bigN_scope), and the corresponding argument scope are fixed automatically.
Notations about BigN
Local Open Scope bigN_scope.
Notation bigN := BigN.t.
Local Notation "0" := BigN.zero : bigN_scope. Local Notation "1" := BigN.one : bigN_scope. Local Notation "2" := BigN.two : bigN_scope. 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
Theorem succ_pred: forall q : bigN,
0 < q -> BigN.succ (BigN.pred q) == q.
BigN is a semi-ring
Lemma BigNring : semi_ring_theory 0 1 BigN.add BigN.mul BigN.eq.
Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y.
Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
(fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
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
| BigN.two => constr:true
| _ => constr:false
end.
Ltac BigNcst t :=
match isBigNcst t with
| true => constr:t
| false => constr:NotConstant
end.
Ltac BigN_to_N t :=
match isBigNcst t with
| true => eval vm_compute in (BigN.to_N t)
| false => constr:NotConstant
end.
Ltac Ncst t :=
match isNcst t with
| true => constr:t
| false => constr:NotConstant
end.
Registration for the "ring" tactic
Add Ring BigNr : BigNring
(decidable BigNeqb_correct,
constants [BigNcst],
power_tac BigNpower [BigN_to_N],
div BigNdiv).
Section TestRing.
Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
Qed.
End TestRing.
We benefit also from an "order" tactic
Ltac bigN_order := BigN.order.
Section TestOrder.
Let test : forall x y : bigN, 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 : bigN, x<=y -> y<=x -> x==y.
End TestOmega.
Todo: micromega