From c8f7dd384b6037b945d75301dc7a35ffe34cadc3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Nov 2016 14:40:03 -0800 Subject: [PATCH] fix(library/init): implicit arguments --- library/init/ordered_group.lean | 75 +++++++++++++++++++++++++++++---- library/init/ordered_ring.lean | 3 +- library/init/ring.lean | 3 +- 3 files changed, 71 insertions(+), 10 deletions(-) diff --git a/library/init/ordered_group.lean b/library/init/ordered_group.lean index 8213199821..2d4e0dc5c3 100644 --- a/library/init/ordered_group.lean +++ b/library/init/ordered_group.lean @@ -7,7 +7,6 @@ prelude import init.group universe variable u -variable α : Type u class ordered_mul_cancel_comm_monoid (α : Type u) extends comm_monoid α, left_cancel_semigroup α, @@ -37,7 +36,8 @@ instance order_pair_of_ordered_cancel_comm_monoid @ordered_mul_cancel_comm_monoid.to_order_pair α s section -variables [s : 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_mul_cancel_comm_monoid.mul_le_mul_left α s a b h c @@ -52,6 +52,62 @@ lemma lt_of_add_lt_add_left {a b c : α} (h : a + b < a + c) : b < c := @ordered_mul_cancel_comm_monoid.lt_of_mul_lt_mul_left α s a b c h end +section +variable {α : Type u} +variable [ordered_cancel_comm_monoid α] + +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, +begin + rw add_zero at this, + assumption +end + +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, +begin + rw zero_add at this, + assumption +end + +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, +begin rw [add_zero] at this, assumption end + +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, +begin rw [zero_add] at this, assumption end + +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) +end + class ordered_mul_comm_group (α : Type u) extends comm_group α, order_pair α := (mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) (mul_lt_mul_left : ∀ a b : α, a < b → ∀ c : α, c * a < c * b) @@ -62,24 +118,27 @@ ordered_mul_comm_group instance add_comm_group_of_ordered_comm_group (α : Type u) [s : ordered_comm_group α] : add_comm_group α := @ordered_mul_comm_group.to_comm_group α s -lemma ordered_mul_comm_group.le_of_mul_le_mul_left [s : ordered_mul_comm_group α] {a b c : α} - (h : a * b ≤ a * c) : b ≤ c := +section +variable {α : Type u} +variable [ordered_mul_comm_group α] + +lemma ordered_mul_comm_group.le_of_mul_le_mul_left {a b c : α} (h : a * b ≤ a * c) : b ≤ c := have a⁻¹ * (a * b) ≤ a⁻¹ * (a * c), from ordered_mul_comm_group.mul_le_mul_left _ _ h _, begin simp [inv_mul_cancel_left] at this, assumption end -lemma ordered_mul_comm_group.lt_of_mul_lt_mul_left [s : ordered_mul_comm_group α] {a b c : α} - (h : a * b < a * c) : b < c := +lemma ordered_mul_comm_group.lt_of_mul_lt_mul_left {a b c : α} (h : a * b < a * c) : b < c := have a⁻¹ * (a * b) < a⁻¹ * (a * c), from ordered_mul_comm_group.mul_lt_mul_left _ _ h _, begin simp [inv_mul_cancel_left] at this, assumption end +end -instance ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid [s : ordered_mul_comm_group α] : ordered_mul_cancel_comm_monoid α := +instance ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid (α : Type u) [s : ordered_mul_comm_group α] : ordered_mul_cancel_comm_monoid α := { s with mul_left_cancel := @mul_left_cancel α _, mul_right_cancel := @mul_right_cancel α _, le_of_mul_le_mul_left := @ordered_mul_comm_group.le_of_mul_le_mul_left α _, lt_of_mul_lt_mul_left := @ordered_mul_comm_group.lt_of_mul_lt_mul_left α _ } -instance ordered_comm_group.to_ordered_cancel_comm_monoid [s : ordered_comm_group α] : ordered_cancel_comm_monoid α := +instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) [s : ordered_comm_group α] : ordered_cancel_comm_monoid α := @ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid α s class decidable_linear_ordered_mul_comm_group (α : Type u) diff --git a/library/init/ordered_ring.lean b/library/init/ordered_ring.lean index 90395db38e..6b53c5d348 100644 --- a/library/init/ordered_ring.lean +++ b/library/init/ordered_ring.lean @@ -7,7 +7,6 @@ prelude import init.ordered_group init.ring universe variable u -variable α : Type u structure ordered_semiring (α : Type u) extends semiring α, ordered_mul_cancel_comm_monoid α renaming @@ -25,6 +24,8 @@ structure ordered_semiring (α : Type u) ordered_semiring.to_ordered_mul_cancel_comm_monoid to be an instance -/ attribute [class] ordered_semiring +variable {α : Type u} + instance add_comm_group_of_ordered_semiring (α : Type u) [s : ordered_semiring α] : semiring α := @ordered_semiring.to_semiring α s diff --git a/library/init/ring.lean b/library/init/ring.lean index fd7938cbec..12aee72050 100644 --- a/library/init/ring.lean +++ b/library/init/ring.lean @@ -7,12 +7,13 @@ prelude import init.group universe variable u -variable α : Type 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