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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*********************************************************)
(** Axiomatisation of the classical reals *)
(*********************************************************)
Require Export ZArith_base.
Require Export Rdefinitions.
Local Open Scope R_scope.
(*********************************************************)
(** * Field axioms *)
(*********************************************************)
(*********************************************************)
(** ** Addition *)
(*********************************************************)
(**********)
Axiom Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
Hint Resolve Rplus_comm: real.
(**********)
Axiom Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
Hint Resolve Rplus_assoc: real.
(**********)
Axiom Rplus_opp_r : forall r:R, r + - r = 0.
Hint Resolve Rplus_opp_r: real.
(**********)
Axiom Rplus_0_l : forall r:R, 0 + r = r.
Hint Resolve Rplus_0_l: real.
(***********************************************************)
(** ** Multiplication *)
(***********************************************************)
(**********)
Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
Hint Resolve Rmult_comm: real.
(**********)
Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
Hint Resolve Rmult_assoc: real.
(**********)
Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
Hint Resolve Rinv_l: real.
(**********)
Axiom Rmult_1_l : forall r:R, 1 * r = r.
Hint Resolve Rmult_1_l: real.
(**********)
Axiom R1_neq_R0 : 1 <> 0.
Hint Resolve R1_neq_R0: real.
(*********************************************************)
(** ** Distributivity *)
(*********************************************************)
(**********)
Axiom
Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
Hint Resolve Rmult_plus_distr_l: real.
(*********************************************************)
(** * Order axioms *)
(*********************************************************)
(*********************************************************)
(** ** Total Order *)
(*********************************************************)
(**********)
Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}.
(*********************************************************)
(** ** Lower *)
(*********************************************************)
(**********)
Axiom Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
(**********)
Axiom Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
(**********)
Axiom Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
(**********)
Axiom
Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
(**********************************************************)
(** * Injection from N to R *)
(**********************************************************)
(**********)
Fixpoint INR (n:nat) : R :=
match n with
| O => 0
| S O => 1
| S n => INR n + 1
end.
Arguments INR n%nat.
(**********************************************************)
(** * Injection from [Z] to [R] *)
(**********************************************************)
(**********)
Definition IZR (z:Z) : R :=
match z with
| Z0 => 0
| Zpos n => INR (Pos.to_nat n)
| Zneg n => - INR (Pos.to_nat n)
end.
Arguments IZR z%Z.
(**********************************************************)
(** * [R] Archimedean *)
(**********************************************************)
(**********)
Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
(**********************************************************)
(** * [R] Complete *)
(**********************************************************)
(**********)
Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.
(**********)
Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m.
(**********)
Definition is_lub (E:R -> Prop) (m:R) :=
is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
(**********)
Axiom
completeness :
forall E:R -> Prop,
bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.
|
