]> matita.cs.unibo.it Git - helm.git/blob - matita/dama/rings.ma
closed all axioms
[helm.git] / matita / dama / rings.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/rings/".
16
17 include "groups.ma".
18
19 record is_ring (G:abelian_group) (mult:G→G→G) (one:G) : Prop
20
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;
25     (* ring properties *)
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)
29  }.
30  
31 record ring : Type \def
32  { r_abelian_group:> abelian_group;
33    mult: r_abelian_group → r_abelian_group → r_abelian_group;
34    one: r_abelian_group;
35    r_ring_properties: is_ring r_abelian_group mult one
36  }.
37
38 theorem mult_assoc: ∀R:ring.associative ? (mult R).
39  intros;
40  apply (mult_assoc_ ? ? ? (r_ring_properties R)).
41 qed.
42
43 theorem one_neutral_left: ∀R:ring.left_neutral ? (mult R) (one R).
44  intros;
45  apply (one_neutral_left_ ? ? ? (r_ring_properties R)).
46 qed.
47
48 theorem one_neutral_right: ∀R:ring.right_neutral ? (mult R) (one R).
49  intros;
50  apply (one_neutral_right_ ? ? ? (r_ring_properties R)).
51 qed.
52
53 theorem mult_plus_distr_left: ∀R:ring.distributive_left ? (mult R) (plus R).
54  intros;
55  apply (mult_plus_distr_left_ ? ? ? (r_ring_properties R)).
56 qed.
57
58 theorem mult_plus_distr_right: ∀R:ring.distributive_right ? (mult R) (plus R).
59  intros;
60  apply (mult_plus_distr_right_ ? ? ? (r_ring_properties R)).
61 qed.
62
63 theorem not_eq_zero_one: ∀R:ring.0 ≠ one R.
64  intros;
65  apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)).
66 qed.
67
68 interpretation "Ring mult" 'times a b =
69  (cic:/matita/rings/mult.con _ a b).
70
71 notation "1" with precedence 89
72 for @{ 'one }.
73
74 interpretation "Ring one" 'one =
75  (cic:/matita/rings/one.con _).
76
77 lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
78  intros;
79  generalize in match (zero_neutral R 0); intro;
80  generalize in match (eq_f ? ? (λy.y*x) ? ? H); intro; clear H;
81  rewrite > mult_plus_distr_right in H1;
82  generalize in match (eq_f ? ? (λy.-(0*x)+y) ? ? H1); intro; clear H1;
83  rewrite < plus_assoc in H;
84  rewrite > opp_inverse in H;
85  rewrite > zero_neutral in H;
86  assumption.
87 qed.
88
89 lemma eq_mult_x_zero_zero: ∀R:ring.∀x:R.x*0=0.
90 intros;
91 generalize in match (zero_neutral R 0);
92 intro;
93 generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H;
94 (*CSC: qua funzionava prima della patch all'unificazione!*)
95 rewrite > (mult_plus_distr_left R) in H1;
96 generalize in match (eq_f ? ? (λy. (-(x*0)) +y) ? ? H1);intro;
97 clear H1;
98 rewrite < plus_assoc in H;
99 rewrite > opp_inverse in H;
100 rewrite > zero_neutral in H;
101 assumption.
102 qed.
103