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 (**************************************************************************)
19 record is_ring (G:abelian_group) (mult:G→G→G) (one:G) : Prop
21 { (* multiplicative monoid properties *)
22 mult_assoc_: associative ? mult;
23 one_neutral_left_: left_neutral ? mult one;
24 one_neutral_right_: right_neutral ? mult one;
26 mult_plus_distr_left_: distributive_left ? mult (plus G);
27 mult_plus_distr_right_: distributive_right ? mult (plus G);
28 not_eq_zero_one_: (0 ≠ one)
31 record ring : Type \def
32 { r_abelian_group:> abelian_group;
33 mult: r_abelian_group → r_abelian_group → r_abelian_group;
35 r_ring_properties: is_ring r_abelian_group mult one
38 theorem mult_assoc: ∀R:ring.associative ? (mult R).
40 apply (mult_assoc_ ? ? ? (r_ring_properties R)).
43 theorem one_neutral_left: ∀R:ring.left_neutral ? (mult R) (one R).
45 apply (one_neutral_left_ ? ? ? (r_ring_properties R)).
48 theorem one_neutral_right: ∀R:ring.right_neutral ? (mult R) (one R).
50 apply (one_neutral_right_ ? ? ? (r_ring_properties R)).
53 theorem mult_plus_distr_left: ∀R:ring.distributive_left ? (mult R) (plus R).
55 apply (mult_plus_distr_left_ ? ? ? (r_ring_properties R)).
58 theorem mult_plus_distr_right: ∀R:ring.distributive_right ? (mult R) (plus R).
60 apply (mult_plus_distr_right_ ? ? ? (r_ring_properties R)).
63 theorem not_eq_zero_one: ∀R:ring.0 ≠ one R.
65 apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)).
68 interpretation "Ring mult" 'times a b = (mult ? a b).
70 notation "1" with precedence 89
73 interpretation "Ring one" 'one = (one ?).
75 lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
77 generalize in match (zero_neutral R 0); intro;
78 generalize in match (eq_f ? ? (λy.y*x) ? ? H); intro; clear H;
79 rewrite > mult_plus_distr_right in H1;
80 generalize in match (eq_f ? ? (λy.-(0*x)+y) ? ? H1); intro; clear H1;
81 rewrite < plus_assoc in H;
82 rewrite > opp_inverse in H;
83 rewrite > zero_neutral in H;
87 lemma eq_mult_x_zero_zero: ∀R:ring.∀x:R.x*0=0.
89 generalize in match (zero_neutral R 0);
91 generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H;
92 (*CSC: qua funzionava prima della patch all'unificazione!*)
93 rewrite > (mult_plus_distr_left R) in H1;
94 generalize in match (eq_f ? ? (λy. (-(x*0)) +y) ? ? H1);intro;
96 rewrite < plus_assoc in H;
97 rewrite > opp_inverse in H;
98 rewrite > zero_neutral in H;