← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Numbers/Natural/BigN/BigN.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Numbers/Natural/BigN/BigN.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: BigN.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
10
 
 
11
(** * Natural numbers in base 2^31 *)
 
12
 
 
13
(**
 
14
Author: Arnaud Spiwack
 
15
*)
 
16
 
 
17
Require Export Int31.
 
18
Require Import CyclicAxioms.
 
19
Require Import Cyclic31.
 
20
Require Import NSig.
 
21
Require Import NSigNAxioms.
 
22
Require Import NMake.
 
23
Require Import NSub.
 
24
 
 
25
Module BigN <: NType := NMake.Make Int31Cyclic.
 
26
 
 
27
(** Module [BigN] implements [NAxiomsSig] *)
 
28
 
 
29
Module Export BigNAxiomsMod := NSig_NAxioms BigN.
 
30
Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod.
 
31
 
 
32
(** Notations about [BigN] *)
 
33
 
 
34
Notation bigN := BigN.t.
 
35
 
 
36
Delimit Scope bigN_scope with bigN.
 
37
Bind Scope bigN_scope with bigN.
 
38
Bind Scope bigN_scope with BigN.t.
 
39
Bind Scope bigN_scope with BigN.t_.
 
40
 
 
41
Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *)
 
42
Infix "+" := BigN.add : bigN_scope.
 
43
Infix "-" := BigN.sub : bigN_scope.
 
44
Infix "*" := BigN.mul : bigN_scope.
 
45
Infix "/" := BigN.div : bigN_scope.
 
46
Infix "?=" := BigN.compare : bigN_scope.
 
47
Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
 
48
Infix "<" := BigN.lt : bigN_scope.
 
49
Infix "<=" := BigN.le : bigN_scope.
 
50
Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
 
51
Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
 
52
Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 
53
 
 
54
Open Scope bigN_scope.
 
55
 
 
56
(** Example of reasoning about [BigN] *)
 
57
 
 
58
Theorem succ_pred: forall q:bigN,
 
59
  0 < q -> BigN.succ (BigN.pred q) == q.
 
60
Proof.
 
61
intros; apply succ_pred.
 
62
intro H'; rewrite H' in H; discriminate.
 
63
Qed.
 
64
 
 
65
(** [BigN] is a semi-ring *)
 
66
 
 
67
Lemma BigNring :
 
68
 semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
 
69
Proof.
 
70
constructor.
 
71
exact add_0_l.
 
72
exact add_comm.
 
73
exact add_assoc.
 
74
exact mul_1_l.
 
75
exact mul_0_l.
 
76
exact mul_comm.
 
77
exact mul_assoc.
 
78
exact mul_add_distr_r.
 
79
Qed.
 
80
 
 
81
Add Ring BigNr : BigNring.
 
82
 
 
83
(** Todo: tactic translating from [BigN] to [Z] + omega *)
 
84
 
 
85
(** Todo: micromega *)