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/CRings".
19 include "CoRN_notation.ma".
21 (* $Id: CRings.v,v 1.8 2004/04/23 10:00:53 lcf Exp $ *)
23 (*#* printing [*] %\ensuremath\times% #×# *)
25 (*#* printing [^] %\ensuremath{\hat{\ }}% #^# *)
27 (*#* printing {*} %\ensuremath\times% #×# *)
29 (*#* printing {**} %\ensuremath\ast% #∗# *)
31 (*#* printing {^} %\ensuremath{\hat{\ }}% #^# *)
33 (*#* printing One %\ensuremath{\mathbf1}% #1# *)
35 (*#* printing Two %\ensuremath{\mathbf2}% #2# *)
37 (*#* printing Three %\ensuremath{\mathbf3}% #3# *)
39 (*#* printing Four %\ensuremath{\mathbf4}% #4# *)
41 (*#* printing Six %\ensuremath{\mathbf6}% #6# *)
43 (*#* printing Eight %\ensuremath{\mathbf8}% #8# *)
45 (*#* printing Nine %\ensuremath{\mathbf9}% #9# *)
47 (*#* printing Twelve %\ensuremath{\mathbf{12}}% #12# *)
49 (*#* printing Sixteen %\ensuremath{\mathbf{16}}% #16# *)
51 (*#* printing Eighteen %\ensuremath{\mathbf{18}}% #18# *)
53 (*#* printing TwentyFour %\ensuremath{\mathbf{24}}% #24# *)
55 (*#* printing FortyEight %\ensuremath{\mathbf{48}}% #48# *)
57 include "algebra/CSums.ma".
69 (* Constructive RINGS *)
72 We actually define commutative rings with identity.
73 ** Definition of the notion of Ring
76 inline "cic:/CoRN/algebra/CRings/distributive.con".
79 Implicit Arguments distributive [S].
82 inline "cic:/CoRN/algebra/CRings/is_CRing.ind".
84 inline "cic:/CoRN/algebra/CRings/CRing.ind".
86 coercion "cic:/matita/CoRN-Decl/algebra/CRings/cr_crr.con" 0 (* compounds *).
88 inline "cic:/CoRN/algebra/CRings/cr_plus.con".
90 inline "cic:/CoRN/algebra/CRings/cr_inv.con".
92 inline "cic:/CoRN/algebra/CRings/cr_minus.con".
99 %\begin{nameconvention}%
100 In the names of lemmas, we will denote [One] with [one],
101 and [[*]] with [mult].
102 %\end{nameconvention}%
106 Implicit Arguments cr_mult [c].
110 Section CRing_axioms.
115 %\begin{convention}% Let [R] be a ring.
119 inline "cic:/CoRN/algebra/CRings/R.var".
121 inline "cic:/CoRN/algebra/CRings/CRing_is_CRing.con".
123 inline "cic:/CoRN/algebra/CRings/mult_assoc.con".
125 inline "cic:/CoRN/algebra/CRings/mult_commutes.con".
127 inline "cic:/CoRN/algebra/CRings/mult_mon.con".
131 inline "cic:/CoRN/algebra/CRings/dist.con".
133 inline "cic:/CoRN/algebra/CRings/ring_non_triv.con".
135 inline "cic:/CoRN/algebra/CRings/mult_wd.con".
137 inline "cic:/CoRN/algebra/CRings/mult_wdl.con".
139 inline "cic:/CoRN/algebra/CRings/mult_wdr.con".
141 (* Begin_SpecReals *)
148 Section Ring_constructions.
152 ** Ring constructions
158 inline "cic:/CoRN/algebra/CRings/R.var".
161 The multiplicative monoid of a ring is defined as follows.
164 inline "cic:/CoRN/algebra/CRings/Build_multCMonoid.con".
167 End Ring_constructions.
173 Section Ring_unfolded.
178 %\begin{convention}% Let [R] be a ring.
182 inline "cic:/CoRN/algebra/CRings/R.var".
186 inline "cic:/CoRN/algebra/CRings/mmR.con".
190 inline "cic:/CoRN/algebra/CRings/mult_assoc_unfolded.con".
192 inline "cic:/CoRN/algebra/CRings/mult_commut_unfolded.con".
195 Hint Resolve mult_commut_unfolded: algebra.
198 inline "cic:/CoRN/algebra/CRings/mult_one.con".
200 inline "cic:/CoRN/algebra/CRings/one_mult.con".
202 inline "cic:/CoRN/algebra/CRings/ring_dist_unfolded.con".
205 Hint Resolve ring_dist_unfolded: algebra.
208 inline "cic:/CoRN/algebra/CRings/ring_distl_unfolded.con".
215 Hint Resolve mult_assoc_unfolded: algebra.
219 Hint Resolve ring_non_triv mult_one one_mult mult_commut_unfolded: algebra.
223 Hint Resolve ring_dist_unfolded ring_distl_unfolded: algebra.
232 %\begin{convention}% Let [R] be a ring.
236 inline "cic:/CoRN/algebra/CRings/R.var".
238 inline "cic:/CoRN/algebra/CRings/one_ap_zero.con".
240 inline "cic:/CoRN/algebra/CRings/is_zero_rht.con".
242 inline "cic:/CoRN/algebra/CRings/is_zero_lft.con".
245 Implicit Arguments is_zero_rht [S].
249 Implicit Arguments is_zero_lft [S].
252 inline "cic:/CoRN/algebra/CRings/cring_mult_zero.con".
255 Hint Resolve cring_mult_zero: algebra.
258 inline "cic:/CoRN/algebra/CRings/x_mult_zero.con".
260 inline "cic:/CoRN/algebra/CRings/cring_mult_zero_op.con".
263 Hint Resolve cring_mult_zero_op: algebra.
266 inline "cic:/CoRN/algebra/CRings/cring_inv_mult_lft.con".
269 Hint Resolve cring_inv_mult_lft: algebra.
272 inline "cic:/CoRN/algebra/CRings/cring_inv_mult_rht.con".
275 Hint Resolve cring_inv_mult_rht: algebra.
278 inline "cic:/CoRN/algebra/CRings/cring_mult_ap_zero.con".
280 inline "cic:/CoRN/algebra/CRings/cring_mult_ap_zero_op.con".
282 inline "cic:/CoRN/algebra/CRings/inv_mult_invol.con".
284 inline "cic:/CoRN/algebra/CRings/ring_dist_minus.con".
287 Hint Resolve ring_dist_minus: algebra.
290 inline "cic:/CoRN/algebra/CRings/ring_distl_minus.con".
293 Hint Resolve ring_distl_minus: algebra.
301 Hint Resolve cring_mult_zero cring_mult_zero_op: algebra.
305 Hint Resolve inv_mult_invol: algebra.
309 Hint Resolve cring_inv_mult_lft cring_inv_mult_rht: algebra.
313 Hint Resolve ring_dist_minus: algebra.
317 Hint Resolve ring_distl_minus: algebra.
320 (* Begin_SpecReals *)
324 Some auxiliary functions and operations over a ring;
325 especially geared towards CReals.
329 Section exponentiation.
339 inline "cic:/CoRN/algebra/CRings/R.var".
343 inline "cic:/CoRN/algebra/CRings/nexp.con".
345 inline "cic:/CoRN/algebra/CRings/nexp_well_def.con".
347 inline "cic:/CoRN/algebra/CRings/nexp_strong_ext.con".
349 inline "cic:/CoRN/algebra/CRings/nexp_op.con".
351 (* Begin_SpecReals *)
360 Implicit Arguments nexp_op [R].
363 (* Begin_SpecReals *)
366 Section nat_injection.
370 *** The injection of natural numbers into a ring
371 %\begin{convention}% Let [R] be a ring.
375 inline "cic:/CoRN/algebra/CRings/R.var".
378 The injection of Coq natural numbers into a ring is called [nring].
379 Note that this need not really be an injection; when it is, the ring is said
380 to have characteristic [0].
383 inline "cic:/CoRN/algebra/CRings/nring.con".
385 inline "cic:/CoRN/algebra/CRings/Char0.con".
389 inline "cic:/CoRN/algebra/CRings/nring_comm_plus.con".
391 inline "cic:/CoRN/algebra/CRings/nring_comm_mult.con".
393 (* Begin_SpecReals *)
402 Hint Resolve nring_comm_plus nring_comm_mult: algebra.
405 (* Begin_SpecReals *)
408 Implicit Arguments nring [R].
413 inline "cic:/CoRN/algebra/CRings/one_plus_one.con".
415 inline "cic:/CoRN/algebra/CRings/x_plus_x.con".
418 Hint Resolve one_plus_one x_plus_x: algebra.
422 In a ring of characteristic zero, [nring] is really an injection.
425 inline "cic:/CoRN/algebra/CRings/nring_different.con".
428 Section int_injection.
432 *** The injection of integers into a ring
438 inline "cic:/CoRN/algebra/CRings/R.var".
441 The injection of Coq integers into a ring is called [zring]. Again,
442 this need not really be an injection.
444 The first definition is now obsolete, having been replaced by a more efficient
445 one. It is kept to avoid having to redo all the proofs.
448 inline "cic:/CoRN/algebra/CRings/zring_old.con".
450 inline "cic:/CoRN/algebra/CRings/zring_old_zero.con".
453 Hint Resolve zring_old_zero: algebra.
456 inline "cic:/CoRN/algebra/CRings/zring_old_diff.con".
459 Hint Resolve zring_old_diff.
462 inline "cic:/CoRN/algebra/CRings/zring_old_plus_nat.con".
465 Hint Resolve zring_old_plus_nat: algebra.
468 inline "cic:/CoRN/algebra/CRings/zring_old_inv_nat.con".
471 Hint Resolve zring_old_inv_nat: algebra.
475 Hint Resolve zring_old_diff: algebra.
478 inline "cic:/CoRN/algebra/CRings/zring_old_plus.con".
481 Hint Resolve zring_old_plus: algebra.
484 inline "cic:/CoRN/algebra/CRings/zring_old_inv.con".
487 Hint Resolve zring_old_inv: algebra.
490 inline "cic:/CoRN/algebra/CRings/zring_old_minus.con".
493 Hint Resolve zring_old_minus: algebra.
496 inline "cic:/CoRN/algebra/CRings/zring_old_mult.con".
499 Hint Resolve zring_old_mult: algebra.
502 inline "cic:/CoRN/algebra/CRings/zring_old_one.con".
505 Hint Resolve zring_old_one: algebra.
508 inline "cic:/CoRN/algebra/CRings/zring_old_inv_one.con".
510 (*#************** new def of zring. ***********************)
512 (*#* The [zring] function can be defined directly. This is done here.
515 inline "cic:/CoRN/algebra/CRings/pring_aux.con".
517 inline "cic:/CoRN/algebra/CRings/pring.con".
519 inline "cic:/CoRN/algebra/CRings/zring.con".
521 inline "cic:/CoRN/algebra/CRings/pring_aux_lemma.con".
523 inline "cic:/CoRN/algebra/CRings/double_nring.con".
526 Hint Resolve pring_aux_lemma double_nring: algebra.
529 inline "cic:/CoRN/algebra/CRings/pring_aux_nring.con".
532 Hint Resolve pring_aux_nring: algebra.
535 inline "cic:/CoRN/algebra/CRings/pring_convert.con".
538 Hint Resolve pring_convert: algebra.
541 inline "cic:/CoRN/algebra/CRings/zring_zring_old.con".
544 Hint Resolve zring_zring_old: algebra.
547 inline "cic:/CoRN/algebra/CRings/zring_zero.con".
549 inline "cic:/CoRN/algebra/CRings/zring_diff.con".
551 inline "cic:/CoRN/algebra/CRings/zring_plus_nat.con".
553 inline "cic:/CoRN/algebra/CRings/zring_inv_nat.con".
555 inline "cic:/CoRN/algebra/CRings/zring_plus.con".
557 inline "cic:/CoRN/algebra/CRings/zring_inv.con".
559 inline "cic:/CoRN/algebra/CRings/zring_minus.con".
561 inline "cic:/CoRN/algebra/CRings/zring_mult.con".
563 inline "cic:/CoRN/algebra/CRings/zring_one.con".
565 inline "cic:/CoRN/algebra/CRings/zring_inv_one.con".
572 Implicit Arguments zring [R].
576 Hint Resolve pring_convert zring_zero zring_diff zring_plus_nat zring_inv_nat
577 zring_plus zring_inv zring_minus zring_mult zring_one zring_inv_one:
587 %\begin{convention}% Let [R] be a ring.
591 inline "cic:/CoRN/algebra/CRings/R.var".
594 *** Infinite Ring sums
598 Section infinite_ring_sums.
601 inline "cic:/CoRN/algebra/CRings/Sum_upto.con".
603 inline "cic:/CoRN/algebra/CRings/sum_upto_O.con".
605 inline "cic:/CoRN/algebra/CRings/Sum_from_upto.con".
608 Here's an alternative def of [Sum_from_upto], with a lemma that
609 it's equivalent to the original.
612 inline "cic:/CoRN/algebra/CRings/seq_from.con".
614 inline "cic:/CoRN/algebra/CRings/Sum_from_upto_alt.con".
617 End infinite_ring_sums.
621 Section ring_sums_over_lists.
624 (*#* *** Ring Sums over Lists
627 inline "cic:/CoRN/algebra/CRings/RList_Mem.con".
629 inline "cic:/CoRN/algebra/CRings/List_Sum_upto.con".
631 inline "cic:/CoRN/algebra/CRings/list_sum_upto_O.con".
633 inline "cic:/CoRN/algebra/CRings/List_Sum_from_upto.con".
636 End ring_sums_over_lists.
644 ** Distribution properties
651 Section Dist_properties.
654 inline "cic:/CoRN/algebra/CRings/R.var".
656 inline "cic:/CoRN/algebra/CRings/dist_1b.con".
659 Hint Resolve dist_1b: algebra.
662 inline "cic:/CoRN/algebra/CRings/dist_2a.con".
665 Hint Resolve dist_2a: algebra.
668 inline "cic:/CoRN/algebra/CRings/dist_2b.con".
671 Hint Resolve dist_2b: algebra.
674 inline "cic:/CoRN/algebra/CRings/mult_distr_sum0_lft.con".
677 Hint Resolve mult_distr_sum0_lft.
680 inline "cic:/CoRN/algebra/CRings/mult_distr_sum_lft.con".
683 Hint Resolve mult_distr_sum_lft: algebra.
686 inline "cic:/CoRN/algebra/CRings/mult_distr_sum_rht.con".
688 inline "cic:/CoRN/algebra/CRings/sumx_const.con".
695 Hint Resolve dist_1b dist_2a dist_2b mult_distr_sum_lft mult_distr_sum_rht
700 ** Properties of exponentiation (with the exponent in [nat])
707 Section NExp_properties.
710 inline "cic:/CoRN/algebra/CRings/R.var".
712 inline "cic:/CoRN/algebra/CRings/nexp_wd.con".
714 inline "cic:/CoRN/algebra/CRings/nexp_strext.con".
716 inline "cic:/CoRN/algebra/CRings/nexp_Sn.con".
719 Hint Resolve nexp_wd nexp_Sn: algebra.
722 inline "cic:/CoRN/algebra/CRings/nexp_plus.con".
725 Hint Resolve nexp_plus: algebra.
728 inline "cic:/CoRN/algebra/CRings/one_nexp.con".
731 Hint Resolve one_nexp: algebra.
734 inline "cic:/CoRN/algebra/CRings/mult_nexp.con".
737 Hint Resolve mult_nexp: algebra.
740 inline "cic:/CoRN/algebra/CRings/nexp_mult.con".
743 Hint Resolve nexp_mult: algebra.
746 inline "cic:/CoRN/algebra/CRings/zero_nexp.con".
749 Hint Resolve zero_nexp: algebra.
752 inline "cic:/CoRN/algebra/CRings/inv_nexp_even.con".
755 Hint Resolve inv_nexp_even: algebra.
758 inline "cic:/CoRN/algebra/CRings/inv_nexp_two.con".
761 Hint Resolve inv_nexp_two: algebra.
764 inline "cic:/CoRN/algebra/CRings/inv_nexp_odd.con".
767 Hint Resolve inv_nexp_odd: algebra.
770 inline "cic:/CoRN/algebra/CRings/nexp_one.con".
773 Hint Resolve nexp_one: algebra.
776 inline "cic:/CoRN/algebra/CRings/nexp_two.con".
779 Hint Resolve nexp_two: algebra.
782 inline "cic:/CoRN/algebra/CRings/inv_one_even_nexp.con".
785 Hint Resolve inv_one_even_nexp: algebra.
788 inline "cic:/CoRN/algebra/CRings/inv_one_odd_nexp.con".
791 Hint Resolve inv_one_odd_nexp: algebra.
794 inline "cic:/CoRN/algebra/CRings/square_plus.con".
796 inline "cic:/CoRN/algebra/CRings/square_minus.con".
798 inline "cic:/CoRN/algebra/CRings/nexp_funny.con".
801 Hint Resolve nexp_funny: algebra.
804 inline "cic:/CoRN/algebra/CRings/nexp_funny'.con".
807 Hint Resolve nexp_funny': algebra.
815 Hint Resolve nexp_wd nexp_Sn nexp_plus one_nexp mult_nexp nexp_mult zero_nexp
816 inv_nexp_even inv_nexp_two inv_nexp_odd nexp_one nexp_two nexp_funny
817 inv_one_even_nexp inv_one_odd_nexp nexp_funny' one_nexp square_plus
818 square_minus: algebra.
826 ** Functional Operations
828 Now for partial functions.
831 Let [R] be a ring and let [F,G:(PartFunct R)] with predicates
832 respectively [P] and [Q].
836 inline "cic:/CoRN/algebra/CRings/R.var".
838 inline "cic:/CoRN/algebra/CRings/F.var".
840 inline "cic:/CoRN/algebra/CRings/G.var".
844 inline "cic:/CoRN/algebra/CRings/P.con".
846 inline "cic:/CoRN/algebra/CRings/Q.con".
851 Section Part_Function_Mult.
854 inline "cic:/CoRN/algebra/CRings/part_function_mult_strext.con".
856 inline "cic:/CoRN/algebra/CRings/Fmult.con".
859 End Part_Function_Mult.
863 Section Part_Function_Nth_Power.
866 inline "cic:/CoRN/algebra/CRings/n.var".
868 inline "cic:/CoRN/algebra/CRings/part_function_nth_strext.con".
870 inline "cic:/CoRN/algebra/CRings/Fnth.con".
873 End Part_Function_Nth_Power.
877 %\begin{convention}% Let [R':R->CProp].
881 inline "cic:/CoRN/algebra/CRings/R'.var".
883 inline "cic:/CoRN/algebra/CRings/included_FMult.con".
885 inline "cic:/CoRN/algebra/CRings/included_FMult'.con".
887 inline "cic:/CoRN/algebra/CRings/included_FMult''.con".
889 inline "cic:/CoRN/algebra/CRings/n.var".
891 inline "cic:/CoRN/algebra/CRings/included_FNth.con".
893 inline "cic:/CoRN/algebra/CRings/included_FNth'.con".
899 inline "cic:/CoRN/algebra/CRings/Fscalmult.con".
902 Implicit Arguments Fmult [R].
906 Implicit Arguments Fscalmult [R].
910 Implicit Arguments Fnth [R].
914 Section ScalarMultiplication.
917 inline "cic:/CoRN/algebra/CRings/R.var".
919 inline "cic:/CoRN/algebra/CRings/F.var".
923 inline "cic:/CoRN/algebra/CRings/P.con".
927 inline "cic:/CoRN/algebra/CRings/R'.var".
929 inline "cic:/CoRN/algebra/CRings/included_FScalMult.con".
931 inline "cic:/CoRN/algebra/CRings/included_FScalMult'.con".
934 End ScalarMultiplication.
938 Hint Resolve included_FMult included_FScalMult included_FNth : included.
942 Hint Immediate included_FMult' included_FMult'' included_FScalMult'
943 included_FNth' : included.