From 0bcf5c8f5d7ee2ce2161778c3169b8ea344830ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Apr 2018 15:53:14 -0700 Subject: [PATCH] chore(*): remove algebra --- library/init/algebra/classes.lean | 290 ----------- library/init/algebra/default.lean | 8 - library/init/algebra/field.lean | 464 ------------------ library/init/algebra/functions.lean | 482 ------------------ library/init/algebra/group.lean | 430 ---------------- library/init/algebra/order.lean | 240 --------- library/init/algebra/ordered_field.lean | 484 ------------------ library/init/algebra/ordered_group.lean | 620 ------------------------ library/init/algebra/ordered_ring.lean | 384 --------------- library/init/algebra/ring.lean | 332 ------------- library/init/data/ordering/lemmas.lean | 4 +- library/init/default.lean | 2 +- 12 files changed, 4 insertions(+), 3736 deletions(-) delete mode 100644 library/init/algebra/classes.lean delete mode 100644 library/init/algebra/default.lean delete mode 100644 library/init/algebra/field.lean delete mode 100644 library/init/algebra/functions.lean delete mode 100644 library/init/algebra/group.lean delete mode 100644 library/init/algebra/order.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/classes.lean b/library/init/algebra/classes.lean deleted file mode 100644 index 3b084005bb..0000000000 --- a/library/init/algebra/classes.lean +++ /dev/null @@ -1,290 +0,0 @@ -/- -Copyright (c) 2017 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -prelude -import init.logic init.data.ordering.basic -universes u v - -class is_symm_op (α : Type u) (β : out_param (Type v)) (op : α → α → β) : Prop := -(symm_op : ∀ a b, op a b = op b a) - -class is_commutative (α : Type u) (op : α → α → α) : Prop := -(comm : ∀ a b, op a b = op b a) - -instance is_symm_op_of_is_commutative (α : Type u) (op : α → α → α) [is_commutative α op] : is_symm_op α α op := -{symm_op := is_commutative.comm op} - -class is_associative (α : Type u) (op : α → α → α) : Prop := -(assoc : ∀ a b c, op (op a b) c = op a (op b c)) - -class is_left_id (α : Type u) (op : α → α → α) (o : out_param α) : Prop := -(left_id : ∀ a, op o a = a) - -class is_right_id (α : Type u) (op : α → α → α) (o : out_param α) : Prop := -(right_id : ∀ a, op a o = a) - -class is_left_null (α : Type u) (op : α → α → α) (o : out_param α) : Prop := -(left_null : ∀ a, op o a = o) - -class is_right_null (α : Type u) (op : α → α → α) (o : out_param α) : Prop := -(right_null : ∀ a, op a o = o) - -class is_left_cancel (α : Type u) (op : α → α → α) : Prop := -(left_cancel : ∀ a b c, op a b = op a c → b = c) - -class is_right_cancel (α : Type u) (op : α → α → α) : Prop := -(right_cancel : ∀ a b c, op a b = op c b → a = c) - -class is_idempotent (α : Type u) (op : α → α → α) : Prop := -(idempotent : ∀ a, op a a = a) - -class is_left_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param $ α → α → α) : Prop := -(left_distrib : ∀ a b c, op₁ a (op₂ b c) = op₂ (op₁ a b) (op₁ a c)) - -class is_right_distrib (α : Type u) (op₁ : α → α → α) (op₂ : out_param $ α → α → α) : Prop := -(right_distrib : ∀ a b c, op₁ (op₂ a b) c = op₂ (op₁ a c) (op₁ b c)) - -class is_left_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) : Prop := -(left_inv : ∀ a, op (inv a) a = o) - -class is_right_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) : Prop := -(right_inv : ∀ a, op a (inv a) = o) - -class is_cond_left_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) (p : out_param $ α → Prop) : Prop := -(left_inv : ∀ a, p a → op (inv a) a = o) - -class is_cond_right_inv (α : Type u) (op : α → α → α) (inv : out_param $ α → α) (o : out_param α) (p : out_param $ α → Prop) : Prop := -(right_inv : ∀ a, p a → op a (inv a) = o) - -class is_distinct (α : Type u) (a : α) (b : α) : Prop := -(distinct : a ≠ b) - -/- --- The following type class doesn't seem very useful, a regular simp lemma should work for this. -class is_inv (α : Type u) (β : Type v) (f : α → β) (g : out β → α) : Prop := -(inv : ∀ a, g (f a) = a) - --- The following one can also be handled using a regular simp lemma -class is_idempotent (α : Type u) (f : α → α) : Prop := -(idempotent : ∀ a, f (f a) = f a) --/ - -class is_irrefl (α : Type u) (r : α → α → Prop) : Prop := -(irrefl : ∀ a, ¬ r a a) - -class is_refl (α : Type u) (r : α → α → Prop) : Prop := -(refl : ∀ a, r a a) - -class is_symm (α : Type u) (r : α → α → Prop) : Prop := -(symm : ∀ a b, r a b → r b a) - -instance is_symm_op_of_is_symm (α : Type u) (r : α → α → Prop) [is_symm α r] : is_symm_op α Prop r := -{symm_op := λ a b, propext $ iff.intro (is_symm.symm a b) (is_symm.symm b a)} - -class is_asymm (α : Type u) (r : α → α → Prop) : Prop := -(asymm : ∀ a b, r a b → ¬ r b a) - -class is_antisymm (α : Type u) (r : α → α → Prop) : Prop := -(antisymm : ∀ a b, r a b → r b a → a = b) - -class is_trans (α : Type u) (r : α → α → Prop) : Prop := -(trans : ∀ a b c, r a b → r b c → r a c) - -class is_total (α : Type u) (r : α → α → Prop) : Prop := -(total : ∀ a b, r a b ∨ r b a) - -class is_preorder (α : Type u) (r : α → α → Prop) extends is_refl α r, is_trans α r : Prop. - -class is_total_preorder (α : Type u) (r : α → α → Prop) extends is_trans α r, is_total α r : Prop. - -instance is_total_preorder_is_preorder (α : Type u) (r : α → α → Prop) [s : is_total_preorder α r] : is_preorder α r := -{trans := s.trans, - refl := λ a, or.elim (is_total.total r a a) id id} - -class is_partial_order (α : Type u) (r : α → α → Prop) extends is_preorder α r, is_antisymm α r : Prop. - -class is_linear_order (α : Type u) (r : α → α → Prop) extends is_partial_order α r, is_total α r : Prop. - -class is_equiv (α : Type u) (r : α → α → Prop) extends is_preorder α r, is_symm α r : Prop. - -class is_per (α : Type u) (r : α → α → Prop) extends is_symm α r, is_trans α r : Prop. - -class is_strict_order (α : Type u) (r : α → α → Prop) extends is_irrefl α r, is_trans α r : Prop. - -class is_incomp_trans (α : Type u) (lt : α → α → Prop) : Prop := -(incomp_trans : ∀ a b c, (¬ lt a b ∧ ¬ lt b a) → (¬ lt b c ∧ ¬ lt c b) → (¬ lt a c ∧ ¬ lt c a)) - -class is_strict_weak_order (α : Type u) (lt : α → α → Prop) extends is_strict_order α lt, is_incomp_trans α lt : Prop. - -class is_trichotomous (α : Type u) (lt : α → α → Prop) : Prop := -(trichotomous : ∀ a b, lt a b ∨ a = b ∨ lt b a) - -class is_strict_total_order (α : Type u) (lt : α → α → Prop) extends is_trichotomous α lt, is_strict_weak_order α lt. - -instance eq_is_equiv (α : Type u) : is_equiv α (=) := -{symm := @eq.symm _, trans := @eq.trans _, refl := eq.refl} - -section -variables {α : Type u} {r : α → α → Prop} -local infix `≺`:50 := r - -lemma irrefl [is_irrefl α r] (a : α) : ¬ a ≺ a := -is_irrefl.irrefl _ a - -lemma refl [is_refl α r] (a : α) : a ≺ a := -is_refl.refl _ a - -lemma trans [is_trans α r] {a b c : α} : a ≺ b → b ≺ c → a ≺ c := -is_trans.trans _ _ _ - -lemma symm [is_symm α r] {a b : α} : a ≺ b → b ≺ a := -is_symm.symm _ _ - -lemma antisymm [is_antisymm α r] {a b : α} : a ≺ b → b ≺ a → a = b := -is_antisymm.antisymm _ _ - -lemma asymm [is_asymm α r] {a b : α} : a ≺ b → ¬ b ≺ a := -is_asymm.asymm _ _ - -lemma trichotomous [is_trichotomous α r] : ∀ (a b : α), a ≺ b ∨ a = b ∨ b ≺ a := -is_trichotomous.trichotomous r - -lemma incomp_trans [is_incomp_trans α r] {a b c : α} : (¬ a ≺ b ∧ ¬ b ≺ a) → (¬ b ≺ c ∧ ¬ c ≺ b) → (¬ a ≺ c ∧ ¬ c ≺ a) := -is_incomp_trans.incomp_trans _ _ _ - -instance is_asymm_of_is_trans_of_is_irrefl [is_trans α r] [is_irrefl α r] : is_asymm α r := -⟨λ a b h₁ h₂, absurd (trans h₁ h₂) (irrefl a)⟩ - -section explicit_relation_variants -variable (r) - -@[elab_simple] -lemma irrefl_of [is_irrefl α r] (a : α) : ¬ a ≺ a := irrefl a - -@[elab_simple] -lemma refl_of [is_refl α r] (a : α) : a ≺ a := refl a - -@[elab_simple] -lemma trans_of [is_trans α r] {a b c : α} : a ≺ b → b ≺ c → a ≺ c := trans - -@[elab_simple] -lemma symm_of [is_symm α r] {a b : α} : a ≺ b → b ≺ a := symm - -@[elab_simple] -lemma asymm_of [is_asymm α r] {a b : α} : a ≺ b → ¬ b ≺ a := asymm - -@[elab_simple] -lemma total_of [is_total α r] (a b : α) : a ≺ b ∨ b ≺ a := -is_total.total _ _ _ - -@[elab_simple] -lemma trichotomous_of [is_trichotomous α r] : ∀ (a b : α), a ≺ b ∨ a = b ∨ b ≺ a := trichotomous - -@[elab_simple] -lemma incomp_trans_of [is_incomp_trans α r] {a b c : α} : (¬ a ≺ b ∧ ¬ b ≺ a) → (¬ b ≺ c ∧ ¬ c ≺ b) → (¬ a ≺ c ∧ ¬ c ≺ a) := incomp_trans - -end explicit_relation_variants - -end - -namespace strict_weak_order -section -parameters {α : Type u} {r : α → α → Prop} -local infix `≺`:50 := r - -def equiv (a b : α) : Prop := -¬ a ≺ b ∧ ¬ b ≺ a - -parameter [is_strict_weak_order α r] - -local infix ` ≈ `:50 := equiv - -lemma erefl (a : α) : a ≈ a := -⟨irrefl a, irrefl a⟩ - -lemma esymm {a b : α} : a ≈ b → b ≈ a := -λ ⟨h₁, h₂⟩, ⟨h₂, h₁⟩ - -lemma etrans {a b c : α} : a ≈ b → b ≈ c → a ≈ c := -incomp_trans - -lemma not_lt_of_equiv {a b : α} : a ≈ b → ¬ a ≺ b := -λ h, h.1 - -lemma not_lt_of_equiv' {a b : α} : a ≈ b → ¬ b ≺ a := -λ h, h.2 - -instance : is_equiv α equiv := -{refl := erefl, trans := @etrans, symm := @esymm} -end - -/- Notation for the equivalence relation induced by lt -/ -notation a ` ≈[`:50 lt `]` b:50 := @equiv _ lt a b -end strict_weak_order - -lemma is_strict_weak_order_of_is_total_preorder {α : Type u} {le : α → α → Prop} {lt : α → α → Prop} [decidable_rel le] [s : is_total_preorder α le] - (h : ∀ a b, lt a b ↔ ¬ le b a) : is_strict_weak_order α lt := -{ - trans := - λ a b c hab hbc, - have nba : ¬ le b a, from iff.mp (h _ _) hab, - have ncb : ¬ le c b, from iff.mp (h _ _) hbc, - have hab : le a b, from or.resolve_left (total_of le b a) nba, - have nca : ¬ le c a, from λ hca : le c a, - have hcb : le c b, from trans_of le hca hab, - absurd hcb ncb, - iff.mpr (h _ _) nca, - - irrefl := λ a hlt, absurd (refl_of le a) (iff.mp (h _ _) hlt), - - incomp_trans := λ a b c ⟨nab, nba⟩ ⟨nbc, ncb⟩, - have hba : le b a, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) nab), - have hab : le a b, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) nba), - have hcb : le c b, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) nbc), - have hbc : le b c, from decidable.of_not_not (iff.mp (not_iff_not_of_iff (h _ _)) ncb), - have hac : le a c, from trans_of le hab hbc, - have hca : le c a, from trans_of le hcb hba, - and.intro - (λ n, absurd hca (iff.mp (h _ _) n)) - (λ n, absurd hac (iff.mp (h _ _) n)) -} - -lemma lt_of_lt_of_incomp {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] [decidable_rel lt] - : ∀ {a b c}, lt a b → (¬ lt b c ∧ ¬ lt c b) → lt a c := -λ a b c hab ⟨nbc, ncb⟩, - have nca : ¬ lt c a, from λ hca, absurd (trans_of lt hca hab) ncb, - decidable.by_contradiction $ - λ nac : ¬ lt a c, - have ¬ lt a b ∧ ¬ lt b a, from incomp_trans_of lt ⟨nac, nca⟩ ⟨ncb, nbc⟩, - absurd hab this.1 - -lemma lt_of_incomp_of_lt {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] [decidable_rel lt] - : ∀ {a b c}, (¬ lt a b ∧ ¬ lt b a) → lt b c → lt a c := -λ a b c ⟨nab, nba⟩ hbc, - have nca : ¬ lt c a, from λ hca, absurd (trans_of lt hbc hca) nba, - decidable.by_contradiction $ - λ nac : ¬ lt a c, - have ¬ lt b c ∧ ¬ lt c b, from incomp_trans_of lt ⟨nba, nab⟩ ⟨nac, nca⟩, - absurd hbc this.1 - -lemma eq_of_incomp {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b} : (¬ lt a b ∧ ¬ lt b a) → a = b := -λ ⟨nab, nba⟩, - match trichotomous_of lt a b with - | or.inl hab := absurd hab nab - | or.inr (or.inl hab) := hab - | or.inr (or.inr hba) := absurd hba nba - end - -lemma eq_of_eqv_lt {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] {a b} : a ≈[lt] b → a = b := -eq_of_incomp - -lemma incomp_iff_eq {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] [is_irrefl α lt] (a b) : (¬ lt a b ∧ ¬ lt b a) ↔ a = b := -iff.intro eq_of_incomp (λ hab, eq.subst hab (and.intro (irrefl_of lt a) (irrefl_of lt a))) - -lemma eqv_lt_iff_eq {α : Type u} {lt : α → α → Prop} [is_trichotomous α lt] [is_irrefl α lt] (a b) : a ≈[lt] b ↔ a = b := -incomp_iff_eq a b - -lemma not_lt_of_lt {α : Type u} {lt : α → α → Prop} [is_strict_order α lt] {a b} : lt a b → ¬ lt b a := -λ h₁ h₂, absurd (trans_of lt h₁ h₂) (irrefl_of lt _) diff --git a/library/init/algebra/default.lean b/library/init/algebra/default.lean deleted file mode 100644 index 4fac2fd37b..0000000000 --- a/library/init/algebra/default.lean +++ /dev/null @@ -1,8 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -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.functions diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean deleted file mode 100644 index e4e9648587..0000000000 --- a/library/init/algebra/field.lean +++ /dev/null @@ -1,464 +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) - -variable {α : Type u} - -section division_ring -variables [division_ring α] - -protected definition algebra.div (a b : α) : α := -a * b⁻¹ - -instance division_ring_has_div [division_ring α] : has_div α := -⟨algebra.div⟩ - -lemma division_def (a b : α) : a / b = a * b⁻¹ := -rfl - -@[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 inv_ne_zero {a : α} (h : a ≠ 0) : a⁻¹ ≠ 0 := -by rw inv_eq_one_div; exact one_div_ne_zero 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". α 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 : α} (ha : a ≠ 0) (hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (b * a) := -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 - -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 division_ring.one_div_neg_eq_neg_one_div {a : α} (h : a ≠ 0) : 1 / (- a) = - (1 / a) := -have -1 ≠ (0:α), from - (assume : -1 = 0, absurd (eq.symm (calc - 1 = -(-1) : (neg_neg (1:α)).symm - ... = -0 : by rw this - ... = (0:α) : neg_zero)) zero_ne_one), -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 h this) - ... = (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 : α) (ha : a ≠ 0) : b / (- a) = - (b / a) := -calc - b / (- a) = b * (1 / (- a)) : by rw [← inv_eq_one_div, division_def] - ... = b * -(1 / a) : by rw (division_ring.one_div_neg_eq_neg_one_div ha) - ... = -(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 division_ring.neg_div_neg_eq (a : α) {b : α} (hb : b ≠ 0) : (-a) / (-b) = a / b := -by rw [(div_neg_eq_neg_div _ hb), neg_div, neg_neg] - -lemma division_ring.one_div_one_div {a : α} (h : a ≠ 0) : 1 / (1 / a) = a := -eq.symm (eq_one_div_of_mul_eq_one_left (mul_one_div_cancel h)) - -lemma division_ring.inv_inv {a : α} (h : a ≠ 0) : a⁻¹⁻¹ = a := -by rw [inv_eq_one_div, inv_eq_one_div, division_ring.one_div_one_div h] - -lemma division_ring.eq_of_one_div_eq_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : 1 / a = 1 / b) : a = b := -by rw [← division_ring.one_div_one_div ha, h, (division_ring.one_div_one_div hb)] - -lemma mul_inv_eq {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (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 ha hb - ... = (b * a)⁻¹ : by simp - -lemma division_ring.one_div_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : 1 / (a / b) = b / a := -by rw [one_div_eq_inv, division_def, mul_inv_eq (inv_ne_zero hb) ha, - division_ring.inv_inv hb, division_def] - -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_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] - -end division_ring - -class field (α : Type u) extends division_ring α, comm_ring α - -section field - -variable [field α] - -lemma field.one_div_mul_one_div {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (a * b) := -by rw [(division_ring.one_div_mul_one_div ha hb), mul_comm b] - -lemma field.div_mul_right {a b : α} (hb : b ≠ 0) (h : a * b ≠ 0) : a / (a * b) = 1 / b := -have a ≠ 0, from ne_zero_of_mul_ne_zero_right h, - eq.symm (calc - 1 / b = a * ((1 / a) * (1 / b)) : by rw [← mul_assoc, mul_one_div_cancel this, one_mul] - ... = a * (1 / (b * a)) : by rw (division_ring.one_div_mul_one_div this hb) - ... = a * (a * b)⁻¹ : by rw [inv_eq_one_div, mul_comm a b]) - -lemma field.div_mul_left {a b : α} (ha : a ≠ 0) (h : a * b ≠ 0) : b / (a * b) = 1 / a := -have b * a ≠ 0, from mul_ne_zero_comm h, -by rw [mul_comm a, (field.div_mul_right ha this)] - -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) := -have a * b ≠ 0, from (division_ring.mul_ne_zero ha hb), -by rw [add_comm, ← field.div_mul_left ha this, ← field.div_mul_right hb this, - division_def, division_def, division_def, ← right_distrib] - -local attribute [simp] mul_assoc mul_comm mul_left_comm - -lemma field.div_mul_div (a : α) {b : α} (c : α) {d : α} (hb : b ≠ 0) (hd : d ≠ 0) : - (a / b) * (c / d) = (a * c) / (b * d) := -begin simp [division_def], rw [mul_inv_eq hd hb, mul_comm d⁻¹] end - -lemma mul_div_mul_left (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : - (c * a) / (c * b) = a / b := -by rw [← field.div_mul_div _ _ hc hb, div_self hc, one_mul] - -lemma mul_div_mul_right (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : - (a * c) / (b * c) = a / b := -by rw [mul_comm a, mul_comm b, mul_div_mul_left _ hb hc] - -lemma div_mul_eq_mul_div (a b c : α) : (b / c) * a = (b * a) / c := -by simp [division_def] - -lemma field.div_mul_eq_mul_div_comm (a b : α) {c : α} (hc : c ≠ 0) : - (b / c) * a = b * (a / c) := -by rw [div_mul_eq_mul_div, ← one_mul c, ← field.div_mul_div _ _ (ne.symm zero_ne_one) hc, - 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 _ hb hd, ← mul_div_mul_left _ hd 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, - ← field.div_mul_eq_mul_div_comm _ _ hb, h, div_mul_eq_mul_div, div_mul_cancel _ hd] - -lemma field.div_div_eq_mul_div (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : - a / (b / c) = (a * c) / b := -by rw [div_eq_mul_one_div, division_ring.one_div_div hb hc, ← mul_div_assoc] - -lemma field.div_div_eq_div_mul (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : - (a / b) / c = a / (b * c) := -by rw [div_eq_mul_one_div, field.div_mul_div _ _ hb hc, mul_one] - -lemma field.div_div_div_div_eq (a : α) {b c d : α} (hb : b ≠ 0) (hc : c ≠ 0) (hd : d ≠ 0) : - (a / b) / (c / d) = (a * d) / (b * c) := -by rw [field.div_div_eq_mul_div _ hc hd, div_mul_eq_mul_div, - field.div_div_eq_div_mul _ hb hc] - -lemma field.div_mul_eq_div_mul_one_div (a : α) {b c : α} (hb : b ≠ 0) (hc : c ≠ 0) : - a / (b * c) = (a / b) * (1 / c) := -by rw [← field.div_div_eq_div_mul _ hb hc, ← div_eq_mul_one_div] - -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, ← div_self h, div_mul_eq_mul_div, h₂, mul_div_cancel_left _ h] - -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, ← div_self h, ← mul_div_assoc, h2, mul_div_cancel _ h] - -end field - -class discrete_field (α : Type u) extends field α := -(has_decidable_eq : decidable_eq α) -(inv_zero : inv zero = zero) - -attribute [instance] discrete_field.has_decidable_eq - -section discrete_field -variable [discrete_field α] - --- many of the lemmas in discrete_field are the same as lemmas in field or division ring, --- but with fewer hypotheses since 0⁻¹ = 0 and equality is decidable. - -lemma discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero - (a b : α) (h : a * b = 0) : a = 0 ∨ b = 0 := -decidable.by_cases - (assume : a = 0, or.inl this) - (assume : a ≠ 0, - or.inr (by rw [← one_mul b, ← inv_mul_cancel this, mul_assoc, h, mul_zero])) - -instance discrete_field.to_integral_domain [s : discrete_field α] : integral_domain α := -{ eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero, - ..s } - -lemma inv_zero : 0⁻¹ = (0:α) := -discrete_field.inv_zero α - -lemma one_div_zero : 1 / 0 = (0:α) := -calc - 1 / 0 = (1:α) * 0⁻¹ : by rw division_def - ... = 1 * 0 : by rw inv_zero - ... = (0:α) : by rw mul_zero - -lemma div_zero (a : α) : a / 0 = 0 := -by rw [div_eq_mul_one_div, one_div_zero, mul_zero] - -lemma ne_zero_of_one_div_ne_zero {a : α} (h : 1 / a ≠ 0) : a ≠ 0 := -assume ha : a = 0, begin rw [ha, one_div_zero] at h, contradiction end - -lemma eq_zero_of_one_div_eq_zero {a : α} (h : 1 / a = 0) : a = 0 := -decidable.by_cases - (assume ha, ha) - (assume ha, false.elim ((one_div_ne_zero ha) h)) - -lemma one_div_mul_one_div' (a b : α) : (1 / a) * (1 / b) = 1 / (b * a) := -decidable.by_cases - (assume : a = 0, - by rw [this, div_zero, zero_mul, mul_zero, div_zero]) - (assume ha : a ≠ 0, - decidable.by_cases - (assume : b = 0, - by rw [this, div_zero, mul_zero, zero_mul, div_zero]) - (assume : b ≠ 0, division_ring.one_div_mul_one_div ha this)) - -lemma one_div_neg_eq_neg_one_div (a : α) : 1 / (- a) = - (1 / a) := -decidable.by_cases - (assume : a = 0, by rw [this, neg_zero, div_zero, neg_zero]) - (assume : a ≠ 0, division_ring.one_div_neg_eq_neg_one_div this) - -lemma neg_div_neg_eq (a b : α) : (-a) / (-b) = a / b := -decidable.by_cases - (assume hb : b = 0, by rw [hb, neg_zero, div_zero, div_zero]) - (assume hb : b ≠ 0, division_ring.neg_div_neg_eq _ hb) - -lemma one_div_one_div (a : α) : 1 / (1 / a) = a := -decidable.by_cases - (assume ha : a = 0, by rw [ha, div_zero, div_zero]) - (assume ha : a ≠ 0, division_ring.one_div_one_div ha) - -lemma eq_of_one_div_eq_one_div {a b : α} (h : 1 / a = 1 / b) : a = b := -decidable.by_cases - (assume ha : a = 0, - have hb : b = 0, from eq_zero_of_one_div_eq_zero (by rw [← h, ha, div_zero]), - hb.symm ▸ ha) - (assume ha : a ≠ 0, - have hb : b ≠ 0, from ne_zero_of_one_div_ne_zero (h ▸ (one_div_ne_zero ha)), - division_ring.eq_of_one_div_eq_one_div ha hb h) - -lemma mul_inv' (a b : α) : (b * a)⁻¹ = a⁻¹ * b⁻¹ := -decidable.by_cases - (assume ha : a = 0, by rw [ha, mul_zero, inv_zero, zero_mul]) - (assume ha : a ≠ 0, - decidable.by_cases - (assume hb : b = 0, by rw [hb, zero_mul, inv_zero, mul_zero]) - (assume hb : b ≠ 0, mul_inv_eq ha hb)) - --- the following are specifically for fields -lemma one_div_mul_one_div (a b : α) : (1 / a) * (1 / b) = 1 / (a * b) := -by rw [one_div_mul_one_div', mul_comm b] - -lemma div_mul_right {a : α} (b : α) (ha : a ≠ 0) : a / (a * b) = 1 / b := -decidable.by_cases - (assume hb : b = 0, by rw [hb, mul_zero, div_zero, div_zero]) - (assume hb : b ≠ 0, field.div_mul_right hb (mul_ne_zero ha hb)) - -lemma div_mul_left (a : α) {b : α} (hb : b ≠ 0) : b / (a * b) = 1 / a := -by rw [mul_comm a, div_mul_right _ hb] - -lemma div_mul_div (a b c d : α) : (a / b) * (c / d) = (a * c) / (b * d) := -decidable.by_cases - (assume hb : b = 0, by rw [hb, div_zero, zero_mul, zero_mul, div_zero]) - (assume hb : b ≠ 0, - decidable.by_cases - (assume hd : d = 0, by rw [hd, div_zero, mul_zero, mul_zero, div_zero]) - (assume hd : d ≠ 0, field.div_mul_div _ _ hb hd)) - -lemma mul_div_mul_left' (a b : α) {c : α} (hc : c ≠ 0) : (c * a) / (c * b) = a / b := -decidable.by_cases - (assume hb : b = 0, by rw [hb, mul_zero, div_zero, div_zero]) - (assume hb : b ≠ 0, mul_div_mul_left _ hb hc) - -lemma mul_div_mul_right' (a b : α) {c : α} (hc : c ≠ 0) : (a * c) / (b * c) = a / b := -by rw [mul_comm a, mul_comm b, (mul_div_mul_left' _ _ hc)] - -lemma div_mul_eq_mul_div_comm (a b c : α) : (b / c) * a = b * (a / c) := -decidable.by_cases - (assume hc : c = 0, by rw [hc, div_zero, zero_mul, div_zero, mul_zero]) - (assume hc : c ≠ 0, field.div_mul_eq_mul_div_comm _ _ hc) - -lemma one_div_div (a b : α) : 1 / (a / b) = b / a := -decidable.by_cases - (assume ha : a = 0, by rw [ha, zero_div, div_zero, div_zero]) - (assume ha : a ≠ 0, - decidable.by_cases - (assume hb : b = 0, by rw [hb, div_zero, zero_div, div_zero]) - (assume hb : b ≠ 0, division_ring.one_div_div ha 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_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_helper {a : α} (b : α) (h : a ≠ 0) : (1 / (a * b)) * a = 1 / b := -by rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h] - -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 discrete_field diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean deleted file mode 100644 index 56fcf72a62..0000000000 --- a/library/init/algebra/functions.lean +++ /dev/null @@ -1,482 +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_field - -universe u - -definition min {α : Type u} [decidable_linear_order α] (a b : α) : α := if a ≤ b then a else b -definition max {α : Type u} [decidable_linear_order α] (a b : α) : α := if a ≤ b then b else a -definition abs {α : Type u} [decidable_linear_ordered_comm_group α] (a : α) : α := max a (-a) - -section -open decidable tactic -variables {α : Type u} [decidable_linear_order α] - -private meta def min_tac_step : tactic unit := -solve1 $ intros ->> `[unfold min max] ->> try `[simp [*, if_pos, if_neg]] ->> try `[apply le_refl] ->> try `[apply le_of_not_le, assumption] - -meta def tactic.interactive.min_tac (a b : interactive.parse lean.parser.pexpr) : tactic unit := -interactive.by_cases (none, ``(%%a ≤ %%b)); min_tac_step - -lemma min_le_left (a b : α) : min a b ≤ a := -by min_tac a b - -lemma min_le_right (a b : α) : min a b ≤ b := -by min_tac a b - -lemma le_min {a b c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b := -by min_tac a b - -lemma le_max_left (a b : α) : a ≤ max a b := -by min_tac a b - -lemma le_max_right (a b : α) : b ≤ max a b := -by min_tac a b - -lemma max_le {a b c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c := -by min_tac a b - -lemma eq_min {a b c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) (h₃ : ∀{d}, d ≤ a → d ≤ b → d ≤ c) : c = min a b := -le_antisymm (le_min h₁ h₂) (h₃ (min_le_left a b) (min_le_right a b)) - -lemma min_comm (a b : α) : min a b = min b a := -eq_min (min_le_right a b) (min_le_left a b) (λ c h₁ h₂, le_min h₂ h₁) - -lemma min_assoc (a b c : α) : min (min a b) c = min a (min b c) := -begin - apply eq_min, - { apply le_trans, apply min_le_left, apply min_le_left }, - { apply le_min, apply le_trans, apply min_le_left, apply min_le_right, apply min_le_right }, - { intros d h₁ h₂, apply le_min, apply le_min h₁, apply le_trans h₂, apply min_le_left, - apply le_trans h₂, apply min_le_right } -end - -lemma min_left_comm : ∀ (a b c : α), min a (min b c) = min b (min a c) := -left_comm (@min α _) (@min_comm α _) (@min_assoc α _) - -@[simp] -lemma min_self (a : α) : min a a = a := -by min_tac a a - -lemma min_eq_left {a b : α} (h : a ≤ b) : min a b = a := -begin apply eq.symm, apply eq_min (le_refl _) h, intros, assumption end - -lemma min_eq_right {a b : α} (h : b ≤ a) : min a b = b := -eq.subst (min_comm b a) (min_eq_left h) - -lemma eq_max {a b c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) (h₃ : ∀{d}, a ≤ d → b ≤ d → c ≤ d) : c = max a b := -le_antisymm (h₃ (le_max_left a b) (le_max_right a b)) (max_le h₁ h₂) - -lemma max_comm (a b : α) : max a b = max b a := -eq_max (le_max_right a b) (le_max_left a b) (λ c h₁ h₂, max_le h₂ h₁) - -lemma max_assoc (a b c : α) : max (max a b) c = max a (max b c) := -begin - apply eq_max, - { apply le_trans, apply le_max_left a b, apply le_max_left }, - { apply max_le, apply le_trans, apply le_max_right a b, apply le_max_left, apply le_max_right }, - { intros d h₁ h₂, apply max_le, apply max_le h₁, apply le_trans (le_max_left _ _) h₂, - apply le_trans (le_max_right _ _) h₂} -end - -lemma max_left_comm : ∀ (a b c : α), max a (max b c) = max b (max a c) := -left_comm (@max α _) (@max_comm α _) (@max_assoc α _) - -@[simp] -lemma max_self (a : α) : max a a = a := -by min_tac a a - -lemma max_eq_left {a b : α} (h : b ≤ a) : max a b = a := -begin apply eq.symm, apply eq_max (le_refl _) h, intros, assumption end - -lemma max_eq_right {a b : α} (h : a ≤ b) : max a b = b := -eq.subst (max_comm b a) (max_eq_left h) - -/- these rely on lt_of_lt -/ - -lemma min_eq_left_of_lt {a b : α} (h : a < b) : min a b = a := -min_eq_left (le_of_lt h) - -lemma min_eq_right_of_lt {a b : α} (h : b < a) : min a b = b := -min_eq_right (le_of_lt h) - -lemma max_eq_left_of_lt {a b : α} (h : b < a) : max a b = a := -max_eq_left (le_of_lt h) - -lemma max_eq_right_of_lt {a b : α} (h : a < b) : max a b = b := -max_eq_right (le_of_lt h) - -/- these use the fact that it is a linear ordering -/ - -lemma lt_min {a b c : α} (h₁ : a < b) (h₂ : a < c) : a < min b c := -or.elim (le_or_gt b c) - (assume h : b ≤ c, by min_tac b c) - (assume h : b > c, by min_tac b c) - -lemma max_lt {a b c : α} (h₁ : a < c) (h₂ : b < c) : max a b < c := -or.elim (le_or_gt a b) - (assume h : a ≤ b, by min_tac a b) - (assume h : a > b, by min_tac a b) -end - - -section -variables {α : Type u} [decidable_linear_ordered_cancel_comm_monoid α] - -lemma min_add_add_left (a b c : α) : min (a + b) (a + c) = a + min b c := -eq.symm (eq_min - (show a + min b c ≤ a + b, from add_le_add_left (min_le_left _ _) _) - (show a + min b c ≤ a + c, from add_le_add_left (min_le_right _ _) _) - (assume d, - assume : d ≤ a + b, - assume : d ≤ a + c, - decidable.by_cases - (assume : b ≤ c, by rwa [min_eq_left this]) - (assume : ¬ b ≤ c, by rwa [min_eq_right (le_of_lt (lt_of_not_ge this))]))) - -lemma min_add_add_right (a b c : α) : min (a + c) (b + c) = min a b + c := -begin rw [add_comm a c, add_comm b c, add_comm _ c], apply min_add_add_left end - -lemma max_add_add_left (a b c : α) : max (a + b) (a + c) = a + max b c := -eq.symm (eq_max - (add_le_add_left (le_max_left _ _) _) - (add_le_add_left (le_max_right _ _) _) - (assume d, - assume : a + b ≤ d, - assume : a + c ≤ d, - decidable.by_cases - (assume : b ≤ c, by rwa [max_eq_right this]) - (assume : ¬ b ≤ c, by rwa [max_eq_left (le_of_lt (lt_of_not_ge this))]))) - -lemma max_add_add_right (a b c : α) : max (a + c) (b + c) = max a b + c := -begin rw [add_comm a c, add_comm b c, add_comm _ c], apply max_add_add_left end -end - -section -variables {α : Type u} [decidable_linear_ordered_comm_group α] - -lemma max_neg_neg (a b : α) : max (-a) (-b) = - min a b := -eq.symm (eq_max - (show -a ≤ -(min a b), from neg_le_neg $ min_le_left a b) - (show -b ≤ -(min a b), from neg_le_neg $ min_le_right a b) - (assume d, - assume H₁ : -a ≤ d, - assume H₂ : -b ≤ d, - have H : -d ≤ min a b, - from le_min (neg_le_of_neg_le H₁) (neg_le_of_neg_le H₂), - show -(min a b) ≤ d, from neg_le_of_neg_le H)) - -lemma min_eq_neg_max_neg_neg (a b : α) : min a b = - max (-a) (-b) := -by rw [max_neg_neg, neg_neg] - -lemma min_neg_neg (a b : α) : min (-a) (-b) = - max a b := -by rw [min_eq_neg_max_neg_neg, neg_neg, neg_neg] - -lemma max_eq_neg_min_neg_neg (a b : α) : max a b = - min (-a) (-b) := -by rw [min_neg_neg, neg_neg] -end - -section decidable_linear_ordered_comm_group -variables {α : Type u} [decidable_linear_ordered_comm_group α] - -lemma abs_of_nonneg {a : α} (h : a ≥ 0) : abs a = a := -have h' : -a ≤ a, from le_trans (neg_nonpos_of_nonneg h) h, -max_eq_left h' - -lemma abs_of_pos {a : α} (h : a > 0) : abs a = a := -abs_of_nonneg (le_of_lt h) - -lemma abs_of_nonpos {a : α} (h : a ≤ 0) : abs a = -a := -have h' : a ≤ -a, from le_trans h (neg_nonneg_of_nonpos h), -max_eq_right h' - -lemma abs_of_neg {a : α} (h : a < 0) : abs a = -a := -abs_of_nonpos (le_of_lt h) - -lemma abs_zero : abs 0 = (0:α) := -abs_of_nonneg (le_refl _) - -lemma abs_neg (a : α) : abs (-a) = abs a := -begin unfold abs, rw [max_comm, neg_neg] end - -lemma abs_pos_of_pos {a : α} (h : a > 0) : abs a > 0 := -by rwa (abs_of_pos h) - -lemma abs_pos_of_neg {a : α} (h : a < 0) : abs a > 0 := -abs_neg a ▸ abs_pos_of_pos (neg_pos_of_neg h) - -lemma abs_sub (a b : α) : abs (a - b) = abs (b - a) := -by rw [← neg_sub, abs_neg] - -lemma ne_zero_of_abs_ne_zero {a : α} (h : abs a ≠ 0) : a ≠ 0 := -assume ha, h (eq.symm ha ▸ abs_zero) - -/- these assume a linear order -/ - -lemma eq_zero_of_neg_eq {a : α} (h : -a = a) : a = 0 := -match lt_trichotomy a 0 with -| or.inl h₁ := - have a > 0, from h ▸ neg_pos_of_neg h₁, - absurd h₁ (lt_asymm this) -| or.inr (or.inl h₁) := h₁ -| or.inr (or.inr h₁) := - have a < 0, from h ▸ neg_neg_of_pos h₁, - absurd h₁ (lt_asymm this) -end - -lemma abs_nonneg (a : α) : abs a ≥ 0 := -or.elim (le_total 0 a) - (assume h : 0 ≤ a, by rwa (abs_of_nonneg h)) - (assume h : a ≤ 0, calc - 0 ≤ -a : neg_nonneg_of_nonpos h - ... = abs a : eq.symm (abs_of_nonpos h)) - -lemma abs_abs (a : α) : abs (abs a) = abs a := -abs_of_nonneg $ abs_nonneg a - -lemma le_abs_self (a : α) : a ≤ abs a := -or.elim (le_total 0 a) - (assume h : 0 ≤ a, - begin rw [abs_of_nonneg h] end) - (assume h : a ≤ 0, le_trans h $ abs_nonneg a) - -lemma neg_le_abs_self (a : α) : -a ≤ abs a := -abs_neg a ▸ le_abs_self (-a) - -lemma eq_zero_of_abs_eq_zero {a : α} (h : abs a = 0) : a = 0 := -have h₁ : a ≤ 0, from h ▸ le_abs_self a, -have h₂ : -a ≤ 0, from h ▸ abs_neg a ▸ le_abs_self (-a), -le_antisymm h₁ (nonneg_of_neg_nonpos h₂) - -lemma eq_of_abs_sub_eq_zero {a b : α} (h : abs (a - b) = 0) : a = b := -have a - b = 0, from eq_zero_of_abs_eq_zero h, -show a = b, from eq_of_sub_eq_zero this - -lemma abs_pos_of_ne_zero {a : α} (h : a ≠ 0) : abs a > 0 := -or.elim (lt_or_gt_of_ne h) abs_pos_of_neg abs_pos_of_pos - -lemma abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (abs a) := -or.elim (le_total 0 a) - (assume h : 0 ≤ a, eq.symm (abs_of_nonneg h) ▸ h1) - (assume h : a ≤ 0, eq.symm (abs_of_nonpos h) ▸ h2) - -lemma abs_le_of_le_of_neg_le {a b : α} (h1 : a ≤ b) (h2 : -a ≤ b) : abs a ≤ b := -abs_by_cases (λ x : α, x ≤ b) h1 h2 - -lemma abs_lt_of_lt_of_neg_lt {a b : α} (h1 : a < b) (h2 : -a < b) : abs a < b := -abs_by_cases (λ x : α, x < b) h1 h2 - -private lemma aux1 {a b : α} (h1 : a + b ≥ 0) (h2 : a ≥ 0) : abs (a + b) ≤ abs a + abs b := -decidable.by_cases - (assume h3 : b ≥ 0, calc - abs (a + b) ≤ abs (a + b) : by apply le_refl - ... = a + b : by rw (abs_of_nonneg h1) - ... = abs a + b : by rw (abs_of_nonneg h2) - ... = abs a + abs b : by rw (abs_of_nonneg h3)) - (assume h3 : ¬ b ≥ 0, - have h4 : b ≤ 0, from le_of_lt (lt_of_not_ge h3), - calc - abs (a + b) = a + b : by rw (abs_of_nonneg h1) - ... = abs a + b : by rw (abs_of_nonneg h2) - ... ≤ abs a + 0 : add_le_add_left h4 _ - ... ≤ abs a + -b : add_le_add_left (neg_nonneg_of_nonpos h4) _ - ... = abs a + abs b : by rw (abs_of_nonpos h4)) - -private lemma aux2 {a b : α} (h1 : a + b ≥ 0) : abs (a + b) ≤ abs a + abs b := -or.elim (le_total b 0) - (assume h2 : b ≤ 0, - have h3 : ¬ a < 0, from - assume h4 : a < 0, - have h5 : a + b < 0, - begin - have aux := add_lt_add_of_lt_of_le h4 h2, - rwa [add_zero] at aux - end, - not_lt_of_ge h1 h5, - aux1 h1 (le_of_not_gt h3)) - (assume h2 : 0 ≤ b, - begin - have h3 : abs (b + a) ≤ abs b + abs a, - begin - rw add_comm at h1, - exact aux1 h1 h2 - end, - rw [add_comm, add_comm (abs a)], - exact h3 - end) - -lemma abs_add_le_abs_add_abs (a b : α) : abs (a + b) ≤ abs a + abs b := -or.elim (le_total 0 (a + b)) - (assume h2 : 0 ≤ a + b, aux2 h2) - (assume h2 : a + b ≤ 0, - have h3 : -a + -b = -(a + b), by rw neg_add, - have h4 : -(a + b) ≥ 0, from neg_nonneg_of_nonpos h2, - have h5 : -a + -b ≥ 0, begin rw [← h3] at h4, exact h4 end, - calc - abs (a + b) = abs (-a + -b) : by rw [← abs_neg, neg_add] - ... ≤ abs (-a) + abs (-b) : aux2 h5 - ... = abs a + abs b : by rw [abs_neg, abs_neg]) - -lemma abs_sub_abs_le_abs_sub (a b : α) : abs a - abs b ≤ abs (a - b) := -have h1 : abs a - abs b + abs b ≤ abs (a - b) + abs b, from -calc - abs a - abs b + abs b = abs a : by rw sub_add_cancel - ... = abs (a - b + b) : by rw sub_add_cancel - ... ≤ abs (a - b) + abs b : by apply abs_add_le_abs_add_abs, -le_of_add_le_add_right h1 - -lemma abs_sub_le (a b c : α) : abs (a - c) ≤ abs (a - b) + abs (b - c) := -calc - abs (a - c) = abs (a - b + (b - c)) : by rw [sub_eq_add_neg, sub_eq_add_neg, sub_eq_add_neg, - add_assoc, neg_add_cancel_left] - ... ≤ abs (a - b) + abs (b - c) : by apply abs_add_le_abs_add_abs - -lemma abs_add_three (a b c : α) : abs (a + b + c) ≤ abs a + abs b + abs c := -begin - apply le_trans, - apply abs_add_le_abs_add_abs, - apply le_trans, - apply add_le_add_right, - apply abs_add_le_abs_add_abs, - apply le_refl -end - -lemma dist_bdd_within_interval {a b lb ub : α} (h : lb < ub) (hal : lb ≤ a) (hau : a ≤ ub) - (hbl : lb ≤ b) (hbu : b ≤ ub) : abs (a - b) ≤ ub - lb := -begin - cases (decidable.em (b ≤ a)) with hba hba, - rw (abs_of_nonneg (sub_nonneg_of_le hba)), - apply sub_le_sub, - apply hau, - apply hbl, - rw [abs_of_neg (sub_neg_of_lt (lt_of_not_ge hba)), neg_sub], - apply sub_le_sub, - apply hbu, - apply hal -end - -end decidable_linear_ordered_comm_group - - -section decidable_linear_ordered_comm_ring -variables {α : Type u} [decidable_linear_ordered_comm_ring α] - -lemma abs_mul (a b : α) : abs (a * b) = abs a * abs b := -or.elim (le_total 0 a) - (assume h1 : 0 ≤ a, - or.elim (le_total 0 b) - (assume h2 : 0 ≤ b, - calc - abs (a * b) = a * b : abs_of_nonneg (mul_nonneg h1 h2) - ... = abs a * b : by rw (abs_of_nonneg h1) - ... = abs a * abs b : by rw (abs_of_nonneg h2)) - (assume h2 : b ≤ 0, - calc - abs (a * b) = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonneg_of_nonpos h1 h2) - ... = a * -b : by rw neg_mul_eq_mul_neg - ... = abs a * -b : by rw (abs_of_nonneg h1) - ... = abs a * abs b : by rw (abs_of_nonpos h2))) - (assume h1 : a ≤ 0, - or.elim (le_total 0 b) - (assume h2 : 0 ≤ b, - calc - abs (a * b) = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonpos_of_nonneg h1 h2) - ... = -a * b : by rw neg_mul_eq_neg_mul - ... = abs a * b : by rw (abs_of_nonpos h1) - ... = abs a * abs b : by rw (abs_of_nonneg h2)) - (assume h2 : b ≤ 0, - calc - abs (a * b) = a * b : abs_of_nonneg (mul_nonneg_of_nonpos_of_nonpos h1 h2) - ... = -a * -b : by rw neg_mul_neg - ... = abs a * -b : by rw (abs_of_nonpos h1) - ... = abs a * abs b : by rw (abs_of_nonpos h2))) - - -lemma abs_mul_abs_self (a : α) : abs a * abs a = a * a := -abs_by_cases (λ x, x * x = a * a) rfl (neg_mul_neg a a) - -lemma abs_mul_self (a : α) : abs (a * a) = a * a := -by rw [abs_mul, abs_mul_abs_self] - -lemma sub_le_of_abs_sub_le_left {a b c : α} (h : abs (a - b) ≤ c) : b - c ≤ a := -if hz : 0 ≤ a - b then - (calc - a ≥ b : le_of_sub_nonneg hz - ... ≥ b - c : sub_le_self _ (le_trans (abs_nonneg _) h)) -else - have habs : b - a ≤ c, by rwa [abs_of_neg (lt_of_not_ge hz), neg_sub] at h, - have habs' : b ≤ c + a, from le_add_of_sub_right_le habs, - sub_left_le_of_le_add habs' - -lemma sub_le_of_abs_sub_le_right {a b c : α} (h : abs (a - b) ≤ c) : a - c ≤ b := -sub_le_of_abs_sub_le_left (abs_sub a b ▸ h) - -lemma sub_lt_of_abs_sub_lt_left {a b c : α} (h : abs (a - b) < c) : b - c < a := -if hz : 0 ≤ a - b then - (calc - a ≥ b : le_of_sub_nonneg hz - ... > b - c : sub_lt_self _ (lt_of_le_of_lt (abs_nonneg _) h)) -else - have habs : b - a < c, by rwa [abs_of_neg (lt_of_not_ge hz), neg_sub] at h, - have habs' : b < c + a, from lt_add_of_sub_right_lt habs, - sub_left_lt_of_lt_add habs' - - -lemma sub_lt_of_abs_sub_lt_right {a b c : α} (h : abs (a - b) < c) : a - c < b := -sub_lt_of_abs_sub_lt_left (abs_sub a b ▸ h) - -lemma abs_sub_square (a b : α) : abs (a - b) * abs (a - b) = a * a + b * b - (1 + 1) * a * b := -begin - rw abs_mul_abs_self, - simp [left_distrib, right_distrib, add_assoc, add_comm, add_left_comm, mul_comm] -end - -lemma eq_zero_of_mul_self_add_mul_self_eq_zero {x y : α} (h : x * x + y * y = 0) : x = 0 := -have x * x ≤ (0 : α), from calc - x * x ≤ x * x + y * y : le_add_of_nonneg_right (mul_self_nonneg y) - ... = 0 : h, -eq_zero_of_mul_self_eq_zero (le_antisymm this (mul_self_nonneg x)) - -lemma abs_abs_sub_abs_le_abs_sub (a b : α) : abs (abs a - abs b) ≤ abs (a - b) := -begin - apply nonneg_le_nonneg_of_squares_le, - apply abs_nonneg, - iterate {rw abs_sub_square}, - iterate {rw abs_mul_abs_self}, - apply sub_le_sub_left, - iterate {rw mul_assoc}, - apply mul_le_mul_of_nonneg_left, - rw [← abs_mul], - apply le_abs_self, - apply le_of_lt, - apply add_pos, - apply zero_lt_one, - apply zero_lt_one -end - -end decidable_linear_ordered_comm_ring - -section discrete_linear_ordered_field -variables {α : Type u} [discrete_linear_ordered_field α] - -lemma abs_div (a b : α) : abs (a / b) = abs a / abs b := -decidable.by_cases - (assume h : b = 0, by rw [h, abs_zero, div_zero, div_zero, abs_zero]) - (assume h : b ≠ 0, - have h₁ : abs b ≠ 0, from - assume h₂, h (eq_zero_of_abs_eq_zero h₂), - eq_div_of_mul_eq _ _ h₁ - (show abs (a / b) * abs b = abs a, by rw [← abs_mul, div_mul_cancel _ h])) - -lemma abs_one_div (a : α) : abs (1 / a) = 1 / abs a := -by rw [abs_div, abs_of_nonneg (zero_le_one : 1 ≥ (0 : α))] - -end discrete_linear_ordered_field diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean deleted file mode 100644 index ec15584c03..0000000000 --- a/library/init/algebra/group.lean +++ /dev/null @@ -1,430 +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 - -/- 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_comm mul_assoc mul_left_comm - -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 tt tgt ->> copy_attribute `simp src tt tgt ->> copy_attribute `instance src tt tgt - -/- 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⟩ - -@[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 diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean deleted file mode 100644 index 6d405d3172..0000000000 --- a/library/init/algebra/order.lean +++ /dev/null @@ -1,240 +0,0 @@ -/- -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -prelude -import init.logic init.classical init.meta.name init.algebra.classes -/- 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} - -set_option auto_param.check_exists false -class preorder (α : Type u) extends has_le α, has_lt α := -(le_refl : ∀ a : α, a ≤ a) -(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c) -(lt := λ a b, a ≤ b ∧ ¬ b ≤ a) -(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac) - -class partial_order (α : Type u) extends preorder α := -(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b) - -class linear_order (α : Type u) extends partial_order α := -(le_total : ∀ a b : α, a ≤ b ∨ b ≤ a) - -@[refl] lemma le_refl [preorder α] : ∀ a : α, a ≤ a := -preorder.le_refl - -@[trans] lemma le_trans [preorder α] : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c := -preorder.le_trans - -lemma lt_iff_le_not_le [preorder α] : ∀ {a b : α}, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := -preorder.lt_iff_le_not_le _ - -lemma lt_of_le_not_le [preorder α] : ∀ {a b : α}, a ≤ b → ¬ b ≤ a → a < b -| a b hab hba := lt_iff_le_not_le.mpr ⟨hab, hba⟩ - -lemma le_not_le_of_lt [preorder α] : ∀ {a b : α}, a < b → a ≤ b ∧ ¬ b ≤ a -| a b hab := lt_iff_le_not_le.mp hab - -lemma le_antisymm [partial_order α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b := -partial_order.le_antisymm - -lemma le_of_eq [preorder α] {a b : α} : a = b → a ≤ b := -λ h, h ▸ le_refl a - -lemma le_antisymm_iff [partial_order α] {a b : α} : a = b ↔ a ≤ b ∧ b ≤ a := -⟨λe, ⟨le_of_eq e, le_of_eq e.symm⟩, λ⟨h1, h2⟩, le_antisymm h1 h2⟩ - -@[trans] lemma ge_trans [preorder α] : ∀ {a b c : α}, a ≥ b → b ≥ c → a ≥ c := -λ a b c h₁ h₂, le_trans h₂ h₁ - -lemma le_total [linear_order α] : ∀ a b : α, a ≤ b ∨ b ≤ a := -linear_order.le_total - -lemma le_of_not_ge [linear_order α] {a b : α} : ¬ a ≥ b → a ≤ b := -or.resolve_left (le_total b a) - -lemma le_of_not_le [linear_order α] {a b : α} : ¬ a ≤ b → b ≤ a := -or.resolve_left (le_total a b) - -lemma lt_irrefl [preorder α] : ∀ a : α, ¬ a < a -| a haa := match le_not_le_of_lt haa with - | ⟨h1, h2⟩ := false.rec _ (h2 h1) - end - -lemma gt_irrefl [preorder α] : ∀ a : α, ¬ a > a := -lt_irrefl - -@[trans] lemma lt_trans [preorder α] : ∀ {a b c : α}, a < b → b < c → a < c -| a b c hab hbc := - match le_not_le_of_lt hab, le_not_le_of_lt hbc with - | ⟨hab, hba⟩, ⟨hbc, hcb⟩ := lt_of_le_not_le (le_trans hab hbc) (λ hca, hcb (le_trans hca hab)) - end - -def lt.trans := @lt_trans - -@[trans] lemma gt_trans [preorder α] : ∀ {a b c : α}, a > b → b > c → a > c := -λ a b c h₁ h₂, lt_trans h₂ h₁ - -def gt.trans := @gt_trans - -lemma ne_of_lt [preorder α] {a b : α} (h : a < b) : a ≠ b := -λ he, absurd h (he ▸ lt_irrefl a) - -lemma ne_of_gt [preorder α] {a b : α} (h : a > b) : a ≠ b := -λ he, absurd h (he ▸ lt_irrefl a) - -lemma lt_asymm [preorder α] {a b : α} (h : a < b) : ¬ b < a := -λ h1 : b < a, lt_irrefl a (lt_trans h h1) - -lemma not_lt_of_gt [linear_order α] {a b : α} (h : a > b) : ¬ a < b := -lt_asymm h - -lemma le_of_lt [preorder α] : ∀ {a b : α}, a < b → a ≤ b -| a b hab := (le_not_le_of_lt hab).left - -@[trans] lemma lt_of_lt_of_le [preorder α] : ∀ {a b c : α}, a < b → b ≤ c → a < c -| a b c hab hbc := - let ⟨hab, hba⟩ := le_not_le_of_lt hab in - lt_of_le_not_le (le_trans hab hbc) $ λ hca, hba (le_trans hbc hca) - -@[trans] lemma lt_of_le_of_lt [preorder α] : ∀ {a b c : α}, a ≤ b → b < c → a < c -| a b c hab hbc := - let ⟨hbc, hcb⟩ := le_not_le_of_lt hbc in - lt_of_le_not_le (le_trans hab hbc) $ λ hca, hcb (le_trans hca hab) - -@[trans] lemma gt_of_gt_of_ge [preorder α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c := -lt_of_le_of_lt h₂ h₁ - -@[trans] lemma gt_of_ge_of_gt [preorder α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c := -lt_of_lt_of_le h₂ h₁ - -lemma not_le_of_gt [preorder α] {a b : α} (h : a > b) : ¬ a ≤ b := -(le_not_le_of_lt h).right - -lemma not_lt_of_ge [preorder α] {a b : α} (h : a ≥ b) : ¬ a < b := -λ hab, not_le_of_gt hab h - -lemma lt_or_eq_of_le [partial_order α] : ∀ {a b : α}, a ≤ b → a < b ∨ a = b -| a b hab := classical.by_cases - (λ hba : b ≤ a, or.inr (le_antisymm hab hba)) - (λ hba, or.inl (lt_of_le_not_le hab hba)) - -lemma le_of_lt_or_eq [preorder α] : ∀ {a b : α}, (a < b ∨ a = b) → a ≤ b -| a b (or.inl hab) := le_of_lt hab -| a b (or.inr hab) := hab ▸ le_refl _ - -lemma le_iff_lt_or_eq [partial_order α] : ∀ {a b : α}, a ≤ b ↔ a < b ∨ a = b -| a b := ⟨lt_or_eq_of_le, le_of_lt_or_eq⟩ - -lemma lt_of_le_of_ne [partial_order α] {a b : α} : a ≤ b → a ≠ b → a < b := -λ h₁ h₂, or.resolve_right (lt_or_eq_of_le h₁) h₂ - -lemma lt_trichotomy [linear_order α] (a b : α) : a < b ∨ a = b ∨ b < a := -or.elim (le_total a b) - (λ h : a ≤ b, or.elim (lt_or_eq_of_le h) - (λ h : a < b, or.inl h) - (λ h : a = b, or.inr (or.inl h))) - (λ h : b ≤ a, or.elim (lt_or_eq_of_le h) - (λ h : b < a, or.inr (or.inr h)) - (λ h : b = a, or.inr (or.inl h.symm))) - -lemma le_of_not_gt [linear_order α] {a b : α} (h : ¬ a > b) : a ≤ b := -match lt_trichotomy a b with -| or.inl hlt := le_of_lt hlt -| or.inr (or.inl heq) := heq ▸ le_refl a -| or.inr (or.inr hgt) := absurd hgt h -end - -lemma lt_of_not_ge [linear_order α] {a b : α} (h : ¬ a ≥ b) : a < b := -match lt_trichotomy a b with -| or.inl hlt := hlt -| or.inr (or.inl heq) := absurd (heq ▸ le_refl a : a ≥ b) h -| or.inr (or.inr hgt) := absurd (le_of_lt hgt) h -end - -lemma lt_or_ge [linear_order α] (a b : α) : a < b ∨ a ≥ b := -match lt_trichotomy a b with -| or.inl hlt := or.inl hlt -| or.inr (or.inl heq) := or.inr (heq ▸ le_refl a) -| or.inr (or.inr hgt) := or.inr (le_of_lt hgt) -end - -lemma le_or_gt [linear_order α] (a b : α) : a ≤ b ∨ a > b := -or.swap (lt_or_ge b a) - -lemma lt_or_gt_of_ne [linear_order α] {a b : α} (h : a ≠ b) : a < b ∨ a > b := -match lt_trichotomy a b with -| or.inl hlt := or.inl hlt -| or.inr (or.inl heq) := absurd heq h -| or.inr (or.inr hgt) := or.inr hgt -end - -lemma le_of_eq_or_lt [preorder α] {a b : α} (h : a = b ∨ a < b) : a ≤ b := -or.elim h le_of_eq le_of_lt - -lemma ne_iff_lt_or_gt [linear_order α] {a b : α} : a ≠ b ↔ a < b ∨ a > b := -⟨lt_or_gt_of_ne, λo, or.elim o ne_of_lt ne_of_gt⟩ - -lemma lt_iff_not_ge [linear_order α] (x y : α) : x < y ↔ ¬ x ≥ y := -⟨not_le_of_gt, lt_of_not_ge⟩ - -instance decidable_lt_of_decidable_le [preorder α] - [decidable_rel ((≤) : α → α → Prop)] : - decidable_rel ((<) : α → α → Prop) -| a b := - if hab : a ≤ b then - if hba : b ≤ a then - is_false $ λ hab', not_le_of_gt hab' hba - else - is_true $ lt_of_le_not_le hab hba - else - is_false $ λ hab', hab (le_of_lt hab') - -instance decidable_eq_of_decidable_le [partial_order α] - [decidable_rel ((≤) : α → α → Prop)] : - decidable_eq α -| a b := - if hab : a ≤ b then - if hba : b ≤ a then - is_true (le_antisymm hab hba) - else - is_false (λ heq, hba (heq ▸ le_refl _)) - else - is_false (λ heq, hab (heq ▸ le_refl _)) - -class decidable_linear_order (α : Type u) extends linear_order α := -(decidable_le : decidable_rel (≤)) -(decidable_eq : decidable_eq α := @decidable_eq_of_decidable_le _ _ decidable_le) -(decidable_lt : decidable_rel ((<) : α → α → Prop) := - @decidable_lt_of_decidable_le _ _ decidable_le) - -instance [decidable_linear_order α] (a b : α) : decidable (a < b) := -decidable_linear_order.decidable_lt α a b - -instance [decidable_linear_order α] (a b : α) : decidable (a ≤ b) := -decidable_linear_order.decidable_le α a b - -instance [decidable_linear_order α] (a b : α) : decidable (a = b) := -decidable_linear_order.decidable_eq α a b - -lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a := -if h₁ : a = b then or.inl h₁ -else or.inr (lt_of_not_ge (λ hge, h (lt_of_le_of_ne hge h₁))) - -instance [decidable_linear_order α] : is_total_preorder α (≤) := -{trans := @le_trans _ _, total := le_total} - -/- TODO(Leo): decide whether we should keep this instance or not -/ -instance is_strict_weak_order_of_decidable_linear_order [decidable_linear_order α] : is_strict_weak_order α (<) := -is_strict_weak_order_of_is_total_preorder lt_iff_not_ge - -/- TODO(Leo): decide whether we should keep this instance or not -/ -instance is_strict_total_order_of_decidable_linear_order [decidable_linear_order α] : is_strict_total_order α (<) := -{ trichotomous := lt_trichotomy } diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean deleted file mode 100644 index c1941d7d84..0000000000 --- a/library/init/algebra/ordered_field.lean +++ /dev/null @@ -1,484 +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 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 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 two_pos : (2:α) > 0 := -begin unfold bit0, exact add_pos zero_lt_one zero_lt_one end - -lemma two_ne_zero : (2:α) ≠ 0 := -ne.symm (ne_of_lt two_pos) - -lemma add_halves (a : α) : a / 2 + a / 2 = a := -calc - a / 2 + a / 2 = (a + a) / 2 : by rw div_add_div_same - ... = (a * 1 + a * 1) / 2 : by rw mul_one - ... = (a * (1 + 1)) / 2 : by rw left_distrib - ... = (a * 2) / 2 : by rw one_add_one_eq_two - ... = a : by rw [@mul_div_cancel α _ _ _ 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 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 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 : α} (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b ≤ c / d) - (he : e > 0) : a / (b * e) ≤ c / (d * e) := -begin - have h₁ := field.div_mul_eq_div_mul_one_div a hb (ne_of_gt he), - have h₂ := field.div_mul_eq_div_mul_one_div c hd (ne_of_gt he), - 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 - ... = (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 [← division_ring.one_div_one_div (ne_of_gt ha)], - 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 ← division_ring.one_div_one_div (ne_of_lt this) 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 - -end linear_ordered_field - -class discrete_linear_ordered_field (α : Type u) extends linear_ordered_field α, - decidable_linear_ordered_comm_ring α := -(inv_zero : inv zero = zero) - -section discrete_linear_ordered_field -variables {α : Type u} - -instance discrete_linear_ordered_field.to_discrete_field [s : discrete_linear_ordered_field α] : discrete_field α := -{ has_decidable_eq := @decidable_linear_ordered_comm_ring.decidable_eq α (@discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring α s), - ..s } - -variables [discrete_linear_ordered_field α] - -lemma pos_of_one_div_pos {a : α} (h : 0 < 1 / a) : 0 < a := - have h1 : 0 < 1 / (1 / a), from one_div_pos_of_pos h, - have h2 : 1 / a ≠ 0, from - (assume h3 : 1 / a = 0, - have h4 : 1 / (1 / a) = 0, from eq.symm h3 ▸ div_zero 1, - absurd h4 (ne.symm (ne_of_lt h1))), - (division_ring.one_div_one_div (ne_zero_of_one_div_ne_zero h2)) ▸ h1 - -lemma neg_of_one_div_neg {a : α} (h : 1 / a < 0) : a < 0 := -have h1 : 0 < - (1 / a), from neg_pos_of_neg h, -have ha : a ≠ 0, from ne_zero_of_one_div_ne_zero (ne_of_lt h), -have h2 : 0 < 1 / (-a), from eq.symm (division_ring.one_div_neg_eq_neg_one_div ha) ▸ h1, -have h3 : 0 < -a, from pos_of_one_div_pos h2, -neg_of_neg_pos h3 - -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 discrete_linear_ordered_field diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean deleted file mode 100644 index a684706866..0000000000 --- a/library/init/algebra/ordered_group.lean +++ /dev/null @@ -1,620 +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_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_comm_monoid -variable {α : Type u} -variable [s : ordered_cancel_comm_monoid α] - -lemma add_le_add_left {a b : α} (h : a ≤ b) (c : α) : c + a ≤ c + b := -@ordered_cancel_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_comm_monoid.le_of_add_le_add_left α s a b c h -end ordered_cancel_comm_monoid - -section ordered_cancel_comm_monoid -variable {α : Type u} -variable [ordered_cancel_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_comm_monoid - -class ordered_comm_group (α : Type u) extends add_comm_group α, partial_order α := -(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) -(add_lt_add_left : ∀ a b : α, a < b → ∀ c : α, c + a < c + b) - -section ordered_comm_group -variable {α : Type u} -variable [ordered_comm_group α] - -lemma ordered_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_comm_group.add_le_add_left _ _ h _, -begin simp [neg_add_cancel_left] at this, assumption end - -lemma ordered_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_comm_group.add_lt_add_left _ _ h _, -begin simp [neg_add_cancel_left] at this, assumption end -end ordered_comm_group - -instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) [s : ordered_comm_group α] : ordered_cancel_comm_monoid α := -{ add_left_cancel := @add_left_cancel α _, - add_right_cancel := @add_right_cancel α _, - le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left α _, - ..s } - -section ordered_comm_group -variables {α : Type u} [ordered_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_comm_group - -class decidable_linear_ordered_comm_group (α : Type u) - extends add_comm_group α, decidable_linear_order α := -(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b) -(add_lt_add_left : ∀ a b : α, a < b → ∀ c : α, c + a < c + b) - -instance decidable_linear_ordered_comm_group.to_ordered_comm_group (α : Type u) - [s : decidable_linear_ordered_comm_group α] : ordered_comm_group α := -{ add := s.add, ..s } - -class decidable_linear_ordered_cancel_comm_monoid (α : Type u) - extends ordered_cancel_comm_monoid α, decidable_linear_order α diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean deleted file mode 100644 index 8d5de60171..0000000000 --- a/library/init/algebra/ordered_ring.lean +++ /dev/null @@ -1,384 +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_comm_monoid α := -(mul_le_mul_of_nonneg_left: ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b) -(mul_le_mul_of_nonneg_right: ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c) -(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) - -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 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_comm_group α, zero_ne_one_class α := -(mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) -(mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b) - -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_le_mul_of_nonneg_left := @ordered_ring.mul_le_mul_of_nonneg_left α _, - mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right α _, - 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_le_mul_of_nonneg_left := @mul_le_mul_of_nonneg_left α _, - mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right α _, - 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_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_le_mul_of_nonneg_left := @linear_ordered_semiring.mul_le_mul_of_nonneg_left α s, - mul_le_mul_of_nonneg_right := @linear_ordered_semiring.mul_le_mul_of_nonneg_right α 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 0049623031..0000000000 --- a/library/init/algebra/ring.lean +++ /dev/null @@ -1,332 +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 α - -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 diff --git a/library/init/data/ordering/lemmas.lean b/library/init/data/ordering/lemmas.lean index f227b5ef43..292b3a07b2 100644 --- a/library/init/data/ordering/lemmas.lean +++ b/library/init/data/ordering/lemmas.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.data.ordering.basic init.meta init.algebra.classes init.ite_simp +import init.data.ordering.basic init.meta init.ite_simp set_option default_priority 100 universes u @@ -30,12 +30,14 @@ local attribute [simp] cmp_using @[simp] lemma cmp_using_eq_lt (a b : α) : (cmp_using lt a b = ordering.lt) = lt a b := by simp +/- @[simp] lemma cmp_using_eq_gt [is_strict_order α lt] (a b : α) : (cmp_using lt a b = ordering.gt) = lt b a := begin simp, apply propext, apply iff.intro, { exact λ h, h.2 }, { intro hba, split, { intro hab, exact absurd (trans hab hba) (irrefl a) }, { assumption } } end +-/ @[simp] lemma cmp_using_eq_eq (a b : α) : (cmp_using lt a b = ordering.eq) = (¬ lt a b ∧ ¬ lt b a) := by simp diff --git a/library/init/default.lean b/library/init/default.lean index 4c3cbead5c..13d326eb78 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.core init.logic init.category init.data.basic init.version import init.propext init.funext init.category.combinators init.function init.classical -import init.util init.coe init.wf init.meta init.meta.well_founded_tactics init.algebra init.data +import init.util init.coe init.wf init.meta init.meta.well_founded_tactics init.data @[user_attribute] meta def debugger.attr : user_attribute :=