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".
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".
95 Notation One := (cr_one _).
100 (* Begin_SpecReals *)
103 %\begin{nameconvention}%
104 In the names of lemmas, we will denote [One] with [one],
105 and [[*]] with [mult].
106 %\end{nameconvention}%
110 Implicit Arguments cr_mult [c].
114 Infix "[*]" := cr_mult (at level 40, left associativity).
123 %\begin{convention}% Let [R] be a ring.
127 alias id "R" = "cic:/CoRN/algebra/CRings/CRing_axioms/R.var".
129 inline "cic:/CoRN/algebra/CRings/CRing_is_CRing.con".
131 inline "cic:/CoRN/algebra/CRings/mult_assoc.con".
133 inline "cic:/CoRN/algebra/CRings/mult_commutes.con".
135 inline "cic:/CoRN/algebra/CRings/mult_mon.con".
139 inline "cic:/CoRN/algebra/CRings/dist.con".
141 inline "cic:/CoRN/algebra/CRings/ring_non_triv.con".
143 inline "cic:/CoRN/algebra/CRings/mult_wd.con".
145 inline "cic:/CoRN/algebra/CRings/mult_wdl.con".
147 inline "cic:/CoRN/algebra/CRings/mult_wdr.con".
149 (* Begin_SpecReals *)
156 Section Ring_constructions
160 ** Ring constructions
166 alias id "R" = "cic:/CoRN/algebra/CRings/Ring_constructions/R.var".
169 The multiplicative monoid of a ring is defined as follows.
172 inline "cic:/CoRN/algebra/CRings/Build_multCMonoid.con".
175 End Ring_constructions
181 Section Ring_unfolded
186 %\begin{convention}% Let [R] be a ring.
190 alias id "R" = "cic:/CoRN/algebra/CRings/Ring_unfolded/R.var".
194 inline "cic:/CoRN/algebra/CRings/Ring_unfolded/mmR.con" "Ring_unfolded__".
198 inline "cic:/CoRN/algebra/CRings/mult_assoc_unfolded.con".
200 inline "cic:/CoRN/algebra/CRings/mult_commut_unfolded.con".
203 Hint Resolve mult_commut_unfolded: algebra.
206 inline "cic:/CoRN/algebra/CRings/mult_one.con".
208 inline "cic:/CoRN/algebra/CRings/one_mult.con".
210 inline "cic:/CoRN/algebra/CRings/ring_dist_unfolded.con".
213 Hint Resolve ring_dist_unfolded: algebra.
216 inline "cic:/CoRN/algebra/CRings/ring_distl_unfolded.con".
223 Hint Resolve mult_assoc_unfolded: algebra.
227 Hint Resolve ring_non_triv mult_one one_mult mult_commut_unfolded: algebra.
231 Hint Resolve ring_dist_unfolded ring_distl_unfolded: algebra.
240 %\begin{convention}% Let [R] be a ring.
244 alias id "R" = "cic:/CoRN/algebra/CRings/Ring_basics/R.var".
246 inline "cic:/CoRN/algebra/CRings/one_ap_zero.con".
248 inline "cic:/CoRN/algebra/CRings/is_zero_rht.con".
250 inline "cic:/CoRN/algebra/CRings/is_zero_lft.con".
253 Implicit Arguments is_zero_rht [S].
257 Implicit Arguments is_zero_lft [S].
260 inline "cic:/CoRN/algebra/CRings/cring_mult_zero.con".
263 Hint Resolve cring_mult_zero: algebra.
266 inline "cic:/CoRN/algebra/CRings/x_mult_zero.con".
268 inline "cic:/CoRN/algebra/CRings/cring_mult_zero_op.con".
271 Hint Resolve cring_mult_zero_op: algebra.
274 inline "cic:/CoRN/algebra/CRings/cring_inv_mult_lft.con".
277 Hint Resolve cring_inv_mult_lft: algebra.
280 inline "cic:/CoRN/algebra/CRings/cring_inv_mult_rht.con".
283 Hint Resolve cring_inv_mult_rht: algebra.
286 inline "cic:/CoRN/algebra/CRings/cring_mult_ap_zero.con".
288 inline "cic:/CoRN/algebra/CRings/cring_mult_ap_zero_op.con".
290 inline "cic:/CoRN/algebra/CRings/inv_mult_invol.con".
292 inline "cic:/CoRN/algebra/CRings/ring_dist_minus.con".
295 Hint Resolve ring_dist_minus: algebra.
298 inline "cic:/CoRN/algebra/CRings/ring_distl_minus.con".
301 Hint Resolve ring_distl_minus: algebra.
309 Hint Resolve cring_mult_zero cring_mult_zero_op: algebra.
313 Hint Resolve inv_mult_invol: algebra.
317 Hint Resolve cring_inv_mult_lft cring_inv_mult_rht: algebra.
321 Hint Resolve ring_dist_minus: algebra.
325 Hint Resolve ring_distl_minus: algebra.
328 (* Begin_SpecReals *)
332 Some auxiliary functions and operations over a ring;
333 especially geared towards CReals.
337 Section exponentiation
347 alias id "R" = "cic:/CoRN/algebra/CRings/exponentiation/R.var".
351 inline "cic:/CoRN/algebra/CRings/nexp.con".
353 inline "cic:/CoRN/algebra/CRings/nexp_well_def.con".
355 inline "cic:/CoRN/algebra/CRings/nexp_strong_ext.con".
357 inline "cic:/CoRN/algebra/CRings/nexp_op.con".
359 (* Begin_SpecReals *)
368 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
372 Implicit Arguments nexp_op [R].
375 (* Begin_SpecReals *)
378 Section nat_injection
382 *** The injection of natural numbers into a ring
383 %\begin{convention}% Let [R] be a ring.
387 alias id "R" = "cic:/CoRN/algebra/CRings/nat_injection/R.var".
390 The injection of Coq natural numbers into a ring is called [nring].
391 Note that this need not really be an injection; when it is, the ring is said
392 to have characteristic [0].
395 inline "cic:/CoRN/algebra/CRings/nring.con".
397 inline "cic:/CoRN/algebra/CRings/Char0.con".
401 inline "cic:/CoRN/algebra/CRings/nring_comm_plus.con".
403 inline "cic:/CoRN/algebra/CRings/nring_comm_mult.con".
405 (* Begin_SpecReals *)
414 Hint Resolve nring_comm_plus nring_comm_mult: algebra.
417 (* Begin_SpecReals *)
420 Implicit Arguments nring [R].
426 Notation Two := (nring 2).
430 Notation Three := (nring 3).
434 Notation Four := (nring 4).
438 Notation Six := (nring 6).
442 Notation Eight := (nring 8).
446 Notation Twelve := (nring 12).
450 Notation Sixteen := (nring 16).
454 Notation Nine := (nring 9).
458 Notation Eighteen := (nring 18).
462 Notation TwentyFour := (nring 24).
466 Notation FortyEight := (nring 48).
469 inline "cic:/CoRN/algebra/CRings/one_plus_one.con".
471 inline "cic:/CoRN/algebra/CRings/x_plus_x.con".
474 Hint Resolve one_plus_one x_plus_x: algebra.
478 In a ring of characteristic zero, [nring] is really an injection.
481 inline "cic:/CoRN/algebra/CRings/nring_different.con".
484 Section int_injection
488 *** The injection of integers into a ring
494 alias id "R" = "cic:/CoRN/algebra/CRings/int_injection/R.var".
497 The injection of Coq integers into a ring is called [zring]. Again,
498 this need not really be an injection.
500 The first definition is now obsolete, having been replaced by a more efficient
501 one. It is kept to avoid having to redo all the proofs.
504 inline "cic:/CoRN/algebra/CRings/zring_old.con".
506 inline "cic:/CoRN/algebra/CRings/zring_old_zero.con".
509 Hint Resolve zring_old_zero: algebra.
512 inline "cic:/CoRN/algebra/CRings/zring_old_diff.con".
515 Hint Resolve zring_old_diff.
518 inline "cic:/CoRN/algebra/CRings/zring_old_plus_nat.con".
521 Hint Resolve zring_old_plus_nat: algebra.
524 inline "cic:/CoRN/algebra/CRings/zring_old_inv_nat.con".
527 Hint Resolve zring_old_inv_nat: algebra.
531 Hint Resolve zring_old_diff: algebra.
534 inline "cic:/CoRN/algebra/CRings/zring_old_plus.con".
537 Hint Resolve zring_old_plus: algebra.
540 inline "cic:/CoRN/algebra/CRings/zring_old_inv.con".
543 Hint Resolve zring_old_inv: algebra.
546 inline "cic:/CoRN/algebra/CRings/zring_old_minus.con".
549 Hint Resolve zring_old_minus: algebra.
552 inline "cic:/CoRN/algebra/CRings/zring_old_mult.con".
555 Hint Resolve zring_old_mult: algebra.
558 inline "cic:/CoRN/algebra/CRings/zring_old_one.con".
561 Hint Resolve zring_old_one: algebra.
564 inline "cic:/CoRN/algebra/CRings/zring_old_inv_one.con".
566 (*#************** new def of zring. ***********************)
568 (*#* The [zring] function can be defined directly. This is done here.
571 inline "cic:/CoRN/algebra/CRings/pring_aux.con".
573 inline "cic:/CoRN/algebra/CRings/pring.con".
575 inline "cic:/CoRN/algebra/CRings/zring.con".
577 inline "cic:/CoRN/algebra/CRings/pring_aux_lemma.con".
579 inline "cic:/CoRN/algebra/CRings/double_nring.con".
582 Hint Resolve pring_aux_lemma double_nring: algebra.
585 inline "cic:/CoRN/algebra/CRings/pring_aux_nring.con".
588 Hint Resolve pring_aux_nring: algebra.
591 inline "cic:/CoRN/algebra/CRings/pring_convert.con".
594 Hint Resolve pring_convert: algebra.
597 inline "cic:/CoRN/algebra/CRings/zring_zring_old.con".
600 Hint Resolve zring_zring_old: algebra.
603 inline "cic:/CoRN/algebra/CRings/zring_zero.con".
605 inline "cic:/CoRN/algebra/CRings/zring_diff.con".
607 inline "cic:/CoRN/algebra/CRings/zring_plus_nat.con".
609 inline "cic:/CoRN/algebra/CRings/zring_inv_nat.con".
611 inline "cic:/CoRN/algebra/CRings/zring_plus.con".
613 inline "cic:/CoRN/algebra/CRings/zring_inv.con".
615 inline "cic:/CoRN/algebra/CRings/zring_minus.con".
617 inline "cic:/CoRN/algebra/CRings/zring_mult.con".
619 inline "cic:/CoRN/algebra/CRings/zring_one.con".
621 inline "cic:/CoRN/algebra/CRings/zring_inv_one.con".
628 Implicit Arguments zring [R].
632 Hint Resolve pring_convert zring_zero zring_diff zring_plus_nat zring_inv_nat
633 zring_plus zring_inv zring_minus zring_mult zring_one zring_inv_one:
643 %\begin{convention}% Let [R] be a ring.
647 alias id "R" = "cic:/CoRN/algebra/CRings/Ring_sums/R.var".
650 *** Infinite Ring sums
654 Section infinite_ring_sums
657 inline "cic:/CoRN/algebra/CRings/Sum_upto.con".
659 inline "cic:/CoRN/algebra/CRings/sum_upto_O.con".
661 inline "cic:/CoRN/algebra/CRings/Sum_from_upto.con".
664 Here's an alternative def of [Sum_from_upto], with a lemma that
665 it's equivalent to the original.
668 inline "cic:/CoRN/algebra/CRings/seq_from.con".
670 inline "cic:/CoRN/algebra/CRings/Sum_from_upto_alt.con".
673 End infinite_ring_sums
677 Section ring_sums_over_lists
680 (*#* *** Ring Sums over Lists
683 inline "cic:/CoRN/algebra/CRings/RList_Mem.con".
685 inline "cic:/CoRN/algebra/CRings/List_Sum_upto.con".
687 inline "cic:/CoRN/algebra/CRings/list_sum_upto_O.con".
689 inline "cic:/CoRN/algebra/CRings/List_Sum_from_upto.con".
692 End ring_sums_over_lists
700 ** Distribution properties
707 Section Dist_properties
710 alias id "R" = "cic:/CoRN/algebra/CRings/Dist_properties/R.var".
712 inline "cic:/CoRN/algebra/CRings/dist_1b.con".
715 Hint Resolve dist_1b: algebra.
718 inline "cic:/CoRN/algebra/CRings/dist_2a.con".
721 Hint Resolve dist_2a: algebra.
724 inline "cic:/CoRN/algebra/CRings/dist_2b.con".
727 Hint Resolve dist_2b: algebra.
730 inline "cic:/CoRN/algebra/CRings/mult_distr_sum0_lft.con".
733 Hint Resolve mult_distr_sum0_lft.
736 inline "cic:/CoRN/algebra/CRings/mult_distr_sum_lft.con".
739 Hint Resolve mult_distr_sum_lft: algebra.
742 inline "cic:/CoRN/algebra/CRings/mult_distr_sum_rht.con".
744 inline "cic:/CoRN/algebra/CRings/sumx_const.con".
751 Hint Resolve dist_1b dist_2a dist_2b mult_distr_sum_lft mult_distr_sum_rht
756 ** Properties of exponentiation (with the exponent in [nat])
763 Section NExp_properties
766 alias id "R" = "cic:/CoRN/algebra/CRings/NExp_properties/R.var".
768 inline "cic:/CoRN/algebra/CRings/nexp_wd.con".
770 inline "cic:/CoRN/algebra/CRings/nexp_strext.con".
772 inline "cic:/CoRN/algebra/CRings/nexp_Sn.con".
775 Hint Resolve nexp_wd nexp_Sn: algebra.
778 inline "cic:/CoRN/algebra/CRings/nexp_plus.con".
781 Hint Resolve nexp_plus: algebra.
784 inline "cic:/CoRN/algebra/CRings/one_nexp.con".
787 Hint Resolve one_nexp: algebra.
790 inline "cic:/CoRN/algebra/CRings/mult_nexp.con".
793 Hint Resolve mult_nexp: algebra.
796 inline "cic:/CoRN/algebra/CRings/nexp_mult.con".
799 Hint Resolve nexp_mult: algebra.
802 inline "cic:/CoRN/algebra/CRings/zero_nexp.con".
805 Hint Resolve zero_nexp: algebra.
808 inline "cic:/CoRN/algebra/CRings/inv_nexp_even.con".
811 Hint Resolve inv_nexp_even: algebra.
814 inline "cic:/CoRN/algebra/CRings/inv_nexp_two.con".
817 Hint Resolve inv_nexp_two: algebra.
820 inline "cic:/CoRN/algebra/CRings/inv_nexp_odd.con".
823 Hint Resolve inv_nexp_odd: algebra.
826 inline "cic:/CoRN/algebra/CRings/nexp_one.con".
829 Hint Resolve nexp_one: algebra.
832 inline "cic:/CoRN/algebra/CRings/nexp_two.con".
835 Hint Resolve nexp_two: algebra.
838 inline "cic:/CoRN/algebra/CRings/inv_one_even_nexp.con".
841 Hint Resolve inv_one_even_nexp: algebra.
844 inline "cic:/CoRN/algebra/CRings/inv_one_odd_nexp.con".
847 Hint Resolve inv_one_odd_nexp: algebra.
850 inline "cic:/CoRN/algebra/CRings/square_plus.con".
852 inline "cic:/CoRN/algebra/CRings/square_minus.con".
854 inline "cic:/CoRN/algebra/CRings/nexp_funny.con".
857 Hint Resolve nexp_funny: algebra.
860 inline "cic:/CoRN/algebra/CRings/nexp_funny'.con".
863 Hint Resolve nexp_funny': algebra.
871 Hint Resolve nexp_wd nexp_Sn nexp_plus one_nexp mult_nexp nexp_mult zero_nexp
872 inv_nexp_even inv_nexp_two inv_nexp_odd nexp_one nexp_two nexp_funny
873 inv_one_even_nexp inv_one_odd_nexp nexp_funny' one_nexp square_plus
874 square_minus: algebra.
882 ** Functional Operations
884 Now for partial functions.
887 Let [R] be a ring and let [F,G:(PartFunct R)] with predicates
888 respectively [P] and [Q].
892 alias id "R" = "cic:/CoRN/algebra/CRings/CRing_Ops/R.var".
894 alias id "F" = "cic:/CoRN/algebra/CRings/CRing_Ops/F.var".
896 alias id "G" = "cic:/CoRN/algebra/CRings/CRing_Ops/G.var".
900 inline "cic:/CoRN/algebra/CRings/CRing_Ops/P.con" "CRing_Ops__".
902 inline "cic:/CoRN/algebra/CRings/CRing_Ops/Q.con" "CRing_Ops__".
907 Section Part_Function_Mult
910 inline "cic:/CoRN/algebra/CRings/part_function_mult_strext.con".
912 inline "cic:/CoRN/algebra/CRings/Fmult.con".
915 End Part_Function_Mult
919 Section Part_Function_Nth_Power
922 alias id "n" = "cic:/CoRN/algebra/CRings/CRing_Ops/Part_Function_Nth_Power/n.var".
924 inline "cic:/CoRN/algebra/CRings/part_function_nth_strext.con".
926 inline "cic:/CoRN/algebra/CRings/Fnth.con".
929 End Part_Function_Nth_Power
933 %\begin{convention}% Let [R':R->CProp].
937 alias id "R'" = "cic:/CoRN/algebra/CRings/CRing_Ops/R'.var".
939 inline "cic:/CoRN/algebra/CRings/included_FMult.con".
941 inline "cic:/CoRN/algebra/CRings/included_FMult'.con".
943 inline "cic:/CoRN/algebra/CRings/included_FMult''.con".
945 alias id "n" = "cic:/CoRN/algebra/CRings/CRing_Ops/n.var".
947 inline "cic:/CoRN/algebra/CRings/included_FNth.con".
949 inline "cic:/CoRN/algebra/CRings/included_FNth'.con".
955 inline "cic:/CoRN/algebra/CRings/Fscalmult.con".
958 Implicit Arguments Fmult [R].
962 Infix "{*}" := Fmult (at level 40, left associativity).
966 Implicit Arguments Fscalmult [R].
970 Infix "{**}" := Fscalmult (at level 40, left associativity).
974 Implicit Arguments Fnth [R].
978 Infix "{^}" := Fnth (at level 30, right associativity).
982 Section ScalarMultiplication
985 alias id "R" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/R.var".
987 alias id "F" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/F.var".
991 inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/P.con" "ScalarMultiplication__".
995 alias id "R'" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/R'.var".
997 inline "cic:/CoRN/algebra/CRings/included_FScalMult.con".
999 inline "cic:/CoRN/algebra/CRings/included_FScalMult'.con".
1002 End ScalarMultiplication
1006 Hint Resolve included_FMult included_FScalMult included_FNth : included.
1010 Hint Immediate included_FMult' included_FMult'' included_FScalMult'
1011 included_FNth' : included.