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 include "CoRN_notation.ma".
21 (* $Id: COrdFields.v,v 1.6 2004/04/23 10:00:52 lcf Exp $ *)
23 (*#* printing [<] %\ensuremath<% #<# *)
25 (*#* printing [<=] %\ensuremath{\leq}% #≤# *)
27 (*#* printing [>] %\ensuremath>% #># *)
29 (*#* printing OneNZ %\ensuremath{\mathbf1}% #1# *)
31 (*#* printing TwoNZ %\ensuremath{\mathbf2}% #2# *)
33 (*#* printing ThreeNZ %\ensuremath{\mathbf3}% #3# *)
35 (*#* printing FourNZ %\ensuremath{\mathbf4}% #4# *)
37 (*#* printing SixNZ %\ensuremath{\mathbf6}% #6# *)
39 (*#* printing EightNZ %\ensuremath{\mathbf8}% #8# *)
41 (*#* printing NineNZ %\ensuremath{\mathbf9}% #9# *)
43 (*#* printing TwelveNZ %\ensuremath{\mathbf{12}}% #12# *)
45 (*#* printing SixteenNZ %\ensuremath{\mathbf{16}}% #16# *)
47 (*#* printing EighteenNZ %\ensuremath{\mathbf{18}}% #18# *)
49 (*#* printing TwentyFourNZ %\ensuremath{\mathbf{24}}% #24# *)
51 (*#* printing FortyEightNZ %\ensuremath{\mathbf{48}}% #48# *)
53 include "tactics/FieldReflection.ma".
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".
86 coercion "cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con" 0 (* compounds *).
89 %\begin{nameconvention}%
90 In the names of lemmas, [ [<] ] is written as [less] and "[Zero [<] ]"
92 %\end{nameconvention}%
96 Implicit Arguments cof_less [c].
99 inline "cic:/CoRN/algebra/COrdFields/greater.con".
102 Implicit Arguments greater [F].
108 Less or equal is defined as ``not greater than''.
111 inline "cic:/CoRN/algebra/COrdFields/leEq.con".
114 %\begin{nameconvention}%
115 In the names of lemmas, [ [<=] ] is written as [leEq] and
116 [Zero [<=] ] is written as [nonneg].
117 %\end{nameconvention}%
121 Implicit Arguments leEq [F].
125 Section COrdField_axioms.
129 ** Ordered field axioms
135 inline "cic:/CoRN/algebra/COrdFields/F.var".
137 inline "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con".
139 inline "cic:/CoRN/algebra/COrdFields/less_strorder.con".
141 inline "cic:/CoRN/algebra/COrdFields/less_transitive_unfolded.con".
143 inline "cic:/CoRN/algebra/COrdFields/less_antisymmetric_unfolded.con".
145 inline "cic:/CoRN/algebra/COrdFields/less_irreflexive.con".
147 inline "cic:/CoRN/algebra/COrdFields/less_irreflexive_unfolded.con".
149 inline "cic:/CoRN/algebra/COrdFields/plus_resp_less_rht.con".
151 inline "cic:/CoRN/algebra/COrdFields/mult_resp_pos.con".
153 inline "cic:/CoRN/algebra/COrdFields/less_conf_ap.con".
155 inline "cic:/CoRN/algebra/COrdFields/less_wdr.con".
157 inline "cic:/CoRN/algebra/COrdFields/less_wdl.con".
160 End COrdField_axioms.
164 Declare Left Step less_wdl.
168 Declare Right Step less_wdr.
172 Section OrdField_basics.
181 Let in the rest of this section (and all subsections)
182 [R] be an ordered field
186 inline "cic:/CoRN/algebra/COrdFields/R.var".
188 inline "cic:/CoRN/algebra/COrdFields/less_imp_ap.con".
190 inline "cic:/CoRN/algebra/COrdFields/Greater_imp_ap.con".
192 inline "cic:/CoRN/algebra/COrdFields/ap_imp_less.con".
195 Now properties which can be derived.
198 inline "cic:/CoRN/algebra/COrdFields/less_cotransitive.con".
200 inline "cic:/CoRN/algebra/COrdFields/less_cotransitive_unfolded.con".
202 inline "cic:/CoRN/algebra/COrdFields/pos_ap_zero.con".
204 (* Main characterization of less *)
206 inline "cic:/CoRN/algebra/COrdFields/leEq_not_eq.con".
212 (*#**********************************)
215 Section Basic_Properties_of_leEq.
218 (*#**********************************)
220 (*#* ** Basic properties of [ [<=] ]
223 inline "cic:/CoRN/algebra/COrdFields/R.var".
225 inline "cic:/CoRN/algebra/COrdFields/leEq_wdr.con".
227 inline "cic:/CoRN/algebra/COrdFields/leEq_wdl.con".
229 inline "cic:/CoRN/algebra/COrdFields/leEq_reflexive.con".
232 Declare Left Step leEq_wdl.
236 Declare Right Step leEq_wdr.
239 inline "cic:/CoRN/algebra/COrdFields/eq_imp_leEq.con".
241 inline "cic:/CoRN/algebra/COrdFields/leEq_imp_eq.con".
243 inline "cic:/CoRN/algebra/COrdFields/lt_equiv_imp_eq.con".
245 inline "cic:/CoRN/algebra/COrdFields/less_leEq_trans.con".
247 inline "cic:/CoRN/algebra/COrdFields/leEq_less_trans.con".
249 inline "cic:/CoRN/algebra/COrdFields/leEq_transitive.con".
251 inline "cic:/CoRN/algebra/COrdFields/less_leEq.con".
254 End Basic_Properties_of_leEq.
258 Declare Left Step leEq_wdl.
262 Declare Right Step leEq_wdr.
266 Section infinity_of_cordfields.
270 ** Infinity of ordered fields
272 In an ordered field we have that [One[+]One] and
273 [One[+]One[+]One] and so on are all apart from zero.
274 We first show this, so that we can define [TwoNZ], [ThreeNZ]
275 and so on. These are elements of [NonZeros], so that we can write
279 inline "cic:/CoRN/algebra/COrdFields/R.var".
281 inline "cic:/CoRN/algebra/COrdFields/pos_one.con".
283 inline "cic:/CoRN/algebra/COrdFields/nring_less_succ.con".
285 inline "cic:/CoRN/algebra/COrdFields/nring_less.con".
287 inline "cic:/CoRN/algebra/COrdFields/nring_leEq.con".
289 inline "cic:/CoRN/algebra/COrdFields/nring_apart.con".
291 inline "cic:/CoRN/algebra/COrdFields/nring_ap_zero.con".
293 inline "cic:/CoRN/algebra/COrdFields/nring_ap_zero'.con".
295 inline "cic:/CoRN/algebra/COrdFields/nring_ap_zero_imp.con".
297 inline "cic:/CoRN/algebra/COrdFields/Snring.con".
299 include "tactics/Transparent_algebra.ma".
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".
307 include "tactics/Opaque_algebra.ma".
314 *** Properties of one up to four
315 %\begin{nameconvention}%
316 In the names of lemmas, we denote the numbers 0,1,2,3,4 and so on, by
317 [zero], [one], [two] etc.
318 %\end{nameconvention}%
321 inline "cic:/CoRN/algebra/COrdFields/less_plusOne.con".
323 inline "cic:/CoRN/algebra/COrdFields/zero_lt_posplus1.con".
325 inline "cic:/CoRN/algebra/COrdFields/plus_one_ext_less.con".
327 inline "cic:/CoRN/algebra/COrdFields/one_less_two.con".
329 inline "cic:/CoRN/algebra/COrdFields/two_less_three.con".
331 inline "cic:/CoRN/algebra/COrdFields/three_less_four.con".
333 inline "cic:/CoRN/algebra/COrdFields/pos_two.con".
335 inline "cic:/CoRN/algebra/COrdFields/one_less_three.con".
337 inline "cic:/CoRN/algebra/COrdFields/two_less_four.con".
339 inline "cic:/CoRN/algebra/COrdFields/pos_three.con".
341 inline "cic:/CoRN/algebra/COrdFields/one_less_four.con".
343 inline "cic:/CoRN/algebra/COrdFields/pos_four.con".
345 inline "cic:/CoRN/algebra/COrdFields/two_ap_zero.con".
347 inline "cic:/CoRN/algebra/COrdFields/three_ap_zero.con".
349 inline "cic:/CoRN/algebra/COrdFields/four_ap_zero.con".
356 Section More_than_four.
359 (*#* *** Properties of some other numbers *)
361 inline "cic:/CoRN/algebra/COrdFields/pos_six.con".
363 inline "cic:/CoRN/algebra/COrdFields/pos_eight.con".
365 inline "cic:/CoRN/algebra/COrdFields/pos_nine.con".
367 inline "cic:/CoRN/algebra/COrdFields/pos_twelve.con".
369 inline "cic:/CoRN/algebra/COrdFields/pos_sixteen.con".
371 inline "cic:/CoRN/algebra/COrdFields/pos_eighteen.con".
373 inline "cic:/CoRN/algebra/COrdFields/pos_twentyfour.con".
375 inline "cic:/CoRN/algebra/COrdFields/pos_fortyeight.con".
377 inline "cic:/CoRN/algebra/COrdFields/six_ap_zero.con".
379 inline "cic:/CoRN/algebra/COrdFields/eight_ap_zero.con".
381 inline "cic:/CoRN/algebra/COrdFields/nine_ap_zero.con".
383 inline "cic:/CoRN/algebra/COrdFields/twelve_ap_zero.con".
385 inline "cic:/CoRN/algebra/COrdFields/sixteen_ap_zero.con".
387 inline "cic:/CoRN/algebra/COrdFields/eighteen_ap_zero.con".
389 inline "cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con".
391 inline "cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con".
398 End infinity_of_cordfields.
402 Declare Left Step leEq_wdl.
406 Declare Right Step leEq_wdr.
410 Section consequences_of_infinity.
414 *** Consequences of infinity
417 inline "cic:/CoRN/algebra/COrdFields/F.var".
419 inline "cic:/CoRN/algebra/COrdFields/square_eq.con".
422 Ordered fields have characteristic zero.
425 inline "cic:/CoRN/algebra/COrdFields/char0_OrdField.con".
428 End consequences_of_infinity.
431 (*#**********************************)
434 Section Properties_of_Ordering.
437 (*#**********************************)
440 ** Properties of [[<]]
443 inline "cic:/CoRN/algebra/COrdFields/R.var".
446 We do not use a special predicate for positivity,
447 (e.g.%\% [PosP]), but just write [Zero [<] x].
448 Reasons: it is more natural; in ordinary mathematics we also write [Zero [<] x]
458 *** Addition and subtraction%\label{section:less_plus_minus}%
462 inline "cic:/CoRN/algebra/COrdFields/plus_resp_less_lft.con".
464 inline "cic:/CoRN/algebra/COrdFields/inv_resp_less.con".
467 Transparent cg_minus.
470 inline "cic:/CoRN/algebra/COrdFields/minus_resp_less.con".
473 Transparent cg_minus.
476 inline "cic:/CoRN/algebra/COrdFields/minus_resp_less_rht.con".
478 inline "cic:/CoRN/algebra/COrdFields/plus_resp_less_both.con".
481 For versions of [plus_resp_less_both] where one [ [<] ] in the
482 assumption is replaced by [ [<=] ]%, see
483 Section~\ref{section:leEq-plus-minus}%.
488 inline "cic:/CoRN/algebra/COrdFields/plus_cancel_less.con".
490 inline "cic:/CoRN/algebra/COrdFields/inv_cancel_less.con".
494 Lemmas where an operation is transformed into the inverse operation on
495 the other side of an inequality are called laws for shifting.
496 %\begin{nameconvention}%
497 The names of laws for shifting start with [shift_], and then come
498 the operation and the inequality, in the order in which they occur in the
500 If the shifted operand changes sides w.r.t.%\% the operation and its inverse,
501 the name gets a prime.
502 %\end{nameconvention}%
504 It would be nicer to write the laws for shifting as bi-implications,
505 However, it is impractical to use these in
506 Coq%(see the Coq shortcoming in Section~\ref{section:setoid-basics})%.
509 inline "cic:/CoRN/algebra/COrdFields/shift_less_plus.con".
511 inline "cic:/CoRN/algebra/COrdFields/shift_less_plus'.con".
513 inline "cic:/CoRN/algebra/COrdFields/shift_less_minus.con".
515 inline "cic:/CoRN/algebra/COrdFields/shift_less_minus'.con".
517 inline "cic:/CoRN/algebra/COrdFields/shift_plus_less.con".
519 inline "cic:/CoRN/algebra/COrdFields/shift_plus_less'.con".
521 inline "cic:/CoRN/algebra/COrdFields/shift_minus_less.con".
523 inline "cic:/CoRN/algebra/COrdFields/shift_minus_less'.con".
526 Some special cases of laws for shifting.
529 inline "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus.con".
531 inline "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con".
533 inline "cic:/CoRN/algebra/COrdFields/qltone.con".
540 Section multiplication.
544 *** Multiplication and division
545 By Convention%~\ref{convention:div-form}%
546 in CFields% (Section~\ref{section:fields})%, we often have redundant premises
547 in lemmas. E.g.%\% the informal statement
548 ``for all [x,y : R] with [Zero [<] x] and [Zero [<] y]
549 we have [Zero [<] y[/]x]''
550 is formalized as follows.
552 forall (x y : R) x_, (Zero [<] x) -> (Zero [<] y) -> (Zero [<] y[/]x[//]H)
554 We do this to keep it easy to use such lemmas.
558 inline "cic:/CoRN/algebra/COrdFields/mult_resp_less.con".
560 inline "cic:/CoRN/algebra/COrdFields/recip_resp_pos.con".
562 inline "cic:/CoRN/algebra/COrdFields/div_resp_less_rht.con".
564 inline "cic:/CoRN/algebra/COrdFields/div_resp_pos.con".
566 inline "cic:/CoRN/algebra/COrdFields/mult_resp_less_lft.con".
568 inline "cic:/CoRN/algebra/COrdFields/mult_resp_less_both.con".
570 inline "cic:/CoRN/algebra/COrdFields/recip_resp_less.con".
572 inline "cic:/CoRN/algebra/COrdFields/div_resp_less.con".
574 (*#* Cancellation laws
577 inline "cic:/CoRN/algebra/COrdFields/mult_cancel_less.con".
582 %For namegiving, see the Section~\ref{section:less_plus_minus}
586 inline "cic:/CoRN/algebra/COrdFields/shift_div_less.con".
588 inline "cic:/CoRN/algebra/COrdFields/shift_div_less'.con".
590 inline "cic:/CoRN/algebra/COrdFields/shift_less_div.con".
592 inline "cic:/CoRN/algebra/COrdFields/shift_less_mult.con".
594 inline "cic:/CoRN/algebra/COrdFields/shift_less_mult'.con".
596 inline "cic:/CoRN/algebra/COrdFields/shift_mult_less.con".
598 (*#* Other properties of multiplication and division
601 inline "cic:/CoRN/algebra/COrdFields/minusOne_less.con".
603 inline "cic:/CoRN/algebra/COrdFields/swap_div.con".
605 inline "cic:/CoRN/algebra/COrdFields/eps_div_less_eps.con".
607 inline "cic:/CoRN/algebra/COrdFields/pos_div_two.con".
609 inline "cic:/CoRN/algebra/COrdFields/pos_div_two'.con".
612 Apply mult_cancel_less with (Two::R).
614 rstepl eps[+]Zero; rstepr eps[+]eps.
615 Apply plus_resp_less_lft.
620 inline "cic:/CoRN/algebra/COrdFields/pos_div_three.con".
622 inline "cic:/CoRN/algebra/COrdFields/pos_div_three'.con".
624 inline "cic:/CoRN/algebra/COrdFields/pos_div_four.con".
626 inline "cic:/CoRN/algebra/COrdFields/pos_div_four'.con".
628 inline "cic:/CoRN/algebra/COrdFields/pos_div_six.con".
630 inline "cic:/CoRN/algebra/COrdFields/pos_div_eight.con".
632 inline "cic:/CoRN/algebra/COrdFields/pos_div_nine.con".
634 inline "cic:/CoRN/algebra/COrdFields/pos_div_twelve.con".
636 inline "cic:/CoRN/algebra/COrdFields/pos_div_sixteen.con".
638 inline "cic:/CoRN/algebra/COrdFields/pos_div_eighteen.con".
640 inline "cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con".
642 inline "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con".
653 *** Miscellaneous properties
656 inline "cic:/CoRN/algebra/COrdFields/nring_pos.con".
658 inline "cic:/CoRN/algebra/COrdFields/less_nring.con".
660 inline "cic:/CoRN/algebra/COrdFields/pos_nring_fac.con".
662 inline "cic:/CoRN/algebra/COrdFields/Smallest_less_Average.con".
664 inline "cic:/CoRN/algebra/COrdFields/Average_less_Greatest.con".
666 inline "cic:/CoRN/algebra/COrdFields/Sum_resp_less.con".
668 inline "cic:/CoRN/algebra/COrdFields/Sumx_resp_less.con".
670 inline "cic:/CoRN/algebra/COrdFields/positive_Sum_two.con".
672 inline "cic:/CoRN/algebra/COrdFields/positive_Sumx.con".
674 inline "cic:/CoRN/algebra/COrdFields/negative_Sumx.con".
681 End Properties_of_Ordering.