refactor(algebra/quadratic_discriminant): drop linearity condition; cleanup (#4656)

Renames:

- `discriminant_le_zero` to `discrim_le_zero`
- `discriminant_lt_zero` to `discrim_lt_zero`

Author: jcommelin

src/algebra/ordered_ring.lean

@@ -343,6 +343,25 @@ lt_of_not_ge (λ ha, absurd h (mul_nonpos_of_nonneg_of_nonpos ha hb).not_lt)
 lemma neg_of_mul_pos_right (h : 0 < a * b) (ha : a ≤ 0) : b < 0 :=
 lt_of_not_ge (λ hb, absurd h (mul_nonpos_of_nonpos_of_nonneg ha hb).not_lt)
 
+lemma exists_lt_mul_self (a : α) : ∃ x : α, a < x * x :=
+begin
+  by_cases ha : 0 ≤ a,
+  { use (a + 1),
+    calc a = a * 1 : by rw mul_one
+    ... < (a + 1) * (a + 1) : mul_lt_mul (lt_add_one _) (le_add_of_nonneg_left ha)
+                                         zero_lt_one (add_nonneg ha zero_le_one) },
+  { rw not_le at ha,
+    use 1,
+    calc a < 0     : ha
+       ... < 1 * 1 : by simpa only [mul_one] using zero_lt_one }
+end
+
+lemma exists_le_mul_self (a : α) : ∃ x : α, a ≤ x * x :=
+begin
+  obtain ⟨x, hx⟩ := exists_lt_mul_self a,
+  exact ⟨x, le_of_lt hx⟩
+end
+
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_semiring.to_nontrivial {α : Type*} [linear_ordered_semiring α] :
   nontrivial α :=

src/algebra/quadratic_discriminant.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou
 -/
+import algebra.invertible
 import tactic.linarith
 
 /-!
@@ -12,78 +13,71 @@ This file defines the discriminant of a quadratic and gives the solution to a qu
 
 ## Main definition
 
-The discriminant of a quadratic `a*x*x + b*x + c` is `b*b - 4*a*c`.
+- `discrim a b c`: the discriminant of a quadratic `a * x * x + b * x + c` is `b * b - 4 * a * c`.
 
 ## Main statements
-• Roots of a quadratic can be written as `(-b + s) / (2 * a)` or `(-b - s) / (2 * a)`,
-  where `s` is the square root of the discriminant.
-• If the discriminant has no square root, then the corresponding quadratic has no root.
-• If a quadratic is always non-negative, then its discriminant is non-positive.
+
+- `quadratic_eq_zero_iff`: roots of a quadratic can be written as
+  `(-b + s) / (2 * a)` or `(-b - s) / (2 * a)`, where `s` is the square root of the discriminant.
+- `quadratic_ne_zero_of_discrim_ne_square`: if the discriminant has no square root,
+  then the corresponding quadratic has no root.
+- `discrim_le_zero`: if a quadratic is always non-negative, then its discriminant is non-positive.
 
 ## Tags
 
 polynomial, quadratic, discriminant, root
 -/
 
-variables {α : Type*}
+section ring
+variables {R : Type*}
 
-section lemmas
+/-- Discriminant of a quadratic -/
+def discrim [ring R] (a b c : R) : R := b^2 - 4 * a * c
 
-variables [linear_ordered_field α] {a b c : α}
+variables [integral_domain R] {a b c : R}
 
-lemma exists_le_mul_self : ∀ a : α, ∃ x : α, a ≤ x * x :=
+/--
+A quadratic has roots if and only if its discriminant equals some square.
+-/
+lemma quadratic_eq_zero_iff_discrim_eq_square (h2 : (2 : R) ≠ 0) (ha : a ≠ 0) (x : R) :
+  a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2 :=
 begin
-  classical, -- TODO: otherwise linarith performance sucks
-  assume a, cases le_total 1 a with ha ha,
-  { use a, exact le_mul_of_one_le_left (by linarith) ha },
-  { use 1, linarith }
+  split,
+  { assume h,
+    calc discrim a b c
+        = 4 * a * (a * x * x + b * x + c) + b * b - 4 * a * c : by { rw [h, discrim], ring }
+    ... = (2*a*x + b)^2 : by ring },
+  { assume h,
+    have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero h2 h2) ha,
+    apply mul_left_cancel' ha,
+    calc
+      2 * 2 * a * (a * x * x + b * x + c) = (2 * a * x + b) ^ 2 - (b ^ 2 - 4 * a * c) : by ring
+      ... = 0 : by { rw [← h, discrim], ring }
+      ... = 2*2*a*0 : by ring }
 end
 
