feat(algebra/order_functions): add simp rules for min/max_eq_left/rig…

…ht (closes #306)

algebra/field_power.lean

@@ -11,57 +11,57 @@ import algebra.group_power tactic.wlog
 universe u
 
 section field_power
-open int nat 
+open int nat
 variables {α : Type u} [division_ring α]
 
 @[simp] lemma zero_gpow : ∀ z : ℕ, z ≠ 0 → (0 : α)^z = 0
-| 0 h := absurd rfl h 
-| (k+1) h := zero_mul _ 
+| 0 h := absurd rfl h
+| (k+1) h := zero_mul _
 
-def fpow (a : α) : ℤ → α 
-| (of_nat n) := a ^ n 
+def fpow (a : α) : ℤ → α
+| (of_nat n) := a ^ n
 | -[1+n] := 1/(a ^ (n+1))
 
 lemma unit_pow {a : α} (ha : a ≠ 0) : ∀ n : ℕ, a ^ n = ↑((units.mk0 a ha)^n)
 | 0 := by simp; refl
-| (k+1) := by simp [_root_.pow_add]; congr; apply unit_pow 
+| (k+1) := by simp [_root_.pow_add]; congr; apply unit_pow
 
 lemma fpow_eq_gpow {a : α} (h : a ≠ 0) : ∀ (z : ℤ), fpow a z = ↑(gpow (units.mk0 a h) z)
-| (of_nat k) := by simp only [fpow, gpow]; apply unit_pow 
-| -[1+k] := by simp [fpow, gpow]; congr; apply unit_pow 
+| (of_nat k) := by simp only [fpow, gpow]; apply unit_pow
+| -[1+k] := by simp [fpow, gpow]; congr; apply unit_pow
 
-lemma fpow_inv (a : α) : fpow a (-1) = a⁻¹ := 
-begin change fpow a -[1+0] = a⁻¹, simp [fpow] end 
+lemma fpow_inv (a : α) : fpow a (-1) = a⁻¹ :=
+begin change fpow a -[1+0] = a⁻¹, simp [fpow] end
 
 lemma fpow_ne_zero_of_ne_zero {a : α} (ha : a ≠ 0) : ∀ (z : ℤ), fpow a z ≠ 0
 | (of_nat n) := pow_ne_zero _ ha
 | -[1+n] := one_div_ne_zero $ pow_ne_zero _ ha
 
 
 @[simp] lemma fpow_zero {a : α} : fpow a 0 = 1 :=
-pow_zero _ 
+pow_zero _
 
-lemma fpow_add {a : α} (ha : a ≠ 0) (z1 z2 : ℤ) : fpow a (z1 + z2) = fpow a z1 * fpow a z2 := 
-begin simp only [fpow_eq_gpow ha], rw ←units.mul_coe, congr, apply gpow_add end 
+lemma fpow_add {a : α} (ha : a ≠ 0) (z1 z2 : ℤ) : fpow a (z1 + z2) = fpow a z1 * fpow a z2 :=
+begin simp only [fpow_eq_gpow ha], rw ←units.mul_coe, congr, apply gpow_add end
 
 end field_power
 
 section discrete_field_power
-open int nat 
+open int nat
 variables {α : Type u} [discrete_field α]
 
 lemma zero_fpow : ∀ z : ℤ, z ≠ 0 → fpow (0 : α) z = 0
 | (of_nat n) h :=
   have h2 : n ≠ 0, from assume : n = 0, by simpa [this] using h,
   by simp [h, h2, fpow]
-| -[1+n] h := 
+| -[1+n] h :=
   have h1 : (0 : α) ^ (n+1) = 0, from zero_mul _,
   by simp [fpow, h1]
 
 end discrete_field_power
 
 section ordered_field_power
-open int 
+open int
 
 variables {α : Type u} [discrete_linear_ordered_field α]
 
@@ -71,15 +71,15 @@ lemma fpow_nonneg_of_nonneg {a : α} (ha : a ≥ 0) : ∀ (z : ℤ), fpow a z 
 
 
 lemma fpow_le_of_le {x : α} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : fpow x a ≤ fpow x b :=
-begin 
+begin
   induction a with a a; induction b with b b,
-  { simp only [fpow], 
-    apply pow_le_pow hx, 
+  { simp only [fpow],
+    apply pow_le_pow hx,
     apply le_of_coe_nat_le_coe_nat h },
-  { apply absurd h, 
+  { apply absurd h,
     apply not_le_of_gt,
     exact lt_of_lt_of_le (neg_succ_lt_zero _) (of_nat_nonneg _) },
-  { simp only [fpow, one_div_eq_inv], 
+  { simp only [fpow, one_div_eq_inv],
     apply le_trans (inv_le_one _); apply one_le_pow_of_one_le hx },
   { simp only [fpow],
     apply (one_div_le_one_div _ _).2,
@@ -90,16 +90,16 @@ begin
     repeat { apply pow_pos (lt_of_lt_of_le zero_lt_one hx) } }
 end
 
-lemma pow_le_max_of_min_le {x : α} (hx : x ≥ 1) {a b c : ℤ} (h : min a b ≤ c) : 
+lemma pow_le_max_of_min_le {x : α} (hx : x ≥ 1) {a b c : ℤ} (h : min a b ≤ c) :
       fpow x (-c) ≤ max (fpow x (-a)) (fpow x (-b)) :=
-begin 
+begin
   wlog hle : a ≤ b,
   have hnle : -b ≤ -a, from neg_le_neg hle,
   have hfle : fpow x (-b) ≤ fpow x (-a), from fpow_le_of_le hx hnle,
-  have : fpow x (-c) ≤ fpow x (-a), 
+  have : fpow x (-c) ≤ fpow x (-a),
   { apply fpow_le_of_le hx,
-    simpa [hle, min_eq_left] using h },
-  simpa [hfle, max_eq_left] using this 
-end 
+    simpa [hle] using h },
+  simpa [hfle] using this
+end
 
-end ordered_field_power 
+end ordered_field_power

algebra/order_functions.lean

@@ -3,13 +3,15 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import algebra.ordered_group order.lattice 
+import algebra.ordered_group order.lattice
 
 open lattice
 
 universes u v
 variables {α : Type u} {β : Type v}
 
+attribute [simp] max_eq_left max_eq_right min_eq_left min_eq_right
+
 section
 variables [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b c d : α}
 
@@ -35,14 +37,14 @@ have a ≤ b → (a ≤ c ∨ b ≤ c ↔ a ≤ c),
   from assume h, or_iff_left_of_imp $ le_trans h,
 have b ≤ a → (a ≤ c ∨ b ≤ c ↔ b ≤ c),
   from assume h, or_iff_right_of_imp $ le_trans h,
-by cases le_total a b; simp [*, min_eq_left, min_eq_right]
+by cases le_total a b; simp *
 
 lemma le_max_iff : a ≤ max b c ↔ a ≤ b ∨ a ≤ c :=
 have b ≤ c → (a ≤ b ∨ a ≤ c ↔ a ≤ c),
   from assume h, or_iff_right_of_imp $ assume h', le_trans h' h,
 have c ≤ b → (a ≤ b ∨ a ≤ c ↔ a ≤ b),
   from assume h, or_iff_left_of_imp $ assume h', le_trans h' h,
-by cases le_total b c; simp [*, max_eq_left, max_eq_right]
+by cases le_total b c; simp *
 
 lemma max_lt_iff : max a b < c ↔ (a < c ∧ b < c) :=
 by rw [lt_iff_not_ge]; simp [(≥), le_max_iff, not_or_distrib]
@@ -66,10 +68,10 @@ theorem max.right_comm (a b c : α) : max (max a b) c = max (max a c) b :=
 right_comm max max_comm max_assoc a b c
 
 lemma max_distrib_of_monotone (hf : monotone f) : f (max a b) = max (f a) (f b) :=
-by cases le_total a b; simp [max_eq_right, max_eq_left, h, hf h]
+by cases le_total a b; simp [h, hf h]
 
 lemma min_distrib_of_monotone (hf : monotone f) : f (min a b) = min (f a) (f b) :=
-by cases le_total a b; simp [min_eq_right, min_eq_left, h, hf h]
+by cases le_total a b; simp [h, hf h]
 
 theorem min_choice (a b : α) : min a b = a ∨ min a b = b :=
 by by_cases h : a ≤ b; simp [min, h]
@@ -78,23 +80,23 @@ theorem max_choice (a b : α) : max a b = a ∨ max a b = b :=
 by by_cases h : a ≤ b; simp [max, h]
 
 lemma le_of_max_le_left {a b c : α} (h : max a b ≤ c) : a ≤ c :=
-le_trans (le_max_left _ _) h 
+le_trans (le_max_left _ _) h
 
 lemma le_of_max_le_right {a b c : α} (h : max a b ≤ c) : b ≤ c :=
-le_trans (le_max_right _ _) h 
+le_trans (le_max_right _ _) h
 
 end
 
-lemma min_add {α : Type u} [decidable_linear_ordered_comm_group α] (a b c : α) : 
+lemma min_add {α : Type u} [decidable_linear_ordered_comm_group α] (a b c : α) :
       min a b + c = min (a + c) (b + c) :=
-if hle : a ≤ b then 
+if hle : a ≤ b then
   have a - c ≤ b - c, from sub_le_sub hle (le_refl _),
-  by simp [*, min_eq_left] at *
-else 
+  by simp * at *
+else
   have b - c ≤ a - c, from sub_le_sub (le_of_lt (lt_of_not_ge hle)) (le_refl _),
-  by simp [*, min_eq_right] at *
+  by simp * at *
 
-lemma min_sub {α : Type u} [decidable_linear_ordered_comm_group α] (a b c : α) : 
+lemma min_sub {α : Type u} [decidable_linear_ordered_comm_group α] (a b c : α) :
       min a b - c = min (a - c) (b - c) :=
 by simp [min_add, sub_eq_add_neg]
 
@@ -145,12 +147,12 @@ abs_le_of_le_of_neg_le
   (by simp [le_max_iff, le_trans (neg_le_neg hab) (neg_le_abs_self a)])
 
 lemma min_le_add_of_nonneg_right {a b : α} (hb : b ≥ 0) : min a b ≤ a + b :=
-calc 
+calc
   min a b ≤ a     : by apply min_le_left
       ... ≤ a + b : le_add_of_nonneg_right hb
 
 lemma min_le_add_of_nonneg_left {a b : α} (ha : a ≥ 0) : min a b ≤ a + b :=
-calc 
+calc
   min a b ≤ b     : by apply min_le_right
       ... ≤ a + b : le_add_of_nonneg_left ha
 

analysis/measure_theory/lebesgue_measure.lean

@@ -182,7 +182,7 @@ le_infi $ λ a, le_infi $ λ b, le_infi $ λ h, begin
     (lebesgue_length_mono $ inter_subset_inter_left _ h)
     (lebesgue_length_mono $ diff_subset_diff_left h)) _,
   cases le_total a c with hac hca; cases le_total b c with hbc hcb;
-    simp [*, max_eq_right, max_eq_left, min_eq_left, min_eq_right, -sub_eq_add_neg, sub_add_sub_cancel'];
+    simp [*, -sub_eq_add_neg, sub_add_sub_cancel'];
     rw [← ennreal.coe_add, ennreal.coe_le_coe],
   { simp [*, nnreal.of_real_add_of_real, -sub_eq_add_neg, sub_add_sub_cancel'] },
   { rw nnreal.of_real_of_nonpos,

computability/partrec_code.lean

@@ -689,7 +689,7 @@ theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n :=
       exact ⟨(max k₁ k₂).succ, nat.le_succ_of_le $
         le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, a,
         evaln_mono (nat.succ_le_succ $ nat.le_succ_of_le $ le_max_left _ _) hk₁,
-        by simpa [nat.succ_eq_add_one, a0] using
+        by simpa [nat.succ_eq_add_one, a0, -max_eq_left, -max_eq_right] using
           evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂⟩ } }
 end, λ ⟨k, h⟩, evaln_sound h⟩
 
@@ -777,7 +777,7 @@ begin
       (snd.comp (primrec.unpair.comp n))
       (hlup.comp $ L.pair $ (k.pair cf).pair z)
       (_ : primrec _),
-    have L := L.comp fst, have z := z.comp fst, have y := snd, 
+    have L := L.comp fst, have z := z.comp fst, have y := snd,
     refine option_bind
       (hlup.comp $ L.pair $
         (((k'.pair c).comp fst).comp fst).pair

data/list/basic.lean

@@ -1903,17 +1903,10 @@ theorem take_prefix (n) (l : list α) : take n l <+: l := ⟨_, take_append_drop
 theorem drop_suffix (n) (l : list α) : drop n l <:+ l := ⟨_, take_append_drop _ _⟩
 
 theorem prefix_iff_eq_append {l₁ l₂ : list α} : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
-⟨λ h, let ⟨r, e⟩ := h in begin
-  rwa append_inj_left ((take_append_drop (length l₁) l₂).trans e.symm) _,
-  simp [min_eq_left, length_le_of_sublist (sublist_of_prefix h)],
-end, λ e, ⟨_, e⟩⟩
+⟨by rintros ⟨r, rfl⟩; simp, λ e, ⟨_, e⟩⟩
 
 theorem suffix_iff_eq_append {l₁ l₂ : list α} : l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ :=
-⟨λ ⟨r, e⟩, begin
-  rwa append_inj_right ((take_append_drop (length l₂ - length l₁) l₂).trans e.symm) _,
-  simp [min_eq_left, nat.sub_le, e.symm],
-  apply nat.add_sub_cancel_left
-end, λ e, ⟨_, e⟩⟩
+⟨by rintros ⟨r, rfl⟩; simp [nat.add_sub_cancel_left], λ e, ⟨_, e⟩⟩
 
 theorem prefix_iff_eq_take {l₁ l₂ : list α} : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
 ⟨λ h, append_right_cancel $