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
(* Evgeny Makarov, INRIA, 2007 *)
9
(************************************************************************)
11
Require Import Setoid.
14
(** Generic properties of ordered rings on a setoid equality *)
16
Set Implicit Arguments.
18
Module Import OrderedRingSyntax.
21
Reserved Notation "x ~= y" (at level 70, no associativity).
22
Reserved Notation "x [=] y" (at level 70, no associativity).
23
Reserved Notation "x [~=] y" (at level 70, no associativity).
24
Reserved Notation "x [<] y" (at level 70, no associativity).
25
Reserved Notation "x [<=] y" (at level 70, no associativity).
26
End OrderedRingSyntax.
31
Variable (rO rI : R) (rplus rtimes rminus: R -> R -> R) (ropp : R -> R).
32
Variable req rle rlt : R -> R -> Prop.
35
Notation "x + y" := (rplus x y).
36
Notation "x * y " := (rtimes x y).
37
Notation "x - y " := (rminus x y).
38
Notation "- x" := (ropp x).
39
Notation "x == y" := (req x y).
40
Notation "x ~= y" := (~ req x y).
41
Notation "x <= y" := (rle x y).
42
Notation "x < y" := (rlt x y).
44
Record SOR : Type := mk_SOR_theory {
45
SORsetoid : Setoid_Theory R req;
46
SORplus_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2;
47
SORtimes_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2;
48
SORopp_wd : forall x1 x2, x1 == x2 -> -x1 == -x2;
49
SORle_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 <= y1 <-> x2 <= y2);
50
SORlt_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 < y1 <-> x2 < y2);
51
SORrt : ring_theory rO rI rplus rtimes rminus ropp req;
52
SORle_refl : forall n : R, n <= n;
53
SORle_antisymm : forall n m : R, n <= m -> m <= n -> n == m;
54
SORle_trans : forall n m p : R, n <= m -> m <= p -> n <= p;
55
SORlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m;
56
SORlt_trichotomy : forall n m : R, n < m \/ n == m \/ m < n;
57
SORplus_le_mono_l : forall n m p : R, n <= m -> p + n <= p + m;
58
SORtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m;
62
(* We cannot use Relation_Definitions.order.ord_antisym and
63
Relations_1.Antisymmetric because they refer to Leibniz equality *)
67
Section STRICT_ORDERED_RING.
70
Variable (rO rI : R) (rplus rtimes rminus: R -> R -> R) (ropp : R -> R).
71
Variable req rle rlt : R -> R -> Prop.
73
Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
77
Notation "x + y" := (rplus x y).
78
Notation "x * y " := (rtimes x y).
79
Notation "x - y " := (rminus x y).
80
Notation "- x" := (ropp x).
81
Notation "x == y" := (req x y).
82
Notation "x ~= y" := (~ req x y).
83
Notation "x <= y" := (rle x y).
84
Notation "x < y" := (rlt x y).
88
reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _ )
89
symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ )
90
transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ )
94
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
96
exact sor.(SORplus_wd).
98
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
100
exact sor.(SORtimes_wd).
102
Add Morphism ropp with signature req ==> req as ropp_morph.
104
exact sor.(SORopp_wd).
106
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
108
exact sor.(SORle_wd).
110
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
112
exact sor.(SORlt_wd).
115
Add Ring SOR : sor.(SORrt).
117
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
119
intros x1 x2 H1 y1 y2 H2.
120
rewrite (sor.(SORrt).(Rsub_def) x1 y1).
121
rewrite (sor.(SORrt).(Rsub_def) x2 y2).
122
rewrite H1; now rewrite H2.
125
Theorem Rneq_symm : forall n m : R, n ~= m -> m ~= n.
127
intros n m H1 H2; rewrite H2 in H1; now apply H1.
130
(* Propeties of plus, minus and opp *)
132
Theorem Rplus_0_l : forall n : R, 0 + n == n.
137
Theorem Rplus_0_r : forall n : R, n + 0 == n.
142
Theorem Rtimes_0_r : forall n : R, n * 0 == 0.
147
Theorem Rplus_comm : forall n m : R, n + m == m + n.
152
Theorem Rtimes_0_l : forall n : R, 0 * n == 0.
157
Theorem Rtimes_comm : forall n m : R, n * m == m * n.
162
Theorem Rminus_eq_0 : forall n m : R, n - m == 0 <-> n == m.
165
split; intro H. setoid_replace n with ((n - m) + m) by ring. rewrite H.
166
now rewrite Rplus_0_l.
170
Theorem Rplus_cancel_l : forall n m p : R, p + n == p + m <-> n == m.
172
intros n m p; split; intro H.
173
setoid_replace n with (- p + (p + n)) by ring.
174
setoid_replace m with (- p + (p + m)) by ring. now rewrite H.
180
Theorem Rle_refl : forall n : R, n <= n.
181
Proof sor.(SORle_refl).
183
Theorem Rle_antisymm : forall n m : R, n <= m -> m <= n -> n == m.
184
Proof sor.(SORle_antisymm).
186
Theorem Rle_trans : forall n m p : R, n <= m -> m <= p -> n <= p.
187
Proof sor.(SORle_trans).
189
Theorem Rlt_trichotomy : forall n m : R, n < m \/ n == m \/ m < n.
190
Proof sor.(SORlt_trichotomy).
192
Theorem Rlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m.
193
Proof sor.(SORlt_le_neq).
195
Theorem Rneq_0_1 : 0 ~= 1.
196
Proof sor.(SORneq_0_1).
198
Theorem Req_em : forall n m : R, n == m \/ n ~= m.
200
intros n m. destruct (Rlt_trichotomy n m) as [H | [H | H]]; try rewrite Rlt_le_neq in H.
201
right; now destruct H.
203
right; apply Rneq_symm; now destruct H.
206
Theorem Req_dne : forall n m : R, ~ ~ n == m <-> n == m.
208
intros n m; destruct (Req_em n m) as [H | H].
210
split. intro H1; false_hyp H H1. auto.
213
Theorem Rle_lt_eq : forall n m : R, n <= m <-> n < m \/ n == m.
215
intros n m; rewrite Rlt_le_neq.
216
split; [intro H | intros [[H1 H2] | H]].
217
destruct (Req_em n m) as [H1 | H1]. now right. left; now split.
219
rewrite H; apply Rle_refl.
222
Ltac le_less := rewrite Rle_lt_eq; left; try assumption.
223
Ltac le_equal := rewrite Rle_lt_eq; right; try reflexivity; try assumption.
224
Ltac le_elim H := rewrite Rle_lt_eq in H; destruct H as [H | H].
226
Theorem Rlt_trans : forall n m p : R, n < m -> m < p -> n < p.
228
intros n m p; repeat rewrite Rlt_le_neq; intros [H1 H2] [H3 H4]; split.
229
now apply Rle_trans with m.
230
intro H. rewrite H in H1. pose proof (Rle_antisymm H3 H1). now apply H4.
233
Theorem Rle_lt_trans : forall n m p : R, n <= m -> m < p -> n < p.
235
intros n m p H1 H2; le_elim H1.
236
now apply Rlt_trans with (m := m). now rewrite H1.
239
Theorem Rlt_le_trans : forall n m p : R, n < m -> m <= p -> n < p.
241
intros n m p H1 H2; le_elim H2.
242
now apply Rlt_trans with (m := m). now rewrite <- H2.
245
Theorem Rle_gt_cases : forall n m : R, n <= m \/ m < n.
247
intros n m; destruct (Rlt_trichotomy n m) as [H | [H | H]].
248
left; now le_less. left; now le_equal. now right.
251
Theorem Rlt_neq : forall n m : R, n < m -> n ~= m.
253
intros n m; rewrite Rlt_le_neq; now intros [_ H].
256
Theorem Rle_ngt : forall n m : R, n <= m <-> ~ m < n.
259
intros H H1; assert (H2 : n < n) by now apply Rle_lt_trans with m. now apply (Rlt_neq H2).
260
intro H. destruct (Rle_gt_cases n m) as [H1 | H1]. assumption. false_hyp H1 H.
263
Theorem Rlt_nge : forall n m : R, n < m <-> ~ m <= n.
266
intros H H1; assert (H2 : n < n) by now apply Rlt_le_trans with m. now apply (Rlt_neq H2).
267
intro H. destruct (Rle_gt_cases m n) as [H1 | H1]. false_hyp H1 H. assumption.
270
(* Plus, minus and order *)
272
Theorem Rplus_le_mono_l : forall n m p : R, n <= m <-> p + n <= p + m.
275
apply sor.(SORplus_le_mono_l).
276
intro H. apply (sor.(SORplus_le_mono_l) (p + n) (p + m) (- p)) in H.
277
setoid_replace (- p + (p + n)) with n in H by ring.
278
setoid_replace (- p + (p + m)) with m in H by ring. assumption.
281
Theorem Rplus_le_mono_r : forall n m p : R, n <= m <-> n + p <= m + p.
283
intros n m p; rewrite (Rplus_comm n p); rewrite (Rplus_comm m p).
284
apply Rplus_le_mono_l.
287
Theorem Rplus_lt_mono_l : forall n m p : R, n < m <-> p + n < p + m.
289
intros n m p; do 2 rewrite Rlt_le_neq. rewrite Rplus_cancel_l.
290
now rewrite <- Rplus_le_mono_l.
293
Theorem Rplus_lt_mono_r : forall n m p : R, n < m <-> n + p < m + p.
296
rewrite (Rplus_comm n p); rewrite (Rplus_comm m p); apply Rplus_lt_mono_l.
299
Theorem Rplus_lt_mono : forall n m p q : R, n < m -> p < q -> n + p < m + q.
301
intros n m p q H1 H2.
302
apply Rlt_trans with (m + p); [now apply -> Rplus_lt_mono_r | now apply -> Rplus_lt_mono_l].
305
Theorem Rplus_le_mono : forall n m p q : R, n <= m -> p <= q -> n + p <= m + q.
307
intros n m p q H1 H2.
308
apply Rle_trans with (m + p); [now apply -> Rplus_le_mono_r | now apply -> Rplus_le_mono_l].
311
Theorem Rplus_lt_le_mono : forall n m p q : R, n < m -> p <= q -> n + p < m + q.
313
intros n m p q H1 H2.
314
apply Rlt_le_trans with (m + p); [now apply -> Rplus_lt_mono_r | now apply -> Rplus_le_mono_l].
317
Theorem Rplus_le_lt_mono : forall n m p q : R, n <= m -> p < q -> n + p < m + q.
319
intros n m p q H1 H2.
320
apply Rle_lt_trans with (m + p); [now apply -> Rplus_le_mono_r | now apply -> Rplus_lt_mono_l].
323
Theorem Rplus_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n + m.
325
intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_lt_mono.
328
Theorem Rplus_pos_nonneg : forall n m : R, 0 < n -> 0 <= m -> 0 < n + m.
330
intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_lt_le_mono.
333
Theorem Rplus_nonneg_pos : forall n m : R, 0 <= n -> 0 < m -> 0 < n + m.
335
intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_le_lt_mono.
338
Theorem Rplus_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n + m.
340
intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_le_mono.
343
Theorem Rle_le_minus : forall n m : R, n <= m <-> 0 <= m - n.
345
intros n m. rewrite (@Rplus_le_mono_r n m (- n)).
346
setoid_replace (n + - n) with 0 by ring.
347
now setoid_replace (m + - n) with (m - n) by ring.
350
Theorem Rlt_lt_minus : forall n m : R, n < m <-> 0 < m - n.
352
intros n m. rewrite (@Rplus_lt_mono_r n m (- n)).
353
setoid_replace (n + - n) with 0 by ring.
354
now setoid_replace (m + - n) with (m - n) by ring.
357
Theorem Ropp_lt_mono : forall n m : R, n < m <-> - m < - n.
359
intros n m. split; intro H.
360
apply -> (@Rplus_lt_mono_l n m (- n - m)) in H.
361
setoid_replace (- n - m + n) with (- m) in H by ring.
362
now setoid_replace (- n - m + m) with (- n) in H by ring.
363
apply -> (@Rplus_lt_mono_l (- m) (- n) (n + m)) in H.
364
setoid_replace (n + m + - m) with n in H by ring.
365
now setoid_replace (n + m + - n) with m in H by ring.
368
Theorem Ropp_pos_neg : forall n : R, 0 < - n <-> n < 0.
370
intro n; rewrite (Ropp_lt_mono n 0). now setoid_replace (- 0) with 0 by ring.
373
(* Times and order *)
375
Theorem Rtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m.
376
Proof sor.(SORtimes_pos_pos).
378
Theorem Rtimes_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n * m.
381
le_elim H1. le_elim H2.
382
le_less; now apply Rtimes_pos_pos.
383
rewrite <- H2; rewrite Rtimes_0_r; le_equal.
384
rewrite <- H1; rewrite Rtimes_0_l; le_equal.
387
Theorem Rtimes_pos_neg : forall n m : R, 0 < n -> m < 0 -> n * m < 0.
389
intros n m H1 H2. apply -> Ropp_pos_neg.
390
setoid_replace (- (n * m)) with (n * (- m)) by ring.
391
apply Rtimes_pos_pos. assumption. now apply <- Ropp_pos_neg.
394
Theorem Rtimes_neg_neg : forall n m : R, n < 0 -> m < 0 -> 0 < n * m.
397
setoid_replace (n * m) with ((- n) * (- m)) by ring.
398
apply Rtimes_pos_pos; now apply <- Ropp_pos_neg.
401
Theorem Rtimes_square_nonneg : forall n : R, 0 <= n * n.
403
intro n; destruct (Rlt_trichotomy 0 n) as [H | [H | H]].
404
le_less; now apply Rtimes_pos_pos.
405
rewrite <- H, Rtimes_0_l; le_equal.
406
le_less; now apply Rtimes_neg_neg.
409
Theorem Rtimes_neq_0 : forall n m : R, n ~= 0 /\ m ~= 0 -> n * m ~= 0.
412
destruct (Rlt_trichotomy n 0) as [H3 | [H3 | H3]];
413
destruct (Rlt_trichotomy m 0) as [H4 | [H4 | H4]];
414
try (false_hyp H3 H1); try (false_hyp H4 H2).
415
apply Rneq_symm. apply Rlt_neq. now apply Rtimes_neg_neg.
416
apply Rlt_neq. rewrite Rtimes_comm. now apply Rtimes_pos_neg.
417
apply Rlt_neq. now apply Rtimes_pos_neg.
418
apply Rneq_symm. apply Rlt_neq. now apply Rtimes_pos_pos.
421
(* The following theorems are used to build a morphism from Z to R and
422
prove its properties in ZCoeff.v. They are not used in RingMicromega.v. *)
424
(* Surprisingly, multilication is needed to prove the following theorem *)
426
Theorem Ropp_neg_pos : forall n : R, - n < 0 <-> 0 < n.
428
intro n; setoid_replace n with (- - n) by ring. rewrite Ropp_pos_neg.
429
now setoid_replace (- - n) with n by ring.
432
Theorem Rlt_0_1 : 0 < 1.
434
apply <- Rlt_le_neq. split.
435
setoid_replace 1 with (1 * 1) by ring. apply Rtimes_square_nonneg.
439
Theorem Rlt_succ_r : forall n : R, n < 1 + n.
441
intro n. rewrite <- (Rplus_0_l n); setoid_replace (1 + (0 + n)) with (1 + n) by ring.
442
apply -> Rplus_lt_mono_r. apply Rlt_0_1.
445
Theorem Rlt_lt_succ : forall n m : R, n < m -> n < 1 + m.
447
intros n m H; apply Rlt_trans with m. assumption. apply Rlt_succ_r.
450
(*Theorem Rtimes_lt_mono_pos_l : forall n m p : R, 0 < p -> n < m -> p * n < p * m.
452
intros n m p H1 H2. apply <- Rlt_lt_minus.
453
setoid_replace (p * m - p * n) with (p * (m - n)) by ring.
454
apply Rtimes_pos_pos. assumption. now apply -> Rlt_lt_minus.
457
End STRICT_ORDERED_RING.
added
removed
contrib/micromega/OrderedRing.v
