Tips on calculations with Reals

Stream: new members

[Adomas Baliuka]

How would one approach the following? Third grade math, took me forever to do and it's insanely ugly. After getting it to type-check, I tried for 10 more minutes to "golf" it but I regularly break it and have to backtrack...

I guess the main problem is that the tactics don't realize that log 2 and 1 - x are non-zero?

import Mathlib
open Real

lemma move_factor_one_minus {x : ℝ} (h : 1 ≠ x): (1-x) * (1 /(1-x)) = 1 := by
    field_simp
    apply div_self
    exact sub_ne_zero.mpr h

lemma move_factor' {x y z : ℝ} (hy : 0 ≠ y) (hz : z ≠ 0) : (x / y) * (1 / z) = x / (y * z) := by
    field_simp

lemma zero_ne_mul_of_ne_zero  {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : 0 ≠ x * y := by
    simp_all only [ne_eq, zero_eq_mul, or_self, not_false_eq_true]

lemma factor_out_denom (a b x : ℝ) (hx : x ≠ 0) : a / x - b/x = (a - b) / x := by field_simp

lemma the_calculation {x : ℝ} (hx : x ≠ 0) (h2 : x ≠ 1) :
    -1 / (1 - x) / log 2 - x⁻¹ / log 2 = -1 / (x * (1 - x) * log 2) :=
  have zero_ne_one_neg_mul_log2 : 0 ≠ (1 - x) * log 2 := by
    exact zero_ne_mul_of_ne_zero (sub_ne_zero.mpr h2.symm) (by norm_num)
  calc
    _ = -(1 / ((1 - x) * log 2) * (x / x)) - 1 / (x * log 2) := by field_simp
    _ = -(1 / ((1 - x) * log 2) * x * (1 / x)) - 1 / (x * log 2) := by
      simp_all only [ne_eq,log_eq_zero, one_div,mul_inv_rev,not_false_eq_true,div_self,
      mul_one,mul_inv_cancel_right₀]
    _ = -(1 / ((1 - x) * log 2) * x * (1 / x)) - ((1-x) * (1 /(1-x))) / (x * log 2) := by
      rw [move_factor_one_minus h2.symm]
    _ = -(x  / ((1 - x) * log 2) * (1 / x)) - (1-x) / (x * log 2) / (1-x) := by ring
    _ = -(x  / (((1 - x) * log 2 * x) )) - (1-x) / (x * log 2) / (1-x) := by
        rw [move_factor' zero_ne_one_neg_mul_log2 hx]
    _ = -(x  / ((1 - x) * log 2 * x) ) - (1-x) / (x * log 2 * (1-x)) := by field_simp
    _ = -x / ((1 - x) * log 2 * x) - (1-x) / ((1 - x) * log 2 * x) := by ring
    _ = (-x - (1-x)) / ((1 - x) * log 2 * x) := by
      have : (1 - x) * log 2 * x ≠ 0 := by
        exact mul_ne_zero zero_ne_one_neg_mul_log2.symm hx
      rw [factor_out_denom (-x) (1-x) _ this]
    _ = -1 / (x * (1 - x) * log 2) := by ring

[Andrew Yang]

lemma the_calculation {x : ℝ} (hx : x ≠ 0) (h2 : x ≠ 1) :
    -1 / (1 - x) / log 2 - x⁻¹ / log 2 = -1 / (x * (1 - x) * log 2) := by
  apply neg_injective
  simp only [neg_div, neg_sub, sub_neg_eq_add, neg_neg, ← one_div]
  rw [← add_div, ← div_div]
  rw [div_add_div]
  · simp
  · exact hx
  · exact sub_ne_zero.mpr h2.symm

[Adomas Baliuka]

Wow... How did you do it this fast? Any tricks? How did you decide to start with neg_injective?

[Andrew Yang]

First of all about your helper lemmas:
Usually you can guess what name a lemma should be based on its signature.
For example (a - b)/x = a/x - b/x (your factor_out_denom) would be called docs#sub_div (and to rewrite in the other direction you do ← sub_neg). by exact? (or loogle) would help you find it too.
And x * y ≠ 0 would be docs#mul_ne_zero, and a/b + c/d = (a*d+b*c)/(b*d) would be docs#div_add_div etc.
Now, the main part of the proof is 1/(1-x) + 1/x = 1/(x*(1-x), so I first got rid of the negation
via apply neg_injective and the next simp line.
rw [← add_div, ← div_div] then makes both sides of the form ?_ / log 2, and rw [div_add_div] adds the two fractions together. Then just trust that simp can take care of the rest.
(I ungolfed the proof a bit to retro fit this explanation)

[Andrew Yang]

Or maybe this calc proof is more readable?

lemma the_calculation {x : ℝ} (hx : x ≠ 0) (h2 : x ≠ 1) :
    -1 / (1 - x) / log 2 - x⁻¹ / log 2 = -1 / (x * (1 - x) * log 2) :=
  calc
    _ = -(1/x + 1/(1-x)) / log 2 := by
      simp [neg_div, add_div, sub_eq_add_neg]
    _ = -(1 / (x * (1 - x))) / log 2 := by
      congr
      rw [div_add_div]
      · simp
      · exact hx
      · exact sub_ne_zero.mpr h2.symm
    _ = -1 / (x * (1 - x) * log 2) := by
      simp only [div_div, neg_div]

[Yaël Dillies]

You mean docs#sub_div, not sub_neg, Andrew.

[David Loeffler]

Here's a 2-line proof:

lemma the_calculation {x : ℝ} (hx : x ≠ 0) (h2 : x ≠ 1) :
    -1 / (1 - x) / log 2 - x⁻¹ / log 2 = -1 / (x * (1 - x) * log 2) := by
  field_simp [sub_ne_zero.mpr h2.symm]
  ring

The point is that field_simp takes an optional argument, which is a list of proofs that things are not zero. Here sub_ne_zero.mpr h2.symm is a proof that 1 - x ≠ 0, which is the information field_simp needs to clear denominators.