chore(*): remove algebra
This commit is contained in:
Leonardo de Moura
parent
7aaac31e35
commit
0bcf5c8f5d
12 changed files with 4 additions and 3736 deletions
|
|
@ -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 _)
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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 }
|
||||
|
|
@ -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
|
||||
|
|
@ -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 α
|
||||
|
|
@ -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 }
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue