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
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
9
(************************************************************************)
11
(*i $Id: BigZ.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
14
Require Import ZMulOrder.
16
Require Import ZSigZAxioms.
19
Module BigZ <: ZType := ZMake.Make BigN.
21
(** Module [BigZ] implements [ZAxiomsSig] *)
23
Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
24
Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod.
26
(** Notations about [BigZ] *)
28
Notation bigZ := BigZ.t.
30
Delimit Scope bigZ_scope with bigZ.
31
Bind Scope bigZ_scope with bigZ.
32
Bind Scope bigZ_scope with BigZ.t.
33
Bind Scope bigZ_scope with BigZ.t_.
35
Notation Local "0" := BigZ.zero : bigZ_scope.
36
Infix "+" := BigZ.add : bigZ_scope.
37
Infix "-" := BigZ.sub : bigZ_scope.
38
Notation "- x" := (BigZ.opp x) : bigZ_scope.
39
Infix "*" := BigZ.mul : bigZ_scope.
40
Infix "/" := BigZ.div : bigZ_scope.
41
Infix "?=" := BigZ.compare : bigZ_scope.
42
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
43
Infix "<" := BigZ.lt : bigZ_scope.
44
Infix "<=" := BigZ.le : bigZ_scope.
45
Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
46
Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
47
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
49
Open Scope bigZ_scope.
51
(** Some additional results about [BigZ] *)
53
Theorem spec_to_Z: forall n:bigZ,
54
BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
56
intros n; case n; simpl; intros p;
57
generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
58
intros p1 H1; case H1; auto.
59
intros p1 H1; case H1; auto.
63
([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
65
intros n; case n; simpl; intros p;
66
generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
67
intros p1 H1; case H1; auto.
68
intros p1 H1; case H1; auto.
71
Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
72
BigN.to_Z (BigZ.to_N n) = [n].
74
intros n; case n; simpl; intros p;
75
generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
76
intros p1 _ H1; case H1; auto.
77
intros p1 H1; case H1; auto.
80
Lemma sub_opp : forall x y : bigZ, x - y == x + (- y).
82
red; intros; zsimpl; auto.
85
Lemma add_opp : forall x : bigZ, x + (- x) == 0.
87
red; intros; zsimpl; auto with zarith.
90
(** [BigZ] is a ring *)
93
ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
102
exact Zmul_add_distr_r.
107
Add Ring BigZr : BigZring.
109
(** Todo: tactic translating from [BigZ] to [Z] + omega *)
111
(** Todo: micromega *)