<commit_before>/-
Copyright (c) 2014 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: algebra.ring
Authors: <NAME>, <NAME>

Structures with multiplicative and additive components, including semirings, rings, and fields.
The development is modeled after Isabelle's library.
-/

import logic.eq logic.connectives data.unit data.sigma data.prod
import algebra.function algebra.binary algebra.group
open eq eq.ops

namespace algebra

variable {A : Type}

/- auxiliary classes -/

structure distrib [class] (A : Type) extends has_mul A, has_add A :=
(left_distrib : ∀a b c, mul a (add b c) = add (mul a b) (mul a c))
(right_distrib : ∀a b c, mul (add a b) c = add (mul a c) (mul b c))

theorem left_distrib [s : distrib A] (a b c : A) : a * (b + c) = a * b + a * c :=
!distrib.left_distrib

theorem right_distrib [s: distrib A] (a b c : A) : (a + b) * c = a * c + b * c :=
!distrib.right_distrib

structure mul_zero_class [class] (A : Type) extends has_mul A, has_zero A :=
(zero_mul : ∀a, mul zero a = zero)
(mul_zero : ∀a, mul a zero = zero)

theorem zero_mul [s : mul_zero_class A] (a : A) : 0 * a = 0 := !mul_zero_class.zero_mul
theorem mul_zero [s : mul_zero_class A] (a : A) : a * 0 = 0 := !mul_zero_class.mul_zero

structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A :=
(zero_ne_one : zero ≠ one)

theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := @zero_ne_one_class.zero_ne_one A s

/- semiring -/

structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A,
    mul_zero_class A, zero_ne_one_class A

section semiring
  variables [s : semiring A] (a b c : A)
  include s

  theorem ne_zero_of_mul_ne_zero_right {a b : A} (H : a * b ≠ 0) : a ≠ 0 :=
  assume H1 : a = 0,
  have H2 : a * b = 0, from H1⁻¹ ▸ zero_mul b,
  H H2

  theorem ne_zero_of_mul_ne_zero_left {a b : A} (H : a * b ≠ 0) : b ≠ 0 :=
  assume H1 : b = 0,
  have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero a,
  H H2
end semiring

/- comm semiring -/

structure comm_semiring [class] (A : Type) extends semiring A, comm_semigroup A
-- TODO: we could also define a cancelative comm_semiring, i.e. satisfying
-- c ≠ 0 → c * a = c * b → a = b.

section comm_semiring
  variables [s : comm_semiring A] (a b c : A)
  include s

  definition dvd (a b : A) : Prop := ∃c, b = a * c
  infix `|` := dvd

  theorem dvd.intro {a b c : A} (H : a * c = b) : a | b :=
  exists.intro _ H⁻¹

  theorem dvd.intro_left {a b c : A} (H : c * a = b) : a | b :=
  dvd.intro (!mul.comm ▸ H)

  theorem exists_eq_mul_right_of_dvd {a b : A} (H : a | b) : ∃c, b = a * c := H

  theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = a * c → P) : P :=
  exists.elim H₁ H₂

  theorem exists_eq_mul_left_of_dvd {a b : A} (H : a | b) : ∃c, b = c * a :=
  dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (H1 ⬝ !mul.comm))

  theorem dvd.elim_left {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = c * a → P) : P :=
  exists.elim (exists_eq_mul_left_of_dvd H₁) (take c, assume H₃ : b = c * a, H₂ c H₃)

  theorem dvd.refl : a | a := dvd.intro !mul_one

  theorem dvd.trans {a b c : A} (H₁ : a | b) (H₂ : b | c) : a | c :=
  dvd.elim H₁
    (take d, assume H₃ : b = a * d,
      dvd.elim H₂
        (take e, assume H₄ : c = b * e,
          dvd.intro
            (calc
              a * (d * e) = (a * d) * e : mul.assoc
                ... = b * e : H₃
                ... = c : H₄)))

  theorem eq_zero_of_zero_dvd {a : A} (H : 0 | a) : a = 0 :=
    dvd.elim H (take c, assume H' : a = 0 * c, H' ⬝ !zero_mul)

  theorem dvd_zero : a | 0 := dvd.intro !mul_zero

  theorem one_dvd : 1 | a := dvd.intro !one_mul

  theorem dvd_mul_right : a | a * b := dvd.intro rfl

  theorem dvd_mul_left : a | b * a := mul.comm a b ▸ dvd_mul_right a b

  theorem dvd_mul_of_dvd_left {a b : A} (H : a | b) (c : A) : a | b * c :=
  dvd.elim H
    (take d,
      assume H₁ : b = a * d,
      dvd.intro
        (calc
          a * (d * c) = a * d * c : (!mul.assoc)⁻¹
             ... = b * c : H₁))

  theorem dvd_mul_of_dvd_right {a b : A} (H : a | b) (c : A) : a | c * b :=
  !mul.comm ▸ (dvd_mul_of_dvd_left H _)

  theorem mul_dvd_mul {a b c d : A} (dvd_ab : a | b) (dvd_cd : c | d) : a * c | b * d :=
  dvd.elim dvd_ab
    (take e, assume Haeb : b = a * e,
      dvd.elim dvd_cd
        (take f, assume Hcfd : d = c * f,
          dvd.intro
            (calc
              a * c * (e * f) = a * (c * (e * f)) : mul.assoc
                ... = a * (e * (c * f)) : mul.left_comm
                ... = a * e * (c * f) : (!mul.assoc)⁻¹
                ... = b * (c * f) : Haeb
                ... = b * d : Hcfd)))

  theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b | c) : a | c :=
  dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))

  theorem dvd_of_mul_left_dvd {a b c : A} (H : a * b | c) : b | c :=
  dvd_of_mul_right_dvd (mul.comm a b ▸ H)

  theorem dvd_add {a b c : A} (Hab : a | b) (Hac : a | c) : a | b + c :=
  dvd.elim Hab
    (take d, assume Hadb : b = a * d,
      dvd.elim Hac
        (take e, assume Haec : c = a * e,
          dvd.intro (show a * (d + e) = b + c, from Hadb⁻¹ ▸ Haec⁻¹ ▸ left_distrib a d e)))
