golden ratio calculation

Stream: maths

[Kevin Buzzard]

import data.real.basic
import tactic.ring

open real

noncomputable def phi := (1 + sqrt 5) / 2

lemma phi_squared : phi ^ 2 = phi + 1 :=
begin
  rw pow_two,
  show (1 + sqrt 5) / 2 * ((1 + sqrt 5) / 2) = (1 + sqrt 5) / 2 + 1,
  -- First goal: get rid of divisions.
  rw div_mul_div,
  symmetry, -- kind of annoying that I have to stop my rewrite,
  rw eq_div_iff_mul_eq,
    swap,norm_num,
  -- Now multiplying out will remove them so use ring
  suffices : 2 * sqrt 5 + 6 = (sqrt 5 + 2) * sqrt 5 + 1,
    -- Now use ring as a not-quite-goal-killing tactic
    ring, exact this, -- is this poor coding style? Feels safe to me
  -- Now get sqrt 5's together
  rw [add_mul,←pow_two],
  -- ... and kill them
  rw sqr_sqrt,
    swap,norm_num,
  -- Now ring will do it.
  ring,
end

This came up today when talking to the UGs about some analysis. It's still a lot more painful than I'd like it to be. Am I missing any tricks which would make the argument shorter? I feel like my first instinct with all of these things is to get rid of denominators, so I can start using ring. Should it be?

I feel like I could sometimes use a slightly beefed-up version of ring which starts by locating all denominators, multiplying everything up by a common denominator, introducing subgoals saying that all of them are non-zero (because they always are in maths) and then killing the main identity with ring leaving me just the job of justifying that all the denominators are non-zero.

[Kevin Buzzard]

Thinking about this more, I realise that actually this is different from the ring tactic -- I could do with a clear_denominator tactic, which takes a goal of the form e.g. a + b/c + (d+e-f)/g = h / i with variables in a field, and reduces it to goals c ne 0, g ne 0, i ne 0 and a*c*g*i + b*g*i+(d+e-f)*c*i=h*c*g. That looks to me like something one could write an algorithm for. Am I being naive? It could eliminate denominators one by one. I don't care how horrible the final goal is, because in many cases I'll be able to prove it using ring.

[Patrick Massot]

I thought about this at some point, the difficulty is to push the multiplication through the expression, but it should be possible

[Rob Lewis]

There's a preprocessing step in linarith that does this for numeric denominators. If someone is interested in implementing this, maybe there's inspiration to be found there, although I can't promise it's the cleanest code.

[Rob Lewis]

IIRC, it walks through the term first to compute a coefficient that will cancel all denominators in the term. You need more than a bare coefficient though, you need some sort of tree to represent which part to distribute to which side of a product.

[Kevin Buzzard]

Does it deal with (a/b)/(c/d) = e / f?

[Rob Lewis]

Ugh, apparently not.

example (a : ℚ) (ha : a > 0) : ((4/3)/(5/2))*a > 0 :=
by linarith -- fails

[Patrick Massot]

Simon, stop playing with python, we need your super powers! :santa:

[Mario Carneiro]

lemma phi_squared : phi ^ 2 = phi + 1 :=
begin
  have : 2 * phi - 1 = sqrt 5,
  { rw [sub_eq_iff_eq_add'],
    exact mul_div_cancel' _ two_ne_zero },
  have : (2 * phi - 1) ^ 2 - 5 = 0,
  { have : 2 * phi - 1 = sqrt 5,
    { rw [sub_eq_iff_eq_add'],
      exact mul_div_cancel' _ two_ne_zero },
    rw [sub_eq_zero, this, sqr_sqrt], norm_num },
  apply eq_of_mul_eq_mul_left (by norm_num : (4:ℝ) ≠ 0),
  rw [← sub_eq_zero, ← this], ring,
end

[Kenny Lau]

lemma phi_squared : phi ^ 2 = phi + 1 :=
by rw [phi, div_pow (_:ℝ) two_ne_zero, pow_two, add_mul_self_eq,
  mul_self_sqrt (show (0:ℝ) ≤ 5, by norm_num)]; ring

[Mario Carneiro]

oh right, ring knows about div