← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/Raxioms.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/Reals/Raxioms.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: Raxioms.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
(*********************************************************)
 
12
(**    Axiomatisation of the classical reals             *)
 
13
(*********************************************************)
 
14
 
 
15
Require Export ZArith_base.
 
16
Require Export Rdefinitions.
 
17
Open Local Scope R_scope.
 
18
 
 
19
(*********************************************************)
 
20
(** *            Field axioms                            *)
 
21
(*********************************************************)
 
22
 
 
23
(*********************************************************)
 
24
(** **   Addition                                        *)
 
25
(*********************************************************)
 
26
 
 
27
(**********)
 
28
Axiom Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
 
29
Hint Resolve Rplus_comm: real.
 
30
 
 
31
(**********)
 
32
Axiom Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
 
33
Hint Resolve Rplus_assoc: real.
 
34
 
 
35
(**********)
 
36
Axiom Rplus_opp_r : forall r:R, r + - r = 0.
 
37
Hint Resolve Rplus_opp_r: real v62.
 
38
 
 
39
(**********)
 
40
Axiom Rplus_0_l : forall r:R, 0 + r = r.
 
41
Hint Resolve Rplus_0_l: real.
 
42
 
 
43
(***********************************************************)       
 
44
(** **    Multiplication                                   *)
 
45
(***********************************************************)
 
46
 
 
47
(**********)
 
48
Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
 
49
Hint Resolve Rmult_comm: real v62. 
 
50
 
 
51
(**********)
 
52
Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
 
53
Hint Resolve Rmult_assoc: real v62.
 
54
 
 
55
(**********)
 
56
Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
 
57
Hint Resolve Rinv_l: real.
 
58
 
 
59
(**********)
 
60
Axiom Rmult_1_l : forall r:R, 1 * r = r.
 
61
Hint Resolve Rmult_1_l: real.
 
62
 
 
63
(**********)
 
64
Axiom R1_neq_R0 : 1 <> 0.
 
65
Hint Resolve R1_neq_R0: real.
 
66
 
 
67
(*********************************************************)
 
68
(** **   Distributivity                                  *)
 
69
(*********************************************************)
 
70
 
 
71
(**********)
 
72
Axiom
 
73
  Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
 
74
Hint Resolve Rmult_plus_distr_l: real v62.
 
75
 
 
76
(*********************************************************)
 
77
(** *    Order axioms                                    *)
 
78
(*********************************************************)
 
79
(*********************************************************)
 
80
(** **   Total Order                                     *)
 
81
(*********************************************************)
 
82
 
 
83
(**********)
 
84
Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}.
 
85
 
 
86
(*********************************************************)
 
87
(** **   Lower                                           *)
 
88
(*********************************************************)
 
89
 
 
90
(**********)
 
91
Axiom Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
 
92
 
 
93
(**********)
 
94
Axiom Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
 
95
 
 
96
(**********)
 
97
Axiom Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
 
98
 
 
99
(**********)
 
100
Axiom
 
101
  Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
 
102
 
 
103
Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
 
104
 
 
105
(**********************************************************) 
 
106
(** *    Injection from N to R                            *)
 
107
(**********************************************************)
 
108
 
 
109
(**********)
 
110
Boxed Fixpoint INR (n:nat) : R :=
 
111
  match n with
 
112
  | O => 0
 
113
  | S O => 1
 
114
  | S n => INR n + 1
 
115
  end.  
 
116
Arguments Scope INR [nat_scope].
 
117
 
 
118
 
 
119
(**********************************************************) 
 
120
(** *    Injection from [Z] to [R]                        *)
 
121
(**********************************************************)
 
122
 
 
123
(**********)
 
124
Definition IZR (z:Z) : R :=
 
125
  match z with
 
126
  | Z0 => 0
 
127
  | Zpos n => INR (nat_of_P n)
 
128
  | Zneg n => - INR (nat_of_P n)
 
129
  end.  
 
130
Arguments Scope IZR [Z_scope].
 
131
 
 
132
(**********************************************************)
 
133
(** *    [R] Archimedean                                  *)
 
134
(**********************************************************)
 
135
 
 
136
(**********)
 
137
Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
 
138
 
 
139
(**********************************************************)
 
140
(** *    [R] Complete                                     *)
 
141
(**********************************************************)
 
142
 
 
143
(**********)
 
144
Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.
 
145
 
 
146
(**********)
 
147
Definition bound (E:R -> Prop) :=  exists m : R, is_upper_bound E m.
 
148
 
 
149
(**********)
 
150
Definition is_lub (E:R -> Prop) (m:R) :=
 
151
  is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
 
152
 
 
153
(**********)
 
154
Axiom
 
155
  completeness :
 
156
    forall E:R -> Prop,
 
157
      bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.