# Zulip Chat Archive

## 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 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 (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, { 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 (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