Library Coq.Numbers.Natural.BigN.BigN



Natural numbers in base 2^31


Author: Arnaud Spiwack

Require Export Int31.
Require Import CyclicAxioms.
Require Import Cyclic31.
Require Import NSig.
Require Import NSigNAxioms.
Require Import NMake.
Require Import NSub.

Module BigN <: NType := NMake.Make Int31Cyclic.

Module BigN implements NAxiomsSig

Module Export BigNAxiomsMod := NSig_NAxioms BigN.
Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod.

Notations about BigN

Notation bigN := BigN.t.

Delimit Scope bigN_scope with bigN.

Notation Local "0" := BigN.zero : bigN_scope. Infix "+" := BigN.add : bigN_scope.
Infix "-" := BigN.sub : bigN_scope.
Infix "*" := BigN.mul : bigN_scope.
Infix "/" := BigN.div : bigN_scope.
Infix "?=" := BigN.compare : bigN_scope.
Infix "==" := BigN.eq (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 "[ i ]" := (BigN.to_Z i) : bigN_scope.

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 BigN.zero BigN.one BigN.add BigN.mul BigN.eq.

Add Ring BigNr : BigNring.

Todo: tactic translating from BigN to Z + omega

Todo: micromega