Zulip Chat Archive

Stream: new members

Topic: Multiplying both sides of an expression by a constant


ROCKY KAMEN-RUBIO (May 15 2020 at 17:02):

MWE
Is there an automated way to do stuff like this? The best I can think of is to prove 2!= 0, multiply both sides by 2, rw mul_add, mul_sub, add_mul, add_sub a bunch of times, then prove 2*(1/2) = 1 and apply that with some other algebra. I feel like there should be a faster way I'm missing.

example (a b c d e f g : ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
sorry,
end

More Context
I'm having trouble massaging this identity to prove Binet's formula for the Fibonacci numbers.

import data.real.basic
import data.nat.basic
import data.nat.fib
import tactic
noncomputable theory
def phi :  := ((1 + real.sqrt 5) / 2)
def psi :  := ((1 - real.sqrt 5) / 2)

lemma psi_phi_identity (k : ) : phi ^ k - psi ^ k + (phi ^ (k + 1) - psi ^ (k + 1)) = phi ^ (k + 2) - psi ^ (k + 2) :=
begin
induction k with n hn,
{simp only [pow_one, zero_add, pow_zero, sub_self],
rw phi,
rw psi,
rw pow_succ,
simp only [div_pow, pow_one, mul_add, add_mul],
sorry,},
sorry,
end

Matt Earnshaw (May 15 2020 at 17:28):

how about:

example (a b c d e f g : ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
  field_simp,
  rw  add_assoc,
  rw h,
  ring,
end

Matt Earnshaw (May 15 2020 at 17:29):

sadly not of great generality

Kevin Buzzard (May 15 2020 at 17:31):

Here are some thoughts on Binet's formula which might end up in Mathematics in Lean at some point.

Mario Carneiro (May 15 2020 at 17:31):

example (a b c d e f g : ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
  apply_fun (λ x, x/2) at h,
  convert h; ring,
end

Kevin Buzzard (May 15 2020 at 17:31):

hey, where is the ring++ usage??

Mario Carneiro (May 15 2020 at 17:32):

that works too:

example (a b c d e f g : ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
  ring_rw [h / 2],
end

Mario Carneiro (May 15 2020 at 17:33):

modulo the existence of the tactic

Reid Barton (May 15 2020 at 17:34):

Mario Carneiro said:

modulo the existence of the tactic

Now you are proving like a mathematician!

Johan Commelin (May 15 2020 at 17:42):

The tactic is left as an exercise for the reader

Kevin Buzzard (May 15 2020 at 17:55):

Of course Mochizuki also left a tactic as an exercise for the reader, and it's stumped Scholze.

Patrick Massot (May 15 2020 at 19:49):

What happened to rumors of Mochizuki's work being published?

Johan Commelin (May 15 2020 at 19:55):

Last thing I heard, it happened.

Johan Commelin (May 15 2020 at 19:55):

Peter Woit had a long discussion on his blog, and he summarised it in some 40 page pdf

Kevin Buzzard (May 15 2020 at 20:09):

PRIMS announced they were going to do it


Last updated: Dec 20 2023 at 11:08 UTC