-lemma exists_lt_mul_self : ∀ a : α, ∃ x : α, a < x * x :=
+/-- A quadratic has no root if its discriminant has no square root. -/
+lemma quadratic_ne_zero_of_discrim_ne_square (h2 : (2 : R) ≠ 0) (ha : a ≠ 0)
+  (h : ∀ s : R, discrim a b c ≠ s * s) (x : R) :
+  a * x * x + b * x + c ≠ 0 :=
 begin
-  classical, -- todo: otherwise linarith performance sucks
-  assume a, rcases (exists_le_mul_self a) with ⟨x, hx⟩,
-  cases le_total 0 x with hx' hx',
-  { use (x + 1),
-    have : (x+1)*(x+1) = x*x + 2*x + 1, {ring},
-    exact lt_of_le_of_lt hx (by rw this; linarith) },
-  { use (x - 1),
-    have : (x-1)*(x-1) = x*x - 2*x + 1, {ring},
-    exact lt_of_le_of_lt hx (by rw this; linarith) }
+  assume h',
+  rw [quadratic_eq_zero_iff_discrim_eq_square h2 ha, pow_two] at h',
+  exact h _ h'
 end
 
-end lemmas
-
-variables [linear_ordered_field α] {a b c x : α}
-
-/-- Discriminant of a quadratic -/
-def discrim [ring α] (a b c : α) : α := b^2 - 4 * a * c
+end ring
 
-/--
-A quadratic has roots if and only if its discriminant equals some square.
--/
-lemma quadratic_eq_zero_iff_discrim_eq_square (ha : a ≠ 0) :
-  ∀ x : α, a * x * x + b * x + c = 0 ↔  discrim a b c = (2 * a * x + b)^2 :=
-by classical; exact -- TODO: otherwise linarith performance sucks
-assume x, iff.intro
-  (assume h, calc
-      discrim a b c = 4*a*(a*x*x + b*x + c) + b*b - 4*a*c : by rw [h, discrim]; ring
-      ... = (2*a*x + b)^2 : by ring)
-  (assume h,
-    have ha : 2*2*a ≠ 0 := mul_ne_zero (mul_ne_zero two_ne_zero two_ne_zero) ha,
-    mul_left_cancel' ha $
-    calc
-      2 * 2 * a * (a * x * x + b * x + c) = (2*a*x + b)^2 - (b^2 - 4*a*c) : by ring
-      ... = 0 : by { rw [← h, discrim], ring }
-      ... = 2*2*a*0 : by ring)
+section field
+variables {K : Type*} [field K] [invertible (2 : K)] {a b c x : K}
 
 /-- Roots of a quadratic -/
-lemma quadratic_eq_zero_iff (ha : a ≠ 0) {s : α} (h : discrim a b c = s * s) :
-  ∀ x : α, a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) := assume x,
+lemma quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :
+  a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) :=
 begin
-  classical, -- TODO: otherwise linarith performance sucks
-  rw [quadratic_eq_zero_iff_discrim_eq_square ha, h, pow_two, mul_self_eq_mul_self_iff],
-  have ne : 2 * a ≠ 0 := mul_ne_zero two_ne_zero ha,
+  have h2 : (2 : K) ≠ 0 := nonzero_of_invertible 2,
+  rw [quadratic_eq_zero_iff_discrim_eq_square h2 ha, h, pow_two, mul_self_eq_mul_self_iff],
+  have ne : 2 * a ≠ 0 := mul_ne_zero h2 ha,
   have : x = 2 * a * x / (2 * a) := (mul_div_cancel_left x ne).symm,
   have h₁ : 2 * a * ((-b + s) / (2 * a)) = -b + s := mul_div_cancel' _ ne,
   have h₂ : 2 * a * ((-b - s) / (2 * a)) = -b - s := mul_div_cancel' _ ne,
@@ -95,7 +89,7 @@ begin
 end
 
 /-- A quadratic has roots if its discriminant has square roots -/
-lemma exist_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) :
+lemma exists_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) :
   ∃ x, a * x * x + b * x + c = 0 :=
 begin
   rcases h with ⟨s, hs⟩,
@@ -105,79 +99,70 @@ begin
 end
 
 /-- Root of a quadratic when its discriminant equals zero -/
-lemma quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) :
-  ∀ x : α, a * x * x + b * x + c = 0 ↔ x = -b / (2 * a) := assume x,
+lemma quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) (x : K) :
+  a * x * x + b * x + c = 0 ↔ x = -b / (2 * a) :=
 begin
-  classical, -- TODO: otherwise linarith performance sucks
-  have : discrim a b c = 0 * 0 := eq.trans h (by ring),
-  rw quadratic_eq_zero_iff ha this,
-  simp
+  have : discrim a b c = 0 * 0, by rw [h, mul_zero],
+  rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self]
 end
 
-/-- A quadratic has no root if its discriminant has no square root. -/
-lemma quadratic_ne_zero_of_discrim_ne_square (ha : a ≠ 0) (h : ∀ s : α, discrim a b c ≠ s * s) :
-  ∀ (x : α), a * x * x + b * x + c ≠ 0 :=
-begin
-  assume x h',
-  rw [quadratic_eq_zero_iff_discrim_eq_square ha, pow_two] at h',
-  have := h _,
-  contradiction
-end
+end field
+
+section linear_ordered_field
+variables {K : Type*} [linear_ordered_field K] {a b c : K}
 
 /-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
-lemma discriminant_le_zero {a b c : α} (h : ∀ x : α,  0 ≤ a*x*x + b*x + c) : discrim a b c ≤ 0 :=
-by classical; exact -- TODO: otherwise linarith performance sucks
+lemma discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a b c ≤ 0 :=
 have hc : 0 ≤ c, by { have := h 0, linarith },
 begin
   rw [discrim, pow_two],
-  cases lt_trichotomy a 0 with ha ha,
+  obtain ha|rfl|ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0,
   -- if a < 0
