summaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN/BigN.v
blob: 41c255b1851ee50f47aca1b405d2ae650158aef4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: BigN.v 11282 2008-07-28 11:51:53Z msozeau $ i*)

(** * 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.
Bind Scope bigN_scope with bigN.
Bind Scope bigN_scope with BigN.t.
Bind Scope bigN_scope with BigN.t_.

Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *)
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.
Proof.
intros; apply succ_pred.
intro H'; rewrite H' in H; discriminate.
Qed.

(** [BigN] is a semi-ring *)

Lemma BigNring :
 semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
Proof.
constructor.
exact add_0_l.
exact add_comm.
exact add_assoc.
exact mul_1_l.
exact mul_0_l.
exact mul_comm.
exact mul_assoc.
exact mul_add_distr_r.
Qed.

Typeclasses unfold NZadd NZsub NZmul.

Add Ring BigNr : BigNring.

(** Todo: tactic translating from [BigN] to [Z] + omega *)

(** Todo: micromega *)