end comm_semiring

/- ring -/

structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A, zero_ne_one_class A

theorem ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 :=
have H : a * 0 + 0 = a * 0 + a * 0, from calc
  a * 0 + 0 = a * 0 : add_zero
        ... = a * (0 + 0) : {(add_zero 0)⁻¹}
        ... = a * 0 + a * 0 : ring.left_distrib,
show a * 0 = 0, from (add.left_cancel H)⁻¹

theorem ring.zero_mul [s : ring A] (a : A) : 0 * a = 0 :=
have H : 0 * a + 0 = 0 * a + 0 * a, from calc
  0 * a + 0 = 0 * a : add_zero
        ... = (0 + 0) * a : {(add_zero 0)⁻¹}
        ... = 0 * a + 0 * a : ring.right_distrib,
show 0 * a = 0, from  (add.left_cancel H)⁻¹<commit_msg>feat(library/algebra/ring): simplify ring theorems using rewrite tactic<commit_after>/-
Copyright (c) 2014 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: algebra.ring
Authors: <NAME>, <NAME>

Structures with multiplicative and additive components, including semirings, rings, and fields.
The development is modeled after Isabelle's library.
-/

import logic.eq logic.connectives data.unit data.sigma data.prod
import algebra.function algebra.binary algebra.group
open eq eq.ops

namespace algebra

variable {A : Type}

/- auxiliary classes -/

structure distrib [class] (A : Type) extends has_mul A, has_add A :=
(left_distrib : ∀a b c, mul a (add b c) = add (mul a b) (mul a c))
(right_distrib : ∀a b c, mul (add a b) c = add (mul a c) (mul b c))

theorem left_distrib [s : distrib A] (a b c : A) : a * (b + c) = a * b + a * c :=
!distrib.left_distrib

theorem right_distrib [s: distrib A] (a b c : A) : (a + b) * c = a * c + b * c :=
!distrib.right_distrib

structure mul_zero_class [class] (A : Type) extends has_mul A, has_zero A :=
(zero_mul : ∀a, mul zero a = zero)
(mul_zero : ∀a, mul a zero = zero)

theorem zero_mul [s : mul_zero_class A] (a : A) : 0 * a = 0 := !mul_zero_class.zero_mul
theorem mul_zero [s : mul_zero_class A] (a : A) : a * 0 = 0 := !mul_zero_class.mul_zero

structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A :=
(zero_ne_one : zero ≠ one)

theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := @zero_ne_one_class.zero_ne_one A s

/- semiring -/

structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A,
    mul_zero_class A, zero_ne_one_class A

section semiring
  variables [s : semiring A] (a b c : A)
  include s

  theorem ne_zero_of_mul_ne_zero_right {a b : A} (H : a * b ≠ 0) : a ≠ 0 :=
  assume H1 : a = 0,
  have H2 : a * b = 0, from H1⁻¹ ▸ zero_mul b,
  H H2

  theorem ne_zero_of_mul_ne_zero_left {a b : A} (H : a * b ≠ 0) : b ≠ 0 :=
  assume H1 : b = 0,
  have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero a,
  H H2
end semiring

/- comm semiring -/

structure comm_semiring [class] (A : Type) extends semiring A, comm_semigroup A
-- TODO: we could also define a cancelative comm_semiring, i.e. satisfying
-- c ≠ 0 → c * a = c * b → a = b.

