Zulip Chat Archive

Stream: maths

Topic: golden ratio calculation


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 21:00):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 26 2019 at 21:07):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 26 2019 at 22:54):

oh right, ring knows about div


Last updated: May 14 2021 at 18:28 UTC