blob: e5e950acd4cfb1b5347bd23209d5bc139c6c0ae6 (
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
(*i $Id: BigZ.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
Require Export BigN.
Require Import ZMulOrder.
Require Import ZSig.
Require Import ZSigZAxioms.
Require Import ZMake.
Module BigZ <: ZType := ZMake.Make BigN.
(** Module [BigZ] implements [ZAxiomsSig] *)
Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod.
(** Notations about [BigZ] *)
Notation bigZ := BigZ.t.
Delimit Scope bigZ_scope with bigZ.
Bind Scope bigZ_scope with bigZ.
Bind Scope bigZ_scope with BigZ.t.
Bind Scope bigZ_scope with BigZ.t_.
Notation Local "0" := BigZ.zero : bigZ_scope.
Infix "+" := BigZ.add : bigZ_scope.
Infix "-" := BigZ.sub : bigZ_scope.
Notation "- x" := (BigZ.opp x) : bigZ_scope.
Infix "*" := BigZ.mul : bigZ_scope.
Infix "/" := BigZ.div : bigZ_scope.
Infix "?=" := BigZ.compare : bigZ_scope.
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
Infix "<" := BigZ.lt : bigZ_scope.
Infix "<=" := BigZ.le : bigZ_scope.
Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
Open Scope bigZ_scope.
(** Some additional results about [BigZ] *)
Theorem spec_to_Z: forall n:bigZ,
BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
Proof.
intros n; case n; simpl; intros p;
generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
intros p1 H1; case H1; auto.
intros p1 H1; case H1; auto.
Qed.
Theorem spec_to_N n:
([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
Proof.
intros n; case n; simpl; intros p;
generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
intros p1 H1; case H1; auto.
intros p1 H1; case H1; auto.
Qed.
Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
BigN.to_Z (BigZ.to_N n) = [n].
Proof.
intros n; case n; simpl; intros p;
generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
intros p1 _ H1; case H1; auto.
intros p1 H1; case H1; auto.
Qed.
Lemma sub_opp : forall x y : bigZ, x - y == x + (- y).
Proof.
red; intros; zsimpl; auto.
Qed.
Lemma add_opp : forall x : bigZ, x + (- x) == 0.
Proof.
red; intros; zsimpl; auto with zarith.
Qed.
(** [BigZ] is a ring *)
Lemma BigZring :
ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
Proof.
constructor.
exact Zadd_0_l.
exact Zadd_comm.
exact Zadd_assoc.
exact Zmul_1_l.
exact Zmul_comm.
exact Zmul_assoc.
exact Zmul_add_distr_r.
exact sub_opp.
exact add_opp.
Qed.
Add Ring BigZr : BigZring.
(** Todo: tactic translating from [BigZ] to [Z] + omega *)
(** Todo: micromega *)
|
