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
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
Todo: tactic translating from BigN to Z + omega

Todo: micromega