-  by_cases hb : b = 0,
-  { rw hb at *,
-    rcases exists_lt_mul_self (-c/a) with ⟨x, hx⟩,
-    have := mul_lt_mul_of_neg_left hx ha,
-    rw [mul_div_cancel' _ (ne_of_lt ha), ← mul_assoc] at this,
-    have h₂ := h x, linarith },
-  { by_cases hc' : c = 0,
-    { rw hc' at *,
-      have : -(a*-b*-b + b*-b + 0) = (1-a)*(b*b), {ring},
-      have h := h (-b), rw [← neg_nonpos, this] at h,
-      have : b * b ≤ 0 := nonpos_of_mul_nonpos_left h (by linarith),
-      linarith },
-    { have h := h (-c/b),
-      have : a*(-c/b)*(-c/b) + b*(-c/b) + c = a*((c/b)*(c/b)),
-      { rw mul_div_cancel' _ hb, ring },
-      rw this at h,
-      have : 0 ≤ a := nonneg_of_mul_nonneg_right h (mul_self_pos $ div_ne_zero hc' hb),
-      linarith [ha] } },
-  cases ha with ha ha,
+  { by_cases hb : b = 0,
+    { rw hb at *,
+      rcases exists_lt_mul_self (-c / a) with ⟨x, hx⟩,
+      have := mul_lt_mul_of_neg_left hx ha,
+      rw [mul_div_cancel' _ (ne_of_lt ha), ← mul_assoc] at this,
+      have h₂ := h x, linarith },
+    { by_cases hc' : c = 0,
+      { rw hc' at *,
+        have : -(a * -b * -b + b * -b + 0) = (1 - a) * (b * b), {ring},
+        have h := h (-b), rw [← neg_nonpos, this] at h,
+        have : b * b ≤ 0 := nonpos_of_mul_nonpos_left h (by linarith),
+        linarith },
+      { have h := h (-c / b),
+        have : a * (-c / b) * (-c / b) + b * (-c / b) + c = a * ((c / b) * (c / b)),
+        { rw mul_div_cancel' _ hb, ring },
+        rw this at h,
+        have : 0 ≤ a := nonneg_of_mul_nonneg_right h (mul_self_pos $ div_ne_zero hc' hb),
+        linarith [ha] } } },
   -- if a = 0
-  by_cases hb : b = 0,
-    { rw [ha, hb], linarith },
-    { have := h ((-c-1)/b), rw [ha, mul_div_cancel' _ hb] at this, linarith },
+  { by_cases hb : b = 0,
+    { rw [hb], linarith },
+    { have := h ((-c - 1) / b), rw [mul_div_cancel' _ hb] at this, linarith } },
   -- if a > 0
-  have := calc
-    4*a* (a*(-(b/a)*(1/2))*(-(b/a)*(1/2)) + b*(-(b/a)*(1/2)) + c)
-      = (a*(b/a)) * (a*(b/a)) - 2*(a*(b/a))*b + 4*a*c : by ring
-    ... = -(b*b - 4*a*c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
-  have ha' : 0 ≤ 4*a, {linarith},
-  have h := (mul_nonneg ha' (h (-(b/a) * (1/2)))),
-  rw this at h, rwa ← neg_nonneg
+  { have := calc
+      4 * a * (a * (-(b / a) * (1 / 2)) * (-(b / a) * (1 / 2)) + b * (-(b / a) * (1 / 2)) + c)
+          = (a * (b / a)) * (a * (b / a)) - 2 * (a * (b / a)) * b + 4 * a * c : by ring
+      ... = -(b * b - 4 * a * c) : by { simp only [mul_div_cancel' b (ne_of_gt ha)], ring },
+    have ha' : 0 ≤ 4 * a, by linarith,
+    have h := (mul_nonneg ha' (h (-(b / a) * (1 / 2)))),
+    rw this at h, rwa ← neg_nonneg }
 end
 
 /--
 If a polynomial of degree 2 is always positive, then its discriminant is negative,
 at least when the coefficient of the quadratic term is nonzero.
 -/
-lemma discriminant_lt_zero {a b c : α} (ha : a ≠ 0) (h : ∀ x : α,  0 < a*x*x + b*x + c) :
-  discrim a b c < 0 :=
+lemma discrim_lt_zero (ha : a ≠ 0) (h : ∀ x : K, 0 < a * x * x + b * x + c) : discrim a b c < 0 :=
 begin
-  classical, -- TODO: otherwise linarith performance sucks
-  have : ∀ x : α, 0 ≤ a*x*x + b*x + c := assume x, le_of_lt (h x),
-  refine lt_of_le_of_ne (discriminant_le_zero this) _,
+  have : ∀ x : K, 0 ≤ a*x*x + b*x + c := assume x, le_of_lt (h x),
+  refine lt_of_le_of_ne (discrim_le_zero this) _,
   assume h',
   have := h (-b / (2 * a)),
   have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0,
   { rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))] },
   linarith
 end
+
+end linear_ordered_field