lean2/hott/algebra/group.hlean

566 lines
18 KiB
Text
Raw Normal View History

2014-12-12 04:14:53 +00:00
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.group
Authors: Jeremy Avigad, Leonardo de Moura
Various multiplicative and additive structures. Partially modeled on Isabelle's library.
-/
2014-12-12 19:19:06 +00:00
import algebra.binary
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
open eq truncation binary -- note: ⁻¹ will be overloaded
2014-12-12 04:14:53 +00:00
namespace path_algebra
variable {A : Type}
/- overloaded symbols -/
structure has_mul [class] (A : Type) :=
(mul : A → A → A)
structure has_add [class] (A : Type) :=
(add : A → A → A)
structure has_one [class] (A : Type) :=
(one : A)
structure has_zero [class] (A : Type) :=
(zero : A)
structure has_inv [class] (A : Type) :=
(inv : A → A)
structure has_neg [class] (A : Type) :=
(neg : A → A)
infixl `*` := has_mul.mul
infixl `+` := has_add.add
postfix `⁻¹` := has_inv.inv
prefix `-` := has_neg.neg
notation 1 := !has_one.one
notation 0 := !has_zero.zero
/- semigroup -/
structure semigroup [class] (A : Type) extends has_mul A :=
(carrier_hset : is_hset A)
2014-12-12 19:19:06 +00:00
(mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
2014-12-12 04:14:53 +00:00
!semigroup.mul_assoc
structure comm_semigroup [class] (A : Type) extends semigroup A :=
2014-12-12 19:19:06 +00:00
(mul_comm : ∀a b, mul a b = mul b a)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
2014-12-12 04:14:53 +00:00
!comm_semigroup.mul_comm
2014-12-12 19:19:06 +00:00
theorem mul_left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
binary.left_comm (@mul_comm A s) (@mul_assoc A s) a b c
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b :=
binary.right_comm (@mul_comm A s) (@mul_assoc A s) a b c
2014-12-12 04:14:53 +00:00
structure left_cancel_semigroup [class] (A : Type) extends semigroup A :=
2014-12-12 19:19:06 +00:00
(mul_left_cancel : ∀a b c, mul a b = mul a c → b = c)
2014-12-12 04:14:53 +00:00
theorem mul_left_cancel [s : left_cancel_semigroup A] {a b c : A} :
2014-12-12 19:19:06 +00:00
a * b = a * c → b = c :=
2014-12-12 04:14:53 +00:00
!left_cancel_semigroup.mul_left_cancel
structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
2014-12-12 19:19:06 +00:00
(mul_right_cancel : ∀a b c, mul a b = mul c b → a = c)
2014-12-12 04:14:53 +00:00
theorem mul_right_cancel [s : right_cancel_semigroup A] {a b c : A} :
2014-12-12 19:19:06 +00:00
a * b = c * b → a = c :=
2014-12-12 04:14:53 +00:00
!right_cancel_semigroup.mul_right_cancel
/- additive semigroup -/
structure add_semigroup [class] (A : Type) extends has_add A :=
2014-12-12 19:19:06 +00:00
(add_assoc : ∀a b c, add (add a b) c = add a (add b c))
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
2014-12-12 04:14:53 +00:00
!add_semigroup.add_assoc
structure add_comm_semigroup [class] (A : Type) extends add_semigroup A :=
2014-12-12 19:19:06 +00:00
(add_comm : ∀a b, add a b = add b a)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
2014-12-12 04:14:53 +00:00
!add_comm_semigroup.add_comm
theorem add_left_comm [s : add_comm_semigroup A] (a b c : A) :
2014-12-12 19:19:06 +00:00
a + (b + c) = b + (a + c) :=
binary.left_comm (@add_comm A s) (@add_assoc A s) a b c
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
binary.right_comm (@add_comm A s) (@add_assoc A s) a b c
2014-12-12 04:14:53 +00:00
structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
2014-12-12 19:19:06 +00:00
(add_left_cancel : ∀a b c, add a b = add a c → b = c)
2014-12-12 04:14:53 +00:00
theorem add_left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
2014-12-12 19:19:06 +00:00
a + b = a + c → b = c :=
2014-12-12 04:14:53 +00:00
!add_left_cancel_semigroup.add_left_cancel
structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
2014-12-12 19:19:06 +00:00
(add_right_cancel : ∀a b c, add a b = add c b → a = c)
2014-12-12 04:14:53 +00:00
theorem add_right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
2014-12-12 19:19:06 +00:00
a + b = c + b → a = c :=
2014-12-12 04:14:53 +00:00
!add_right_cancel_semigroup.add_right_cancel
/- monoid -/
structure monoid [class] (A : Type) extends semigroup A, has_one A :=
2014-12-12 19:19:06 +00:00
(mul_left_id : ∀a, mul one a = a) (mul_right_id : ∀a, mul a one = a)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_left_id [s : monoid A] (a : A) : 1 * a = a := !monoid.mul_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_right_id [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_right_id
2014-12-12 04:14:53 +00:00
structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
/- additive monoid -/
structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
2014-12-12 19:19:06 +00:00
(add_left_id : ∀a, add zero a = a) (add_right_id : ∀a, add a zero = a)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_left_id [s : add_monoid A] (a : A) : 0 + a = a := !add_monoid.add_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_right_id [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_right_id
2014-12-12 04:14:53 +00:00
structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
/- group -/
structure group [class] (A : Type) extends monoid A, has_inv A :=
2014-12-12 19:19:06 +00:00
(mul_left_inv : ∀a, mul (inv a) a = one)
2014-12-12 04:14:53 +00:00
-- Note: with more work, we could derive the axiom mul_left_id
section group
variable [s : group A]
include s
2014-12-12 19:19:06 +00:00
theorem mul_left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a⁻¹ * (a * b) = a⁻¹ * a * b : mul_assoc
... = 1 * b : mul_left_inv
... = b : mul_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem inv_mul_cancel_right (a b : A) : a * b⁻¹ * b = a :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a * b⁻¹ * b = a * (b⁻¹ * b) : mul_assoc
... = a * 1 : mul_left_inv
... = a : mul_right_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem inv_unique {a b : A} (H : a * b = 1) : a⁻¹ = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a⁻¹ = a⁻¹ * 1 : mul_right_id
... = a⁻¹ * (a * b) : H
... = b : inv_mul_cancel_left
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem inv_one : 1⁻¹ = 1 := inv_unique (mul_left_id 1)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_unique (mul_left_inv a)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem inv_inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a = (a⁻¹)⁻¹ : inv_inv
... = b : inv_unique (H⁻¹ ▹ (mul_left_inv _))
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
--theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
2014-12-12 04:14:53 +00:00
--iff.intro (assume H, inv_inj H) (assume H, congr_arg _ H)
2014-12-12 19:19:06 +00:00
--theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 :=
2014-12-12 04:14:53 +00:00
--inv_one ▹ !inv_eq_inv_iff_eq
2014-12-12 19:19:06 +00:00
theorem eq_inv_imp_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
2014-12-12 04:14:53 +00:00
H⁻¹ ▹ (inv_inv b)⁻¹
2014-12-12 19:19:06 +00:00
--theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
2014-12-12 04:14:53 +00:00
--iff.intro !eq_inv_imp_eq_inv !eq_inv_imp_eq_inv
2014-12-12 19:19:06 +00:00
theorem mul_right_inv (a : A) : a * a⁻¹ = 1 :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv
... = 1 : mul_left_inv
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a * (a⁻¹ * b) = a * a⁻¹ * b : mul_assoc
... = 1 * b : mul_right_inv
... = b : mul_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_inv_cancel_right (a b : A) : a * b * b⁻¹ = a :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a * b * b⁻¹ = a * (b * b⁻¹) : mul_assoc
... = a * 1 : mul_right_inv
... = a : mul_right_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem inv_mul (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
2014-12-12 04:14:53 +00:00
inv_unique
(calc
2014-12-12 19:19:06 +00:00
a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul_assoc
... = a * a⁻¹ : mul_inv_cancel_left
... = 1 : mul_right_inv)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem mul_inv_eq_one_imp_eq {a b : A} (H : a * b⁻¹ = 1) : a = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a = a * b⁻¹ * b : inv_mul_cancel_right
... = 1 * b : H
... = b : mul_left_id
2014-12-12 04:14:53 +00:00
-- TODO: better names for the next eight theorems? (Also for additive ones.)
2014-12-12 19:19:06 +00:00
theorem mul_eq_imp_eq_mul_inv {a b c : A} (H : a * b = c) : a = c * b⁻¹ :=
2014-12-12 04:14:53 +00:00
H ▹ !mul_inv_cancel_right⁻¹
2014-12-12 19:19:06 +00:00
theorem mul_eq_imp_eq_inv_mul {a b c : A} (H : a * b = c) : b = a⁻¹ * c :=
2014-12-12 04:14:53 +00:00
H ▹ !inv_mul_cancel_left⁻¹
2014-12-12 19:19:06 +00:00
theorem eq_mul_imp_inv_mul_eq {a b c : A} (H : a = b * c) : b⁻¹ * a = c :=
2014-12-12 04:14:53 +00:00
H⁻¹ ▹ !inv_mul_cancel_left
2014-12-12 19:19:06 +00:00
theorem eq_mul_imp_mul_inv_eq {a b c : A} (H : a = b * c) : a * c⁻¹ = b :=
2014-12-12 04:14:53 +00:00
H⁻¹ ▹ !mul_inv_cancel_right
2014-12-12 19:19:06 +00:00
theorem mul_inv_eq_imp_eq_mul {a b c : A} (H : a * b⁻¹ = c) : a = c * b :=
2014-12-12 04:14:53 +00:00
!inv_inv ▹ (mul_eq_imp_eq_mul_inv H)
2014-12-12 19:19:06 +00:00
theorem inv_mul_eq_imp_eq_mul {a b c : A} (H : a⁻¹ * b = c) : b = a * c :=
2014-12-12 04:14:53 +00:00
!inv_inv ▹ (mul_eq_imp_eq_inv_mul H)
2014-12-12 19:19:06 +00:00
theorem eq_inv_mul_imp_mul_eq {a b c : A} (H : a = b⁻¹ * c) : b * a = c :=
2014-12-12 04:14:53 +00:00
!inv_inv ▹ (eq_mul_imp_inv_mul_eq H)
2014-12-12 19:19:06 +00:00
theorem eq_mul_inv_imp_mul_eq {a b c : A} (H : a = b * c⁻¹) : a * c = b :=
2014-12-12 04:14:53 +00:00
!inv_inv ▹ (eq_mul_imp_mul_inv_eq H)
2014-12-12 19:19:06 +00:00
--theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
2014-12-12 04:14:53 +00:00
--iff.intro mul_eq_imp_eq_inv_mul eq_inv_mul_imp_mul_eq
2014-12-12 19:19:06 +00:00
--theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
2014-12-12 04:14:53 +00:00
--iff.intro mul_eq_imp_eq_mul_inv eq_mul_inv_imp_mul_eq
definition group.to_left_cancel_semigroup [instance] : left_cancel_semigroup A :=
left_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s)
(take a b c,
2014-12-12 19:19:06 +00:00
assume H : a * b = a * c,
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
b = a⁻¹ * (a * b) : inv_mul_cancel_left
... = a⁻¹ * (a * c) : H
... = c : inv_mul_cancel_left)
2014-12-12 04:14:53 +00:00
definition group.to_right_cancel_semigroup [instance] : right_cancel_semigroup A :=
right_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s)
(take a b c,
2014-12-12 19:19:06 +00:00
assume H : a * b = c * b,
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a = (a * b) * b⁻¹ : mul_inv_cancel_right
... = (c * b) * b⁻¹ : H
... = c : mul_inv_cancel_right)
2014-12-12 04:14:53 +00:00
end group
structure comm_group [class] (A : Type) extends group A, comm_monoid A
/- additive group -/
structure add_group [class] (A : Type) extends add_monoid A, has_neg A :=
2014-12-12 19:19:06 +00:00
(add_left_inv : ∀a, add (neg a) a = zero)
2014-12-12 04:14:53 +00:00
section add_group
variables [s : add_group A]
include s
2014-12-12 19:19:06 +00:00
theorem add_left_inv (a : A) : -a + a = 0 := !add_group.add_left_inv
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_add_cancel_left (a b : A) : -a + (a + b) = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
-a + (a + b) = -a + a + b : add_assoc
... = 0 + b : add_left_inv
... = b : add_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_add_cancel_right (a b : A) : a + -b + b = a :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a + -b + b = a + (-b + b) : add_assoc
... = a + 0 : add_left_inv
... = a : add_right_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_unique {a b : A} (H : a + b = 0) : -a = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
-a = -a + 0 : add_right_id
... = -a + (a + b) : H
... = b : neg_add_cancel_left
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_zero : -0 = 0 := neg_unique (add_left_id 0)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_neg (a : A) : -(-a) = a := neg_unique (add_left_inv a)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_inj {a b : A} (H : -a = -b) : a = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a = -(-a) : neg_neg
... = b : neg_unique (H⁻¹ ▹ (add_left_inv _))
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
--theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
2014-12-12 04:14:53 +00:00
--iff.intro (assume H, neg_inj H) (assume H, congr_arg _ H)
2014-12-12 19:19:06 +00:00
--theorem neg_eq_zero_iff_eq_zero (a b : A) : -a = 0 ↔ a = 0 :=
2014-12-12 04:14:53 +00:00
--neg_zero ▹ !neg_eq_neg_iff_eq
2014-12-12 19:19:06 +00:00
theorem eq_neg_imp_eq_neg {a b : A} (H : a = -b) : b = -a :=
2014-12-12 04:14:53 +00:00
H⁻¹ ▹ (neg_neg b)⁻¹
2014-12-12 19:19:06 +00:00
--theorem eq_neg_iff_eq_neg (a b : A) : a = -b ↔ b = -a :=
2014-12-12 04:14:53 +00:00
--iff.intro !eq_neg_imp_eq_neg !eq_neg_imp_eq_neg
2014-12-12 19:19:06 +00:00
theorem add_right_inv (a : A) : a + -a = 0 :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a + -a = -(-a) + -a : neg_neg
... = 0 : add_left_inv
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_neg_cancel_left (a b : A) : a + (-a + b) = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a + (-a + b) = a + -a + b : add_assoc
... = 0 + b : add_right_inv
... = b : add_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_neg_cancel_right (a b : A) : a + b + -b = a :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a + b + -b = a + (b + -b) : add_assoc
... = a + 0 : add_right_inv
... = a : add_right_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_add (a b : A) : -(a + b) = -b + -a :=
2014-12-12 04:14:53 +00:00
neg_unique
(calc
2014-12-12 19:19:06 +00:00
a + b + (-b + -a) = a + (b + (-b + -a)) : add_assoc
... = a + -a : add_neg_cancel_left
... = 0 : add_right_inv)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_eq_imp_eq_add_neg {a b c : A} (H : a + b = c) : a = c + -b :=
2014-12-12 04:14:53 +00:00
H ▹ !add_neg_cancel_right⁻¹
2014-12-12 19:19:06 +00:00
theorem add_eq_imp_eq_neg_add {a b c : A} (H : a + b = c) : b = -a + c :=
2014-12-12 04:14:53 +00:00
H ▹ !neg_add_cancel_left⁻¹
2014-12-12 19:19:06 +00:00
theorem eq_add_imp_neg_add_eq {a b c : A} (H : a = b + c) : -b + a = c :=
2014-12-12 04:14:53 +00:00
H⁻¹ ▹ !neg_add_cancel_left
2014-12-12 19:19:06 +00:00
theorem eq_add_imp_add_neg_eq {a b c : A} (H : a = b + c) : a + -c = b :=
2014-12-12 04:14:53 +00:00
H⁻¹ ▹ !add_neg_cancel_right
2014-12-12 19:19:06 +00:00
theorem add_neg_eq_imp_eq_add {a b c : A} (H : a + -b = c) : a = c + b :=
2014-12-12 04:14:53 +00:00
!neg_neg ▹ (add_eq_imp_eq_add_neg H)
2014-12-12 19:19:06 +00:00
theorem neg_add_eq_imp_eq_add {a b c : A} (H : -a + b = c) : b = a + c :=
2014-12-12 04:14:53 +00:00
!neg_neg ▹ (add_eq_imp_eq_neg_add H)
2014-12-12 19:19:06 +00:00
theorem eq_neg_add_imp_add_eq {a b c : A} (H : a = -b + c) : b + a = c :=
2014-12-12 04:14:53 +00:00
!neg_neg ▹ (eq_add_imp_neg_add_eq H)
2014-12-12 19:19:06 +00:00
theorem eq_add_neg_imp_add_eq {a b c : A} (H : a = b + -c) : a + c = b :=
2014-12-12 04:14:53 +00:00
!neg_neg ▹ (eq_add_imp_add_neg_eq H)
2014-12-12 19:19:06 +00:00
--theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
2014-12-12 04:14:53 +00:00
--iff.intro add_eq_imp_eq_neg_add eq_neg_add_imp_add_eq
2014-12-12 19:19:06 +00:00
--theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b :=
2014-12-12 04:14:53 +00:00
--iff.intro add_eq_imp_eq_add_neg eq_add_neg_imp_add_eq
definition add_group.to_left_cancel_semigroup [instance] :
add_left_cancel_semigroup A :=
add_left_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s)
(take a b c,
2014-12-12 19:19:06 +00:00
assume H : a + b = a + c,
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
b = -a + (a + b) : neg_add_cancel_left
... = -a + (a + c) : H
... = c : neg_add_cancel_left)
2014-12-12 04:14:53 +00:00
definition add_group.to_add_right_cancel_semigroup [instance] :
add_right_cancel_semigroup A :=
add_right_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s)
(take a b c,
2014-12-12 19:19:06 +00:00
assume H : a + b = c + b,
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a = (a + b) + -b : add_neg_cancel_right
... = (c + b) + -b : H
... = c : add_neg_cancel_right)
2014-12-12 04:14:53 +00:00
/- minus -/
-- TODO: derive corresponding facts for div in a field
definition minus [reducible] (a b : A) : A := a + -b
2014-12-12 04:14:53 +00:00
infix `-` := minus
2014-12-12 19:19:06 +00:00
theorem minus_self (a : A) : a - a = 0 := !add_right_inv
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem minus_add_cancel (a b : A) : a - b + b = a := !neg_add_cancel_right
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_minus_cancel (a b : A) : a + b - b = a := !add_neg_cancel_right
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem minus_eq_zero_imp_eq {a b : A} (H : a - b = 0) : a = b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a = (a - b) + b : minus_add_cancel
... = 0 + b : H
... = b : add_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
--theorem eq_iff_minus_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
2014-12-12 04:14:53 +00:00
--iff.intro (assume H, H ▹ !minus_self) (assume H, minus_eq_zero_imp_eq H)
2014-12-12 19:19:06 +00:00
theorem zero_minus (a : A) : 0 - a = -a := !add_left_id
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem minus_zero (a : A) : a - 0 = a := (neg_zero⁻¹) ▹ !add_right_id
2014-12-12 04:14:53 +00:00
theorem minus_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▹ idp
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_minus_eq (a b : A) : -(a - b) = b - a :=
2014-12-12 04:14:53 +00:00
neg_unique
(calc
2014-12-12 19:19:06 +00:00
a - b + (b - a) = a - b + b - a : add_assoc
... = a - a : minus_add_cancel
... = 0 : minus_self)
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_minus_eq (a b c : A) : a + (b - c) = a + b - c := !add_assoc⁻¹
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem minus_add_eq_minus_swap (a b c : A) : a - (b + c) = a - c - b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a - (b + c) = a + (-c - b) : neg_add
... = a - c - b : add_assoc
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
--theorem minus_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
2014-12-12 04:14:53 +00:00
--iff.intro (assume H, add_neg_eq_imp_eq_add H) (assume H, eq_add_imp_add_neg_eq H)
2014-12-12 19:19:06 +00:00
--theorem eq_minus_iff_add_eq (a b c : A) : a = b - c ↔ a + c = b :=
2014-12-12 04:14:53 +00:00
--iff.intro (assume H, eq_add_neg_imp_add_eq H) (assume H, add_eq_imp_eq_add_neg H)
2014-12-12 19:19:06 +00:00
--theorem minus_eq_minus_iff {a b c d : A} (H : a - b = c - d) : a = b ↔ c = d :=
2014-12-12 04:14:53 +00:00
--calc
2014-12-12 19:19:06 +00:00
-- a = b ↔ a - b = 0 : eq_iff_minus_eq_zero
-- ... ↔ c - d = 0 : H ▹ !iff.refl
-- ... ↔ c = d : iff.symm (eq_iff_minus_eq_zero c d)
2014-12-12 04:14:53 +00:00
end add_group
structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A
section add_comm_group
variable [s : add_comm_group A]
include s
2014-12-12 19:19:06 +00:00
theorem minus_add_eq (a b c : A) : a - (b + c) = a - b - c :=
2014-12-12 04:14:53 +00:00
!add_comm ▹ !minus_add_eq_minus_swap
2014-12-12 19:19:06 +00:00
theorem neg_add_eq_minus (a b : A) : -a + b = b - a := !add_comm
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := !add_comm ▹ !neg_add
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem minus_add_right_comm (a b c : A) : a - b + c = a + c - b := !add_right_comm
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem minus_minus_eq (a b c : A) : a - b - c = a - (b + c) :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
a - b - c = a + (-b + -c) : add_assoc
... = a + -(b + c) : neg_add_distrib
... = a - (b + c) : idp
2014-12-12 04:14:53 +00:00
2014-12-12 19:19:06 +00:00
theorem add_minus_cancel_left (a b c : A) : (c + a) - (c + b) = a - b :=
2014-12-12 04:14:53 +00:00
calc
2014-12-12 19:19:06 +00:00
(c + a) - (c + b) = c + a - c - b : minus_add_eq
... = a + c - c - b : add_comm a c
... = a - b : add_minus_cancel
2014-12-12 04:14:53 +00:00
end add_comm_group
/- bundled structures -/
structure Semigroup :=
(carrier : Type) (struct : semigroup carrier)
attribute Semigroup.carrier [coercion]
attribute Semigroup.struct [instance]
2014-12-12 04:14:53 +00:00
structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier)
attribute CommSemigroup.carrier [coercion]
attribute CommSemigroup.struct [instance]
2014-12-12 04:14:53 +00:00
structure Monoid :=
(carrier : Type) (struct : monoid carrier)
attribute Monoid.carrier [coercion]
attribute Monoid.struct [instance]
2014-12-12 04:14:53 +00:00
structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier)
attribute CommMonoid.carrier [coercion]
attribute CommMonoid.struct [instance]
2014-12-12 04:14:53 +00:00
structure Group :=
(carrier : Type) (struct : group carrier)
attribute Group.carrier [coercion]
attribute Group.struct [instance]
2014-12-12 04:14:53 +00:00
structure CommGroup :=
(carrier : Type) (struct : comm_group carrier)
attribute CommGroup.carrier [coercion]
attribute CommGroup.struct [instance]
2014-12-12 04:14:53 +00:00
structure AddSemigroup :=
(carrier : Type) (struct : add_semigroup carrier)
attribute AddSemigroup.carrier [coercion]
attribute AddSemigroup.struct [instance]
2014-12-12 04:14:53 +00:00
structure AddCommSemigroup :=
(carrier : Type) (struct : add_comm_semigroup carrier)
attribute AddCommSemigroup.carrier [coercion]
attribute AddCommSemigroup.struct [instance]
2014-12-12 04:14:53 +00:00
structure AddMonoid :=
(carrier : Type) (struct : add_monoid carrier)
attribute AddMonoid.carrier [coercion]
attribute AddMonoid.struct [instance]
2014-12-12 04:14:53 +00:00
structure AddCommMonoid :=
(carrier : Type) (struct : add_comm_monoid carrier)
attribute AddCommMonoid.carrier [coercion]
attribute AddCommMonoid.struct [instance]
2014-12-12 04:14:53 +00:00
structure AddGroup :=
(carrier : Type) (struct : add_group carrier)
attribute AddGroup.carrier [coercion]
attribute AddGroup.struct [instance]
2014-12-12 04:14:53 +00:00
structure AddCommGroup :=
(carrier : Type) (struct : add_comm_group carrier)
attribute AddCommGroup.carrier [coercion]
attribute AddCommGroup.struct [instance]
2014-12-12 04:14:53 +00:00
end path_algebra