feat(library/algebra): add to developments of group, ordered_group, and ring
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
f923d6a24c
commit
58e325f0af
3 changed files with 206 additions and 11 deletions
|
|
@ -249,6 +249,12 @@ section group
|
|||
theorem eq_mul_inv_imp_mul_eq {a b c : A} (H : a = b * c⁻¹) : a * c = b :=
|
||||
!inv_inv ▸ (eq_mul_imp_mul_inv_eq H)
|
||||
|
||||
theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
|
||||
iff.intro mul_eq_imp_eq_inv_mul eq_inv_mul_imp_mul_eq
|
||||
|
||||
theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
|
||||
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.mul_assoc A s)
|
||||
(take a b c,
|
||||
|
|
@ -371,6 +377,12 @@ section add_group
|
|||
theorem eq_add_neg_imp_add_eq {a b c : A} (H : a = b + -c) : a + c = b :=
|
||||
!neg_neg ▸ (eq_add_imp_add_neg_eq H)
|
||||
|
||||
theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
|
||||
iff.intro add_eq_imp_eq_neg_add eq_neg_add_imp_add_eq
|
||||
|
||||
theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b :=
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -153,8 +153,8 @@ end
|
|||
|
||||
-- TODO: there is more we can do if we have max and min (in order.lean as well)
|
||||
|
||||
-- TODO: there is more we can do if we assume a ≤ b ↔ ∃c. a + c = b, but it is not clear whether
|
||||
-- this gives us any useful generality
|
||||
-- TODO: there is more we can do if we assume a ≤ b ↔ ∃c. a + c = b. This covers the natural numbers,
|
||||
-- but it is not clear whether it provides any further useful generality.
|
||||
|
||||
structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A :=
|
||||
(add_le_left : ∀a b c, le a b → le (add c a) (add c b))
|
||||
|
|
@ -171,4 +171,138 @@ proof
|
|||
!neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H'
|
||||
qed
|
||||
|
||||
section
|
||||
|
||||
variables [s : ordered_comm_group A] (a b c d e : A)
|
||||
include s
|
||||
|
||||
theorem le_imp_neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a :=
|
||||
have H1 : 0 ≤ -a + b, from !add_left_inv ▸ !(add_le_left H),
|
||||
!add_neg_cancel_right ▸ !add_left_id ▸ add_le_right H1 (-b)
|
||||
-- !add_left_id ▸ !add_neg_cancel_right ▸ add_le_right H1 (-b) -- doesn't work?
|
||||
|
||||
theorem neg_le_neg_iff : -a ≤ -b ↔ b ≤ a :=
|
||||
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ le_imp_neg_le_neg H) le_imp_neg_le_neg
|
||||
|
||||
theorem neg_le_zero_iff : -a ≤ 0 ↔ 0 ≤ a :=
|
||||
neg_zero ▸ neg_le_neg_iff a 0
|
||||
|
||||
theorem zero_le_neg_iff : 0 ≤ -a ↔ a ≤ 0 :=
|
||||
neg_zero ▸ neg_le_neg_iff 0 a
|
||||
|
||||
theorem lt_imp_neg_lt_neg {a b : A} (H : a < b) : -b < -a :=
|
||||
have H1 : 0 < -a + b, from !add_left_inv ▸ !(add_lt_left H),
|
||||
!add_neg_cancel_right ▸ !add_left_id ▸ add_lt_right H1 (-b)
|
||||
|
||||
theorem neg_lt_neg_iff : -a < -b ↔ b < a :=
|
||||
iff.intro (take H, neg_neg a ▸ neg_neg b ▸ lt_imp_neg_lt_neg H) lt_imp_neg_lt_neg
|
||||
|
||||
theorem neg_lt_zero_iff : -a < 0 ↔ 0 < a :=
|
||||
neg_zero ▸ neg_lt_neg_iff a 0
|
||||
|
||||
theorem zero_lt_neg_iff : 0 < -a ↔ a < 0 :=
|
||||
neg_zero ▸ neg_lt_neg_iff 0 a
|
||||
|
||||
theorem le_neg_iff : a ≤ -b ↔ b ≤ -a := !neg_neg ▸ !neg_le_neg_iff
|
||||
|
||||
theorem neg_le_iff : -a ≤ b ↔ -b ≤ a := !neg_neg ▸ !neg_le_neg_iff
|
||||
|
||||
theorem lt_neg_iff : a < -b ↔ b < -a := !neg_neg ▸ !neg_lt_neg_iff
|
||||
|
||||
theorem neg_lt_iff : -a < b ↔ -b < a := !neg_neg ▸ !neg_lt_neg_iff
|
||||
|
||||
theorem minus_nonneg_iff : 0 ≤ a - b ↔ b ≤ a := !minus_self ▸ !add_le_right_iff
|
||||
|
||||
theorem minus_nonpos_iff : a - b ≤ 0 ↔ a ≤ b := !minus_self ▸ !add_le_right_iff
|
||||
|
||||
theorem minus_pos_iff : 0 < a - b ↔ b < a := !minus_self ▸ !add_lt_right_iff
|
||||
|
||||
theorem minus_neg_iff : a - b < 0 ↔ a < b := !minus_self ▸ !add_lt_right_iff
|
||||
|
||||
theorem add_le_iff_le_neg_add : a + b ≤ c ↔ b ≤ -a + c :=
|
||||
have H: a + b ≤ c ↔ -a + (a + b) ≤ -a + c, from iff.symm (!add_le_left_iff),
|
||||
!neg_add_cancel_left ▸ H
|
||||
|
||||
theorem add_le_iff_le_minus_left : a + b ≤ c ↔ b ≤ c - a :=
|
||||
!add_comm ▸ !add_le_iff_le_neg_add
|
||||
|
||||
theorem add_le_iff_le_minus_right : a + b ≤ c ↔ a ≤ c - b :=
|
||||
have H: a + b ≤ c ↔ a + b - b ≤ c - b, from iff.symm (!add_le_right_iff),
|
||||
!add_neg_cancel_right ▸ H
|
||||
|
||||
theorem le_add_iff_neg_add_le : a ≤ b + c ↔ -b + a ≤ c :=
|
||||
have H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_left_iff),
|
||||
!neg_add_cancel_left ▸ H
|
||||
|
||||
theorem le_add_iff_minus_left_le : a ≤ b + c ↔ a - b ≤ c :=
|
||||
!add_comm ▸ !le_add_iff_neg_add_le
|
||||
|
||||
theorem le_add_iff_minus_right_le : a ≤ b + c ↔ a - c ≤ b :=
|
||||
have H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_right_iff),
|
||||
!add_neg_cancel_right ▸ H
|
||||
|
||||
theorem add_lt_iff_lt_neg_add : a + b < c ↔ b < -a + c :=
|
||||
have H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_left_iff),
|
||||
!neg_add_cancel_left ▸ H
|
||||
|
||||
theorem add_lt_iff_lt_minus_left : a + b < c ↔ b < c - a :=
|
||||
!add_comm ▸ !add_lt_iff_lt_neg_add
|
||||
|
||||
theorem add_lt_iff_lt_minus_right : a + b < c ↔ a < c - b :=
|
||||
have H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_right_iff),
|
||||
!add_neg_cancel_right ▸ H
|
||||
|
||||
theorem lt_add_iff_neg_add_lt : a < b + c ↔ -b + a < c :=
|
||||
have H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_left_iff),
|
||||
!neg_add_cancel_left ▸ H
|
||||
|
||||
theorem lt_add_iff_minus_left_lt : a < b + c ↔ a - b < c :=
|
||||
!add_comm ▸ !lt_add_iff_neg_add_lt
|
||||
|
||||
theorem lt_add_iff_minus_right_lt : a < b + c ↔ a - c < b :=
|
||||
have H: a < b + c ↔ a - c < b + c - c, from iff.symm (!add_lt_right_iff),
|
||||
!add_neg_cancel_right ▸ H
|
||||
|
||||
-- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0
|
||||
|
||||
theorem minus_eq_imp_le_iff {a b c d : A} (H : a - b = c - d) : a ≤ b ↔ c ≤ d :=
|
||||
calc
|
||||
a ≤ b ↔ a - b ≤ 0 : iff.symm (minus_nonpos_iff a b)
|
||||
... ↔ c - d ≤ 0 : H ▸ !iff.refl
|
||||
... ↔ c ≤ d : minus_nonpos_iff c d
|
||||
|
||||
theorem minus_eq_imp_lt_iff {a b c d : A} (H : a - b = c - d) : a < b ↔ c < d :=
|
||||
calc
|
||||
a < b ↔ a - b < 0 : iff.symm (minus_neg_iff a b)
|
||||
... ↔ c - d < 0 : H ▸ !iff.refl
|
||||
... ↔ c < d : minus_neg_iff c d
|
||||
|
||||
theorem minus_le_left {a b : A} (H : a ≤ b) (c : A) : c - b ≤ c - a :=
|
||||
add_le_left (le_imp_neg_le_neg H) c
|
||||
|
||||
theorem minus_le_right {a b : A} (H : a ≤ b) (c : A) : a - c ≤ b - c := add_le_right H (-c)
|
||||
|
||||
theorem minus_le {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a - d ≤ b - c :=
|
||||
add_le Hab (le_imp_neg_le_neg Hcd)
|
||||
|
||||
theorem minus_lt_left {a b : A} (H : a < b) (c : A) : c - b < c - a :=
|
||||
add_lt_left (lt_imp_neg_lt_neg H) c
|
||||
|
||||
theorem minus_lt_right {a b : A} (H : a < b) (c : A) : a - c < b - c := add_lt_right H (-c)
|
||||
|
||||
theorem minus_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a - d < b - c :=
|
||||
add_lt Hab (lt_imp_neg_lt_neg Hcd)
|
||||
|
||||
theorem minus_le_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a - d < b - c :=
|
||||
add_le_lt Hab (lt_imp_neg_lt_neg Hcd)
|
||||
|
||||
theorem minus_lt_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a - d < b - c :=
|
||||
add_lt_le Hab (le_imp_neg_le_neg Hcd)
|
||||
|
||||
end
|
||||
|
||||
-- TODO: additional facts if the ordering is a linear ordering (e.g. -a = a ↔ a = 0)
|
||||
|
||||
-- TODO: structures with abs
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -44,14 +44,6 @@ theorem zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := !zero_ne_one_class.zer
|
|||
structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A, mul_zero A,
|
||||
zero_ne_one_class A
|
||||
|
||||
section
|
||||
|
||||
variable [s : semiring A]
|
||||
include s
|
||||
|
||||
/- -/
|
||||
end
|
||||
|
||||
structure comm_semiring [class] (A : Type) extends semiring A, comm_semigroup A
|
||||
|
||||
|
||||
|
|
@ -292,7 +284,64 @@ section
|
|||
|
||||
end
|
||||
|
||||
/- ring no_zero_divisors -/
|
||||
|
||||
/- integral domains -/
|
||||
|
||||
-- TODO: some properties here may extend to cancellative semirings. It is worth the effort?
|
||||
|
||||
structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A :=
|
||||
(eq_zero_or_eq_zero_of_mul_eq_zero : ∀a b, mul a b = zero → a = zero ∨ b = zero)
|
||||
|
||||
theorem eq_zero_or_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a b : A} (H : a * b = 0) :
|
||||
a = 0 ∨ b = 0 := !no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero H
|
||||
|
||||
structure integral_domain [class] (A : Type) extends comm_ring_dvd A, no_zero_divisors A
|
||||
|
||||
section
|
||||
|
||||
variables [s : integral_domain A] (a b c d e : A)
|
||||
include s
|
||||
|
||||
theorem mul_ne_zero_of_ne_zero_ne_zero {a b : A} (H1 : a ≠ 0) (H2 : b ≠ 0) : a * b ≠ 0 :=
|
||||
assume H : a * b = 0,
|
||||
or.elim (eq_zero_or_eq_zero_of_mul_eq_zero H) (assume H3, H1 H3) (assume H4, H2 H4)
|
||||
|
||||
theorem mul.cancel_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
|
||||
have H1 : b * a - c * a = 0, from iff.mp !eq_iff_minus_eq_zero H,
|
||||
have H2 : (b - c) * a = 0, from eq.trans !minus_distrib_right H1,
|
||||
have H3 : b - c = 0, from or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
|
||||
iff.elim_right !eq_iff_minus_eq_zero H3
|
||||
|
||||
theorem mul.cancel_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
|
||||
have H1 : a * b - a * c = 0, from iff.mp !eq_iff_minus_eq_zero H,
|
||||
have H2 : a * (b - c) = 0, from eq.trans !minus_distrib_left H1,
|
||||
have H3 : b - c = 0, from or.resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
|
||||
iff.elim_right !eq_iff_minus_eq_zero H3
|
||||
|
||||
-- TODO: do we want the iff versions?
|
||||
|
||||
-- TODO: wait for simplifier
|
||||
theorem square_eq_square_iff (a b : A) : a * a = b * b ↔ a = b ∨ a = -b := sorry
|
||||
|
||||
theorem square_eq_one_iff (a : A) : a * a = 1 ↔ a = 1 ∨ a = -1 := sorry
|
||||
|
||||
-- TODO: c - b * c → c = 0 ∨ b = 1 and variants
|
||||
|
||||
theorem dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : a * b | a * c) : b | c :=
|
||||
dvd_elim Hdvd
|
||||
(take d,
|
||||
assume H : a * b * d = a * c,
|
||||
have H1 : b * d = c, from mul.cancel_left Ha (!mul_assoc ▸ H),
|
||||
dvd_intro H1)
|
||||
|
||||
theorem dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : b * a | c * a) : b | c :=
|
||||
dvd_elim Hdvd
|
||||
(take d,
|
||||
assume H : b * a * d = c * a,
|
||||
have H1 : b * d * a = c * a, from eq.trans !mul_right_comm H,
|
||||
have H2 : b * d = c, from mul.cancel_right Ha H1,
|
||||
dvd_intro H2)
|
||||
|
||||
end
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
Loading…
Reference in a new issue