-
Notifications
You must be signed in to change notification settings - Fork 1
/
sg.v
232 lines (210 loc) · 5.8 KB
/
sg.v
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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
(* This code is copyrighted by its authors; it is distributed under *)
(* the terms of the LGPL license (see LICENSE and description files) *)
Require Import Reals.
Require Import Psatz.
Require Import Rbase_inegalites.
Require Import Rabsolu_complements.
Require Import Tactiques.
Definition sg (x : R) : Z :=
match total_order_T x 0 with
| inleft (left _) => (-1)%Z
| inleft (right _) => 0%Z
| inright _ => 1%Z
end.
Lemma sg_neg : forall r : R, r < 0 -> sg r = (-1)%Z.
Proof.
intros.
unfold sg in |- *.
case (total_order_T r 0).
simple destruct s; intro.
auto.
lra.
intro; lra.
Qed.
Hint Resolve sg_neg: real.
Lemma sg_pos : forall r : R, 0 < r -> sg r = 1%Z.
Proof.
intros.
unfold sg in |- *.
case (total_order_T r 0).
simple destruct s; intro.
lra.
lra.
intro; auto.
Qed.
Hint Resolve sg_pos: real.
Lemma sg_nul : forall r : R, 0 = r -> sg r = 0%Z.
Proof.
intros.
unfold sg in |- *.
case (total_order_T r 0).
simple destruct s; intro.
lra.
auto.
intro; lra.
Qed.
Hint Resolve sg_nul: real.
Lemma sg_mult : forall x y : R, sg (x * y) = (sg x * sg y)%Z.
Proof.
intros.
cut (0 < x \/ 0 = x \/ 0 > x); [ intro | apply Rtotal_order ].
elim H; clear H.
intro; replace (sg x) with 1%Z;
[ rewrite Zmult_comm; rewrite Zmult_1_r
| symmetry in |- *; apply sg_pos; auto ].
cut (0 < y \/ 0 = y \/ 0 > y); [ intro | apply Rtotal_order ].
elim H0; clear H0.
intro; replace (sg y) with 1%Z;
[ apply sg_pos | symmetry in |- *; apply sg_pos; auto ].
apply Rmult_lt_0_compat; [ auto | auto ].
intro.
elim H0.
intro; replace (sg y) with 0%Z;
[ apply sg_nul; symmetry in |- *; apply Rmult_eq_0_compat; right; auto
| symmetry in |- *; apply sg_nul; auto ].
intro; replace (sg y) with (-1)%Z;
[ apply sg_neg | symmetry in |- *; apply sg_neg; auto ].
rewrite Rmult_comm; apply Rlt_sub_O; rewrite Rminus_0_l;
rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_lt_0_compat;
[ auto with real | auto ].
intro.
elim H; clear H.
intro; replace (sg x) with 0%Z;
[ rewrite Zmult_comm; rewrite <- Zmult_0_r_reverse; apply sg_nul;
rewrite <- H; auto with real
| symmetry in |- *; apply sg_nul; auto ].
intro; replace (sg x) with (- (1))%Z;
[ rewrite <- Zopp_mult_distr_l; rewrite Zmult_comm; rewrite Zmult_1_r
| symmetry in |- *; apply sg_neg; auto ].
cut (0 < y \/ 0 = y \/ 0 > y); [ intro | apply Rtotal_order ].
elim H0; clear H0.
intro; replace (sg y) with 1%Z;
[ apply sg_neg | symmetry in |- *; apply sg_pos; auto ].
apply Rlt_sub_O; rewrite Rminus_0_l; rewrite <- Ropp_mult_distr_l_reverse;
apply Rmult_lt_0_compat; [ auto with real | auto ].
intro.
elim H0.
intro; replace (sg y) with 0%Z;
[ apply sg_nul; symmetry in |- *; apply Rmult_eq_0_compat; right; auto
| symmetry in |- *; apply sg_nul; auto ].
intro; replace (sg y) with (-1)%Z;
[ apply sg_pos | symmetry in |- *; apply sg_neg; auto ].
apply Rmult_lt_pos_bis; [ auto | auto ].
Qed.
Hint Resolve sg_mult: real.
Lemma sg_mult_neg :
forall x y : R, 0 < x /\ y < 0 \/ 0 < y /\ x < 0 -> (sg x * sg y)%Z = (-1)%Z.
Proof.
intros.
rewrite <- sg_mult.
elim H; intro.
apply sg_neg.
elim H0; intros.
apply Rmult_lt_reg_l with (/ x).
apply Rinv_0_lt_compat; auto.
rewrite <- Rmult_assoc.
replace (/ x * x) with 1.
rewrite Rmult_comm; rewrite Rmult_1_r.
rewrite Rmult_0_r; auto.
apply Rinv_l_sym; apply Rgt_not_eq; auto.
apply sg_neg.
elim H0.
intros.
rewrite Rmult_comm; apply Rmult_lt_reg_l with (/ y).
apply Rinv_0_lt_compat.
auto.
rewrite <- Rmult_assoc.
replace (/ y * y) with 1.
rewrite Rmult_comm; rewrite Rmult_1_r.
rewrite Rmult_0_r; auto.
apply Rinv_l_sym; apply Rgt_not_eq; auto.
Qed.
Hint Resolve sg_mult_neg: real.
Lemma plus_tard :
forall x y : R,
0 < Rabs x ->
0 < Rabs y -> (sg x * sg y)%Z = (-1)%Z \/ (sg x * sg y)%Z = 1%Z.
Proof.
intros.
cut
(0 < x * y \/ 0 > x * y -> (sg x * sg y)%Z = (-1)%Z \/ (sg x * sg y)%Z = 1%Z).
intro; apply H1.
apply Rdichotomy.
apply Rabsolu_complements.Rabsolu_not_eq.
rewrite Rabs_mult.
apply Rmult_integral_contrapositive.
split;
[ apply Rgt_not_eq; auto with real | apply Rgt_not_eq; auto with real ].
intros.
elim H1.
intro.
right.
rewrite <- sg_mult.
apply sg_pos; auto.
intro.
left.
rewrite <- sg_mult.
apply sg_neg; auto.
Qed.
Hint Resolve plus_tard: real.
Lemma sg_sqr : forall r : R, r <> 0 -> (sg r * sg r)%Z = 1%Z.
Proof.
intros.
cut (r <> 0 -> r < 0 \/ r > 0); [ intros | apply Rdichotomy ].
elim H0; clear H0.
intro; replace (sg r) with (-1)%Z;
[ ring | symmetry in |- *; apply sg_neg; auto ].
intro; replace (sg r) with 1%Z;
[ ring | symmetry in |- *; apply sg_pos; auto ].
auto.
Qed.
Hint Resolve sg_sqr: real.
Lemma Rabsolu_sg : forall r : R, IZR (sg r) * r = Rabs r.
Proof.
intro.
cut (0 < r \/ 0 = r \/ 0 > r); [ intro | apply Rtotal_order ].
elim H.
intro; replace (sg r) with 1%Z;
[ idtac | symmetry in |- *; apply sg_pos; auto ].
simpl in |- *; rewrite Rmult_1_l.
symmetry in |- *; apply Rabs_right.
apply Rgt_ge; auto with real.
intro.
elim H0.
intro.
rewrite <- H1.
rewrite Rabs_R0.
apply Rmult_0_r.
intro; replace (sg r) with (-(1))%Z;
[ idtac | symmetry; apply sg_neg; auto ].
rewrite Ropp_Ropp_IZR.
rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l.
symmetry; apply Rabs_left.
auto.
Qed.
Hint Resolve Rabsolu_sg: real.
Lemma Rabsolu_sg_bis : forall r : R, r = IZR (sg r) * Rabs r.
Proof.
intros.
cut (0 < r \/ 0 = r \/ 0 > r); [ intro | apply Rtotal_order ].
elim H.
intro; replace (sg r) with 1%Z;
[ idtac | symmetry in |- *; apply sg_pos; auto ].
simpl in |- *; rewrite Rmult_1_l.
symmetry in |- *; apply Rabs_right.
apply Rgt_ge; auto with real.
intro.
elim H0.
intro.
rewrite <- H1.
rewrite Rabs_R0.
symmetry in |- *; apply Rmult_0_r.
intro; replace (sg r) with (-(1))%Z;
[ idtac | symmetry; apply sg_neg; auto ].
rewrite Ropp_Ropp_IZR.
rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l.
pattern r at 1 in |- *; RingReplace r (- - r).
apply Ropp_eq_compat; symmetry in |- *; apply Rabs_left.
auto.
Qed.
Hint Resolve Rabsolu_sg_bis: real.