From 55ddbbcb8914b4b4b200540339e2844703e1dd98 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 11 May 2020 21:10:01 +0000 Subject: [PATCH] Remove unshackled files --- library/init/algebra/default.lean | 3 +- library/init/algebra/field.lean | 345 ------------- library/init/algebra/group.lean | 436 ---------------- library/init/algebra/norm_num.lean | 268 ---------- library/init/algebra/ordered_field.lean | 441 ---------------- library/init/algebra/ordered_group.lean | 634 ------------------------ library/init/algebra/ordered_ring.lean | 412 --------------- library/init/algebra/ring.lean | 338 ------------- 8 files changed, 1 insertion(+), 2876 deletions(-) delete mode 100644 library/init/algebra/field.lean delete mode 100644 library/init/algebra/group.lean delete mode 100644 library/init/algebra/norm_num.lean delete mode 100644 library/init/algebra/ordered_field.lean delete mode 100644 library/init/algebra/ordered_group.lean delete mode 100644 library/init/algebra/ordered_ring.lean delete mode 100644 library/init/algebra/ring.lean diff --git a/library/init/algebra/default.lean b/library/init/algebra/default.lean index 6473cbe1a5..7e83c3c3cd 100644 --- a/library/init/algebra/default.lean +++ b/library/init/algebra/default.lean @@ -4,5 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring -import init.algebra.field init.algebra.ordered_field init.algebra.norm_num init.algebra.functions +import init.algebra.functions diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean deleted file mode 100644 index 13649130a1..0000000000 --- a/library/init/algebra/field.lean +++ /dev/null @@ -1,345 +0,0 @@ -/- -Copyright (c) 2014 Robert Lewis. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Robert Lewis, Leonardo de Moura - -Structures with multiplicative and additive components, including division rings and fields. -The development is modeled after Isabelle's library. --/ -prelude -import init.algebra.ring -universe u - -/- Make sure instances defined in this file have lower priority than the ones - defined for concrete structures -/ -set_option default_priority 100 - -set_option old_structure_cmd true - -class division_ring (α : Type u) extends ring α, has_inv α, zero_ne_one_class α := -(mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1) -(inv_mul_cancel : ∀ {a : α}, a ≠ 0 → a⁻¹ * a = 1) -(inv_zero : (0 : α)⁻¹ = 0) - -variable {α : Type u} - -section division_ring -variables [division_ring α] - -protected definition algebra.div (a b : α) : α := -a * b⁻¹ - -instance division_ring_has_div : has_div α := -⟨algebra.div⟩ - -lemma division_def (a b : α) : a / b = a * b⁻¹ := -rfl - -@[simp] lemma inv_zero : 0⁻¹ = (0:α) := -division_ring.inv_zero - -@[simp] lemma div_zero (a : α) : a / 0 = (0:α) := -calc - a / 0 = (a:α) * 0⁻¹ : by rw division_def - ... = a * 0 : by rw inv_zero - ... = (0:α) : by rw mul_zero - -@[simp] -lemma mul_inv_cancel {a : α} (h : a ≠ 0) : a * a⁻¹ = 1 := -division_ring.mul_inv_cancel h - -@[simp] -lemma inv_mul_cancel {a : α} (h : a ≠ 0) : a⁻¹ * a = 1 := -division_ring.inv_mul_cancel h - -@[simp] -lemma one_div_eq_inv (a : α) : 1 / a = a⁻¹ := -one_mul a⁻¹ - -lemma inv_eq_one_div (a : α) : a⁻¹ = 1 / a := -by simp - -local attribute [simp] -division_def mul_comm mul_assoc -mul_left_comm mul_inv_cancel inv_mul_cancel - -lemma div_eq_mul_one_div (a b : α) : a / b = a * (1 / b) := -by simp - -lemma mul_one_div_cancel {a : α} (h : a ≠ 0) : a * (1 / a) = 1 := -by simp [h] - -lemma one_div_mul_cancel {a : α} (h : a ≠ 0) : (1 / a) * a = 1 := -by simp [h] - -lemma div_self {a : α} (h : a ≠ 0) : a / a = 1 := -by simp [h] - -lemma one_div_one : 1 / 1 = (1:α) := -div_self (ne.symm zero_ne_one) - -lemma mul_div_assoc (a b c : α) : (a * b) / c = a * (b / c) := -by simp - -lemma one_div_ne_zero {a : α} (h : a ≠ 0) : 1 / a ≠ 0 := -assume : 1 / a = 0, -have 0 = (1:α), from eq.symm (by rw [← mul_one_div_cancel h, this, mul_zero]), -absurd this zero_ne_one - -lemma ne_zero_of_one_div_ne_zero {a : α} (h : 1 / a ≠ 0) : a ≠ 0 := -assume ha : a = 0, begin rw [ha, div_zero] at h, contradiction end - -lemma inv_ne_zero {a : α} (h : a ≠ 0) : a⁻¹ ≠ 0 := -by rw inv_eq_one_div; exact one_div_ne_zero h - -lemma eq_zero_of_one_div_eq_zero {a : α} (h : 1 / a = 0) : a = 0 := -classical.by_cases - (assume ha, ha) - (assume ha, false.elim ((one_div_ne_zero ha) h)) - -lemma one_inv_eq : 1⁻¹ = (1:α) := -calc 1⁻¹ = 1 * 1⁻¹ : by rw [one_mul] - ... = (1:α) : by simp - -local attribute [simp] one_inv_eq - -lemma div_one (a : α) : a / 1 = a := -by simp - -lemma zero_div (a : α) : 0 / a = 0 := -by simp - --- note: integral domain has a "mul_ne_zero". a commutative division ring is an integral --- domain, but let's not define that class for now. -lemma division_ring.mul_ne_zero {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := -assume : a * b = 0, -have a * 1 = 0, by rw [← mul_one_div_cancel hb, ← mul_assoc, this, zero_mul], -have a = 0, by rwa mul_one at this, -absurd this ha - -lemma mul_ne_zero_comm {a b : α} (h : a * b ≠ 0) : b * a ≠ 0 := -have h₁ : a ≠ 0, from ne_zero_of_mul_ne_zero_right h, -have h₂ : b ≠ 0, from ne_zero_of_mul_ne_zero_left h, -division_ring.mul_ne_zero h₂ h₁ - -lemma eq_one_div_of_mul_eq_one {a b : α} (h : a * b = 1) : b = 1 / a := -have a ≠ 0, from - assume : a = 0, - have 0 = (1:α), by rwa [this, zero_mul] at h, - absurd this zero_ne_one, -have b = (1 / a) * a * b, by rw [one_div_mul_cancel this, one_mul], -show b = 1 / a, by rwa [mul_assoc, h, mul_one] at this - -lemma eq_one_div_of_mul_eq_one_left {a b : α} (h : b * a = 1) : b = 1 / a := -have a ≠ 0, from - assume : a = 0, - have 0 = (1:α), by rwa [this, mul_zero] at h, - absurd this zero_ne_one, -by rw [← h, mul_div_assoc, div_self this, mul_one] - -lemma division_ring.one_div_mul_one_div {a b : α} : (1 / a) * (1 / b) = 1 / (b * a) := -match classical.em (a = 0), classical.em (b = 0) with -| or.inr ha, or.inr hb := - have (b * a) * ((1 / a) * (1 / b)) = 1, - by rw [mul_assoc, ← mul_assoc a, mul_one_div_cancel ha, one_mul, mul_one_div_cancel hb], - eq_one_div_of_mul_eq_one this -| or.inl ha, _ := by simp [ha] -| _ , or.inl hb := by simp [hb] -end - -lemma one_div_neg_one_eq_neg_one : (1:α) / (-1) = -1 := -have (-1) * (-1) = (1:α), by rw [neg_mul_neg, one_mul], -eq.symm (eq_one_div_of_mul_eq_one this) - -lemma one_div_neg_eq_neg_one_div (a : α) : 1 / (- a) = - (1 / a) := -calc - 1 / (- a) = 1 / ((-1) * a) : by rw neg_eq_neg_one_mul - ... = (1 / a) * (1 / (- 1)) : by rw division_ring.one_div_mul_one_div - ... = (1 / a) * (-1) : by rw one_div_neg_one_eq_neg_one - ... = - (1 / a) : by rw [mul_neg_eq_neg_mul_symm, mul_one] - -lemma div_neg_eq_neg_div (a b : α) : b / (- a) = - (b / a) := -calc - b / (- a) = b * (1 / (- a)) : by rw [← inv_eq_one_div, division_def] - ... = b * -(1 / a) : by rw one_div_neg_eq_neg_one_div - ... = -(b * (1 / a)) : by rw neg_mul_eq_mul_neg - ... = - (b * a⁻¹) : by rw inv_eq_one_div - -lemma neg_div (a b : α) : (-b) / a = - (b / a) := -by rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul] - -lemma neg_div_neg_eq (a b : α) : (-a) / (-b) = a / b := -by rw [div_neg_eq_neg_div, neg_div, neg_neg] - -lemma one_div_one_div (a : α) : 1 / (1 / a) = a := -match classical.em (a = 0) with -| or.inl h := by simp [h] -| or.inr h := eq.symm (eq_one_div_of_mul_eq_one_left (mul_one_div_cancel h)) -end - -lemma inv_inv' (a : α) : a⁻¹⁻¹ = a := -by rw [inv_eq_one_div, inv_eq_one_div, one_div_one_div] - -lemma eq_of_one_div_eq_one_div {a b : α} (h : 1 / a = 1 / b) : a = b := -by rw [← one_div_one_div a, h,one_div_one_div] - -lemma mul_inv' (a b : α) : (b * a)⁻¹ = a⁻¹ * b⁻¹ := -eq.symm $ calc - a⁻¹ * b⁻¹ = (1 / a) * (1 / b) : by simp - ... = (1 / (b * a)) : division_ring.one_div_mul_one_div - ... = (b * a)⁻¹ : by simp - -lemma one_div_div (a b : α) : 1 / (a / b) = b / a := -by rw [one_div_eq_inv, division_def, mul_inv', - inv_inv', division_def] - -lemma div_helper {a : α} (b : α) (h : a ≠ 0) : (1 / (a * b)) * a = 1 / b := -by simp only [division_def, mul_inv', one_mul, mul_assoc, inv_mul_cancel h, mul_one] - -lemma mul_div_cancel (a : α) {b : α} (hb : b ≠ 0) : a * b / b = a := -by simp [hb] - -lemma div_mul_cancel (a : α) {b : α} (hb : b ≠ 0) : a / b * b = a := -by simp [hb] - -lemma div_div_eq_mul_div (a b c : α) : - a / (b / c) = (a * c) / b := -by rw [div_eq_mul_one_div, one_div_div, ← mul_div_assoc] - -lemma div_mul_left {a b : α} (hb : b ≠ 0) : b / (a * b) = 1 / a := -by simp only [division_def, mul_inv', ← mul_assoc, mul_inv_cancel hb] - -lemma mul_div_mul_right (a : α) (b : α) {c : α} (hc : c ≠ 0) : - (a * c) / (b * c) = a / b := -by rw [mul_div_assoc, div_mul_left hc, ← mul_div_assoc, mul_one] - -lemma div_add_div_same (a b c : α) : a / c + b / c = (a + b) / c := -eq.symm $ right_distrib a b (c⁻¹) - -lemma div_sub_div_same (a b c : α) : (a / c) - (b / c) = (a - b) / c := -by rw [sub_eq_add_neg, ← neg_div, div_add_div_same, sub_eq_add_neg] - -lemma one_div_mul_add_mul_one_div_eq_one_div_add_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : - (1 / a) * (a + b) * (1 / b) = 1 / a + 1 / b := -by rw [(left_distrib (1 / a)), (one_div_mul_cancel ha), right_distrib, one_mul, - mul_assoc, (mul_one_div_cancel hb), mul_one, add_comm] - -lemma one_div_mul_sub_mul_one_div_eq_one_div_add_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : - (1 / a) * (b - a) * (1 / b) = 1 / a - 1 / b := -by rw [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel ha), mul_sub_right_distrib, - one_mul, mul_assoc, (mul_one_div_cancel hb), mul_one] - -lemma div_eq_one_iff_eq (a : α) {b : α} (hb : b ≠ 0) : a / b = 1 ↔ a = b := -iff.intro - (assume : a / b = 1, calc - a = a / b * b : by simp [hb] - ... = 1 * b : by rw this - ... = b : by simp) - (assume : a = b, by simp [this, hb]) - -lemma eq_of_div_eq_one (a : α) {b : α} (Hb : b ≠ 0) : a / b = 1 → a = b := -iff.mp $ div_eq_one_iff_eq a Hb - -lemma eq_div_iff_mul_eq (a b : α) {c : α} (hc : c ≠ 0) : a = b / c ↔ a * c = b := -iff.intro - (assume : a = b / c, by rw [this, (div_mul_cancel _ hc)]) - (assume : a * c = b, by rw [← this, mul_div_cancel _ hc]) - -lemma eq_div_of_mul_eq (a b : α) {c : α} (hc : c ≠ 0) : a * c = b → a = b / c := -iff.mpr $ eq_div_iff_mul_eq a b hc - -lemma mul_eq_of_eq_div (a b: α) {c : α} (hc : c ≠ 0) : a = b / c → a * c = b := -iff.mp $ eq_div_iff_mul_eq a b hc - -lemma add_div_eq_mul_add_div (a b : α) {c : α} (hc : c ≠ 0) : a + b / c = (a * c + b) / c := -have (a + b / c) * c = a * c + b, by rw [right_distrib, (div_mul_cancel _ hc)], - (iff.mpr (eq_div_iff_mul_eq _ _ hc)) this - -lemma mul_mul_div (a : α) {c : α} (hc : c ≠ 0) : a = a * c * (1 / c) := -by simp [hc] - -lemma eq_of_mul_eq_mul_of_nonzero_left {a b c : α} (h : a ≠ 0) (h₂ : a * b = a * c) : b = c := -by rw [← one_mul b, ← inv_mul_cancel h, mul_assoc, h₂, ← mul_assoc, inv_mul_cancel h, one_mul] - -lemma eq_of_mul_eq_mul_of_nonzero_right {a b c : α} (h : c ≠ 0) (h2 : a * c = b * c) : a = b := -by rw [← mul_one a, ← mul_inv_cancel h, ← mul_assoc, h2, mul_assoc, mul_inv_cancel h, mul_one] - -end division_ring - -class field (α : Type u) extends comm_ring α, has_inv α, zero_ne_one_class α := -(mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1) -(inv_zero : (0 : α)⁻¹ = 0) - -section field - -variable [field α] - -instance field.to_division_ring : division_ring α := -{ inv_mul_cancel := λ _ h, by rw [mul_comm, field.mul_inv_cancel h] - ..show field α, by apply_instance } - -lemma one_div_mul_one_div (a b : α) : (1 / a) * (1 / b) = 1 / (a * b) := -by rw [division_ring.one_div_mul_one_div, mul_comm b] - -lemma div_mul_right {a : α} (b : α) (ha : a ≠ 0) : a / (a * b) = 1 / b := -by rw [mul_comm, div_mul_left ha] - -lemma mul_div_cancel_left {a : α} (b : α) (ha : a ≠ 0) : a * b / a = b := -by rw [mul_comm a, (mul_div_cancel _ ha)] - -lemma mul_div_cancel' (a : α) {b : α} (hb : b ≠ 0) : b * (a / b) = a := -by rw [mul_comm, (div_mul_cancel _ hb)] - -lemma one_div_add_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) := -by rw [add_comm, ← div_mul_left ha, ← div_mul_right _ hb, - division_def, division_def, division_def, ← right_distrib, mul_comm a] - -local attribute [simp] mul_assoc mul_comm mul_left_comm - -lemma div_mul_div (a b c d : α) : - (a / b) * (c / d) = (a * c) / (b * d) := -begin simp [division_def], rw [mul_inv', mul_comm d⁻¹] end - -lemma mul_div_mul_left (a b : α) {c : α} (hc : c ≠ 0) : - (c * a) / (c * b) = a / b := -by rw [← div_mul_div, div_self hc, one_mul] - -lemma div_mul_eq_mul_div (a b c : α) : (b / c) * a = (b * a) / c := -by simp [division_def] - -lemma div_mul_eq_mul_div_comm (a b c : α) : - (b / c) * a = b * (a / c) := -by rw [div_mul_eq_mul_div, ← one_mul c, ← div_mul_div, - div_one, one_mul] - -lemma div_add_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) : - (a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) := -by rw [← mul_div_mul_right _ b hd, ← mul_div_mul_left c d hb, div_add_div_same] - -lemma div_sub_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) : - (a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) := -begin - simp [sub_eq_add_neg], - rw [neg_eq_neg_one_mul, ← mul_div_assoc, div_add_div _ _ hb hd, - ← mul_assoc, mul_comm b, mul_assoc, ← neg_eq_neg_one_mul] -end - -lemma mul_eq_mul_of_div_eq_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) - (hd : d ≠ 0) (h : a / b = c / d) : a * d = c * b := -by rw [← mul_one (a*d), mul_assoc, mul_comm d, ← mul_assoc, ← div_self hb, - ← div_mul_eq_mul_div_comm, h, div_mul_eq_mul_div, div_mul_cancel _ hd] - -lemma div_div_eq_div_mul (a b c : α) : - (a / b) / c = a / (b * c) := -by rw [div_eq_mul_one_div, div_mul_div, mul_one] - -lemma div_div_div_div_eq (a : α) {b c d : α} : - (a / b) / (c / d) = (a * d) / (b * c) := -by rw [div_div_eq_mul_div, div_mul_eq_mul_div, - div_div_eq_div_mul] - -lemma div_mul_eq_div_mul_one_div (a b c : α) : - a / (b * c) = (a / b) * (1 / c) := -by rw [← div_div_eq_div_mul, ← div_eq_mul_one_div] - -end field diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean deleted file mode 100644 index f78268c2f7..0000000000 --- a/library/init/algebra/group.lean +++ /dev/null @@ -1,436 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad, Leonardo de Moura --/ -prelude -import init.logic init.algebra.classes init.meta init.meta.decl_cmds init.meta.smt.rsimp - -/- Make sure instances defined in this file have lower priority than the ones - defined for concrete structures -/ -set_option default_priority 100 - -set_option old_structure_cmd true - -universe u -variables {α : Type u} - -class semigroup (α : Type u) extends has_mul α := -(mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)) - -class comm_semigroup (α : Type u) extends semigroup α := -(mul_comm : ∀ a b : α, a * b = b * a) - -class left_cancel_semigroup (α : Type u) extends semigroup α := -(mul_left_cancel : ∀ a b c : α, a * b = a * c → b = c) - -class right_cancel_semigroup (α : Type u) extends semigroup α := -(mul_right_cancel : ∀ a b c : α, a * b = c * b → a = c) - -class monoid (α : Type u) extends semigroup α, has_one α := -(one_mul : ∀ a : α, 1 * a = a) (mul_one : ∀ a : α, a * 1 = a) - -class comm_monoid (α : Type u) extends monoid α, comm_semigroup α - -class group (α : Type u) extends monoid α, has_inv α := -(mul_left_inv : ∀ a : α, a⁻¹ * a = 1) - -class comm_group (α : Type u) extends group α, comm_monoid α - -lemma mul_assoc [semigroup α] : ∀ a b c : α, a * b * c = a * (b * c) := -semigroup.mul_assoc - -instance semigroup_to_is_associative [semigroup α] : is_associative α (*) := -⟨mul_assoc⟩ - -lemma mul_comm [comm_semigroup α] : ∀ a b : α, a * b = b * a := -comm_semigroup.mul_comm - -instance comm_semigroup_to_is_commutative [comm_semigroup α] : is_commutative α (*) := -⟨mul_comm⟩ - -lemma mul_left_comm [comm_semigroup α] : ∀ a b c : α, a * (b * c) = b * (a * c) := -left_comm has_mul.mul mul_comm mul_assoc - -local attribute [simp] mul_assoc - -lemma mul_right_comm [comm_semigroup α] : ∀ a b c : α, a * b * c = a * c * b := -right_comm has_mul.mul mul_comm mul_assoc - -lemma mul_left_cancel [left_cancel_semigroup α] {a b c : α} : a * b = a * c → b = c := -left_cancel_semigroup.mul_left_cancel a b c - -lemma mul_right_cancel [right_cancel_semigroup α] {a b c : α} : a * b = c * b → a = c := -right_cancel_semigroup.mul_right_cancel a b c - -lemma mul_left_cancel_iff [left_cancel_semigroup α] {a b c : α} : a * b = a * c ↔ b = c := -⟨mul_left_cancel, congr_arg _⟩ - -lemma mul_right_cancel_iff [right_cancel_semigroup α] {a b c : α} : b * a = c * a ↔ b = c := -⟨mul_right_cancel, congr_arg _⟩ - -@[simp] lemma one_mul [monoid α] : ∀ a : α, 1 * a = a := -monoid.one_mul - -@[simp] lemma mul_one [monoid α] : ∀ a : α, a * 1 = a := -monoid.mul_one - -@[simp] lemma mul_left_inv [group α] : ∀ a : α, a⁻¹ * a = 1 := -group.mul_left_inv - -def inv_mul_self := @mul_left_inv - -@[simp] lemma inv_mul_cancel_left [group α] (a b : α) : a⁻¹ * (a * b) = b := -by rw [← mul_assoc, mul_left_inv, one_mul] - -@[simp] lemma inv_mul_cancel_right [group α] (a b : α) : a * b⁻¹ * b = a := -by simp - -@[simp] lemma inv_eq_of_mul_eq_one [group α] {a b : α} (h : a * b = 1) : a⁻¹ = b := -by rw [← mul_one a⁻¹, ←h, ←mul_assoc, mul_left_inv, one_mul] - -@[simp] lemma one_inv [group α] : 1⁻¹ = (1 : α) := -inv_eq_of_mul_eq_one (one_mul 1) - -@[simp] lemma inv_inv [group α] (a : α) : (a⁻¹)⁻¹ = a := -inv_eq_of_mul_eq_one (mul_left_inv a) - -@[simp] lemma mul_right_inv [group α] (a : α) : a * a⁻¹ = 1 := -have a⁻¹⁻¹ * a⁻¹ = 1, by rw mul_left_inv, -by rwa [inv_inv] at this - -def mul_inv_self := @mul_right_inv - -lemma inv_inj [group α] {a b : α} (h : a⁻¹ = b⁻¹) : a = b := -have a = a⁻¹⁻¹, by simp, -begin rw this, simp [h] end - -lemma group.mul_left_cancel [group α] {a b c : α} (h : a * b = a * c) : b = c := -have a⁻¹ * (a * b) = b, by simp, -begin simp [h] at this, rw this end - -lemma group.mul_right_cancel [group α] {a b c : α} (h : a * b = c * b) : a = c := -have a * b * b⁻¹ = a, by simp, -begin simp [h] at this, rw this end - -instance group.to_left_cancel_semigroup [s : group α] : left_cancel_semigroup α := -{ mul_left_cancel := @group.mul_left_cancel α s, ..s } - -instance group.to_right_cancel_semigroup [s : group α] : right_cancel_semigroup α := -{ mul_right_cancel := @group.mul_right_cancel α s, ..s } - -lemma mul_inv_cancel_left [group α] (a b : α) : a * (a⁻¹ * b) = b := -by rw [← mul_assoc, mul_right_inv, one_mul] - -lemma mul_inv_cancel_right [group α] (a b : α) : a * b * b⁻¹ = a := -by rw [mul_assoc, mul_right_inv, mul_one] - -@[simp] lemma mul_inv_rev [group α] (a b : α) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := -inv_eq_of_mul_eq_one begin rw [mul_assoc, ← mul_assoc b, mul_right_inv, one_mul, mul_right_inv] end - -lemma eq_inv_of_eq_inv [group α] {a b : α} (h : a = b⁻¹) : b = a⁻¹ := -by simp [h] - -lemma eq_inv_of_mul_eq_one [group α] {a b : α} (h : a * b = 1) : a = b⁻¹ := -have a⁻¹ = b, from inv_eq_of_mul_eq_one h, -by simp [this.symm] - -lemma eq_mul_inv_of_mul_eq [group α] {a b c : α} (h : a * c = b) : a = b * c⁻¹ := -by simp [h.symm] - -lemma eq_inv_mul_of_mul_eq [group α] {a b c : α} (h : b * a = c) : a = b⁻¹ * c := -by simp [h.symm] - -lemma inv_mul_eq_of_eq_mul [group α] {a b c : α} (h : b = a * c) : a⁻¹ * b = c := -by simp [h] - -lemma mul_inv_eq_of_eq_mul [group α] {a b c : α} (h : a = c * b) : a * b⁻¹ = c := -by simp [h] - -lemma eq_mul_of_mul_inv_eq [group α] {a b c : α} (h : a * c⁻¹ = b) : a = b * c := -by simp [h.symm] - -lemma eq_mul_of_inv_mul_eq [group α] {a b c : α} (h : b⁻¹ * a = c) : a = b * c := -by simp [h.symm, mul_inv_cancel_left] - -lemma mul_eq_of_eq_inv_mul [group α] {a b c : α} (h : b = a⁻¹ * c) : a * b = c := -by rw [h, mul_inv_cancel_left] - -lemma mul_eq_of_eq_mul_inv [group α] {a b c : α} (h : a = c * b⁻¹) : a * b = c := -by simp [h] - -lemma mul_inv [comm_group α] (a b : α) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := -by rw [mul_inv_rev, mul_comm] - -/- αdditive "sister" structures. - Example, add_semigroup mirrors semigroup. - These structures exist just to help automation. - In an alternative design, we could have the binary operation as an - extra argument for semigroup, monoid, group, etc. However, the lemmas - would be hard to index since they would not contain any constant. - For example, mul_assoc would be - - lemma mul_assoc {α : Type u} {op : α → α → α} [semigroup α op] : - ∀ a b c : α, op (op a b) c = op a (op b c) := - semigroup.mul_assoc - - The simplifier cannot effectively use this lemma since the pattern for - the left-hand-side would be - - ?op (?op ?a ?b) ?c - - Remark: we use a tactic for transporting theorems from the multiplicative fragment - to the additive one. --/ - -class add_semigroup (α : Type u) extends has_add α := -(add_assoc : ∀ a b c : α, a + b + c = a + (b + c)) - -class add_comm_semigroup (α : Type u) extends add_semigroup α := -(add_comm : ∀ a b : α, a + b = b + a) - -class add_left_cancel_semigroup (α : Type u) extends add_semigroup α := -(add_left_cancel : ∀ a b c : α, a + b = a + c → b = c) - -class add_right_cancel_semigroup (α : Type u) extends add_semigroup α := -(add_right_cancel : ∀ a b c : α, a + b = c + b → a = c) - -class add_monoid (α : Type u) extends add_semigroup α, has_zero α := -(zero_add : ∀ a : α, 0 + a = a) (add_zero : ∀ a : α, a + 0 = a) - -class add_comm_monoid (α : Type u) extends add_monoid α, add_comm_semigroup α - -class add_group (α : Type u) extends add_monoid α, has_neg α := -(add_left_neg : ∀ a : α, -a + a = 0) - -class add_comm_group (α : Type u) extends add_group α, add_comm_monoid α - -open tactic - -meta def transport_with_dict (dict : name_map name) (src : name) (tgt : name) : command := -copy_decl_using dict src tgt ->> copy_attribute `reducible src tgt tt ->> copy_attribute `simp src tgt tt ->> copy_attribute `instance src tgt tt - -/- Transport multiplicative to additive -/ -meta def transport_multiplicative_to_additive (ls : list (name × name)) : command := -let dict := native.rb_map.of_list ls in -ls.foldl (λ t ⟨src, tgt⟩, do - env ← get_env, - if (env.get tgt).to_bool = ff - then t >> transport_with_dict dict src tgt - else t) -skip - -run_cmd transport_multiplicative_to_additive - [/- map operations -/ - (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg), - (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg), - /- map constructors -/ - (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk), - /- map structures -/ - (`semigroup, `add_semigroup), - (`monoid, `add_monoid), - (`group, `add_group), - (`comm_semigroup, `add_comm_semigroup), - (`comm_monoid, `add_comm_monoid), - (`comm_group, `add_comm_group), - (`left_cancel_semigroup, `add_left_cancel_semigroup), - (`right_cancel_semigroup, `add_right_cancel_semigroup), - (`left_cancel_semigroup.mk, `add_left_cancel_semigroup.mk), - (`right_cancel_semigroup.mk, `add_right_cancel_semigroup.mk), - /- map instances -/ - (`semigroup.to_has_mul, `add_semigroup.to_has_add), - (`monoid.to_has_one, `add_monoid.to_has_zero), - (`group.to_has_inv, `add_group.to_has_neg), - (`comm_semigroup.to_semigroup, `add_comm_semigroup.to_add_semigroup), - (`monoid.to_semigroup, `add_monoid.to_add_semigroup), - (`comm_monoid.to_monoid, `add_comm_monoid.to_add_monoid), - (`comm_monoid.to_comm_semigroup, `add_comm_monoid.to_add_comm_semigroup), - (`group.to_monoid, `add_group.to_add_monoid), - (`comm_group.to_group, `add_comm_group.to_add_group), - (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid), - (`left_cancel_semigroup.to_semigroup, `add_left_cancel_semigroup.to_add_semigroup), - (`right_cancel_semigroup.to_semigroup, `add_right_cancel_semigroup.to_add_semigroup), - /- map projections -/ - (`semigroup.mul_assoc, `add_semigroup.add_assoc), - (`comm_semigroup.mul_comm, `add_comm_semigroup.add_comm), - (`left_cancel_semigroup.mul_left_cancel, `add_left_cancel_semigroup.add_left_cancel), - (`right_cancel_semigroup.mul_right_cancel, `add_right_cancel_semigroup.add_right_cancel), - (`monoid.one_mul, `add_monoid.zero_add), - (`monoid.mul_one, `add_monoid.add_zero), - (`group.mul_left_inv, `add_group.add_left_neg), - (`group.mul, `add_group.add), - (`group.mul_assoc, `add_group.add_assoc), - /- map lemmas -/ - (`mul_assoc, `add_assoc), - (`mul_comm, `add_comm), - (`mul_left_comm, `add_left_comm), - (`mul_right_comm, `add_right_comm), - (`one_mul, `zero_add), - (`mul_one, `add_zero), - (`mul_left_inv, `add_left_neg), - (`mul_left_cancel, `add_left_cancel), - (`mul_right_cancel, `add_right_cancel), - (`mul_left_cancel_iff, `add_left_cancel_iff), - (`mul_right_cancel_iff, `add_right_cancel_iff), - (`inv_mul_cancel_left, `neg_add_cancel_left), - (`inv_mul_cancel_right, `neg_add_cancel_right), - (`eq_inv_mul_of_mul_eq, `eq_neg_add_of_add_eq), - (`inv_eq_of_mul_eq_one, `neg_eq_of_add_eq_zero), - (`inv_inv, `neg_neg), - (`mul_right_inv, `add_right_neg), - (`mul_inv_cancel_left, `add_neg_cancel_left), - (`mul_inv_cancel_right, `add_neg_cancel_right), - (`mul_inv_rev, `neg_add_rev), - (`mul_inv, `neg_add), - (`inv_inj, `neg_inj), - (`group.mul_left_cancel, `add_group.add_left_cancel), - (`group.mul_right_cancel, `add_group.add_right_cancel), - (`group.to_left_cancel_semigroup, `add_group.to_left_cancel_add_semigroup), - (`group.to_right_cancel_semigroup, `add_group.to_right_cancel_add_semigroup), - (`eq_inv_of_eq_inv, `eq_neg_of_eq_neg), - (`eq_inv_of_mul_eq_one, `eq_neg_of_add_eq_zero), - (`eq_mul_inv_of_mul_eq, `eq_add_neg_of_add_eq), - (`inv_mul_eq_of_eq_mul, `neg_add_eq_of_eq_add), - (`mul_inv_eq_of_eq_mul, `add_neg_eq_of_eq_add), - (`eq_mul_of_mul_inv_eq, `eq_add_of_add_neg_eq), - (`eq_mul_of_inv_mul_eq, `eq_add_of_neg_add_eq), - (`mul_eq_of_eq_inv_mul, `add_eq_of_eq_neg_add), - (`mul_eq_of_eq_mul_inv, `add_eq_of_eq_add_neg), - (`one_inv, `neg_zero) -] - -instance add_semigroup_to_is_eq_associative [add_semigroup α] : is_associative α (+) := -⟨add_assoc⟩ - -instance add_comm_semigroup_to_is_eq_commutative [add_comm_semigroup α] : is_commutative α (+) := -⟨add_comm⟩ - -local attribute [simp] add_assoc add_comm add_left_comm - -def neg_add_self := @add_left_neg -def add_neg_self := @add_right_neg -def eq_of_add_eq_add_left := @add_left_cancel -def eq_of_add_eq_add_right := @add_right_cancel - -@[reducible] protected def algebra.sub [add_group α] (a b : α) : α := -a + -b - -instance add_group_has_sub [add_group α] : has_sub α := -⟨algebra.sub⟩ - -local attribute [simp] -lemma sub_eq_add_neg [add_group α] (a b : α) : a - b = a + -b := -rfl - -lemma sub_self [add_group α] (a : α) : a - a = 0 := -add_right_neg a - -lemma sub_add_cancel [add_group α] (a b : α) : a - b + b = a := -neg_add_cancel_right a b - -lemma add_sub_cancel [add_group α] (a b : α) : a + b - b = a := -add_neg_cancel_right a b - -lemma add_sub_assoc [add_group α] (a b c : α) : a + b - c = a + (b - c) := -by rw [sub_eq_add_neg, add_assoc, ←sub_eq_add_neg] - -lemma eq_of_sub_eq_zero [add_group α] {a b : α} (h : a - b = 0) : a = b := -have 0 + b = b, by rw zero_add, -have (a - b) + b = b, by rwa h, -by rwa [sub_eq_add_neg, neg_add_cancel_right] at this - -lemma sub_eq_zero_of_eq [add_group α] {a b : α} (h : a = b) : a - b = 0 := -by rw [h, sub_self] - -lemma sub_eq_zero_iff_eq [add_group α] {a b : α} : a - b = 0 ↔ a = b := -⟨eq_of_sub_eq_zero, sub_eq_zero_of_eq⟩ - -lemma zero_sub [add_group α] (a : α) : 0 - a = -a := -zero_add (-a) - -lemma sub_zero [add_group α] (a : α) : a - 0 = a := -by rw [sub_eq_add_neg, neg_zero, add_zero] - -lemma sub_ne_zero_of_ne [add_group α] {a b : α} (h : a ≠ b) : a - b ≠ 0 := -begin - intro hab, - apply h, - apply eq_of_sub_eq_zero hab -end - -lemma sub_neg_eq_add [add_group α] (a b : α) : a - (-b) = a + b := -by rw [sub_eq_add_neg, neg_neg] - -lemma neg_sub [add_group α] (a b : α) : -(a - b) = b - a := -neg_eq_of_add_eq_zero (by rw [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, add_right_neg]) - -lemma add_sub [add_group α] (a b c : α) : a + (b - c) = a + b - c := -by simp - -lemma sub_add_eq_sub_sub_swap [add_group α] (a b c : α) : a - (b + c) = a - c - b := -by simp - -lemma add_sub_add_right_eq_sub [add_group α] (a b c : α) : (a + c) - (b + c) = a - b := -by rw [sub_add_eq_sub_sub_swap]; simp - -lemma eq_sub_of_add_eq [add_group α] {a b c : α} (h : a + c = b) : a = b - c := -by simp [h.symm] - -lemma sub_eq_of_eq_add [add_group α] {a b c : α} (h : a = c + b) : a - b = c := -by simp [h] - -lemma eq_add_of_sub_eq [add_group α] {a b c : α} (h : a - c = b) : a = b + c := -by simp [h.symm] - -lemma add_eq_of_eq_sub [add_group α] {a b c : α} (h : a = c - b) : a + b = c := -by simp [h] - -lemma sub_add_eq_sub_sub [add_comm_group α] (a b c : α) : a - (b + c) = a - b - c := -by simp - -lemma neg_add_eq_sub [add_comm_group α] (a b : α) : -a + b = b - a := -by simp - -lemma sub_add_eq_add_sub [add_comm_group α] (a b c : α) : a - b + c = a + c - b := -by simp - -lemma sub_sub [add_comm_group α] (a b c : α) : a - b - c = a - (b + c) := -by simp - -lemma sub_add [add_comm_group α] (a b c : α) : a - b + c = a - (b - c) := -by simp - -lemma add_sub_add_left_eq_sub [add_comm_group α] (a b c : α) : (c + a) - (c + b) = a - b := -by simp - -lemma eq_sub_of_add_eq' [add_comm_group α] {a b c : α} (h : c + a = b) : a = b - c := -by simp [h.symm] - -lemma sub_eq_of_eq_add' [add_comm_group α] {a b c : α} (h : a = b + c) : a - b = c := -begin simp [h], rw [add_left_comm], simp end - -lemma eq_add_of_sub_eq' [add_comm_group α] {a b c : α} (h : a - b = c) : a = b + c := -by simp [h.symm] - -lemma add_eq_of_eq_sub' [add_comm_group α] {a b c : α} (h : b = c - a) : a + b = c := -begin simp [h], rw [add_comm c, add_neg_cancel_left] end - -lemma sub_sub_self [add_comm_group α] (a b : α) : a - (a - b) = b := -begin simp, rw [add_comm b, add_neg_cancel_left] end - -lemma add_sub_comm [add_comm_group α] (a b c d : α) : a + b - (c + d) = (a - c) + (b - d) := -by simp - -lemma sub_eq_sub_add_sub [add_comm_group α] (a b c : α) : a - b = c - b + (a - c) := -begin simp, rw [add_left_comm c], simp end - -lemma neg_neg_sub_neg [add_comm_group α] (a b : α) : - (-a - -b) = a - b := -by simp - -/- The following lemmas generate too many instances for rsimp -/ -attribute [no_rsimp] - mul_assoc mul_comm mul_left_comm - add_assoc add_comm add_left_comm diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean deleted file mode 100644 index 9721558d0c..0000000000 --- a/library/init/algebra/norm_num.lean +++ /dev/null @@ -1,268 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Robert Lewis and Leonardo de Moura --/ -prelude -import init.algebra.field init.algebra.ordered_ring -import init.data.nat.lemmas - -namespace norm_num -universe u -variable {α : Type u} - -def add1 [has_add α] [has_one α] (a : α) : α := -a + 1 - -local attribute [reducible] bit0 bit1 add1 -local attribute [simp] right_distrib left_distrib sub_eq_add_neg - -private meta def u : tactic unit := -`[unfold bit0 bit1 add1] - -private meta def usimp : tactic unit := -u >> `[simp [add_comm, add_left_comm]] - -lemma mul_zero [mul_zero_class α] (a : α) : a * 0 = 0 := -by simp - -lemma zero_mul [mul_zero_class α] (a : α) : 0 * a = 0 := -by simp - -lemma mul_one [monoid α] (a : α) : a * 1 = a := -by simp - -lemma mul_bit0 [distrib α] (a b : α) : a * (bit0 b) = bit0 (a * b) := -by simp - -lemma mul_bit0_helper [distrib α] (a b t : α) (h : a * b = t) : a * (bit0 b) = bit0 t := -begin rw [← h], simp end - -lemma mul_bit1 [semiring α] (a b : α) : a * (bit1 b) = bit0 (a * b) + a := -by simp - -lemma mul_bit1_helper [semiring α] (a b s t : α) (hs : a * b = s) (ht : bit0 s + a = t) : - a * (bit1 b) = t := -by simp [hs, ht] - -lemma subst_into_prod [has_mul α] (l r tl tr t : α) (prl : l = tl) (prr : r = tr) (prt : tl * tr = t) : l * r = t := -by simp [prl, prr, prt] - -lemma mk_cong (op : α → α) (a b : α) (h : a = b) : op a = op b := -by simp [h] - -lemma neg_add_neg_eq_of_add_add_eq_zero [add_comm_group α] (a b c : α) (h : c + a + b = 0) : -a + -b = c := -begin - apply add_neg_eq_of_eq_add, - apply neg_eq_of_add_eq_zero, - simp [add_comm, add_left_comm] at h, simp [add_comm], assumption -end - -lemma neg_add_neg_helper [add_comm_group α] (a b c : α) (h : a + b = c) : -a + -b = -c := -begin apply @neg_inj α, simp [neg_add, neg_neg], assumption end - -lemma neg_add_pos_eq_of_eq_add [add_comm_group α] (a b c : α) (h : b = c + a) : -a + b = c := -begin apply neg_add_eq_of_eq_add, simp [add_comm] at h, assumption end - -lemma neg_add_pos_helper1 [add_comm_group α] (a b c : α) (h : b + c = a) : -a + b = -c := -begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq h end - -lemma neg_add_pos_helper2 [add_comm_group α] (a b c : α) (h : a + c = b) : -a + b = c := -begin apply neg_add_eq_of_eq_add, rw h end - -lemma pos_add_neg_helper [add_comm_group α] (a b c : α) (h : b + a = c) : a + b = c := -by rw [← h, add_comm a b] - -lemma subst_into_subtr [add_group α] (l r t : α) (h : l + -r = t) : l - r = t := -by simp [h] - -lemma neg_neg_helper [add_group α] (a b : α) (h : a = -b) : -a = b := -by simp [h] - -lemma neg_mul_neg_helper [ring α] (a b c : α) (h : a * b = c) : (-a) * (-b) = c := -by simp [h] - -lemma neg_mul_pos_helper [ring α] (a b c : α) (h : a * b = c) : (-a) * b = -c := -by simp [h] - -lemma pos_mul_neg_helper [ring α] (a b c : α) (h : a * b = c) : a * (-b) = -c := -by simp [h] - -lemma div_add_helper [field α] (n d b c val : α) (hd : d ≠ 0) (h : n + b * d = val) - (h2 : c * d = val) : n / d + b = c := -begin - apply eq_of_mul_eq_mul_of_nonzero_right hd, - rw [h2, ← h, right_distrib, div_mul_cancel _ hd] -end - -lemma add_div_helper [field α] (n d b c val : α) (hd : d ≠ 0) (h : d * b + n = val) - (h2 : d * c = val) : b + n / d = c := -begin - apply eq_of_mul_eq_mul_of_nonzero_left hd, - rw [h2, ← h, left_distrib, mul_div_cancel' _ hd] -end - -lemma div_mul_helper [field α] (n d c v : α) (h : (n * c) / d = v) : - (n / d) * c = v := -by rw [← h, div_mul_eq_mul_div_comm, mul_div_assoc] - -lemma mul_div_helper [field α] (a n d v : α) (hd : d ≠ 0) (h : (a * n) / d = v) : - a * (n / d) = v := -by rw [← h, mul_div_assoc] - -lemma nonzero_of_div_helper [field α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 := -begin - intro hab, - have habb : (a / b) * b = 0, rw [hab, zero_mul], - rw [div_mul_cancel _ hb] at habb, - exact ha habb -end - -lemma div_helper [field α] (n d v : α) (hd : d ≠ 0) (h : v * d = n) : n / d = v := -begin - apply eq_of_mul_eq_mul_of_nonzero_right hd, - rw (div_mul_cancel _ hd), - exact eq.symm h -end - -lemma div_eq_div_helper [field α] (a b c d v : α) (h1 : a * d = v) (h2 : c * b = v) - (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d := -begin - apply eq_div_of_mul_eq, - exact hd, - rw div_mul_eq_mul_div, - apply eq.symm, - apply eq_div_of_mul_eq, - exact hb, - rw [h1, h2] -end - -lemma subst_into_div [has_div α] (a₁ b₁ a₂ b₂ v : α) (h : a₁ / b₁ = v) (h1 : a₂ = a₁) - (h2 : b₂ = b₁) : a₂ / b₂ = v := -by rw [h1, h2, h] - - -lemma add_comm_four [add_comm_semigroup α] (a b : α) : a + a + (b + b) = (a + b) + (a + b) := -by simp [add_left_comm] - -lemma add_comm_middle [add_comm_semigroup α] (a b c : α) : a + b + c = a + c + b := -by simp [add_comm, add_left_comm] - -lemma bit0_add_bit0 [add_comm_semigroup α] (a b : α) : bit0 a + bit0 b = bit0 (a + b) := -by usimp - -lemma bit0_add_bit0_helper [add_comm_semigroup α] (a b t : α) (h : a + b = t) : - bit0 a + bit0 b = bit0 t := -begin rw [← h], usimp end - -lemma bit1_add_bit0 [add_comm_semigroup α] [has_one α] (a b : α) : bit1 a + bit0 b = bit1 (a + b) := -by rw add_comm; usimp - -lemma bit1_add_bit0_helper [add_comm_semigroup α] [has_one α] (a b t : α) - (h : a + b = t) : bit1 a + bit0 b = bit1 t := -begin rw [← h, add_comm], usimp end - -lemma bit0_add_bit1 [add_comm_semigroup α] [has_one α] (a b : α) : - bit0 a + bit1 b = bit1 (a + b) := -by usimp - -lemma bit0_add_bit1_helper [add_comm_semigroup α] [has_one α] (a b t : α) - (h : a + b = t) : bit0 a + bit1 b = bit1 t := -begin rw [← h], usimp end - -lemma bit1_add_bit1 [add_comm_semigroup α] [has_one α] (a b : α) : - bit1 a + bit1 b = bit0 (add1 (a + b)) := -by usimp - -lemma bit1_add_bit1_helper [add_comm_semigroup α] [has_one α] (a b t s : α) - (h : (a + b) = t) (h2 : add1 t = s) : bit1 a + bit1 b = bit0 s := -begin rw [← h] at h2, rw [← h2], usimp end - -lemma bin_add_zero [add_monoid α] (a : α) : a + 0 = a := -by simp - -lemma bin_zero_add [add_monoid α] (a : α) : 0 + a = a := -by simp - -lemma one_add_bit0 [add_comm_semigroup α] [has_one α] (a : α) : 1 + bit0 a = bit1 a := -begin unfold bit0 bit1, simp [add_comm] end - -lemma bit0_add_one [has_add α] [has_one α] (a : α) : bit0 a + 1 = bit1 a := -rfl - -lemma bit1_add_one [has_add α] [has_one α] (a : α) : bit1 a + 1 = add1 (bit1 a) := -rfl - -lemma bit1_add_one_helper [has_add α] [has_one α] (a t : α) (h : add1 (bit1 a) = t) : - bit1 a + 1 = t := -by rw [← h] - -lemma one_add_bit1 [add_comm_semigroup α] [has_one α] (a : α) : 1 + bit1 a = add1 (bit1 a) := -begin unfold bit0 bit1 add1, simp [add_left_comm] end - -lemma one_add_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α) - (h : add1 (bit1 a) = t) : 1 + bit1 a = t := -begin rw [← h], usimp end - -lemma add1_bit0 [has_add α] [has_one α] (a : α) : add1 (bit0 a) = bit1 a := -rfl - -lemma add1_bit1 [add_comm_semigroup α] [has_one α] (a : α) : - add1 (bit1 a) = bit0 (add1 a) := -by usimp - -lemma add1_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α) (h : add1 a = t) : - add1 (bit1 a) = bit0 t := -begin rw [← h], usimp end - -lemma add1_one [has_add α] [has_one α] : add1 (1 : α) = bit0 1 := -rfl - -lemma add1_zero [add_monoid α] [has_one α] : add1 (0 : α) = 1 := -by usimp - -lemma one_add_one [has_add α] [has_one α] : (1 : α) + 1 = bit0 1 := -rfl - -lemma subst_into_sum [has_add α] (l r tl tr t : α) (prl : l = tl) (prr : r = tr) - (prt : tl + tr = t) : l + r = t := -by rw [← prt, prr, prl] - -lemma neg_zero_helper [add_group α] (a : α) (h : a = 0) : - a = 0 := -begin rw h, simp end - -lemma pos_bit0_helper [linear_ordered_semiring α] (a : α) (h : a > 0) : bit0 a > 0 := -begin u, apply add_pos h h end - -lemma nonneg_bit0_helper [linear_ordered_semiring α] (a : α) (h : a ≥ 0) : bit0 a ≥ 0 := -begin u, apply add_nonneg h h end - -lemma pos_bit1_helper [linear_ordered_semiring α] (a : α) (h : a ≥ 0) : bit1 a > 0 := -begin - u, - apply add_pos_of_nonneg_of_pos, - apply nonneg_bit0_helper _ h, - apply zero_lt_one -end - -lemma nonneg_bit1_helper [linear_ordered_semiring α] (a : α) (h : a ≥ 0) : bit1 a ≥ 0 := -begin apply le_of_lt, apply pos_bit1_helper _ h end - -lemma nonzero_of_pos_helper [linear_ordered_semiring α] (a : α) (h : a > 0) : a ≠ 0 := - ne_of_gt h - -lemma nonzero_of_neg_helper [linear_ordered_ring α] (a : α) (h : a ≠ 0) : -a ≠ 0 := -begin intro ha, apply h, apply neg_inj, rwa neg_zero end - -lemma sub_nat_zero_helper {a b c d: ℕ} (hac : a = c) (hbd : b = d) (hcd : c < d) : a - b = 0 := -begin - simp *, apply nat.sub_eq_zero_of_le, apply le_of_lt, assumption -end - -lemma sub_nat_pos_helper {a b c d e : ℕ} (hac : a = c) (hbd : b = d) (hced : e + d = c) : - a - b = e := -begin -simp *, rw [← hced, nat.add_sub_cancel] -end - -end norm_num diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean deleted file mode 100644 index 5a76d27a7d..0000000000 --- a/library/init/algebra/ordered_field.lean +++ /dev/null @@ -1,441 +0,0 @@ -/- -Copyright (c) 2014 Robert Lewis. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Robert Lewis, Leonardo de Moura --/ -prelude -import init.algebra.ordered_ring init.algebra.field - -set_option old_structure_cmd true - -universe u - -class linear_ordered_field (α : Type u) extends linear_ordered_ring α, field α - -section linear_ordered_field -variables {α : Type u} [linear_ordered_field α] - -lemma mul_zero_lt_mul_inv_of_pos {a : α} (h : 0 < a) : a * 0 < a * (1 / a) := -calc a * 0 = 0 : by rw mul_zero - ... < 1 : zero_lt_one - ... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne.symm (ne_of_lt h))) - ... = a * (1 / a) : by rw inv_eq_one_div - -lemma mul_zero_lt_mul_inv_of_neg {a : α} (h : a < 0) : a * 0 < a * (1 / a) := -calc a * 0 = 0 : by rw mul_zero - ... < 1 : zero_lt_one - ... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne_of_lt h)) - ... = a * (1 / a) : by rw inv_eq_one_div - -lemma one_div_pos_of_pos {a : α} (h : 0 < a) : 0 < 1 / a := -lt_of_mul_lt_mul_left (mul_zero_lt_mul_inv_of_pos h) (le_of_lt h) - -lemma pos_of_one_div_pos {a : α} (h : 0 < 1 / a) : 0 < a := -one_div_one_div a ▸ one_div_pos_of_pos h - -lemma one_div_neg_of_neg {a : α} (h : a < 0) : 1 / a < 0 := -gt_of_mul_lt_mul_neg_left (mul_zero_lt_mul_inv_of_neg h) (le_of_lt h) - -lemma neg_of_one_div_neg {a : α} (h : 1 / a < 0) : a < 0 := -one_div_one_div a ▸ one_div_neg_of_neg h - -lemma le_mul_of_ge_one_right {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ b * a := -suffices b * 1 ≤ b * a, by rwa mul_one at this, -mul_le_mul_of_nonneg_left h hb - -lemma le_mul_of_ge_one_left {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ a * b := -by rw mul_comm; exact le_mul_of_ge_one_right hb h - -lemma lt_mul_of_gt_one_right {a b : α} (hb : b > 0) (h : a > 1) : b < b * a := -suffices b * 1 < b * a, by rwa mul_one at this, -mul_lt_mul_of_pos_left h hb - -lemma one_le_div_of_le (a : α) {b : α} (hb : b > 0) (h : b ≤ a) : 1 ≤ a / b := -have hb' : b ≠ 0, from ne.symm (ne_of_lt hb), -have hbinv : 1 / b > 0, from one_div_pos_of_pos hb, -calc - 1 = b * (1 / b) : eq.symm (mul_one_div_cancel hb') - ... ≤ a * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt hbinv) - ... = a / b : eq.symm $ div_eq_mul_one_div a b - -lemma le_of_one_le_div (a : α) {b : α} (hb : b > 0) (h : 1 ≤ a / b) : b ≤ a := -have hb' : b ≠ 0, from ne.symm (ne_of_lt hb), -calc - b ≤ b * (a / b) : le_mul_of_ge_one_right (le_of_lt hb) h - ... = a : by rw [mul_div_cancel' _ hb'] - -lemma one_lt_div_of_lt (a : α) {b : α} (hb : b > 0) (h : b < a) : 1 < a / b := -have hb' : b ≠ 0, from ne.symm (ne_of_lt hb), -have hbinv : 1 / b > 0, from one_div_pos_of_pos hb, calc - 1 = b * (1 / b) : eq.symm (mul_one_div_cancel hb') - ... < a * (1 / b) : mul_lt_mul_of_pos_right h hbinv - ... = a / b : eq.symm $ div_eq_mul_one_div a b - -lemma lt_of_one_lt_div (a : α) {b : α} (hb : b > 0) (h : 1 < a / b) : b < a := -have hb' : b ≠ 0, from ne.symm (ne_of_lt hb), -calc - b < b * (a / b) : lt_mul_of_gt_one_right hb h - ... = a : by rw [mul_div_cancel' _ hb'] - --- the following lemmas amount to four iffs, for <, ≤, ≥, >. - -lemma mul_le_of_le_div {a b c : α} (hc : 0 < c) (h : a ≤ b / c) : a * c ≤ b := -div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_le_mul_of_nonneg_right h (le_of_lt hc) - -lemma le_div_of_mul_le {a b c : α} (hc : 0 < c) (h : a * c ≤ b) : a ≤ b / c := -calc - a = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc)) - ... ≤ b * (1 / c) : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc)) - ... = b / c : eq.symm $ div_eq_mul_one_div b c - -lemma mul_lt_of_lt_div {a b c : α} (hc : 0 < c) (h : a < b / c) : a * c < b := -div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_lt_mul_of_pos_right h hc - -lemma lt_div_of_mul_lt {a b c : α} (hc : 0 < c) (h : a * c < b) : a < b / c := -calc - a = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc)) - ... < b * (1 / c) : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc) - ... = b / c : eq.symm $ div_eq_mul_one_div b c - -lemma mul_le_of_div_le_of_neg {a b c : α} (hc : c < 0) (h : b / c ≤ a) : a * c ≤ b := -div_mul_cancel b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h (le_of_lt hc) - -lemma div_le_of_mul_le_of_neg {a b c : α} (hc : c < 0) (h : a * c ≤ b) : b / c ≤ a := -calc - a = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc) - ... ≥ b * (1 / c) : mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc)) - ... = b / c : eq.symm $ div_eq_mul_one_div b c - -lemma mul_lt_of_gt_div_of_neg {a b c : α} (hc : c < 0) (h : a > b / c) : a * c < b := -div_mul_cancel b (ne_of_lt hc) ▸ mul_lt_mul_of_neg_right h hc - -lemma div_lt_of_mul_lt_of_pos {a b c : α} (hc : c > 0) (h : b < a * c) : b / c < a := -calc - a = a * c * (1 / c) : mul_mul_div a (ne_of_gt hc) - ... > b * (1 / c) : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc) - ... = b / c : eq.symm $ div_eq_mul_one_div b c - -lemma div_lt_of_mul_gt_of_neg {a b c : α} (hc : c < 0) (h : a * c < b) : b / c < a := -calc - a = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc) - ... > b * (1 / c) : mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc) - ... = b / c : eq.symm $ div_eq_mul_one_div b c - -lemma div_le_of_le_mul {a b c : α} (hb : b > 0) (h : a ≤ b * c) : a / b ≤ c := -calc - a / b = a * (1 / b) : div_eq_mul_one_div a b - ... ≤ (b * c) * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hb)) - ... = (b * c) / b : eq.symm $ div_eq_mul_one_div (b * c) b - ... = c : by rw [mul_div_cancel_left _ (ne.symm (ne_of_lt hb))] - -lemma le_mul_of_div_le {a b c : α} (hc : c > 0) (h : a / c ≤ b) : a ≤ b * c := -calc - a = a / c * c : by rw (div_mul_cancel _ (ne.symm (ne_of_lt hc))) - ... ≤ b * c : mul_le_mul_of_nonneg_right h (le_of_lt hc) - - -- following these in the isabelle file, there are 8 biconditionals for the above with - signs - -- skipping for now - -lemma mul_sub_mul_div_mul_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c < b / d) : - (a * d - b * c) / (c * d) < 0 := -have h1 : a / c - b / d < 0, from calc - a / c - b / d < b / d - b / d : sub_lt_sub_right h _ - ... = 0 : by rw sub_self, -calc - 0 > a / c - b / d : h1 - ... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd - ... = (a * d - b * c) / (c * d) : by rw (mul_comm b c) - -lemma mul_sub_mul_div_mul_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c ≤ b / d) : - (a * d - b * c) / (c * d) ≤ 0 := -have h1 : a / c - b / d ≤ 0, from calc - a / c - b / d ≤ b / d - b / d : sub_le_sub_right h _ - ... = 0 : by rw sub_self, -calc - 0 ≥ a / c - b / d : h1 - ... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd - ... = (a * d - b * c) / (c * d) : by rw (mul_comm b c) - -lemma div_lt_div_of_mul_sub_mul_div_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) - (h : (a * d - b * c) / (c * d) < 0) : a / c < b / d := -have (a * d - c * b) / (c * d) < 0, by rwa [mul_comm c b], -have a / c - b / d < 0, by rwa [div_sub_div _ _ hc hd], -have a / c - b / d + b / d < 0 + b / d, from add_lt_add_right this _, -by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this - - -lemma div_le_div_of_mul_sub_mul_div_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) - (h : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d := -have (a * d - c * b) / (c * d) ≤ 0, by rwa [mul_comm c b], -have a / c - b / d ≤ 0, by rwa [div_sub_div _ _ hc hd], -have a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right this _, -by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this - - -lemma div_pos_of_pos_of_pos {a b : α} : 0 < a → 0 < b → 0 < a / b := -begin - intros, - rw div_eq_mul_one_div, - apply mul_pos, - assumption, - apply one_div_pos_of_pos, - assumption -end - -lemma div_nonneg_of_nonneg_of_pos {a b : α} : 0 ≤ a → 0 < b → 0 ≤ a / b := -begin - intros, rw div_eq_mul_one_div, - apply mul_nonneg, assumption, - apply le_of_lt, - apply one_div_pos_of_pos, - assumption -end - -lemma div_neg_of_neg_of_pos {a b : α} : a < 0 → 0 < b → a / b < 0 := -begin - intros, rw div_eq_mul_one_div, - apply mul_neg_of_neg_of_pos, - assumption, - apply one_div_pos_of_pos, - assumption -end - -lemma div_nonpos_of_nonpos_of_pos {a b : α} : a ≤ 0 → 0 < b → a / b ≤ 0 := -begin - intros, rw div_eq_mul_one_div, - apply mul_nonpos_of_nonpos_of_nonneg, - assumption, - apply le_of_lt, - apply one_div_pos_of_pos, - assumption -end - -lemma div_neg_of_pos_of_neg {a b : α} : 0 < a → b < 0 → a / b < 0 := -begin - intros, rw div_eq_mul_one_div, - apply mul_neg_of_pos_of_neg, - assumption, - apply one_div_neg_of_neg, - assumption -end - -lemma div_nonpos_of_nonneg_of_neg {a b : α} : 0 ≤ a → b < 0 → a / b ≤ 0 := -begin - intros, rw div_eq_mul_one_div, - apply mul_nonpos_of_nonneg_of_nonpos, - assumption, - apply le_of_lt, - apply one_div_neg_of_neg, - assumption -end - -lemma div_pos_of_neg_of_neg {a b : α} : a < 0 → b < 0 → 0 < a / b := -begin - intros, rw div_eq_mul_one_div, - apply mul_pos_of_neg_of_neg, - assumption, - apply one_div_neg_of_neg, - assumption -end - -lemma div_nonneg_of_nonpos_of_neg {a b : α} : a ≤ 0 → b < 0 → 0 ≤ a / b := -begin - intros, rw div_eq_mul_one_div, - apply mul_nonneg_of_nonpos_of_nonpos, - assumption, - apply le_of_lt, - apply one_div_neg_of_neg, - assumption -end - -lemma div_lt_div_of_lt_of_pos {a b c : α} (h : a < b) (hc : 0 < c) : a / c < b / c := -begin - intros, - rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c], - exact mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc) -end - -lemma div_le_div_of_le_of_pos {a b c : α} (h : a ≤ b) (hc : 0 < c) : a / c ≤ b / c := -begin - rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c], - exact mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc)) -end - -lemma div_lt_div_of_lt_of_neg {a b c : α} (h : b < a) (hc : c < 0) : a / c < b / c := -begin - rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c], - exact mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc) -end - -lemma div_le_div_of_le_of_neg {a b c : α} (h : b ≤ a) (hc : c < 0) : a / c ≤ b / c := -begin - rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c], - exact mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc)) -end - -lemma add_halves (a : α) : a / 2 + a / 2 = a := -by { rw [div_add_div_same, ← two_mul, mul_div_cancel_left], exact two_ne_zero } - -lemma sub_self_div_two (a : α) : a - a / 2 = a / 2 := -suffices a / 2 + a / 2 - a / 2 = a / 2, by rwa add_halves at this, -by rw [add_sub_cancel] - -lemma add_midpoint {a b : α} (h : a < b) : a + (b - a) / 2 < b := -begin - rw [← div_sub_div_same, sub_eq_add_neg, add_comm (b/2), ← add_assoc, ← sub_eq_add_neg], - apply add_lt_of_lt_sub_right, - rw [sub_self_div_two, sub_self_div_two], - apply div_lt_div_of_lt_of_pos h two_pos -end - -lemma div_two_sub_self (a : α) : a / 2 - a = - (a / 2) := -suffices a / 2 - (a / 2 + a / 2) = - (a / 2), by rwa add_halves at this, -by rw [sub_add_eq_sub_sub, sub_self, zero_sub] - -lemma add_self_div_two (a : α) : (a + a) / 2 = a := -eq.symm - (iff.mpr (eq_div_iff_mul_eq _ _ (ne_of_gt (add_pos (@zero_lt_one α _) zero_lt_one))) - (begin unfold bit0, rw [left_distrib, mul_one] end)) - -lemma mul_le_mul_of_mul_div_le {a b c d : α} (h : a * (b / c) ≤ d) (hc : c > 0) : b * a ≤ d * c := -begin - rw [← mul_div_assoc] at h, rw [mul_comm b], - apply le_mul_of_div_le hc h -end - -lemma div_two_lt_of_pos {a : α} (h : a > 0) : a / 2 < a := -suffices a / (1 + 1) < a, begin unfold bit0, assumption end, -have ha : a / 2 > 0, from div_pos_of_pos_of_pos h (add_pos zero_lt_one zero_lt_one), -calc - a / 2 < a / 2 + a / 2 : lt_add_of_pos_left _ ha - ... = a : add_halves a - -lemma div_mul_le_div_mul_of_div_le_div_pos {a b c d e : α} (h : a / b ≤ c / d) - (he : e > 0) : a / (b * e) ≤ c / (d * e) := -begin - have h₁ := div_mul_eq_div_mul_one_div a b e, - have h₂ := div_mul_eq_div_mul_one_div c d e, - rw [h₁, h₂], - apply mul_le_mul_of_nonneg_right h, - apply le_of_lt, - apply one_div_pos_of_pos he -end - -lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ c > 0 := -begin - apply exists.intro ((a - b) / (1 + 1)), - split, - {have h2 : a + a > (b + b) + (a - b), - calc - a + a > b + a : add_lt_add_right h _ - ... = b + a + b - b : by rw add_sub_cancel - ... = b + b + a - b : by simp [add_comm, add_left_comm] - ... = (b + b) + (a - b) : by rw add_sub, - have h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2, - exact div_lt_div_of_lt_of_pos h2 two_pos, - rw [one_add_one_eq_two, sub_eq_add_neg], - rw [add_self_div_two, ← div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3, - exact h3}, - exact div_pos_of_pos_of_pos (sub_pos_of_lt h) two_pos -end - -lemma ge_of_forall_ge_sub {a b : α} (h : ∀ ε : α, ε > 0 → a ≥ b - ε) : a ≥ b := -begin - apply le_of_not_gt, - intro hb, - cases exists_add_lt_and_pos_of_lt hb with c hc, - have hc' := h c (and.right hc), - apply (not_le_of_gt (and.left hc)) (le_add_of_sub_right_le hc') -end - -lemma one_div_lt_one_div_of_lt {a b : α} (ha : 0 < a) (h : a < b) : 1 / b < 1 / a := -begin - apply lt_div_of_mul_lt ha, - rw [mul_comm, ← div_eq_mul_one_div], - apply div_lt_of_mul_lt_of_pos (lt_trans ha h), - rwa [one_mul] -end - -lemma one_div_le_one_div_of_le {a b : α} (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a := -(lt_or_eq_of_le h).elim - (λ h, le_of_lt $ one_div_lt_one_div_of_lt ha h) - (λ h, by rw [h]) - -lemma one_div_lt_one_div_of_lt_of_neg {a b : α} (hb : b < 0) (h : a < b) : 1 / b < 1 / a := -begin - apply div_lt_of_mul_gt_of_neg hb, - rw [mul_comm, ← div_eq_mul_one_div], - apply div_lt_of_mul_gt_of_neg (lt_trans h hb), - rwa [one_mul] -end - -lemma one_div_le_one_div_of_le_of_neg {a b : α} (hb : b < 0) (h : a ≤ b) : 1 / b ≤ 1 / a := -(lt_or_eq_of_le h).elim - (λ h, le_of_lt $ one_div_lt_one_div_of_lt_of_neg hb h) - (λ h, by rw [h]) - -lemma le_of_one_div_le_one_div {a b : α} (h : 0 < a) (hl : 1 / a ≤ 1 / b) : b ≤ a := -le_of_not_gt $ λ hn, not_lt_of_ge hl $ one_div_lt_one_div_of_lt h hn - -lemma le_of_one_div_le_one_div_of_neg {a b : α} (h : b < 0) (hl : 1 / a ≤ 1 / b) : b ≤ a := -le_of_not_gt $ λ hn, not_lt_of_ge hl $ one_div_lt_one_div_of_lt_of_neg h hn - -lemma lt_of_one_div_lt_one_div {a b : α} (h : 0 < a) (hl : 1 / a < 1 / b) : b < a := -lt_of_not_ge $ λ hn, not_le_of_gt hl $ one_div_le_one_div_of_le h hn - -lemma lt_of_one_div_lt_one_div_of_neg {a b : α} (h : b < 0) (hl : 1 / a < 1 / b) : b < a := -lt_of_not_ge $ λ hn, not_le_of_gt hl $ one_div_le_one_div_of_le_of_neg h hn - -lemma one_div_le_of_one_div_le_of_pos {a b : α} (ha : a > 0) (h : 1 / a ≤ b) : 1 / b ≤ a := -begin - rw [← one_div_one_div a], - apply one_div_le_one_div_of_le _ h, - apply one_div_pos_of_pos ha -end - -lemma one_div_le_of_one_div_le_of_neg {a b : α} (hb : b < 0) (h : 1 / a ≤ b) : 1 / b ≤ a := -le_of_not_gt $ λ hl, begin - have : a < 0, from lt_trans hl (one_div_neg_of_neg hb), - rw ← one_div_one_div a at hl, - exact not_lt_of_ge h (lt_of_one_div_lt_one_div_of_neg hb hl) -end - -lemma one_lt_one_div {a : α} (h1 : 0 < a) (h2 : a < 1) : 1 < 1 / a := -suffices 1 / 1 < 1 / a, by rwa one_div_one at this, -one_div_lt_one_div_of_lt h1 h2 - -lemma one_le_one_div {a : α} (h1 : 0 < a) (h2 : a ≤ 1) : 1 ≤ 1 / a := -suffices 1 / 1 ≤ 1 / a, by rwa one_div_one at this, -one_div_le_one_div_of_le h1 h2 - -lemma one_div_lt_neg_one {a : α} (h1 : a < 0) (h2 : -1 < a) : 1 / a < -1 := -suffices 1 / a < 1 / -1, by rwa one_div_neg_one_eq_neg_one at this, -one_div_lt_one_div_of_lt_of_neg h1 h2 - -lemma one_div_le_neg_one {a : α} (h1 : a < 0) (h2 : -1 ≤ a) : 1 / a ≤ -1 := -suffices 1 / a ≤ 1 / -1, by rwa one_div_neg_one_eq_neg_one at this, -one_div_le_one_div_of_le_of_neg h1 h2 - -lemma div_lt_div_of_pos_of_lt_of_pos {a b c : α} (hb : 0 < b) (h : b < a) (hc : 0 < c) : c / a < c / b := -begin - apply lt_of_sub_neg, - rw [div_eq_mul_one_div, div_eq_mul_one_div c b, ← mul_sub_left_distrib], - apply mul_neg_of_pos_of_neg, - exact hc, - apply sub_neg_of_lt, - apply one_div_lt_one_div_of_lt; assumption, -end - -lemma div_mul_le_div_mul_of_div_le_div_pos' {a b c d e : α} (h : a / b ≤ c / d) - (he : e > 0) : a / (b * e) ≤ c / (d * e) := -begin - rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div], - apply mul_le_mul_of_nonneg_right h, - apply le_of_lt, - apply one_div_pos_of_pos he -end - -end linear_ordered_field - -class discrete_linear_ordered_field (α : Type u) extends linear_ordered_field α, - decidable_linear_ordered_comm_ring α diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean deleted file mode 100644 index 7018fa2815..0000000000 --- a/library/init/algebra/ordered_group.lean +++ /dev/null @@ -1,634 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad, Leonardo de Moura --/ -prelude -import init.algebra.order init.algebra.group - -/- Make sure instances defined in this file have lower priority than the ones - defined for concrete structures -/ -set_option default_priority 100 - -set_option old_structure_cmd true - -universe u - -class ordered_cancel_add_comm_monoid (α : Type u) - extends add_comm_monoid α, add_left_cancel_semigroup α, - add_right_cancel_semigroup α, partial_order α := -(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) -(le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c) - -section ordered_cancel_add_comm_monoid -variable {α : Type u} -variable [s : ordered_cancel_add_comm_monoid α] - -lemma add_le_add_left {a b : α} (h : a ≤ b) (c : α) : c + a ≤ c + b := -@ordered_cancel_add_comm_monoid.add_le_add_left α s a b h c - -lemma le_of_add_le_add_left {a b c : α} (h : a + b ≤ a + c) : b ≤ c := -@ordered_cancel_add_comm_monoid.le_of_add_le_add_left α s a b c h -end ordered_cancel_add_comm_monoid - -section ordered_cancel_add_comm_monoid -variable {α : Type u} -variable [ordered_cancel_add_comm_monoid α] - -lemma add_lt_add_left {a b : α} (h : a < b) (c : α) : c + a < c + b := -lt_of_le_not_le (add_le_add_left (le_of_lt h) _) $ - mt le_of_add_le_add_left (not_le_of_gt h) - -lemma lt_of_add_lt_add_left {a b c : α} (h : a + b < a + c) : b < c := -lt_of_le_not_le (le_of_add_le_add_left (le_of_lt h)) $ - mt (λ h, add_le_add_left h _) (not_le_of_gt h) - -lemma add_le_add_right {a b : α} (h : a ≤ b) (c : α) : a + c ≤ b + c := -add_comm c a ▸ add_comm c b ▸ add_le_add_left h c - -theorem add_lt_add_right {a b : α} (h : a < b) (c : α) : a + c < b + c := -begin - rw [add_comm a c, add_comm b c], - exact (add_lt_add_left h c) -end - -lemma add_le_add {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := -le_trans (add_le_add_right h₁ c) (add_le_add_left h₂ b) - -lemma le_add_of_nonneg_right {a b : α} (h : b ≥ 0) : a ≤ a + b := -have a + b ≥ a + 0, from add_le_add_left h a, -by rwa add_zero at this - -lemma le_add_of_nonneg_left {a b : α} (h : b ≥ 0) : a ≤ b + a := -have 0 + a ≤ b + a, from add_le_add_right h a, -by rwa zero_add at this - -lemma add_lt_add {a b c d : α} (h₁ : a < b) (h₂ : c < d) : a + c < b + d := -lt_trans (add_lt_add_right h₁ c) (add_lt_add_left h₂ b) - -lemma add_lt_add_of_le_of_lt {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d := -lt_of_le_of_lt (add_le_add_right h₁ c) (add_lt_add_left h₂ b) - -lemma add_lt_add_of_lt_of_le {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := -lt_of_lt_of_le (add_lt_add_right h₁ c) (add_le_add_left h₂ b) - -lemma lt_add_of_pos_right (a : α) {b : α} (h : b > 0) : a < a + b := -have a + 0 < a + b, from add_lt_add_left h a, -by rwa [add_zero] at this - -lemma lt_add_of_pos_left (a : α) {b : α} (h : b > 0) : a < b + a := -have 0 + a < b + a, from add_lt_add_right h a, -by rwa [zero_add] at this - -lemma le_of_add_le_add_right {a b c : α} (h : a + b ≤ c + b) : a ≤ c := -le_of_add_le_add_left - (show b + a ≤ b + c, begin rw [add_comm b a, add_comm b c], assumption end) - -lemma lt_of_add_lt_add_right {a b c : α} (h : a + b < c + b) : a < c := -lt_of_add_lt_add_left - (show b + a < b + c, begin rw [add_comm b a, add_comm b c], assumption end) - --- here we start using properties of zero. -lemma add_nonneg {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b := -zero_add (0:α) ▸ (add_le_add ha hb) - -lemma add_pos {a b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b := - zero_add (0:α) ▸ (add_lt_add ha hb) - -lemma add_pos_of_pos_of_nonneg {a b : α} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b := -zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb) - -lemma add_pos_of_nonneg_of_pos {a b : α} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b := -zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb) - -lemma add_nonpos {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 := -zero_add (0:α) ▸ (add_le_add ha hb) - -lemma add_neg {a b : α} (ha : a < 0) (hb : b < 0) : a + b < 0 := -zero_add (0:α) ▸ (add_lt_add ha hb) - -lemma add_neg_of_neg_of_nonpos {a b : α} (ha : a < 0) (hb : b ≤ 0) : a + b < 0 := -zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb) - -lemma add_neg_of_nonpos_of_neg {a b : α} (ha : a ≤ 0) (hb : b < 0) : a + b < 0 := -zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb) - -lemma add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg - {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 := -iff.intro - (assume hab : a + b = 0, - have ha' : a ≤ 0, from - calc - a = a + 0 : by rw add_zero - ... ≤ a + b : add_le_add_left hb _ - ... = 0 : hab, - have haz : a = 0, from le_antisymm ha' ha, - have hb' : b ≤ 0, from - calc - b = 0 + b : by rw zero_add - ... ≤ a + b : by exact add_le_add_right ha _ - ... = 0 : hab, - have hbz : b = 0, from le_antisymm hb' hb, - and.intro haz hbz) - (assume ⟨ha', hb'⟩, - by rw [ha', hb', add_zero]) - -lemma le_add_of_nonneg_of_le {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c := -zero_add b ▸ add_le_add ha hbc - -lemma le_add_of_le_of_nonneg {a b c : α} (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a := -add_zero b ▸ add_le_add hbc ha - -lemma lt_add_of_pos_of_le {a b c : α} (ha : 0 < a) (hbc : b ≤ c) : b < a + c := -zero_add b ▸ add_lt_add_of_lt_of_le ha hbc - -lemma lt_add_of_le_of_pos {a b c : α} (hbc : b ≤ c) (ha : 0 < a) : b < c + a := -add_zero b ▸ add_lt_add_of_le_of_lt hbc ha - -lemma add_le_of_nonpos_of_le {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c := -zero_add c ▸ add_le_add ha hbc - -lemma add_le_of_le_of_nonpos {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c := -add_zero c ▸ add_le_add hbc ha - -lemma add_lt_of_neg_of_le {a b c : α} (ha : a < 0) (hbc : b ≤ c) : a + b < c := -zero_add c ▸ add_lt_add_of_lt_of_le ha hbc - -lemma add_lt_of_le_of_neg {a b c : α} (hbc : b ≤ c) (ha : a < 0) : b + a < c := -add_zero c ▸ add_lt_add_of_le_of_lt hbc ha - -lemma lt_add_of_nonneg_of_lt {a b c : α} (ha : 0 ≤ a) (hbc : b < c) : b < a + c := -zero_add b ▸ add_lt_add_of_le_of_lt ha hbc - -lemma lt_add_of_lt_of_nonneg {a b c : α} (hbc : b < c) (ha : 0 ≤ a) : b < c + a := -add_zero b ▸ add_lt_add_of_lt_of_le hbc ha - -lemma lt_add_of_pos_of_lt {a b c : α} (ha : 0 < a) (hbc : b < c) : b < a + c := -zero_add b ▸ add_lt_add ha hbc - -lemma lt_add_of_lt_of_pos {a b c : α} (hbc : b < c) (ha : 0 < a) : b < c + a := -add_zero b ▸ add_lt_add hbc ha - -lemma add_lt_of_nonpos_of_lt {a b c : α} (ha : a ≤ 0) (hbc : b < c) : a + b < c := -zero_add c ▸ add_lt_add_of_le_of_lt ha hbc - -lemma add_lt_of_lt_of_nonpos {a b c : α} (hbc : b < c) (ha : a ≤ 0) : b + a < c := -add_zero c ▸ add_lt_add_of_lt_of_le hbc ha - -lemma add_lt_of_neg_of_lt {a b c : α} (ha : a < 0) (hbc : b < c) : a + b < c := -zero_add c ▸ add_lt_add ha hbc - -lemma add_lt_of_lt_of_neg {a b c : α} (hbc : b < c) (ha : a < 0) : b + a < c := -add_zero c ▸ add_lt_add hbc ha - -end ordered_cancel_add_comm_monoid - -class ordered_add_comm_group (α : Type u) extends add_comm_group α, partial_order α := -(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) - -section ordered_add_comm_group -variable {α : Type u} -variable [ordered_add_comm_group α] - -lemma ordered_add_comm_group.add_lt_add_left (a b : α) (h : a < b) (c : α) : c + a < c + b := -begin - rw lt_iff_le_not_le at h ⊢, - split, - { apply ordered_add_comm_group.add_le_add_left _ _ h.1 }, - { intro w, - have w : -c + (c + b) ≤ -c + (c + a) := ordered_add_comm_group.add_le_add_left _ _ w _, - simp only [add_zero, add_comm, add_left_neg, add_left_comm] at w, - exact h.2 w }, -end - -lemma ordered_add_comm_group.le_of_add_le_add_left {a b c : α} (h : a + b ≤ a + c) : b ≤ c := -have -a + (a + b) ≤ -a + (a + c), from ordered_add_comm_group.add_le_add_left _ _ h _, -begin simp [neg_add_cancel_left] at this, assumption end - -lemma ordered_add_comm_group.lt_of_add_lt_add_left {a b c : α} (h : a + b < a + c) : b < c := -have -a + (a + b) < -a + (a + c), from ordered_add_comm_group.add_lt_add_left _ _ h _, -begin simp [neg_add_cancel_left] at this, assumption end -end ordered_add_comm_group - -instance ordered_add_comm_group.to_ordered_cancel_add_comm_monoid (α : Type u) [s : ordered_add_comm_group α] : ordered_cancel_add_comm_monoid α := -{ add_left_cancel := @add_left_cancel α _, - add_right_cancel := @add_right_cancel α _, - le_of_add_le_add_left := @ordered_add_comm_group.le_of_add_le_add_left α _, - ..s } - -section ordered_add_comm_group -variables {α : Type u} [ordered_add_comm_group α] - -lemma neg_le_neg {a b : α} (h : a ≤ b) : -b ≤ -a := -have 0 ≤ -a + b, from add_left_neg a ▸ add_le_add_left h (-a), -have 0 + -b ≤ -a + b + -b, from add_le_add_right this (-b), -by rwa [add_neg_cancel_right, zero_add] at this - -lemma le_of_neg_le_neg {a b : α} (h : -b ≤ -a) : a ≤ b := -suffices -(-a) ≤ -(-b), from - begin simp [neg_neg] at this, assumption end, -neg_le_neg h - -lemma nonneg_of_neg_nonpos {a : α} (h : -a ≤ 0) : 0 ≤ a := -have -a ≤ -0, by rwa neg_zero, -le_of_neg_le_neg this - -lemma neg_nonpos_of_nonneg {a : α} (h : 0 ≤ a) : -a ≤ 0 := -have -a ≤ -0, from neg_le_neg h, -by rwa neg_zero at this - -lemma nonpos_of_neg_nonneg {a : α} (h : 0 ≤ -a) : a ≤ 0 := -have -0 ≤ -a, by rwa neg_zero, -le_of_neg_le_neg this - -lemma neg_nonneg_of_nonpos {a : α} (h : a ≤ 0) : 0 ≤ -a := -have -0 ≤ -a, from neg_le_neg h, -by rwa neg_zero at this - -lemma neg_lt_neg {a b : α} (h : a < b) : -b < -a := -have 0 < -a + b, from add_left_neg a ▸ add_lt_add_left h (-a), -have 0 + -b < -a + b + -b, from add_lt_add_right this (-b), -by rwa [add_neg_cancel_right, zero_add] at this - -lemma lt_of_neg_lt_neg {a b : α} (h : -b < -a) : a < b := -neg_neg a ▸ neg_neg b ▸ neg_lt_neg h - -lemma pos_of_neg_neg {a : α} (h : -a < 0) : 0 < a := -have -a < -0, by rwa neg_zero, -lt_of_neg_lt_neg this - -lemma neg_neg_of_pos {a : α} (h : 0 < a) : -a < 0 := -have -a < -0, from neg_lt_neg h, -by rwa neg_zero at this - -lemma neg_of_neg_pos {a : α} (h : 0 < -a) : a < 0 := -have -0 < -a, by rwa neg_zero, -lt_of_neg_lt_neg this - -lemma neg_pos_of_neg {a : α} (h : a < 0) : 0 < -a := -have -0 < -a, from neg_lt_neg h, -by rwa neg_zero at this - -lemma le_neg_of_le_neg {a b : α} (h : a ≤ -b) : b ≤ -a := -begin - have h := neg_le_neg h, - rwa neg_neg at h -end - -lemma neg_le_of_neg_le {a b : α} (h : -a ≤ b) : -b ≤ a := -begin - have h := neg_le_neg h, - rwa neg_neg at h -end - -lemma lt_neg_of_lt_neg {a b : α} (h : a < -b) : b < -a := -begin - have h := neg_lt_neg h, - rwa neg_neg at h -end - -lemma neg_lt_of_neg_lt {a b : α} (h : -a < b) : -b < a := -begin - have h := neg_lt_neg h, - rwa neg_neg at h -end - -lemma sub_nonneg_of_le {a b : α} (h : b ≤ a) : 0 ≤ a - b := -begin - have h := add_le_add_right h (-b), - rwa add_right_neg at h -end - -lemma le_of_sub_nonneg {a b : α} (h : 0 ≤ a - b) : b ≤ a := -begin - have h := add_le_add_right h b, - rwa [sub_add_cancel, zero_add] at h -end - -lemma sub_nonpos_of_le {a b : α} (h : a ≤ b) : a - b ≤ 0 := -begin - have h := add_le_add_right h (-b), - rwa add_right_neg at h -end - -lemma le_of_sub_nonpos {a b : α} (h : a - b ≤ 0) : a ≤ b := -begin - have h := add_le_add_right h b, - rwa [sub_add_cancel, zero_add] at h -end - -lemma sub_pos_of_lt {a b : α} (h : b < a) : 0 < a - b := -begin - have h := add_lt_add_right h (-b), - rwa add_right_neg at h -end - -lemma lt_of_sub_pos {a b : α} (h : 0 < a - b) : b < a := -begin - have h := add_lt_add_right h b, - rwa [sub_add_cancel, zero_add] at h -end - -lemma sub_neg_of_lt {a b : α} (h : a < b) : a - b < 0 := -begin - have h := add_lt_add_right h (-b), - rwa add_right_neg at h -end - -lemma lt_of_sub_neg {a b : α} (h : a - b < 0) : a < b := -begin - have h := add_lt_add_right h b, - rwa [sub_add_cancel, zero_add] at h -end - -lemma add_le_of_le_neg_add {a b c : α} (h : b ≤ -a + c) : a + b ≤ c := -begin - have h := add_le_add_left h a, - rwa add_neg_cancel_left at h -end - -lemma le_neg_add_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ -a + c := -begin - have h := add_le_add_left h (-a), - rwa neg_add_cancel_left at h -end - -lemma add_le_of_le_sub_left {a b c : α} (h : b ≤ c - a) : a + b ≤ c := -begin - have h := add_le_add_left h a, - rwa [← add_sub_assoc, add_comm a c, add_sub_cancel] at h -end - -lemma le_sub_left_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ c - a := -begin - have h := add_le_add_right h (-a), - rwa [add_comm a b, add_neg_cancel_right] at h -end - -lemma add_le_of_le_sub_right {a b c : α} (h : a ≤ c - b) : a + b ≤ c := -begin - have h := add_le_add_right h b, - rwa sub_add_cancel at h -end - -lemma le_sub_right_of_add_le {a b c : α} (h : a + b ≤ c) : a ≤ c - b := -begin - have h := add_le_add_right h (-b), - rwa add_neg_cancel_right at h -end - -lemma le_add_of_neg_add_le {a b c : α} (h : -b + a ≤ c) : a ≤ b + c := -begin - have h := add_le_add_left h b, - rwa add_neg_cancel_left at h -end - -lemma neg_add_le_of_le_add {a b c : α} (h : a ≤ b + c) : -b + a ≤ c := -begin - have h := add_le_add_left h (-b), - rwa neg_add_cancel_left at h -end - -lemma le_add_of_sub_left_le {a b c : α} (h : a - b ≤ c) : a ≤ b + c := -begin - have h := add_le_add_right h b, - rwa [sub_add_cancel, add_comm] at h -end - -lemma sub_left_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - b ≤ c := -begin - have h := add_le_add_right h (-b), - rwa [add_comm b c, add_neg_cancel_right] at h -end - -lemma le_add_of_sub_right_le {a b c : α} (h : a - c ≤ b) : a ≤ b + c := -begin - have h := add_le_add_right h c, - rwa sub_add_cancel at h -end - -lemma sub_right_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - c ≤ b := -begin - have h := add_le_add_right h (-c), - rwa add_neg_cancel_right at h -end - -lemma le_add_of_neg_add_le_left {a b c : α} (h : -b + a ≤ c) : a ≤ b + c := -begin - rw add_comm at h, - exact le_add_of_sub_left_le h -end - -lemma neg_add_le_left_of_le_add {a b c : α} (h : a ≤ b + c) : -b + a ≤ c := -begin - rw add_comm, - exact sub_left_le_of_le_add h -end - -lemma le_add_of_neg_add_le_right {a b c : α} (h : -c + a ≤ b) : a ≤ b + c := -begin - rw add_comm at h, - exact le_add_of_sub_right_le h -end - -lemma neg_add_le_right_of_le_add {a b c : α} (h : a ≤ b + c) : -c + a ≤ b := -begin - rw add_comm at h, - apply neg_add_le_left_of_le_add h -end - -lemma le_add_of_neg_le_sub_left {a b c : α} (h : -a ≤ b - c) : c ≤ a + b := -le_add_of_neg_add_le_left (add_le_of_le_sub_right h) - -lemma neg_le_sub_left_of_le_add {a b c : α} (h : c ≤ a + b) : -a ≤ b - c := -begin - have h := le_neg_add_of_add_le (sub_left_le_of_le_add h), - rwa add_comm at h -end - -lemma le_add_of_neg_le_sub_right {a b c : α} (h : -b ≤ a - c) : c ≤ a + b := -le_add_of_sub_right_le (add_le_of_le_sub_left h) - -lemma neg_le_sub_right_of_le_add {a b c : α} (h : c ≤ a + b) : -b ≤ a - c := -le_sub_left_of_add_le (sub_right_le_of_le_add h) - -lemma sub_le_of_sub_le {a b c : α} (h : a - b ≤ c) : a - c ≤ b := -sub_left_le_of_le_add (le_add_of_sub_right_le h) - -lemma sub_le_sub_left {a b : α} (h : a ≤ b) (c : α) : c - b ≤ c - a := -add_le_add_left (neg_le_neg h) c - -lemma sub_le_sub_right {a b : α} (h : a ≤ b) (c : α) : a - c ≤ b - c := -add_le_add_right h (-c) - -lemma sub_le_sub {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c := -add_le_add hab (neg_le_neg hcd) - -lemma add_lt_of_lt_neg_add {a b c : α} (h : b < -a + c) : a + b < c := -begin - have h := add_lt_add_left h a, - rwa add_neg_cancel_left at h -end - -lemma lt_neg_add_of_add_lt {a b c : α} (h : a + b < c) : b < -a + c := -begin - have h := add_lt_add_left h (-a), - rwa neg_add_cancel_left at h -end - -lemma add_lt_of_lt_sub_left {a b c : α} (h : b < c - a) : a + b < c := -begin - have h := add_lt_add_left h a, - rwa [← add_sub_assoc, add_comm a c, add_sub_cancel] at h -end - -lemma lt_sub_left_of_add_lt {a b c : α} (h : a + b < c) : b < c - a := -begin - have h := add_lt_add_right h (-a), - rwa [add_comm a b, add_neg_cancel_right] at h -end - -lemma add_lt_of_lt_sub_right {a b c : α} (h : a < c - b) : a + b < c := -begin - have h := add_lt_add_right h b, - rwa sub_add_cancel at h -end - -lemma lt_sub_right_of_add_lt {a b c : α} (h : a + b < c) : a < c - b := -begin - have h := add_lt_add_right h (-b), - rwa add_neg_cancel_right at h -end - -lemma lt_add_of_neg_add_lt {a b c : α} (h : -b + a < c) : a < b + c := -begin - have h := add_lt_add_left h b, - rwa add_neg_cancel_left at h -end - -lemma neg_add_lt_of_lt_add {a b c : α} (h : a < b + c) : -b + a < c := -begin - have h := add_lt_add_left h (-b), - rwa neg_add_cancel_left at h -end - -lemma lt_add_of_sub_left_lt {a b c : α} (h : a - b < c) : a < b + c := -begin - have h := add_lt_add_right h b, - rwa [sub_add_cancel, add_comm] at h -end - -lemma sub_left_lt_of_lt_add {a b c : α} (h : a < b + c) : a - b < c := -begin - have h := add_lt_add_right h (-b), - rwa [add_comm b c, add_neg_cancel_right] at h -end - -lemma lt_add_of_sub_right_lt {a b c : α} (h : a - c < b) : a < b + c := -begin - have h := add_lt_add_right h c, - rwa sub_add_cancel at h -end - -lemma sub_right_lt_of_lt_add {a b c : α} (h : a < b + c) : a - c < b := -begin - have h := add_lt_add_right h (-c), - rwa add_neg_cancel_right at h -end - -lemma lt_add_of_neg_add_lt_left {a b c : α} (h : -b + a < c) : a < b + c := -begin - rw add_comm at h, - exact lt_add_of_sub_left_lt h -end - -lemma neg_add_lt_left_of_lt_add {a b c : α} (h : a < b + c) : -b + a < c := -begin - rw add_comm, - exact sub_left_lt_of_lt_add h -end - -lemma lt_add_of_neg_add_lt_right {a b c : α} (h : -c + a < b) : a < b + c := -begin - rw add_comm at h, - exact lt_add_of_sub_right_lt h -end - -lemma neg_add_lt_right_of_lt_add {a b c : α} (h : a < b + c) : -c + a < b := -begin - rw add_comm at h, - apply neg_add_lt_left_of_lt_add h -end - -lemma lt_add_of_neg_lt_sub_left {a b c : α} (h : -a < b - c) : c < a + b := -lt_add_of_neg_add_lt_left (add_lt_of_lt_sub_right h) - -lemma neg_lt_sub_left_of_lt_add {a b c : α} (h : c < a + b) : -a < b - c := -begin - have h := lt_neg_add_of_add_lt (sub_left_lt_of_lt_add h), - rwa add_comm at h -end - -lemma lt_add_of_neg_lt_sub_right {a b c : α} (h : -b < a - c) : c < a + b := -lt_add_of_sub_right_lt (add_lt_of_lt_sub_left h) - -lemma neg_lt_sub_right_of_lt_add {a b c : α} (h : c < a + b) : -b < a - c := -lt_sub_left_of_add_lt (sub_right_lt_of_lt_add h) - -lemma sub_lt_of_sub_lt {a b c : α} (h : a - b < c) : a - c < b := -sub_left_lt_of_lt_add (lt_add_of_sub_right_lt h) - -lemma sub_lt_sub_left {a b : α} (h : a < b) (c : α) : c - b < c - a := -add_lt_add_left (neg_lt_neg h) c - -lemma sub_lt_sub_right {a b : α} (h : a < b) (c : α) : a - c < b - c := -add_lt_add_right h (-c) - -lemma sub_lt_sub {a b c d : α} (hab : a < b) (hcd : c < d) : a - d < b - c := -add_lt_add hab (neg_lt_neg hcd) - -lemma sub_lt_sub_of_le_of_lt {a b c d : α} (hab : a ≤ b) (hcd : c < d) : a - d < b - c := -add_lt_add_of_le_of_lt hab (neg_lt_neg hcd) - -lemma sub_lt_sub_of_lt_of_le {a b c d : α} (hab : a < b) (hcd : c ≤ d) : a - d < b - c := -add_lt_add_of_lt_of_le hab (neg_le_neg hcd) - -lemma sub_le_self (a : α) {b : α} (h : b ≥ 0) : a - b ≤ a := -calc - a - b = a + -b : rfl - ... ≤ a + 0 : add_le_add_left (neg_nonpos_of_nonneg h) _ - ... = a : by rw add_zero - -lemma sub_lt_self (a : α) {b : α} (h : b > 0) : a - b < a := -calc - a - b = a + -b : rfl - ... < a + 0 : add_lt_add_left (neg_neg_of_pos h) _ - ... = a : by rw add_zero - -lemma add_le_add_three {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : - a + b + c ≤ d + e + f := -begin - apply le_trans, - apply add_le_add, - apply add_le_add, - assumption', - apply le_refl -end - -end ordered_add_comm_group - -class decidable_linear_ordered_add_comm_group (α : Type u) - extends add_comm_group α, decidable_linear_order α := -(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) - -instance decidable_linear_ordered_comm_group.to_ordered_add_comm_group (α : Type u) - [s : decidable_linear_ordered_add_comm_group α] : ordered_add_comm_group α := -{ add := s.add, ..s } - -class decidable_linear_ordered_cancel_add_comm_monoid (α : Type u) - extends ordered_cancel_add_comm_monoid α, decidable_linear_order α - -lemma decidable_linear_ordered_add_comm_group.add_lt_add_left {α} [decidable_linear_ordered_add_comm_group α] - (a b : α) (h : a < b) (c : α) : c + a < c + b := - ordered_add_comm_group.add_lt_add_left a b h c - diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean deleted file mode 100644 index edc3cb33dc..0000000000 --- a/library/init/algebra/ordered_ring.lean +++ /dev/null @@ -1,412 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad, Leonardo de Moura --/ -prelude -import init.algebra.ordered_group init.algebra.ring - -/- Make sure instances defined in this file have lower priority than the ones - defined for concrete structures -/ -set_option default_priority 100 - -set_option old_structure_cmd true - -universe u - -class ordered_semiring (α : Type u) - extends semiring α, ordered_cancel_add_comm_monoid α := -(mul_lt_mul_of_pos_left: ∀ a b c : α, a < b → 0 < c → c * a < c * b) -(mul_lt_mul_of_pos_right: ∀ a b c : α, a < b → 0 < c → a * c < b * c) - -lemma ordered_semiring.mul_le_mul_of_nonneg_left {α} [s : ordered_semiring α] (a b c : α) (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b := -begin - cases classical.em (b ≤ a), { simp [le_antisymm h h₁] }, - cases classical.em (c ≤ 0), { simp [le_antisymm h_1 h₂] }, - exact (le_not_le_of_lt (ordered_semiring.mul_lt_mul_of_pos_left a b c (lt_of_le_not_le h₁ h) (lt_of_le_not_le h₂ h_1))).left, -end - -lemma ordered_semiring.mul_le_mul_of_nonneg_right {α} [s : ordered_semiring α] (a b c : α) (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c := -begin - cases classical.em (b ≤ a), { simp [le_antisymm h h₁] }, - cases classical.em (c ≤ 0), { simp [le_antisymm h_1 h₂] }, - exact (le_not_le_of_lt (ordered_semiring.mul_lt_mul_of_pos_right a b c (lt_of_le_not_le h₁ h) (lt_of_le_not_le h₂ h_1))).left, -end - -variable {α : Type u} - -section ordered_semiring -variable [ordered_semiring α] - -lemma mul_le_mul_of_nonneg_left {a b c : α} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b := -ordered_semiring.mul_le_mul_of_nonneg_left a b c h₁ h₂ - -lemma mul_le_mul_of_nonneg_right {a b c : α} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c := -ordered_semiring.mul_le_mul_of_nonneg_right a b c h₁ h₂ - -lemma mul_lt_mul_of_pos_left {a b c : α} (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b := -ordered_semiring.mul_lt_mul_of_pos_left a b c h₁ h₂ - -lemma mul_lt_mul_of_pos_right {a b c : α} (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c := -ordered_semiring.mul_lt_mul_of_pos_right a b c h₁ h₂ - --- TODO: there are four variations, depending on which variables we assume to be nonneg -lemma mul_le_mul {a b c d : α} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d := -calc - a * b ≤ c * b : mul_le_mul_of_nonneg_right hac nn_b - ... ≤ c * d : mul_le_mul_of_nonneg_left hbd nn_c - -lemma mul_nonneg {a b : α} (ha : a ≥ 0) (hb : b ≥ 0) : a * b ≥ 0 := -have h : 0 * b ≤ a * b, from mul_le_mul_of_nonneg_right ha hb, -by rwa [zero_mul] at h - -lemma mul_nonpos_of_nonneg_of_nonpos {a b : α} (ha : a ≥ 0) (hb : b ≤ 0) : a * b ≤ 0 := -have h : a * b ≤ a * 0, from mul_le_mul_of_nonneg_left hb ha, -by rwa mul_zero at h - -lemma mul_nonpos_of_nonpos_of_nonneg {a b : α} (ha : a ≤ 0) (hb : b ≥ 0) : a * b ≤ 0 := -have h : a * b ≤ 0 * b, from mul_le_mul_of_nonneg_right ha hb, -by rwa zero_mul at h - -lemma mul_lt_mul {a b c d : α} (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) (nn_c : 0 ≤ c) : a * b < c * d := -calc - a * b < c * b : mul_lt_mul_of_pos_right hac pos_b - ... ≤ c * d : mul_le_mul_of_nonneg_left hbd nn_c - -lemma mul_lt_mul' {a b c d : α} (h1 : a ≤ c) (h2 : b < d) (h3 : b ≥ 0) (h4 : c > 0) : - a * b < c * d := -calc - a * b ≤ c * b : mul_le_mul_of_nonneg_right h1 h3 - ... < c * d : mul_lt_mul_of_pos_left h2 h4 - -lemma mul_pos {a b : α} (ha : a > 0) (hb : b > 0) : a * b > 0 := -have h : 0 * b < a * b, from mul_lt_mul_of_pos_right ha hb, -by rwa zero_mul at h - -lemma mul_neg_of_pos_of_neg {a b : α} (ha : a > 0) (hb : b < 0) : a * b < 0 := -have h : a * b < a * 0, from mul_lt_mul_of_pos_left hb ha, -by rwa mul_zero at h - -lemma mul_neg_of_neg_of_pos {a b : α} (ha : a < 0) (hb : b > 0) : a * b < 0 := -have h : a * b < 0 * b, from mul_lt_mul_of_pos_right ha hb, -by rwa zero_mul at h - -lemma mul_self_le_mul_self {a b : α} (h1 : 0 ≤ a) (h2 : a ≤ b) : a * a ≤ b * b := -mul_le_mul h2 h2 h1 (le_trans h1 h2) - -lemma mul_self_lt_mul_self {a b : α} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b := -mul_lt_mul' (le_of_lt h2) h2 h1 (lt_of_le_of_lt h1 h2) -end ordered_semiring - -class linear_ordered_semiring (α : Type u) extends ordered_semiring α, linear_order α := -(zero_lt_one : zero < one) - -section linear_ordered_semiring -variable [linear_ordered_semiring α] - -lemma zero_lt_one : 0 < (1:α) := -linear_ordered_semiring.zero_lt_one - -lemma zero_le_one : 0 ≤ (1:α) := -le_of_lt zero_lt_one - -lemma two_pos : 0 < (2:α) := add_pos zero_lt_one zero_lt_one - -lemma two_ne_zero : (2:α) ≠ 0 := -ne.symm (ne_of_lt two_pos) - -lemma two_gt_one : (2:α) > 1 := -calc (2:α) = 1+1 : one_add_one_eq_two - ... > 1+0 : add_lt_add_left zero_lt_one _ - ... = 1 : add_zero 1 - -lemma two_ge_one : (2:α) ≥ 1 := -le_of_lt two_gt_one - -lemma four_pos : (4:α) > 0 := -add_pos two_pos two_pos - -lemma lt_of_mul_lt_mul_left {a b c : α} (h : c * a < c * b) (hc : c ≥ 0) : a < b := -lt_of_not_ge - (assume h1 : b ≤ a, - have h2 : c * b ≤ c * a, from mul_le_mul_of_nonneg_left h1 hc, - not_lt_of_ge h2 h) - -lemma lt_of_mul_lt_mul_right {a b c : α} (h : a * c < b * c) (hc : c ≥ 0) : a < b := -lt_of_not_ge - (assume h1 : b ≤ a, - have h2 : b * c ≤ a * c, from mul_le_mul_of_nonneg_right h1 hc, - not_lt_of_ge h2 h) - -lemma le_of_mul_le_mul_left {a b c : α} (h : c * a ≤ c * b) (hc : c > 0) : a ≤ b := -le_of_not_gt - (assume h1 : b < a, - have h2 : c * b < c * a, from mul_lt_mul_of_pos_left h1 hc, - not_le_of_gt h2 h) - -lemma le_of_mul_le_mul_right {a b c : α} (h : a * c ≤ b * c) (hc : c > 0) : a ≤ b := -le_of_not_gt - (assume h1 : b < a, - have h2 : b * c < a * c, from mul_lt_mul_of_pos_right h1 hc, - not_le_of_gt h2 h) - -lemma pos_of_mul_pos_left {a b : α} (h : 0 < a * b) (h1 : 0 ≤ a) : 0 < b := -lt_of_not_ge - (assume h2 : b ≤ 0, - have h3 : a * b ≤ 0, from mul_nonpos_of_nonneg_of_nonpos h1 h2, - not_lt_of_ge h3 h) - -lemma pos_of_mul_pos_right {a b : α} (h : 0 < a * b) (h1 : 0 ≤ b) : 0 < a := -lt_of_not_ge - (assume h2 : a ≤ 0, - have h3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg h2 h1, - not_lt_of_ge h3 h) - -lemma nonneg_of_mul_nonneg_left {a b : α} (h : 0 ≤ a * b) (h1 : 0 < a) : 0 ≤ b := -le_of_not_gt - (assume h2 : b < 0, - not_le_of_gt (mul_neg_of_pos_of_neg h1 h2) h) - -lemma nonneg_of_mul_nonneg_right {a b : α} (h : 0 ≤ a * b) (h1 : 0 < b) : 0 ≤ a := -le_of_not_gt - (assume h2 : a < 0, - not_le_of_gt (mul_neg_of_neg_of_pos h2 h1) h) - -lemma neg_of_mul_neg_left {a b : α} (h : a * b < 0) (h1 : 0 ≤ a) : b < 0 := -lt_of_not_ge - (assume h2 : b ≥ 0, - not_lt_of_ge (mul_nonneg h1 h2) h) - -lemma neg_of_mul_neg_right {a b : α} (h : a * b < 0) (h1 : 0 ≤ b) : a < 0 := -lt_of_not_ge - (assume h2 : a ≥ 0, - not_lt_of_ge (mul_nonneg h2 h1) h) - -lemma nonpos_of_mul_nonpos_left {a b : α} (h : a * b ≤ 0) (h1 : 0 < a) : b ≤ 0 := -le_of_not_gt - (assume h2 : b > 0, - not_le_of_gt (mul_pos h1 h2) h) - -lemma nonpos_of_mul_nonpos_right {a b : α} (h : a * b ≤ 0) (h1 : 0 < b) : a ≤ 0 := -le_of_not_gt - (assume h2 : a > 0, - not_le_of_gt (mul_pos h2 h1) h) - -end linear_ordered_semiring - -class decidable_linear_ordered_semiring (α : Type u) extends linear_ordered_semiring α, decidable_linear_order α - -class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α, zero_ne_one_class α := -(mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b) - -lemma ordered_ring.mul_nonneg {α} [s : ordered_ring α] (a b : α) (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : 0 ≤ a * b := -begin - cases classical.em (a ≤ 0), { simp [le_antisymm h h₁] }, - cases classical.em (b ≤ 0), { simp [le_antisymm h_1 h₂] }, - exact (le_not_le_of_lt (ordered_ring.mul_pos a b (lt_of_le_not_le h₁ h) (lt_of_le_not_le h₂ h_1))).left, -end - -lemma ordered_ring.mul_le_mul_of_nonneg_left [s : ordered_ring α] {a b c : α} - (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b := -have 0 ≤ b - a, from sub_nonneg_of_le h₁, -have 0 ≤ c * (b - a), from ordered_ring.mul_nonneg c (b - a) h₂ this, -begin - rw mul_sub_left_distrib at this, - apply le_of_sub_nonneg this -end - -lemma ordered_ring.mul_le_mul_of_nonneg_right [s : ordered_ring α] {a b c : α} - (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c := -have 0 ≤ b - a, from sub_nonneg_of_le h₁, -have 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg (b - a) c this h₂, -begin - rw mul_sub_right_distrib at this, - apply le_of_sub_nonneg this -end - -lemma ordered_ring.mul_lt_mul_of_pos_left [s : ordered_ring α] {a b c : α} - (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b := -have 0 < b - a, from sub_pos_of_lt h₁, -have 0 < c * (b - a), from ordered_ring.mul_pos c (b - a) h₂ this, -begin - rw mul_sub_left_distrib at this, - apply lt_of_sub_pos this -end - -lemma ordered_ring.mul_lt_mul_of_pos_right [s : ordered_ring α] {a b c : α} - (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c := -have 0 < b - a, from sub_pos_of_lt h₁, -have 0 < (b - a) * c, from ordered_ring.mul_pos (b - a) c this h₂, -begin - rw mul_sub_right_distrib at this, - apply lt_of_sub_pos this -end - -instance ordered_ring.to_ordered_semiring [s : ordered_ring α] : ordered_semiring α := -{ mul_zero := mul_zero, - zero_mul := zero_mul, - add_left_cancel := @add_left_cancel α _, - add_right_cancel := @add_right_cancel α _, - le_of_add_le_add_left := @le_of_add_le_add_left α _, - mul_lt_mul_of_pos_left := @ordered_ring.mul_lt_mul_of_pos_left α _, - mul_lt_mul_of_pos_right := @ordered_ring.mul_lt_mul_of_pos_right α _, - ..s } - -section ordered_ring -variable [ordered_ring α] - -lemma mul_le_mul_of_nonpos_left {a b c : α} (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b := -have -c ≥ 0, from neg_nonneg_of_nonpos hc, -have -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left h this, -have -(c * b) ≤ -(c * a), by rwa [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul] at this, -le_of_neg_le_neg this - -lemma mul_le_mul_of_nonpos_right {a b c : α} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c := -have -c ≥ 0, from neg_nonneg_of_nonpos hc, -have b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right h this, -have -(b * c) ≤ -(a * c), by rwa [← neg_mul_eq_mul_neg, ← neg_mul_eq_mul_neg] at this, -le_of_neg_le_neg this - -lemma mul_nonneg_of_nonpos_of_nonpos {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b := -have 0 * b ≤ a * b, from mul_le_mul_of_nonpos_right ha hb, -by rwa zero_mul at this - -lemma mul_lt_mul_of_neg_left {a b c : α} (h : b < a) (hc : c < 0) : c * a < c * b := -have -c > 0, from neg_pos_of_neg hc, -have -c * b < -c * a, from mul_lt_mul_of_pos_left h this, -have -(c * b) < -(c * a), by rwa [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul] at this, -lt_of_neg_lt_neg this - -lemma mul_lt_mul_of_neg_right {a b c : α} (h : b < a) (hc : c < 0) : a * c < b * c := -have -c > 0, from neg_pos_of_neg hc, -have b * -c < a * -c, from mul_lt_mul_of_pos_right h this, -have -(b * c) < -(a * c), by rwa [← neg_mul_eq_mul_neg, ← neg_mul_eq_mul_neg] at this, -lt_of_neg_lt_neg this - -lemma mul_pos_of_neg_of_neg {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b := -have 0 * b < a * b, from mul_lt_mul_of_neg_right ha hb, -by rwa zero_mul at this - -end ordered_ring - -class linear_ordered_ring (α : Type u) extends ordered_ring α, linear_order α := -(zero_lt_one : zero < one) - -instance linear_ordered_ring.to_linear_ordered_semiring [s : linear_ordered_ring α] : linear_ordered_semiring α := -{ mul_zero := mul_zero, - zero_mul := zero_mul, - add_left_cancel := @add_left_cancel α _, - add_right_cancel := @add_right_cancel α _, - le_of_add_le_add_left := @le_of_add_le_add_left α _, - mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left α _, - mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right α _, - le_total := linear_ordered_ring.le_total, - ..s } - -section linear_ordered_ring -variable [linear_ordered_ring α] - -lemma mul_self_nonneg (a : α) : a * a ≥ 0 := -or.elim (le_total 0 a) - (assume h : a ≥ 0, mul_nonneg h h) - (assume h : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos h h) - -lemma pos_and_pos_or_neg_and_neg_of_mul_pos {a b : α} (hab : a * b > 0) : - (a > 0 ∧ b > 0) ∨ (a < 0 ∧ b < 0) := -match lt_trichotomy 0 a with -| or.inl hlt₁ := - match lt_trichotomy 0 b with - | or.inl hlt₂ := or.inl ⟨hlt₁, hlt₂⟩ - | or.inr (or.inl heq₂) := begin rw [← heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end - | or.inr (or.inr hgt₂) := absurd hab (lt_asymm (mul_neg_of_pos_of_neg hlt₁ hgt₂)) - end -| or.inr (or.inl heq₁) := begin rw [← heq₁, zero_mul] at hab, exact absurd hab (lt_irrefl _) end -| or.inr (or.inr hgt₁) := - match lt_trichotomy 0 b with - | or.inl hlt₂ := absurd hab (lt_asymm (mul_neg_of_neg_of_pos hgt₁ hlt₂)) - | or.inr (or.inl heq₂) := begin rw [← heq₂, mul_zero] at hab, exact absurd hab (lt_irrefl _) end - | or.inr (or.inr hgt₂) := or.inr ⟨hgt₁, hgt₂⟩ - end -end - -lemma gt_of_mul_lt_mul_neg_left {a b c : α} (h : c * a < c * b) (hc : c ≤ 0) : a > b := -have nhc : -c ≥ 0, from neg_nonneg_of_nonpos hc, -have h2 : -(c * b) < -(c * a), from neg_lt_neg h, -have h3 : (-c) * b < (-c) * a, from calc - (-c) * b = - (c * b) : by rewrite neg_mul_eq_neg_mul - ... < -(c * a) : h2 - ... = (-c) * a : by rewrite neg_mul_eq_neg_mul, -lt_of_mul_lt_mul_left h3 nhc - - -lemma zero_gt_neg_one : -1 < (0:α) := -begin - have this := neg_lt_neg (@zero_lt_one α _), - rwa neg_zero at this -end - -lemma le_of_mul_le_of_ge_one {a b c : α} (h : a * c ≤ b) (hb : b ≥ 0) (hc : c ≥ 1) : a ≤ b := -have h' : a * c ≤ b * c, from calc - a * c ≤ b : h - ... = b * 1 : by rewrite mul_one - ... ≤ b * c : mul_le_mul_of_nonneg_left hc hb, -le_of_mul_le_mul_right h' (lt_of_lt_of_le zero_lt_one hc) - -lemma nonneg_le_nonneg_of_squares_le {a b : α} (hb : b ≥ 0) (h : a * a ≤ b * b) : a ≤ b := -le_of_not_gt (λhab, not_le_of_gt (mul_self_lt_mul_self hb hab) h) - -lemma mul_self_le_mul_self_iff {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a ≤ b ↔ a * a ≤ b * b := -⟨mul_self_le_mul_self h1, nonneg_le_nonneg_of_squares_le h2⟩ - -lemma mul_self_lt_mul_self_iff {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b := -iff.trans (lt_iff_not_ge _ _) $ iff.trans (not_iff_not_of_iff $ mul_self_le_mul_self_iff h2 h1) $ - iff.symm (lt_iff_not_ge _ _) - -lemma linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero - {a b : α} (h : a * b = 0) : a = 0 ∨ b = 0 := -match lt_trichotomy 0 a with -| or.inl hlt₁ := - match lt_trichotomy 0 b with - | or.inl hlt₂ := - have 0 < a * b, from mul_pos hlt₁ hlt₂, - begin rw h at this, exact absurd this (lt_irrefl _) end - | or.inr (or.inl heq₂) := or.inr heq₂.symm - | or.inr (or.inr hgt₂) := - have 0 > a * b, from mul_neg_of_pos_of_neg hlt₁ hgt₂, - begin rw h at this, exact absurd this (lt_irrefl _) end - end -| or.inr (or.inl heq₁) := or.inl heq₁.symm -| or.inr (or.inr hgt₁) := - match lt_trichotomy 0 b with - | or.inl hlt₂ := - have 0 > a * b, from mul_neg_of_neg_of_pos hgt₁ hlt₂, - begin rw h at this, exact absurd this (lt_irrefl _) end - | or.inr (or.inl heq₂) := or.inr heq₂.symm - | or.inr (or.inr hgt₂) := - have 0 < a * b, from mul_pos_of_neg_of_neg hgt₁ hgt₂, - begin rw h at this, exact absurd this (lt_irrefl _) end - end -end - -end linear_ordered_ring - -class linear_ordered_comm_ring (α : Type u) extends linear_ordered_ring α, comm_monoid α - -instance linear_ordered_comm_ring.to_integral_domain [s: linear_ordered_comm_ring α] : integral_domain α := -{ eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α _, - ..s } - -class decidable_linear_ordered_comm_ring (α : Type u) extends linear_ordered_comm_ring α, - decidable_linear_ordered_add_comm_group α - -instance decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring [d : decidable_linear_ordered_comm_ring α] : - decidable_linear_ordered_semiring α := -let s : linear_ordered_semiring α := @linear_ordered_ring.to_linear_ordered_semiring α _ in -{ zero_mul := @linear_ordered_semiring.zero_mul α s, - mul_zero := @linear_ordered_semiring.mul_zero α s, - add_left_cancel := @linear_ordered_semiring.add_left_cancel α s, - add_right_cancel := @linear_ordered_semiring.add_right_cancel α s, - le_of_add_le_add_left := @linear_ordered_semiring.le_of_add_le_add_left α s, - mul_lt_mul_of_pos_left := @linear_ordered_semiring.mul_lt_mul_of_pos_left α s, - mul_lt_mul_of_pos_right := @linear_ordered_semiring.mul_lt_mul_of_pos_right α s, - ..d } diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean deleted file mode 100644 index e536a21144..0000000000 --- a/library/init/algebra/ring.lean +++ /dev/null @@ -1,338 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad, Leonardo de Moura --/ -prelude -import init.algebra.group - -/- Make sure instances defined in this file have lower priority than the ones - defined for concrete structures -/ -set_option default_priority 100 - -set_option old_structure_cmd true - -universe u - -class distrib (α : Type u) extends has_mul α, has_add α := -(left_distrib : ∀ a b c : α, a * (b + c) = (a * b) + (a * c)) -(right_distrib : ∀ a b c : α, (a + b) * c = (a * c) + (b * c)) - -variable {α : Type u} - -lemma left_distrib [distrib α] (a b c : α) : a * (b + c) = a * b + a * c := -distrib.left_distrib a b c - -def mul_add := @left_distrib - -lemma right_distrib [distrib α] (a b c : α) : (a + b) * c = a * c + b * c := -distrib.right_distrib a b c - -def add_mul := @right_distrib - -class mul_zero_class (α : Type u) extends has_mul α, has_zero α := -(zero_mul : ∀ a : α, 0 * a = 0) -(mul_zero : ∀ a : α, a * 0 = 0) - -@[simp] lemma zero_mul [mul_zero_class α] (a : α) : 0 * a = 0 := -mul_zero_class.zero_mul a - -@[simp] lemma mul_zero [mul_zero_class α] (a : α) : a * 0 = 0 := -mul_zero_class.mul_zero a - -class zero_ne_one_class (α : Type u) extends has_zero α, has_one α := -(zero_ne_one : 0 ≠ (1:α)) - -@[simp] -lemma zero_ne_one [s: zero_ne_one_class α] : 0 ≠ (1:α) := -@zero_ne_one_class.zero_ne_one α s - -@[simp] -lemma one_ne_zero [s: zero_ne_one_class α] : (1:α) ≠ 0 := -assume h, @zero_ne_one_class.zero_ne_one α s h.symm - -/- semiring -/ - -class semiring (α : Type u) extends add_comm_monoid α, monoid α, distrib α, mul_zero_class α - -section semiring - variables [semiring α] - - lemma one_add_one_eq_two : 1 + 1 = (2 : α) := - by unfold bit0 - - theorem two_mul (n : α) : 2 * n = n + n := - eq.trans (right_distrib 1 1 n) (by simp) - - lemma ne_zero_of_mul_ne_zero_right {a b : α} (h : a * b ≠ 0) : a ≠ 0 := - assume : a = 0, - have a * b = 0, by rw [this, zero_mul], - h this - - lemma ne_zero_of_mul_ne_zero_left {a b : α} (h : a * b ≠ 0) : b ≠ 0 := - assume : b = 0, - have a * b = 0, by rw [this, mul_zero], - h this - - lemma distrib_three_right (a b c d : α) : (a + b + c) * d = a * d + b * d + c * d := - by simp [right_distrib] -end semiring - -class comm_semiring (α : Type u) extends semiring α, comm_monoid α - -section comm_semiring - variables [comm_semiring α] (a b c : α) - - instance comm_semiring_has_dvd : has_dvd α := - has_dvd.mk (λ a b, ∃ c, b = a * c) - - -- TODO: this used to not have c explicit, but that seems to be important - -- for use with tactics, similar to exist.intro - theorem dvd.intro {a b : α} (c : α) (h : a * c = b) : a ∣ b := - exists.intro c h^.symm - - def dvd_of_mul_right_eq := @dvd.intro - - theorem dvd.intro_left {a b : α} (c : α) (h : c * a = b) : a ∣ b := - dvd.intro _ (begin rewrite mul_comm at h, apply h end) - - def dvd_of_mul_left_eq := @dvd.intro_left - - theorem exists_eq_mul_right_of_dvd {a b : α} (h : a ∣ b) : ∃ c, b = a * c := h - - theorem dvd.elim {P : Prop} {a b : α} (H₁ : a ∣ b) (H₂ : ∀ c, b = a * c → P) : P := - exists.elim H₁ H₂ - - theorem exists_eq_mul_left_of_dvd {a b : α} (h : a ∣ b) : ∃ c, b = c * a := - dvd.elim h (assume c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c))) - - theorem dvd.elim_left {P : Prop} {a b : α} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P := - exists.elim (exists_eq_mul_left_of_dvd h₁) (assume c, assume h₃ : b = c * a, h₂ c h₃) - - @[simp] theorem dvd_refl : a ∣ a := - dvd.intro 1 (by simp) - - local attribute [simp] mul_assoc mul_comm mul_left_comm - - theorem dvd_trans {a b c : α} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := - match h₁, h₂ with - | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ := - ⟨d * e, show c = a * (d * e), by simp [h₃, h₄]⟩ - end - - def dvd.trans := @dvd_trans - - theorem eq_zero_of_zero_dvd {a : α} (h : 0 ∣ a) : a = 0 := - dvd.elim h (assume c, assume H' : a = 0 * c, eq.trans H' (zero_mul c)) - - @[simp] theorem dvd_zero : a ∣ 0 := dvd.intro 0 (by simp) - - @[simp] theorem one_dvd : 1 ∣ a := dvd.intro a (by simp) - - @[simp] theorem dvd_mul_right : a ∣ a * b := dvd.intro b rfl - - @[simp] theorem dvd_mul_left : a ∣ b * a := dvd.intro b (by simp) - - theorem dvd_mul_of_dvd_left {a b : α} (h : a ∣ b) (c : α) : a ∣ b * c := - dvd.elim h (λ d h', begin rw [h', mul_assoc], apply dvd_mul_right end) - - theorem dvd_mul_of_dvd_right {a b : α} (h : a ∣ b) (c : α) : a ∣ c * b := - begin rw mul_comm, exact dvd_mul_of_dvd_left h _ end - - theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d - | a ._ c ._ ⟨e, rfl⟩ ⟨f, rfl⟩ := ⟨e * f, by simp⟩ - - theorem mul_dvd_mul_left (a : α) {b c : α} (h : b ∣ c) : a * b ∣ a * c := - mul_dvd_mul (dvd_refl a) h - - theorem mul_dvd_mul_right {a b : α} (h : a ∣ b) (c : α) : a * c ∣ b * c := - mul_dvd_mul h (dvd_refl c) - - theorem dvd_add {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c := - dvd.elim h₁ (λ d hd, dvd.elim h₂ (λ e he, dvd.intro (d + e) (by simp [left_distrib, hd, he]))) - - theorem dvd_of_mul_right_dvd {a b c : α} (h : a * b ∣ c) : a ∣ c := - dvd.elim h (begin intros d h₁, rw [h₁, mul_assoc], apply dvd_mul_right end) - - theorem dvd_of_mul_left_dvd {a b c : α} (h : a * b ∣ c) : b ∣ c := - dvd.elim h (λ d ceq, dvd.intro (a * d) (by simp [ceq])) -end comm_semiring - -/- ring -/ - -class ring (α : Type u) extends add_comm_group α, monoid α, distrib α - -local attribute [simp] sub_eq_add_neg - -lemma ring.mul_zero [ring α] (a : α) : a * 0 = 0 := -have a * 0 + 0 = a * 0 + a * 0, from calc - a * 0 + 0 = a * (0 + 0) : by simp - ... = a * 0 + a * 0 : by rw left_distrib, -show a * 0 = 0, from (add_left_cancel this).symm - -lemma ring.zero_mul [ring α] (a : α) : 0 * a = 0 := -have 0 * a + 0 = 0 * a + 0 * a, from calc - 0 * a + 0 = (0 + 0) * a : by simp - ... = 0 * a + 0 * a : by rewrite right_distrib, -show 0 * a = 0, from (add_left_cancel this).symm - -instance ring.to_semiring [s : ring α] : semiring α := -{ mul_zero := ring.mul_zero, zero_mul := ring.zero_mul, ..s } - -lemma neg_mul_eq_neg_mul [s : ring α] (a b : α) : -(a * b) = -a * b := -neg_eq_of_add_eq_zero - begin rw [← right_distrib, add_right_neg, zero_mul] end - -lemma neg_mul_eq_mul_neg [s : ring α] (a b : α) : -(a * b) = a * -b := -neg_eq_of_add_eq_zero - begin rw [← left_distrib, add_right_neg, mul_zero] end - -@[simp] lemma neg_mul_eq_neg_mul_symm [s : ring α] (a b : α) : - a * b = - (a * b) := -eq.symm (neg_mul_eq_neg_mul a b) - -@[simp] lemma mul_neg_eq_neg_mul_symm [s : ring α] (a b : α) : a * - b = - (a * b) := -eq.symm (neg_mul_eq_mul_neg a b) - -lemma neg_mul_neg [s : ring α] (a b : α) : -a * -b = a * b := -by simp - -lemma neg_mul_comm [s : ring α] (a b : α) : -a * b = a * -b := -by simp - -theorem neg_eq_neg_one_mul [s : ring α] (a : α) : -a = -1 * a := -by simp - -lemma mul_sub_left_distrib [s : ring α] (a b c : α) : a * (b - c) = a * b - a * c := -calc - a * (b - c) = a * b + a * -c : left_distrib a b (-c) - ... = a * b - a * c : by simp - -def mul_sub := @mul_sub_left_distrib - -lemma mul_sub_right_distrib [s : ring α] (a b c : α) : (a - b) * c = a * c - b * c := -calc - (a - b) * c = a * c + -b * c : right_distrib a (-b) c - ... = a * c - b * c : by simp - -def sub_mul := @mul_sub_right_distrib - -class comm_ring (α : Type u) extends ring α, comm_semigroup α - -instance comm_ring.to_comm_semiring [s : comm_ring α] : comm_semiring α := -{ mul_zero := mul_zero, zero_mul := zero_mul, ..s } - -section comm_ring - variable [comm_ring α] - - local attribute [simp] add_assoc add_comm add_left_comm mul_comm - - lemma mul_self_sub_mul_self_eq (a b : α) : a * a - b * b = (a + b) * (a - b) := - begin simp [right_distrib, left_distrib], rw [add_comm (-(a*b)), add_left_comm (a*b)], simp end - - lemma mul_self_sub_one_eq (a : α) : a * a - 1 = (a + 1) * (a - 1) := - begin simp [right_distrib, left_distrib], rw [add_left_comm, add_comm (-a), add_left_comm a], simp end - - lemma add_mul_self_eq (a b : α) : (a + b) * (a + b) = a*a + 2*a*b + b*b := - calc (a + b)*(a + b) = a*a + (1+1)*a*b + b*b : by simp [right_distrib, left_distrib] - ... = a*a + 2*a*b + b*b : by rw one_add_one_eq_two - - theorem dvd_neg_of_dvd {a b : α} (h : a ∣ b) : (a ∣ -b) := - dvd.elim h - (assume c, assume : b = a * c, - dvd.intro (-c) (by simp [this])) - - theorem dvd_of_dvd_neg {a b : α} (h : a ∣ -b) : (a ∣ b) := - let t := dvd_neg_of_dvd h in by rwa neg_neg at t - - theorem dvd_neg_iff_dvd (a b : α) : (a ∣ -b) ↔ (a ∣ b) := - ⟨dvd_of_dvd_neg, dvd_neg_of_dvd⟩ - - theorem neg_dvd_of_dvd {a b : α} (h : a ∣ b) : -a ∣ b := - dvd.elim h - (assume c, assume : b = a * c, - dvd.intro (-c) (by simp [this])) - - theorem dvd_of_neg_dvd {a b : α} (h : -a ∣ b) : a ∣ b := - let t := neg_dvd_of_dvd h in by rwa neg_neg at t - - theorem neg_dvd_iff_dvd (a b : α) : (-a ∣ b) ↔ (a ∣ b) := - ⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩ - - theorem dvd_sub {a b c : α} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b - c := - dvd_add h₁ (dvd_neg_of_dvd h₂) - - theorem dvd_add_iff_left {a b c : α} (h : a ∣ c) : a ∣ b ↔ a ∣ b + c := - ⟨λh₂, dvd_add h₂ h, λH, by have t := dvd_sub H h; rwa add_sub_cancel at t⟩ - - theorem dvd_add_iff_right {a b c : α} (h : a ∣ b) : a ∣ c ↔ a ∣ b + c := - by rw add_comm; exact dvd_add_iff_left h -end comm_ring - -class no_zero_divisors (α : Type u) extends has_mul α, has_zero α := -(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ a b : α, a * b = 0 → a = 0 ∨ b = 0) - -lemma eq_zero_or_eq_zero_of_mul_eq_zero [no_zero_divisors α] {a b : α} (h : a * b = 0) : a = 0 ∨ b = 0 := -no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero a b h - -lemma eq_zero_of_mul_self_eq_zero [no_zero_divisors α] {a : α} (h : a * a = 0) : a = 0 := -or.elim (eq_zero_or_eq_zero_of_mul_eq_zero h) (assume h', h') (assume h', h') - -class integral_domain (α : Type u) extends comm_ring α, no_zero_divisors α, zero_ne_one_class α - -section integral_domain - variable [integral_domain α] - - lemma mul_eq_zero_iff_eq_zero_or_eq_zero {a b : α} : a * b = 0 ↔ a = 0 ∨ b = 0 := - ⟨eq_zero_or_eq_zero_of_mul_eq_zero, λo, - or.elim o (λh, by rw h; apply zero_mul) (λh, by rw h; apply mul_zero)⟩ - - lemma mul_ne_zero {a b : α} (h₁ : a ≠ 0) (h₂ : b ≠ 0) : a * b ≠ 0 := - λ h, or.elim (eq_zero_or_eq_zero_of_mul_eq_zero h) (assume h₃, h₁ h₃) (assume h₄, h₂ h₄) - - lemma eq_of_mul_eq_mul_right {a b c : α} (ha : a ≠ 0) (h : b * a = c * a) : b = c := - have b * a - c * a = 0, from sub_eq_zero_of_eq h, - have (b - c) * a = 0, by rw [mul_sub_right_distrib, this], - have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right ha, - eq_of_sub_eq_zero this - - lemma eq_of_mul_eq_mul_left {a b c : α} (ha : a ≠ 0) (h : a * b = a * c) : b = c := - have a * b - a * c = 0, from sub_eq_zero_of_eq h, - have a * (b - c) = 0, by rw [mul_sub_left_distrib, this], - have b - c = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_left ha, - eq_of_sub_eq_zero this - - lemma eq_zero_of_mul_eq_self_right {a b : α} (h₁ : b ≠ 1) (h₂ : a * b = a) : a = 0 := - have hb : b - 1 ≠ 0, from - assume : b - 1 = 0, - have b = 0 + 1, from eq_add_of_sub_eq this, - have b = 1, by rwa zero_add at this, - h₁ this, - have a * b - a = 0, by simp [h₂], - have a * (b - 1) = 0, by rwa [mul_sub_left_distrib, mul_one], - show a = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hb - - lemma eq_zero_of_mul_eq_self_left {a b : α} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 := - eq_zero_of_mul_eq_self_right h₁ (by rwa mul_comm at h₂) - - lemma mul_self_eq_mul_self_iff (a b : α) : a * a = b * b ↔ a = b ∨ a = -b := - iff.intro - (assume : a * a = b * b, - have (a - b) * (a + b) = 0, - by rewrite [mul_comm, ← mul_self_sub_mul_self_eq, this, sub_self], - have a - b = 0 ∨ a + b = 0, from eq_zero_or_eq_zero_of_mul_eq_zero this, - or.elim this - (assume : a - b = 0, or.inl (eq_of_sub_eq_zero this)) - (assume : a + b = 0, or.inr (eq_neg_of_add_eq_zero this))) - (assume : a = b ∨ a = -b, or.elim this - (assume : a = b, by rewrite this) - (assume : a = -b, by rewrite [this, neg_mul_neg])) - - lemma mul_self_eq_one_iff (a : α) : a * a = 1 ↔ a = 1 ∨ a = -1 := - have a * a = 1 * 1 ↔ a = 1 ∨ a = -1, from mul_self_eq_mul_self_iff a 1, - by rwa mul_one at this - -end integral_domain - -/- TODO(Leo): remove the following annotations as soon as we have support for arithmetic - in the SMT tactic framework -/ -attribute [ematch] add_zero zero_add mul_one one_mul mul_zero zero_mul