section comm_semiring
  variables [s : comm_semiring A] (a b c : A)
  include s

  definition dvd (a b : A) : Prop := ∃c, b = a * c
  infix `|` := dvd

  theorem dvd.intro {a b c : A} (H : a * c = b) : a | b :=
  exists.intro _ H⁻¹

  theorem dvd.intro_left {a b c : A} (H : c * a = b) : a | b :=
  dvd.intro (!mul.comm ▸ H)

  theorem exists_eq_mul_right_of_dvd {a b : A} (H : a | b) : ∃c, b = a * c := H

  theorem dvd.elim {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = a * c → P) : P :=
  exists.elim H₁ H₂

  theorem exists_eq_mul_left_of_dvd {a b : A} (H : a | b) : ∃c, b = c * a :=
  dvd.elim H (take c, assume H1 : b = a * c, exists.intro c (H1 ⬝ !mul.comm))

  theorem dvd.elim_left {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, b = c * a → P) : P :=
  exists.elim (exists_eq_mul_left_of_dvd H₁) (take c, assume H₃ : b = c * a, H₂ c H₃)

  theorem dvd.refl : a | a := dvd.intro !mul_one

  theorem dvd.trans {a b c : A} (H₁ : a | b) (H₂ : b | c) : a | c :=
  dvd.elim H₁
    (take d, assume H₃ : b = a * d,
      dvd.elim H₂
        (take e, assume H₄ : c = b * e,
          dvd.intro
            (calc
              a * (d * e) = (a * d) * e : mul.assoc
                ... = b * e : H₃
                ... = c : H₄)))

  theorem eq_zero_of_zero_dvd {a : A} (H : 0 | a) : a = 0 :=
    dvd.elim H (take c, assume H' : a = 0 * c, H' ⬝ !zero_mul)

  theorem dvd_zero : a | 0 := dvd.intro !mul_zero

  theorem one_dvd : 1 | a := dvd.intro !one_mul

  theorem dvd_mul_right : a | a * b := dvd.intro rfl

  theorem dvd_mul_left : a | b * a := mul.comm a b ▸ dvd_mul_right a b

  theorem dvd_mul_of_dvd_left {a b : A} (H : a | b) (c : A) : a | b * c :=
  dvd.elim H
    (take d,
      assume H₁ : b = a * d,
      dvd.intro
        (calc
          a * (d * c) = a * d * c : (!mul.assoc)⁻¹
             ... = b * c : H₁))

  theorem dvd_mul_of_dvd_right {a b : A} (H : a | b) (c : A) : a | c * b :=
  !mul.comm ▸ (dvd_mul_of_dvd_left H _)

  theorem mul_dvd_mul {a b c d : A} (dvd_ab : a | b) (dvd_cd : c | d) : a * c | b * d :=
  dvd.elim dvd_ab
    (take e, assume Haeb : b = a * e,
      dvd.elim dvd_cd
        (take f, assume Hcfd : d = c * f,
          dvd.intro
            (show a * c * (e * f) = b * d,
             by rewrite [mul.assoc, {c*_}mul.left_comm, -mul.assoc, Haeb, Hcfd])))

  theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b | c) : a | c :=
  dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))

  theorem dvd_of_mul_left_dvd {a b c : A} (H : a * b | c) : b | c :=
  dvd_of_mul_right_dvd (mul.comm a b ▸ H)

  theorem dvd_add {a b c : A} (Hab : a | b) (Hac : a | c) : a | b + c :=
  dvd.elim Hab
    (take d, assume Hadb : b = a * d,
      dvd.elim Hac
        (take e, assume Haec : c = a * e,
          dvd.intro (show a * (d + e) = b + c,
                     by rewrite [left_distrib, -Hadb, -Haec])))
end comm_semiring

/- ring -/

structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A, zero_ne_one_class A

theorem ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 :=
have H : a * 0 + 0 = a * 0 + a * 0, from calc
  a * 0 + 0 = a * 0 : add_zero
        ... = a * (0 + 0) : {(add_zero 0)⁻¹}
        ... = a * 0 + a * 0 : ring.left_distrib,
show a * 0 = 0, from (add.left_cancel H)⁻¹

theorem ring.zero_mul [s : ring A] (a : A) : 0 * a = 0 :=
have H : 0 * a + 0 = 0 * a + 0 * a, from calc
  0 * a + 0 = 0 * a : add_zero
        ... = (0 + 0) * a : {(add_zero 0)⁻¹}
        ... = 0 * a + 0 * a : ring.right_distrib,
show 0 * a = 0, from  (add.left_cancel H)⁻¹
{'fraction_non_alphanumeric': 0.15241667377035206, 'fraction_numerical': 0.011593214559713579, 'mean_word_length': 2.2382003864200937, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 20, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6312099', 'n_tokens_mistral': 5284, 'n_tokens_neox': 5038, 'n_words': 1768}