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 *********************)
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# *)
51 include "tactics/FieldReflection.ma".
57 ** Definition of the notion of ordered field
62 inline procedural "cic:/CoRN/algebra/COrdFields/strictorder.ind".
65 Implicit Arguments strictorder [A].
69 Implicit Arguments Build_strictorder [A R].
73 Implicit Arguments so_trans [A R].
77 Implicit Arguments so_asym [A R].
80 inline procedural "cic:/CoRN/algebra/COrdFields/is_COrdField.ind".
82 inline procedural "cic:/CoRN/algebra/COrdFields/COrdField.ind".
85 cic:/matita/CoRN-Procedural/algebra/COrdFields/cof_crr.con
89 %\begin{nameconvention}%
90 In the names of lemmas, [ [<] ] is written as [less] and "[Zero [<] ]"
92 %\end{nameconvention}%
96 Implicit Arguments cof_less [c].
100 Infix "[<]" := cof_less (at level 70, no associativity).
103 inline procedural "cic:/CoRN/algebra/COrdFields/greater.con" as definition.
106 Implicit Arguments greater [F].
110 Infix "[>]" := greater (at level 70, no associativity).
116 Less or equal is defined as ``not greater than''.
119 inline procedural "cic:/CoRN/algebra/COrdFields/leEq.con" as definition.
122 %\begin{nameconvention}%
123 In the names of lemmas, [ [<=] ] is written as [leEq] and
124 [Zero [<=] ] is written as [nonneg].
125 %\end{nameconvention}%
129 Implicit Arguments leEq [F].
133 Infix "[<=]" := leEq (at level 70, no associativity).
137 Section COrdField_axioms
141 ** Ordered field axioms
148 cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var
151 inline procedural "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con" as lemma.
153 inline procedural "cic:/CoRN/algebra/COrdFields/less_strorder.con" as lemma.
155 inline procedural "cic:/CoRN/algebra/COrdFields/less_transitive_unfolded.con" as lemma.
157 inline procedural "cic:/CoRN/algebra/COrdFields/less_antisymmetric_unfolded.con" as lemma.
159 inline procedural "cic:/CoRN/algebra/COrdFields/less_irreflexive.con" as lemma.
161 inline procedural "cic:/CoRN/algebra/COrdFields/less_irreflexive_unfolded.con" as lemma.
163 inline procedural "cic:/CoRN/algebra/COrdFields/plus_resp_less_rht.con" as lemma.
165 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_pos.con" as lemma.
167 inline procedural "cic:/CoRN/algebra/COrdFields/less_conf_ap.con" as lemma.
169 inline procedural "cic:/CoRN/algebra/COrdFields/less_wdr.con" as lemma.
171 inline procedural "cic:/CoRN/algebra/COrdFields/less_wdl.con" as lemma.
178 Declare Left Step less_wdl.
182 Declare Right Step less_wdr.
186 Section OrdField_basics
195 Let in the rest of this section (and all subsections)
196 [R] be an ordered field
201 cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var
204 inline procedural "cic:/CoRN/algebra/COrdFields/less_imp_ap.con" as lemma.
206 inline procedural "cic:/CoRN/algebra/COrdFields/Greater_imp_ap.con" as lemma.
208 inline procedural "cic:/CoRN/algebra/COrdFields/ap_imp_less.con" as lemma.
211 Now properties which can be derived.
214 inline procedural "cic:/CoRN/algebra/COrdFields/less_cotransitive.con" as lemma.
216 inline procedural "cic:/CoRN/algebra/COrdFields/less_cotransitive_unfolded.con" as lemma.
218 inline procedural "cic:/CoRN/algebra/COrdFields/pos_ap_zero.con" as lemma.
220 (* Main characterization of less *)
222 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_not_eq.con" as lemma.
228 (*#**********************************)
231 Section Basic_Properties_of_leEq
234 (*#**********************************)
236 (*#* ** Basic properties of [ [<=] ]
240 cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var
243 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_wdr.con" as lemma.
245 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_wdl.con" as lemma.
247 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_reflexive.con" as lemma.
250 Declare Left Step leEq_wdl.
254 Declare Right Step leEq_wdr.
257 inline procedural "cic:/CoRN/algebra/COrdFields/eq_imp_leEq.con" as lemma.
259 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_imp_eq.con" as lemma.
261 inline procedural "cic:/CoRN/algebra/COrdFields/lt_equiv_imp_eq.con" as lemma.
263 inline procedural "cic:/CoRN/algebra/COrdFields/less_leEq_trans.con" as lemma.
265 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_less_trans.con" as lemma.
267 inline procedural "cic:/CoRN/algebra/COrdFields/leEq_transitive.con" as lemma.
269 inline procedural "cic:/CoRN/algebra/COrdFields/less_leEq.con" as lemma.
272 End Basic_Properties_of_leEq
276 Declare Left Step leEq_wdl.
280 Declare Right Step leEq_wdr.
284 Section infinity_of_cordfields
288 ** Infinity of ordered fields
290 In an ordered field we have that [One[+]One] and
291 [One[+]One[+]One] and so on are all apart from zero.
292 We first show this, so that we can define [TwoNZ], [ThreeNZ]
293 and so on. These are elements of [NonZeros], so that we can write
298 cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var
301 inline procedural "cic:/CoRN/algebra/COrdFields/pos_one.con" as lemma.
303 inline procedural "cic:/CoRN/algebra/COrdFields/nring_less_succ.con" as lemma.
305 inline procedural "cic:/CoRN/algebra/COrdFields/nring_less.con" as lemma.
307 inline procedural "cic:/CoRN/algebra/COrdFields/nring_leEq.con" as lemma.
309 inline procedural "cic:/CoRN/algebra/COrdFields/nring_apart.con" as lemma.
311 inline procedural "cic:/CoRN/algebra/COrdFields/nring_ap_zero.con" as lemma.
313 inline procedural "cic:/CoRN/algebra/COrdFields/nring_ap_zero'.con" as lemma.
315 inline procedural "cic:/CoRN/algebra/COrdFields/nring_ap_zero_imp.con" as lemma.
317 inline procedural "cic:/CoRN/algebra/COrdFields/Snring.con" as definition.
319 include "tactics/Transparent_algebra.ma".
321 inline procedural "cic:/CoRN/algebra/COrdFields/pos_Snring.con" as lemma.
323 inline procedural "cic:/CoRN/algebra/COrdFields/nringS_ap_zero.con" as lemma.
325 inline procedural "cic:/CoRN/algebra/COrdFields/nring_fac_ap_zero.con" as lemma.
327 include "tactics/Opaque_algebra.ma".
334 *** Properties of one up to four
335 %\begin{nameconvention}%
336 In the names of lemmas, we denote the numbers 0,1,2,3,4 and so on, by
337 [zero], [one], [two] etc.
338 %\end{nameconvention}%
341 inline procedural "cic:/CoRN/algebra/COrdFields/less_plusOne.con" as lemma.
343 inline procedural "cic:/CoRN/algebra/COrdFields/zero_lt_posplus1.con" as lemma.
345 inline procedural "cic:/CoRN/algebra/COrdFields/plus_one_ext_less.con" as lemma.
347 inline procedural "cic:/CoRN/algebra/COrdFields/one_less_two.con" as lemma.
349 inline procedural "cic:/CoRN/algebra/COrdFields/two_less_three.con" as lemma.
351 inline procedural "cic:/CoRN/algebra/COrdFields/three_less_four.con" as lemma.
353 inline procedural "cic:/CoRN/algebra/COrdFields/pos_two.con" as lemma.
355 inline procedural "cic:/CoRN/algebra/COrdFields/one_less_three.con" as lemma.
357 inline procedural "cic:/CoRN/algebra/COrdFields/two_less_four.con" as lemma.
359 inline procedural "cic:/CoRN/algebra/COrdFields/pos_three.con" as lemma.
361 inline procedural "cic:/CoRN/algebra/COrdFields/one_less_four.con" as lemma.
363 inline procedural "cic:/CoRN/algebra/COrdFields/pos_four.con" as lemma.
365 inline procedural "cic:/CoRN/algebra/COrdFields/two_ap_zero.con" as lemma.
367 inline procedural "cic:/CoRN/algebra/COrdFields/three_ap_zero.con" as lemma.
369 inline procedural "cic:/CoRN/algebra/COrdFields/four_ap_zero.con" as lemma.
376 Section More_than_four
379 (*#* *** Properties of some other numbers *)
381 inline procedural "cic:/CoRN/algebra/COrdFields/pos_six.con" as lemma.
383 inline procedural "cic:/CoRN/algebra/COrdFields/pos_eight.con" as lemma.
385 inline procedural "cic:/CoRN/algebra/COrdFields/pos_nine.con" as lemma.
387 inline procedural "cic:/CoRN/algebra/COrdFields/pos_twelve.con" as lemma.
389 inline procedural "cic:/CoRN/algebra/COrdFields/pos_sixteen.con" as lemma.
391 inline procedural "cic:/CoRN/algebra/COrdFields/pos_eighteen.con" as lemma.
393 inline procedural "cic:/CoRN/algebra/COrdFields/pos_twentyfour.con" as lemma.
395 inline procedural "cic:/CoRN/algebra/COrdFields/pos_fortyeight.con" as lemma.
397 inline procedural "cic:/CoRN/algebra/COrdFields/six_ap_zero.con" as lemma.
399 inline procedural "cic:/CoRN/algebra/COrdFields/eight_ap_zero.con" as lemma.
401 inline procedural "cic:/CoRN/algebra/COrdFields/nine_ap_zero.con" as lemma.
403 inline procedural "cic:/CoRN/algebra/COrdFields/twelve_ap_zero.con" as lemma.
405 inline procedural "cic:/CoRN/algebra/COrdFields/sixteen_ap_zero.con" as lemma.
407 inline procedural "cic:/CoRN/algebra/COrdFields/eighteen_ap_zero.con" as lemma.
409 inline procedural "cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con" as lemma.
411 inline procedural "cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con" as lemma.
418 End infinity_of_cordfields
422 Declare Left Step leEq_wdl.
426 Declare Right Step leEq_wdr.
430 Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
434 Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
438 Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
442 Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
446 Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
450 Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
454 Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
458 Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
462 Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
466 Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
470 Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
474 Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
478 Section consequences_of_infinity
482 *** Consequences of infinity
486 cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var
489 inline procedural "cic:/CoRN/algebra/COrdFields/square_eq.con" as lemma.
492 Ordered fields have characteristic zero.
495 inline procedural "cic:/CoRN/algebra/COrdFields/char0_OrdField.con" as lemma.
498 End consequences_of_infinity
501 (*#**********************************)
504 Section Properties_of_Ordering
507 (*#**********************************)
510 ** Properties of [[<]]
514 cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var
518 We do not use a special predicate for positivity,
519 (e.g.%\% [PosP]), but just write [Zero [<] x].
520 Reasons: it is more natural; in ordinary mathematics we also write [Zero [<] x]
530 *** Addition and subtraction%\label{section:less_plus_minus}%
534 inline procedural "cic:/CoRN/algebra/COrdFields/plus_resp_less_lft.con" as lemma.
536 inline procedural "cic:/CoRN/algebra/COrdFields/inv_resp_less.con" as lemma.
539 Transparent cg_minus.
542 inline procedural "cic:/CoRN/algebra/COrdFields/minus_resp_less.con" as lemma.
545 Transparent cg_minus.
548 inline procedural "cic:/CoRN/algebra/COrdFields/minus_resp_less_rht.con" as lemma.
550 inline procedural "cic:/CoRN/algebra/COrdFields/plus_resp_less_both.con" as lemma.
553 For versions of [plus_resp_less_both] where one [ [<] ] in the
554 assumption is replaced by [ [<=] ]%, see
555 Section~\ref{section:leEq-plus-minus}%.
560 inline procedural "cic:/CoRN/algebra/COrdFields/plus_cancel_less.con" as lemma.
562 inline procedural "cic:/CoRN/algebra/COrdFields/inv_cancel_less.con" as lemma.
566 Lemmas where an operation is transformed into the inverse operation on
567 the other side of an inequality are called laws for shifting.
568 %\begin{nameconvention}%
569 The names of laws for shifting start with [shift_], and then come
570 the operation and the inequality, in the order in which they occur in the
572 If the shifted operand changes sides w.r.t.%\% the operation and its inverse,
573 the name gets a prime.
574 %\end{nameconvention}%
576 It would be nicer to write the laws for shifting as bi-implications,
577 However, it is impractical to use these in
578 Coq%(see the Coq shortcoming in Section~\ref{section:setoid-basics})%.
581 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_plus.con" as lemma.
583 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_plus'.con" as lemma.
585 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_minus.con" as lemma.
587 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_minus'.con" as lemma.
589 inline procedural "cic:/CoRN/algebra/COrdFields/shift_plus_less.con" as lemma.
591 inline procedural "cic:/CoRN/algebra/COrdFields/shift_plus_less'.con" as lemma.
593 inline procedural "cic:/CoRN/algebra/COrdFields/shift_minus_less.con" as lemma.
595 inline procedural "cic:/CoRN/algebra/COrdFields/shift_minus_less'.con" as lemma.
598 Some special cases of laws for shifting.
601 inline procedural "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus.con" as lemma.
603 inline procedural "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con" as lemma.
605 inline procedural "cic:/CoRN/algebra/COrdFields/qltone.con" as lemma.
612 Section multiplication
616 *** Multiplication and division
617 By Convention%~\ref{convention:div-form}%
618 in CFields% (Section~\ref{section:fields})%, we often have redundant premises
619 in lemmas. E.g.%\% the informal statement
620 ``for all [x,y : R] with [Zero [<] x] and [Zero [<] y]
621 we have [Zero [<] y[/]x]''
622 is formalized as follows.
624 forall (x y : R) x_, (Zero [<] x) -> (Zero [<] y) -> (Zero [<] y[/]x[//]H)
626 We do this to keep it easy to use such lemmas.
630 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_less.con" as lemma.
632 inline procedural "cic:/CoRN/algebra/COrdFields/recip_resp_pos.con" as lemma.
634 inline procedural "cic:/CoRN/algebra/COrdFields/div_resp_less_rht.con" as lemma.
636 inline procedural "cic:/CoRN/algebra/COrdFields/div_resp_pos.con" as lemma.
638 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_less_lft.con" as lemma.
640 inline procedural "cic:/CoRN/algebra/COrdFields/mult_resp_less_both.con" as lemma.
642 inline procedural "cic:/CoRN/algebra/COrdFields/recip_resp_less.con" as lemma.
644 inline procedural "cic:/CoRN/algebra/COrdFields/div_resp_less.con" as lemma.
646 (*#* Cancellation laws
649 inline procedural "cic:/CoRN/algebra/COrdFields/mult_cancel_less.con" as lemma.
654 %For namegiving, see the Section~\ref{section:less_plus_minus}
658 inline procedural "cic:/CoRN/algebra/COrdFields/shift_div_less.con" as lemma.
660 inline procedural "cic:/CoRN/algebra/COrdFields/shift_div_less'.con" as lemma.
662 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_div.con" as lemma.
664 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_mult.con" as lemma.
666 inline procedural "cic:/CoRN/algebra/COrdFields/shift_less_mult'.con" as lemma.
668 inline procedural "cic:/CoRN/algebra/COrdFields/shift_mult_less.con" as lemma.
670 (*#* Other properties of multiplication and division
673 inline procedural "cic:/CoRN/algebra/COrdFields/minusOne_less.con" as lemma.
675 inline procedural "cic:/CoRN/algebra/COrdFields/swap_div.con" as lemma.
677 inline procedural "cic:/CoRN/algebra/COrdFields/eps_div_less_eps.con" as lemma.
679 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_two.con" as lemma.
681 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_two'.con" as lemma.
684 Apply mult_cancel_less with (Two::R).
686 rstepl eps[+]Zero; rstepr eps[+]eps.
687 Apply plus_resp_less_lft.
692 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_three.con" as lemma.
694 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_three'.con" as lemma.
696 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_four.con" as lemma.
698 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_four'.con" as lemma.
700 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_six.con" as lemma.
702 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_eight.con" as lemma.
704 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_nine.con" as lemma.
706 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_twelve.con" as lemma.
708 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_sixteen.con" as lemma.
710 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_eighteen.con" as lemma.
712 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con" as lemma.
714 inline procedural "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con" as lemma.
725 *** Miscellaneous properties
728 inline procedural "cic:/CoRN/algebra/COrdFields/nring_pos.con" as lemma.
730 inline procedural "cic:/CoRN/algebra/COrdFields/less_nring.con" as lemma.
732 inline procedural "cic:/CoRN/algebra/COrdFields/pos_nring_fac.con" as lemma.
734 inline procedural "cic:/CoRN/algebra/COrdFields/Smallest_less_Average.con" as lemma.
736 inline procedural "cic:/CoRN/algebra/COrdFields/Average_less_Greatest.con" as lemma.
738 inline procedural "cic:/CoRN/algebra/COrdFields/Sum_resp_less.con" as lemma.
740 inline procedural "cic:/CoRN/algebra/COrdFields/Sumx_resp_less.con" as lemma.
742 inline procedural "cic:/CoRN/algebra/COrdFields/positive_Sum_two.con" as lemma.
744 inline procedural "cic:/CoRN/algebra/COrdFields/positive_Sumx.con" as lemma.
746 inline procedural "cic:/CoRN/algebra/COrdFields/negative_Sumx.con" as lemma.
753 End Properties_of_Ordering