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