## Stream: maths

### Topic: golden ratio calculation

#### Kevin Buzzard (Feb 26 2019 at 19:34):

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
-- ... 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 (Feb 26 2019 at 20:17):

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 (Feb 26 2019 at 20:26):

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

#### Rob Lewis (Feb 26 2019 at 20:57):

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 (Feb 26 2019 at 20:58):

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 (Feb 26 2019 at 21:00):

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

#### Rob Lewis (Feb 26 2019 at 21:04):

Ugh, apparently not.

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


#### Patrick Massot (Feb 26 2019 at 21:07):

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

#### Mario Carneiro (Feb 26 2019 at 22:23):

lemma phi_squared : phi ^ 2 = phi + 1 :=
begin
have : 2 * phi - 1 = sqrt 5,
exact mul_div_cancel' _ two_ne_zero },
have : (2 * phi - 1) ^ 2 - 5 = 0,
{ have : 2 * phi - 1 = sqrt 5,
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 (Feb 26 2019 at 22:44):

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 (Feb 26 2019 at 22:54):

oh right, ring knows about div

Last updated: May 14 2021 at 18:28 UTC