1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields".
19 (* $Id: COrdFields.v,v 1.6 2004/04/23 10:00:52 lcf Exp $ *)
21 (*#* printing [<] %\ensuremath<% #<# *)
23 (*#* printing [<=] %\ensuremath{\leq}% #≤# *)
25 (*#* printing [>] %\ensuremath>% #># *)
27 (*#* printing OneNZ %\ensuremath{\mathbf1}% #1# *)
29 (*#* printing TwoNZ %\ensuremath{\mathbf2}% #2# *)
31 (*#* printing ThreeNZ %\ensuremath{\mathbf3}% #3# *)
33 (*#* printing FourNZ %\ensuremath{\mathbf4}% #4# *)
35 (*#* printing SixNZ %\ensuremath{\mathbf6}% #6# *)
37 (*#* printing EightNZ %\ensuremath{\mathbf8}% #8# *)
39 (*#* printing NineNZ %\ensuremath{\mathbf9}% #9# *)
41 (*#* printing TwelveNZ %\ensuremath{\mathbf{12}}% #12# *)
43 (*#* printing SixteenNZ %\ensuremath{\mathbf{16}}% #16# *)
45 (*#* printing EighteenNZ %\ensuremath{\mathbf{18}}% #18# *)
47 (*#* printing TwentyFourNZ %\ensuremath{\mathbf{24}}% #24# *)
49 (*#* printing FortyEightNZ %\ensuremath{\mathbf{48}}% #48# *)
59 ** Definition of the notion of ordered field
64 inline cic:/CoRN/algebra/COrdFields/strictorder.ind.
67 Implicit Arguments strictorder [A].
71 Implicit Arguments Build_strictorder [A R].
75 Implicit Arguments so_trans [A R].
79 Implicit Arguments so_asym [A R].
82 inline cic:/CoRN/algebra/COrdFields/is_COrdField.ind.
84 inline cic:/CoRN/algebra/COrdFields/COrdField.ind.
87 %\begin{nameconvention}%
88 In the names of lemmas, [ [<] ] is written as [less] and "[Zero [<] ]"
90 %\end{nameconvention}%
94 Implicit Arguments cof_less [c].
97 inline cic:/CoRN/algebra/COrdFields/greater.con.
100 Implicit Arguments greater [F].
106 Less or equal is defined as ``not greater than''.
109 inline cic:/CoRN/algebra/COrdFields/leEq.con.
112 %\begin{nameconvention}%
113 In the names of lemmas, [ [<=] ] is written as [leEq] and
114 [Zero [<=] ] is written as [nonneg].
115 %\end{nameconvention}%
119 Implicit Arguments leEq [F].
123 Section COrdField_axioms.
127 ** Ordered field axioms
133 inline cic:/CoRN/algebra/COrdFields/F.var.
135 inline cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con.
137 inline cic:/CoRN/algebra/COrdFields/less_strorder.con.
139 inline cic:/CoRN/algebra/COrdFields/less_transitive_unfolded.con.
141 inline cic:/CoRN/algebra/COrdFields/less_antisymmetric_unfolded.con.
143 inline cic:/CoRN/algebra/COrdFields/less_irreflexive.con.
145 inline cic:/CoRN/algebra/COrdFields/less_irreflexive_unfolded.con.
147 inline cic:/CoRN/algebra/COrdFields/plus_resp_less_rht.con.
149 inline cic:/CoRN/algebra/COrdFields/mult_resp_pos.con.
151 inline cic:/CoRN/algebra/COrdFields/less_conf_ap.con.
153 inline cic:/CoRN/algebra/COrdFields/less_wdr.con.
155 inline cic:/CoRN/algebra/COrdFields/less_wdl.con.
158 End COrdField_axioms.
162 Declare Left Step less_wdl.
166 Declare Right Step less_wdr.
170 Section OrdField_basics.
179 Let in the rest of this section (and all subsections)
180 [R] be an ordered field
184 inline cic:/CoRN/algebra/COrdFields/R.var.
186 inline cic:/CoRN/algebra/COrdFields/less_imp_ap.con.
188 inline cic:/CoRN/algebra/COrdFields/Greater_imp_ap.con.
190 inline cic:/CoRN/algebra/COrdFields/ap_imp_less.con.
193 Now properties which can be derived.
196 inline cic:/CoRN/algebra/COrdFields/less_cotransitive.con.
198 inline cic:/CoRN/algebra/COrdFields/less_cotransitive_unfolded.con.
200 inline cic:/CoRN/algebra/COrdFields/pos_ap_zero.con.
202 (* Main characterization of less *)
204 inline cic:/CoRN/algebra/COrdFields/leEq_not_eq.con.
210 (*#**********************************)
213 Section Basic_Properties_of_leEq.
216 (*#**********************************)
218 (*#* ** Basic properties of [ [<=] ]
221 inline cic:/CoRN/algebra/COrdFields/R.var.
223 inline cic:/CoRN/algebra/COrdFields/leEq_wdr.con.
225 inline cic:/CoRN/algebra/COrdFields/leEq_wdl.con.
227 inline cic:/CoRN/algebra/COrdFields/leEq_reflexive.con.
230 Declare Left Step leEq_wdl.
234 Declare Right Step leEq_wdr.
237 inline cic:/CoRN/algebra/COrdFields/eq_imp_leEq.con.
239 inline cic:/CoRN/algebra/COrdFields/leEq_imp_eq.con.
241 inline cic:/CoRN/algebra/COrdFields/lt_equiv_imp_eq.con.
243 inline cic:/CoRN/algebra/COrdFields/less_leEq_trans.con.
245 inline cic:/CoRN/algebra/COrdFields/leEq_less_trans.con.
247 inline cic:/CoRN/algebra/COrdFields/leEq_transitive.con.
249 inline cic:/CoRN/algebra/COrdFields/less_leEq.con.
252 End Basic_Properties_of_leEq.
256 Declare Left Step leEq_wdl.
260 Declare Right Step leEq_wdr.
264 Section infinity_of_cordfields.
268 ** Infinity of ordered fields
270 In an ordered field we have that [One[+]One] and
271 [One[+]One[+]One] and so on are all apart from zero.
272 We first show this, so that we can define [TwoNZ], [ThreeNZ]
273 and so on. These are elements of [NonZeros], so that we can write
277 inline cic:/CoRN/algebra/COrdFields/R.var.
279 inline cic:/CoRN/algebra/COrdFields/pos_one.con.
281 inline cic:/CoRN/algebra/COrdFields/nring_less_succ.con.
283 inline cic:/CoRN/algebra/COrdFields/nring_less.con.
285 inline cic:/CoRN/algebra/COrdFields/nring_leEq.con.
287 inline cic:/CoRN/algebra/COrdFields/nring_apart.con.
289 inline cic:/CoRN/algebra/COrdFields/nring_ap_zero.con.
291 inline cic:/CoRN/algebra/COrdFields/nring_ap_zero'.con.
293 inline cic:/CoRN/algebra/COrdFields/nring_ap_zero_imp.con.
295 inline cic:/CoRN/algebra/COrdFields/Snring.con.
301 inline cic:/CoRN/algebra/COrdFields/pos_Snring.con.
303 inline cic:/CoRN/algebra/COrdFields/nringS_ap_zero.con.
305 inline cic:/CoRN/algebra/COrdFields/nring_fac_ap_zero.con.
316 *** Properties of one up to four
317 %\begin{nameconvention}%
318 In the names of lemmas, we denote the numbers 0,1,2,3,4 and so on, by
319 [zero], [one], [two] etc.
320 %\end{nameconvention}%
323 inline cic:/CoRN/algebra/COrdFields/less_plusOne.con.
325 inline cic:/CoRN/algebra/COrdFields/zero_lt_posplus1.con.
327 inline cic:/CoRN/algebra/COrdFields/plus_one_ext_less.con.
329 inline cic:/CoRN/algebra/COrdFields/one_less_two.con.
331 inline cic:/CoRN/algebra/COrdFields/two_less_three.con.
333 inline cic:/CoRN/algebra/COrdFields/three_less_four.con.
335 inline cic:/CoRN/algebra/COrdFields/pos_two.con.
337 inline cic:/CoRN/algebra/COrdFields/one_less_three.con.
339 inline cic:/CoRN/algebra/COrdFields/two_less_four.con.
341 inline cic:/CoRN/algebra/COrdFields/pos_three.con.
343 inline cic:/CoRN/algebra/COrdFields/one_less_four.con.
345 inline cic:/CoRN/algebra/COrdFields/pos_four.con.
347 inline cic:/CoRN/algebra/COrdFields/two_ap_zero.con.
349 inline cic:/CoRN/algebra/COrdFields/three_ap_zero.con.
351 inline cic:/CoRN/algebra/COrdFields/four_ap_zero.con.
358 Section More_than_four.
361 (*#* *** Properties of some other numbers *)
363 inline cic:/CoRN/algebra/COrdFields/pos_six.con.
365 inline cic:/CoRN/algebra/COrdFields/pos_eight.con.
367 inline cic:/CoRN/algebra/COrdFields/pos_nine.con.
369 inline cic:/CoRN/algebra/COrdFields/pos_twelve.con.
371 inline cic:/CoRN/algebra/COrdFields/pos_sixteen.con.
373 inline cic:/CoRN/algebra/COrdFields/pos_eighteen.con.
375 inline cic:/CoRN/algebra/COrdFields/pos_twentyfour.con.
377 inline cic:/CoRN/algebra/COrdFields/pos_fortyeight.con.
379 inline cic:/CoRN/algebra/COrdFields/six_ap_zero.con.
381 inline cic:/CoRN/algebra/COrdFields/eight_ap_zero.con.
383 inline cic:/CoRN/algebra/COrdFields/nine_ap_zero.con.
385 inline cic:/CoRN/algebra/COrdFields/twelve_ap_zero.con.
387 inline cic:/CoRN/algebra/COrdFields/sixteen_ap_zero.con.
389 inline cic:/CoRN/algebra/COrdFields/eighteen_ap_zero.con.
391 inline cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con.
393 inline cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con.
400 End infinity_of_cordfields.
404 Declare Left Step leEq_wdl.
408 Declare Right Step leEq_wdr.
412 Section consequences_of_infinity.
416 *** Consequences of infinity
419 inline cic:/CoRN/algebra/COrdFields/F.var.
421 inline cic:/CoRN/algebra/COrdFields/square_eq.con.
424 Ordered fields have characteristic zero.
427 inline cic:/CoRN/algebra/COrdFields/char0_OrdField.con.
430 End consequences_of_infinity.
433 (*#**********************************)
436 Section Properties_of_Ordering.
439 (*#**********************************)
442 ** Properties of [[<]]
445 inline cic:/CoRN/algebra/COrdFields/R.var.
448 We do not use a special predicate for positivity,
449 (e.g.%\% [PosP]), but just write [Zero [<] x].
450 Reasons: it is more natural; in ordinary mathematics we also write [Zero [<] x]
460 *** Addition and subtraction%\label{section:less_plus_minus}%
464 inline cic:/CoRN/algebra/COrdFields/plus_resp_less_lft.con.
466 inline cic:/CoRN/algebra/COrdFields/inv_resp_less.con.
469 Transparent cg_minus.
472 inline cic:/CoRN/algebra/COrdFields/minus_resp_less.con.
475 Transparent cg_minus.
478 inline cic:/CoRN/algebra/COrdFields/minus_resp_less_rht.con.
480 inline cic:/CoRN/algebra/COrdFields/plus_resp_less_both.con.
483 For versions of [plus_resp_less_both] where one [ [<] ] in the
484 assumption is replaced by [ [<=] ]%, see
485 Section~\ref{section:leEq-plus-minus}%.
490 inline cic:/CoRN/algebra/COrdFields/plus_cancel_less.con.
492 inline cic:/CoRN/algebra/COrdFields/inv_cancel_less.con.
496 Lemmas where an operation is transformed into the inverse operation on
497 the other side of an inequality are called laws for shifting.
498 %\begin{nameconvention}%
499 The names of laws for shifting start with [shift_], and then come
500 the operation and the inequality, in the order in which they occur in the
502 If the shifted operand changes sides w.r.t.%\% the operation and its inverse,
503 the name gets a prime.
504 %\end{nameconvention}%
506 It would be nicer to write the laws for shifting as bi-implications,
507 However, it is impractical to use these in
508 Coq%(see the Coq shortcoming in Section~\ref{section:setoid-basics})%.
511 inline cic:/CoRN/algebra/COrdFields/shift_less_plus.con.
513 inline cic:/CoRN/algebra/COrdFields/shift_less_plus'.con.
515 inline cic:/CoRN/algebra/COrdFields/shift_less_minus.con.
517 inline cic:/CoRN/algebra/COrdFields/shift_less_minus'.con.
519 inline cic:/CoRN/algebra/COrdFields/shift_plus_less.con.
521 inline cic:/CoRN/algebra/COrdFields/shift_plus_less'.con.
523 inline cic:/CoRN/algebra/COrdFields/shift_minus_less.con.
525 inline cic:/CoRN/algebra/COrdFields/shift_minus_less'.con.
528 Some special cases of laws for shifting.
531 inline cic:/CoRN/algebra/COrdFields/shift_zero_less_minus.con.
533 inline cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con.
535 inline cic:/CoRN/algebra/COrdFields/qltone.con.
542 Section multiplication.
546 *** Multiplication and division
547 By Convention%~\ref{convention:div-form}%
548 in CFields% (Section~\ref{section:fields})%, we often have redundant premises
549 in lemmas. E.g.%\% the informal statement
550 ``for all [x,y : R] with [Zero [<] x] and [Zero [<] y]
551 we have [Zero [<] y[/]x]''
552 is formalized as follows.
554 forall (x y : R) x_, (Zero [<] x) -> (Zero [<] y) -> (Zero [<] y[/]x[//]H)
556 We do this to keep it easy to use such lemmas.
560 inline cic:/CoRN/algebra/COrdFields/mult_resp_less.con.
562 inline cic:/CoRN/algebra/COrdFields/recip_resp_pos.con.
564 inline cic:/CoRN/algebra/COrdFields/div_resp_less_rht.con.
566 inline cic:/CoRN/algebra/COrdFields/div_resp_pos.con.
568 inline cic:/CoRN/algebra/COrdFields/mult_resp_less_lft.con.
570 inline cic:/CoRN/algebra/COrdFields/mult_resp_less_both.con.
572 inline cic:/CoRN/algebra/COrdFields/recip_resp_less.con.
574 inline cic:/CoRN/algebra/COrdFields/div_resp_less.con.
576 (*#* Cancellation laws
579 inline cic:/CoRN/algebra/COrdFields/mult_cancel_less.con.
584 %For namegiving, see the Section~\ref{section:less_plus_minus}
588 inline cic:/CoRN/algebra/COrdFields/shift_div_less.con.
590 inline cic:/CoRN/algebra/COrdFields/shift_div_less'.con.
592 inline cic:/CoRN/algebra/COrdFields/shift_less_div.con.
594 inline cic:/CoRN/algebra/COrdFields/shift_less_mult.con.
596 inline cic:/CoRN/algebra/COrdFields/shift_less_mult'.con.
598 inline cic:/CoRN/algebra/COrdFields/shift_mult_less.con.
600 (*#* Other properties of multiplication and division
603 inline cic:/CoRN/algebra/COrdFields/minusOne_less.con.
605 inline cic:/CoRN/algebra/COrdFields/swap_div.con.
607 inline cic:/CoRN/algebra/COrdFields/eps_div_less_eps.con.
609 inline cic:/CoRN/algebra/COrdFields/pos_div_two.con.
611 inline cic:/CoRN/algebra/COrdFields/pos_div_two'.con.
614 Apply mult_cancel_less with (Two::R).
616 rstepl eps[+]Zero; rstepr eps[+]eps.
617 Apply plus_resp_less_lft.
622 inline cic:/CoRN/algebra/COrdFields/pos_div_three.con.
624 inline cic:/CoRN/algebra/COrdFields/pos_div_three'.con.
626 inline cic:/CoRN/algebra/COrdFields/pos_div_four.con.
628 inline cic:/CoRN/algebra/COrdFields/pos_div_four'.con.
630 inline cic:/CoRN/algebra/COrdFields/pos_div_six.con.
632 inline cic:/CoRN/algebra/COrdFields/pos_div_eight.con.
634 inline cic:/CoRN/algebra/COrdFields/pos_div_nine.con.
636 inline cic:/CoRN/algebra/COrdFields/pos_div_twelve.con.
638 inline cic:/CoRN/algebra/COrdFields/pos_div_sixteen.con.
640 inline cic:/CoRN/algebra/COrdFields/pos_div_eighteen.con.
642 inline cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con.
644 inline cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con.
655 *** Miscellaneous properties
658 inline cic:/CoRN/algebra/COrdFields/nring_pos.con.
660 inline cic:/CoRN/algebra/COrdFields/less_nring.con.
662 inline cic:/CoRN/algebra/COrdFields/pos_nring_fac.con.
664 inline cic:/CoRN/algebra/COrdFields/Smallest_less_Average.con.
666 inline cic:/CoRN/algebra/COrdFields/Average_less_Greatest.con.
668 inline cic:/CoRN/algebra/COrdFields/Sum_resp_less.con.
670 inline cic:/CoRN/algebra/COrdFields/Sumx_resp_less.con.
672 inline cic:/CoRN/algebra/COrdFields/positive_Sum_two.con.
674 inline cic:/CoRN/algebra/COrdFields/positive_Sumx.con.
676 inline cic:/CoRN/algebra/COrdFields/negative_Sumx.con.
683 End Properties_of_Ordering.