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: CRings.v,v 1.8 2004/04/23 10:00:53 lcf Exp $ *)
21 (*#* printing [*] %\ensuremath\times% #×# *)
23 (*#* printing [^] %\ensuremath{\hat{\ }}% #^# *)
25 (*#* printing {*} %\ensuremath\times% #×# *)
27 (*#* printing {**} %\ensuremath\ast% #∗# *)
29 (*#* printing {^} %\ensuremath{\hat{\ }}% #^# *)
31 (*#* printing One %\ensuremath{\mathbf1}% #1# *)
33 (*#* printing Two %\ensuremath{\mathbf2}% #2# *)
35 (*#* printing Three %\ensuremath{\mathbf3}% #3# *)
37 (*#* printing Four %\ensuremath{\mathbf4}% #4# *)
39 (*#* printing Six %\ensuremath{\mathbf6}% #6# *)
41 (*#* printing Eight %\ensuremath{\mathbf8}% #8# *)
43 (*#* printing Nine %\ensuremath{\mathbf9}% #9# *)
45 (*#* printing Twelve %\ensuremath{\mathbf{12}}% #12# *)
47 (*#* printing Sixteen %\ensuremath{\mathbf{16}}% #16# *)
49 (*#* printing Eighteen %\ensuremath{\mathbf{18}}% #18# *)
51 (*#* printing TwentyFour %\ensuremath{\mathbf{24}}% #24# *)
53 (*#* printing FortyEight %\ensuremath{\mathbf{48}}% #48# *)
55 include "algebra/CSums.ma".
67 (* Constructive RINGS *)
70 We actually define commutative rings with identity.
71 ** Definition of the notion of Ring
74 inline procedural "cic:/CoRN/algebra/CRings/distributive.con" as definition.
77 Implicit Arguments distributive [S].
80 inline procedural "cic:/CoRN/algebra/CRings/is_CRing.ind".
82 inline procedural "cic:/CoRN/algebra/CRings/CRing.ind".
85 cic:/matita/CoRN-Procedural/algebra/CRings/cr_crr.con
88 inline procedural "cic:/CoRN/algebra/CRings/cr_plus.con" as definition.
90 inline procedural "cic:/CoRN/algebra/CRings/cr_inv.con" as definition.
92 inline procedural "cic:/CoRN/algebra/CRings/cr_minus.con" as definition.
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.
128 cic:/CoRN/algebra/CRings/CRing_axioms/R.var
131 inline procedural "cic:/CoRN/algebra/CRings/CRing_is_CRing.con" as lemma.
133 inline procedural "cic:/CoRN/algebra/CRings/mult_assoc.con" as lemma.
135 inline procedural "cic:/CoRN/algebra/CRings/mult_commutes.con" as lemma.
137 inline procedural "cic:/CoRN/algebra/CRings/mult_mon.con" as lemma.
141 inline procedural "cic:/CoRN/algebra/CRings/dist.con" as lemma.
143 inline procedural "cic:/CoRN/algebra/CRings/ring_non_triv.con" as lemma.
145 inline procedural "cic:/CoRN/algebra/CRings/mult_wd.con" as lemma.
147 inline procedural "cic:/CoRN/algebra/CRings/mult_wdl.con" as lemma.
149 inline procedural "cic:/CoRN/algebra/CRings/mult_wdr.con" as lemma.
151 (* Begin_SpecReals *)
158 Section Ring_constructions
162 ** Ring constructions
169 cic:/CoRN/algebra/CRings/Ring_constructions/R.var
173 The multiplicative monoid of a ring is defined as follows.
176 inline procedural "cic:/CoRN/algebra/CRings/Build_multCMonoid.con" as definition.
179 End Ring_constructions
185 Section Ring_unfolded
190 %\begin{convention}% Let [R] be a ring.
195 cic:/CoRN/algebra/CRings/Ring_unfolded/R.var
200 inline procedural "cic:/CoRN/algebra/CRings/Ring_unfolded/mmR.con" "Ring_unfolded__" as definition.
204 inline procedural "cic:/CoRN/algebra/CRings/mult_assoc_unfolded.con" as lemma.
206 inline procedural "cic:/CoRN/algebra/CRings/mult_commut_unfolded.con" as lemma.
209 Hint Resolve mult_commut_unfolded: algebra.
212 inline procedural "cic:/CoRN/algebra/CRings/mult_one.con" as lemma.
214 inline procedural "cic:/CoRN/algebra/CRings/one_mult.con" as lemma.
216 inline procedural "cic:/CoRN/algebra/CRings/ring_dist_unfolded.con" as lemma.
219 Hint Resolve ring_dist_unfolded: algebra.
222 inline procedural "cic:/CoRN/algebra/CRings/ring_distl_unfolded.con" as lemma.
229 Hint Resolve mult_assoc_unfolded: algebra.
233 Hint Resolve ring_non_triv mult_one one_mult mult_commut_unfolded: algebra.
237 Hint Resolve ring_dist_unfolded ring_distl_unfolded: algebra.
246 %\begin{convention}% Let [R] be a ring.
251 cic:/CoRN/algebra/CRings/Ring_basics/R.var
254 inline procedural "cic:/CoRN/algebra/CRings/one_ap_zero.con" as lemma.
256 inline procedural "cic:/CoRN/algebra/CRings/is_zero_rht.con" as definition.
258 inline procedural "cic:/CoRN/algebra/CRings/is_zero_lft.con" as definition.
261 Implicit Arguments is_zero_rht [S].
265 Implicit Arguments is_zero_lft [S].
268 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_zero.con" as lemma.
271 Hint Resolve cring_mult_zero: algebra.
274 inline procedural "cic:/CoRN/algebra/CRings/x_mult_zero.con" as lemma.
276 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_zero_op.con" as lemma.
279 Hint Resolve cring_mult_zero_op: algebra.
282 inline procedural "cic:/CoRN/algebra/CRings/cring_inv_mult_lft.con" as lemma.
285 Hint Resolve cring_inv_mult_lft: algebra.
288 inline procedural "cic:/CoRN/algebra/CRings/cring_inv_mult_rht.con" as lemma.
291 Hint Resolve cring_inv_mult_rht: algebra.
294 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_ap_zero.con" as lemma.
296 inline procedural "cic:/CoRN/algebra/CRings/cring_mult_ap_zero_op.con" as lemma.
298 inline procedural "cic:/CoRN/algebra/CRings/inv_mult_invol.con" as lemma.
300 inline procedural "cic:/CoRN/algebra/CRings/ring_dist_minus.con" as lemma.
303 Hint Resolve ring_dist_minus: algebra.
306 inline procedural "cic:/CoRN/algebra/CRings/ring_distl_minus.con" as lemma.
309 Hint Resolve ring_distl_minus: algebra.
317 Hint Resolve cring_mult_zero cring_mult_zero_op: algebra.
321 Hint Resolve inv_mult_invol: algebra.
325 Hint Resolve cring_inv_mult_lft cring_inv_mult_rht: algebra.
329 Hint Resolve ring_dist_minus: algebra.
333 Hint Resolve ring_distl_minus: algebra.
336 (* Begin_SpecReals *)
340 Some auxiliary functions and operations over a ring;
341 especially geared towards CReals.
345 Section exponentiation
356 cic:/CoRN/algebra/CRings/exponentiation/R.var
361 inline procedural "cic:/CoRN/algebra/CRings/nexp.con" as definition.
363 inline procedural "cic:/CoRN/algebra/CRings/nexp_well_def.con" as lemma.
365 inline procedural "cic:/CoRN/algebra/CRings/nexp_strong_ext.con" as lemma.
367 inline procedural "cic:/CoRN/algebra/CRings/nexp_op.con" as definition.
369 (* Begin_SpecReals *)
378 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
382 Implicit Arguments nexp_op [R].
385 (* Begin_SpecReals *)
388 Section nat_injection
392 *** The injection of natural numbers into a ring
393 %\begin{convention}% Let [R] be a ring.
398 cic:/CoRN/algebra/CRings/nat_injection/R.var
402 The injection of Coq natural numbers into a ring is called [nring].
403 Note that this need not really be an injection; when it is, the ring is said
404 to have characteristic [0].
407 inline procedural "cic:/CoRN/algebra/CRings/nring.con" as definition.
409 inline procedural "cic:/CoRN/algebra/CRings/Char0.con" as definition.
413 inline procedural "cic:/CoRN/algebra/CRings/nring_comm_plus.con" as lemma.
415 inline procedural "cic:/CoRN/algebra/CRings/nring_comm_mult.con" as lemma.
417 (* Begin_SpecReals *)
426 Hint Resolve nring_comm_plus nring_comm_mult: algebra.
429 (* Begin_SpecReals *)
432 Implicit Arguments nring [R].
438 Notation Two := (nring 2).
442 Notation Three := (nring 3).
446 Notation Four := (nring 4).
450 Notation Six := (nring 6).
454 Notation Eight := (nring 8).
458 Notation Twelve := (nring 12).
462 Notation Sixteen := (nring 16).
466 Notation Nine := (nring 9).
470 Notation Eighteen := (nring 18).
474 Notation TwentyFour := (nring 24).
478 Notation FortyEight := (nring 48).
481 inline procedural "cic:/CoRN/algebra/CRings/one_plus_one.con" as lemma.
483 inline procedural "cic:/CoRN/algebra/CRings/x_plus_x.con" as lemma.
486 Hint Resolve one_plus_one x_plus_x: algebra.
490 In a ring of characteristic zero, [nring] is really an injection.
493 inline procedural "cic:/CoRN/algebra/CRings/nring_different.con" as lemma.
496 Section int_injection
500 *** The injection of integers into a ring
507 cic:/CoRN/algebra/CRings/int_injection/R.var
511 The injection of Coq integers into a ring is called [zring]. Again,
512 this need not really be an injection.
514 The first definition is now obsolete, having been replaced by a more efficient
515 one. It is kept to avoid having to redo all the proofs.
518 inline procedural "cic:/CoRN/algebra/CRings/zring_old.con" as definition.
520 inline procedural "cic:/CoRN/algebra/CRings/zring_old_zero.con" as lemma.
523 Hint Resolve zring_old_zero: algebra.
526 inline procedural "cic:/CoRN/algebra/CRings/zring_old_diff.con" as lemma.
529 Hint Resolve zring_old_diff.
532 inline procedural "cic:/CoRN/algebra/CRings/zring_old_plus_nat.con" as lemma.
535 Hint Resolve zring_old_plus_nat: algebra.
538 inline procedural "cic:/CoRN/algebra/CRings/zring_old_inv_nat.con" as lemma.
541 Hint Resolve zring_old_inv_nat: algebra.
545 Hint Resolve zring_old_diff: algebra.
548 inline procedural "cic:/CoRN/algebra/CRings/zring_old_plus.con" as lemma.
551 Hint Resolve zring_old_plus: algebra.
554 inline procedural "cic:/CoRN/algebra/CRings/zring_old_inv.con" as lemma.
557 Hint Resolve zring_old_inv: algebra.
560 inline procedural "cic:/CoRN/algebra/CRings/zring_old_minus.con" as lemma.
563 Hint Resolve zring_old_minus: algebra.
566 inline procedural "cic:/CoRN/algebra/CRings/zring_old_mult.con" as lemma.
569 Hint Resolve zring_old_mult: algebra.
572 inline procedural "cic:/CoRN/algebra/CRings/zring_old_one.con" as lemma.
575 Hint Resolve zring_old_one: algebra.
578 inline procedural "cic:/CoRN/algebra/CRings/zring_old_inv_one.con" as lemma.
580 (*#************** new def of zring. ***********************)
582 (*#* The [zring] function can be defined directly. This is done here.
585 inline procedural "cic:/CoRN/algebra/CRings/pring_aux.con" as definition.
587 inline procedural "cic:/CoRN/algebra/CRings/pring.con" as definition.
589 inline procedural "cic:/CoRN/algebra/CRings/zring.con" as definition.
591 inline procedural "cic:/CoRN/algebra/CRings/pring_aux_lemma.con" as lemma.
593 inline procedural "cic:/CoRN/algebra/CRings/double_nring.con" as lemma.
596 Hint Resolve pring_aux_lemma double_nring: algebra.
599 inline procedural "cic:/CoRN/algebra/CRings/pring_aux_nring.con" as lemma.
602 Hint Resolve pring_aux_nring: algebra.
605 inline procedural "cic:/CoRN/algebra/CRings/pring_convert.con" as lemma.
608 Hint Resolve pring_convert: algebra.
611 inline procedural "cic:/CoRN/algebra/CRings/zring_zring_old.con" as lemma.
614 Hint Resolve zring_zring_old: algebra.
617 inline procedural "cic:/CoRN/algebra/CRings/zring_zero.con" as lemma.
619 inline procedural "cic:/CoRN/algebra/CRings/zring_diff.con" as lemma.
621 inline procedural "cic:/CoRN/algebra/CRings/zring_plus_nat.con" as lemma.
623 inline procedural "cic:/CoRN/algebra/CRings/zring_inv_nat.con" as lemma.
625 inline procedural "cic:/CoRN/algebra/CRings/zring_plus.con" as lemma.
627 inline procedural "cic:/CoRN/algebra/CRings/zring_inv.con" as lemma.
629 inline procedural "cic:/CoRN/algebra/CRings/zring_minus.con" as lemma.
631 inline procedural "cic:/CoRN/algebra/CRings/zring_mult.con" as lemma.
633 inline procedural "cic:/CoRN/algebra/CRings/zring_one.con" as lemma.
635 inline procedural "cic:/CoRN/algebra/CRings/zring_inv_one.con" as lemma.
642 Implicit Arguments zring [R].
646 Hint Resolve pring_convert zring_zero zring_diff zring_plus_nat zring_inv_nat
647 zring_plus zring_inv zring_minus zring_mult zring_one zring_inv_one:
657 %\begin{convention}% Let [R] be a ring.
662 cic:/CoRN/algebra/CRings/Ring_sums/R.var
666 *** Infinite Ring sums
670 Section infinite_ring_sums
673 inline procedural "cic:/CoRN/algebra/CRings/Sum_upto.con" as definition.
675 inline procedural "cic:/CoRN/algebra/CRings/sum_upto_O.con" as lemma.
677 inline procedural "cic:/CoRN/algebra/CRings/Sum_from_upto.con" as definition.
680 Here's an alternative def of [Sum_from_upto], with a lemma that
681 it's equivalent to the original.
684 inline procedural "cic:/CoRN/algebra/CRings/seq_from.con" as definition.
686 inline procedural "cic:/CoRN/algebra/CRings/Sum_from_upto_alt.con" as definition.
689 End infinite_ring_sums
693 Section ring_sums_over_lists
696 (*#* *** Ring Sums over Lists
699 inline procedural "cic:/CoRN/algebra/CRings/RList_Mem.con" as definition.
701 inline procedural "cic:/CoRN/algebra/CRings/List_Sum_upto.con" as definition.
703 inline procedural "cic:/CoRN/algebra/CRings/list_sum_upto_O.con" as lemma.
705 inline procedural "cic:/CoRN/algebra/CRings/List_Sum_from_upto.con" as definition.
708 End ring_sums_over_lists
716 ** Distribution properties
723 Section Dist_properties
727 cic:/CoRN/algebra/CRings/Dist_properties/R.var
730 inline procedural "cic:/CoRN/algebra/CRings/dist_1b.con" as lemma.
733 Hint Resolve dist_1b: algebra.
736 inline procedural "cic:/CoRN/algebra/CRings/dist_2a.con" as lemma.
739 Hint Resolve dist_2a: algebra.
742 inline procedural "cic:/CoRN/algebra/CRings/dist_2b.con" as lemma.
745 Hint Resolve dist_2b: algebra.
748 inline procedural "cic:/CoRN/algebra/CRings/mult_distr_sum0_lft.con" as lemma.
751 Hint Resolve mult_distr_sum0_lft.
754 inline procedural "cic:/CoRN/algebra/CRings/mult_distr_sum_lft.con" as lemma.
757 Hint Resolve mult_distr_sum_lft: algebra.
760 inline procedural "cic:/CoRN/algebra/CRings/mult_distr_sum_rht.con" as lemma.
762 inline procedural "cic:/CoRN/algebra/CRings/sumx_const.con" as lemma.
769 Hint Resolve dist_1b dist_2a dist_2b mult_distr_sum_lft mult_distr_sum_rht
774 ** Properties of exponentiation (with the exponent in [nat])
781 Section NExp_properties
785 cic:/CoRN/algebra/CRings/NExp_properties/R.var
788 inline procedural "cic:/CoRN/algebra/CRings/nexp_wd.con" as lemma.
790 inline procedural "cic:/CoRN/algebra/CRings/nexp_strext.con" as lemma.
792 inline procedural "cic:/CoRN/algebra/CRings/nexp_Sn.con" as lemma.
795 Hint Resolve nexp_wd nexp_Sn: algebra.
798 inline procedural "cic:/CoRN/algebra/CRings/nexp_plus.con" as lemma.
801 Hint Resolve nexp_plus: algebra.
804 inline procedural "cic:/CoRN/algebra/CRings/one_nexp.con" as lemma.
807 Hint Resolve one_nexp: algebra.
810 inline procedural "cic:/CoRN/algebra/CRings/mult_nexp.con" as lemma.
813 Hint Resolve mult_nexp: algebra.
816 inline procedural "cic:/CoRN/algebra/CRings/nexp_mult.con" as lemma.
819 Hint Resolve nexp_mult: algebra.
822 inline procedural "cic:/CoRN/algebra/CRings/zero_nexp.con" as lemma.
825 Hint Resolve zero_nexp: algebra.
828 inline procedural "cic:/CoRN/algebra/CRings/inv_nexp_even.con" as lemma.
831 Hint Resolve inv_nexp_even: algebra.
834 inline procedural "cic:/CoRN/algebra/CRings/inv_nexp_two.con" as lemma.
837 Hint Resolve inv_nexp_two: algebra.
840 inline procedural "cic:/CoRN/algebra/CRings/inv_nexp_odd.con" as lemma.
843 Hint Resolve inv_nexp_odd: algebra.
846 inline procedural "cic:/CoRN/algebra/CRings/nexp_one.con" as lemma.
849 Hint Resolve nexp_one: algebra.
852 inline procedural "cic:/CoRN/algebra/CRings/nexp_two.con" as lemma.
855 Hint Resolve nexp_two: algebra.
858 inline procedural "cic:/CoRN/algebra/CRings/inv_one_even_nexp.con" as lemma.
861 Hint Resolve inv_one_even_nexp: algebra.
864 inline procedural "cic:/CoRN/algebra/CRings/inv_one_odd_nexp.con" as lemma.
867 Hint Resolve inv_one_odd_nexp: algebra.
870 inline procedural "cic:/CoRN/algebra/CRings/square_plus.con" as lemma.
872 inline procedural "cic:/CoRN/algebra/CRings/square_minus.con" as lemma.
874 inline procedural "cic:/CoRN/algebra/CRings/nexp_funny.con" as lemma.
877 Hint Resolve nexp_funny: algebra.
880 inline procedural "cic:/CoRN/algebra/CRings/nexp_funny'.con" as lemma.
883 Hint Resolve nexp_funny': algebra.
891 Hint Resolve nexp_wd nexp_Sn nexp_plus one_nexp mult_nexp nexp_mult zero_nexp
892 inv_nexp_even inv_nexp_two inv_nexp_odd nexp_one nexp_two nexp_funny
893 inv_one_even_nexp inv_one_odd_nexp nexp_funny' one_nexp square_plus
894 square_minus: algebra.
902 ** Functional Operations
904 Now for partial functions.
907 Let [R] be a ring and let [F,G:(PartFunct R)] with predicates
908 respectively [P] and [Q].
913 cic:/CoRN/algebra/CRings/CRing_Ops/R.var
917 cic:/CoRN/algebra/CRings/CRing_Ops/F.var
921 cic:/CoRN/algebra/CRings/CRing_Ops/G.var
926 inline procedural "cic:/CoRN/algebra/CRings/CRing_Ops/P.con" "CRing_Ops__" as definition.
928 inline procedural "cic:/CoRN/algebra/CRings/CRing_Ops/Q.con" "CRing_Ops__" as definition.
933 Section Part_Function_Mult
936 inline procedural "cic:/CoRN/algebra/CRings/part_function_mult_strext.con" as lemma.
938 inline procedural "cic:/CoRN/algebra/CRings/Fmult.con" as definition.
941 End Part_Function_Mult
945 Section Part_Function_Nth_Power
949 cic:/CoRN/algebra/CRings/CRing_Ops/Part_Function_Nth_Power/n.var
952 inline procedural "cic:/CoRN/algebra/CRings/part_function_nth_strext.con" as lemma.
954 inline procedural "cic:/CoRN/algebra/CRings/Fnth.con" as definition.
957 End Part_Function_Nth_Power
961 %\begin{convention}% Let [R':R->CProp].
966 cic:/CoRN/algebra/CRings/CRing_Ops/R'.var
969 inline procedural "cic:/CoRN/algebra/CRings/included_FMult.con" as lemma.
971 inline procedural "cic:/CoRN/algebra/CRings/included_FMult'.con" as lemma.
973 inline procedural "cic:/CoRN/algebra/CRings/included_FMult''.con" as lemma.
976 cic:/CoRN/algebra/CRings/CRing_Ops/n.var
979 inline procedural "cic:/CoRN/algebra/CRings/included_FNth.con" as lemma.
981 inline procedural "cic:/CoRN/algebra/CRings/included_FNth'.con" as lemma.
987 inline procedural "cic:/CoRN/algebra/CRings/Fscalmult.con" as definition.
990 Implicit Arguments Fmult [R].
994 Infix "{*}" := Fmult (at level 40, left associativity).
998 Implicit Arguments Fscalmult [R].
1002 Infix "{**}" := Fscalmult (at level 40, left associativity).
1006 Implicit Arguments Fnth [R].
1010 Infix "{^}" := Fnth (at level 30, right associativity).
1014 Section ScalarMultiplication
1018 cic:/CoRN/algebra/CRings/ScalarMultiplication/R.var
1022 cic:/CoRN/algebra/CRings/ScalarMultiplication/F.var
1027 inline procedural "cic:/CoRN/algebra/CRings/ScalarMultiplication/P.con" "ScalarMultiplication__" as definition.
1032 cic:/CoRN/algebra/CRings/ScalarMultiplication/R'.var
1035 inline procedural "cic:/CoRN/algebra/CRings/included_FScalMult.con" as lemma.
1037 inline procedural "cic:/CoRN/algebra/CRings/included_FScalMult'.con" as lemma.
1040 End ScalarMultiplication
1044 Hint Resolve included_FMult included_FScalMult included_FNth : included.
1048 Hint Immediate included_FMult' included_FMult'' included_FScalMult'
1049 included_FNth' : included.