Zulip Chat Archive

Stream: general

Topic: beginner question on proving associativity for an example


view this post on Zulip 0xc0 (Nov 16 2020 at 19:19):

I am new to Lean and am figuring out how to prove that a+b+aba+b+ab is associative over ℝ. I have the following setup but am not sure which tactics to use. Also, I am not sure how to define f to be an infix operator.

import data.real.basic

def f (a b : ) :  :=
  a+b+(a*b)

-- proof idea: expand both sides, then use commutativity of + in ℝ
theorem dummit_foote_1_1_1b :  a b c : , f (f a b) c = f a (f b c) :=
begin
  sorry
end

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:22):

local infixl `|*|` := f

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 19:24):

local infixl `|*|`:70 := f

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:24):

the cheating proof:

theorem dummit_foote_1_1_1b (a b c : ) : f (f a b) c = f a (f b c) :=
by unfold f; ring

view this post on Zulip 0xc0 (Nov 16 2020 at 19:28):

Is there a way to prove this in Lean in which each step is more explicitly written?

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:28):

the more interesting proof:

view this post on Zulip 0xc0 (Nov 16 2020 at 19:31):

What is the intuition for proving via f_plus_one? Is this the result of something in Lean?

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:33):

Well, it is a priori surprising to find out that a+b+aba+b+ab is associative. There should be some "reason" for it, and the reason is that it is multiplication rewritten across the bijection x -> x + 1

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:33):

f_plus_one expresses this fact

view this post on Zulip Shing Tak Lam (Nov 16 2020 at 19:33):

0xc0 said:

Is there a way to prove this in Lean in which each step is more explicitly written?

calc mode is nice for this

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:36):

I like the f_plus_one proof a lot better than just observing that it is an equality of polynomials and so ring has to be able to solve it

view this post on Zulip Reid Barton (Nov 16 2020 at 19:40):

I think you'll find the real reason it's associative is that it arises as the formal group law associated to complex K-theory :upside_down:

view this post on Zulip 0xc0 (Nov 16 2020 at 19:47):

In the "cheating" proof by unfold f; ring, is there a way to see more of Lean's intermediate steps in the ring tactic? I am only seeing

a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:52):

This is an application of #explode:

#explode dummit_foote_1_1_1b

Be warned that the result is not pretty because ring uses a special normal form

view this post on Zulip Mario Carneiro (Nov 16 2020 at 19:54):

The "comprehensible" proof uses simp:

theorem dummit_foote_1_1_1b (a b c : ) : f (f a b) c = f a (f b c) :=
by unfold f; simp [add_assoc, mul_add, mul_comm, mul_left_comm, add_left_comm]

but the #explode of that proof is even longer

view this post on Zulip Mario Carneiro (Nov 16 2020 at 20:04):

It helps to use a notation when looking at ring proofs:

theorem dummit_foote_1_1_1b (a b c : ) : f (f a b) c = f a (f b c) :=
by unfold f; ring

local notation `H[`a` * `x` + `b`]` := tactic.ring.horner a x _ b
#explode dummit_foote_1_1_1b

Last updated: May 11 2021 at 23:11 UTC