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 NDiv GenericMinMax.

The following BigN module regroups both the operations and all the abstract properties:

Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
 NMake.Make Int31Cyclic <+ NTypeIsNAxioms
 <+ !NPropSig <+ !NDivPropFunct <+ HasEqBool2Dec
 <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.

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

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, BigN.eq_bool x y = true -> x==y.

Lemma BigNpower : power_theory 1 BigN.mul BigN.eq (@id N) BigN.power.

Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
 (fun a b => if BigN.eq_bool 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
 | _ => 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

Add Ring BigNr : BigNring
 (decidable BigNeqb_correct,
  constants [BigNcst],
  power_tac BigNpower [Ncst],
  div BigNdiv).

Section TestRing.
Let test : forall x y, 1 + x*y + 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