## Stream: general

### Topic: beginner question on proving associativity for an example

#### 0xc0 (Nov 16 2020 at 19:19):

I am new to Lean and am figuring out how to prove that $a+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


#### Mario Carneiro (Nov 16 2020 at 19:22):

local infixl |*| := f


#### Kevin Buzzard (Nov 16 2020 at 19:24):

local infixl |*|:70 := f


#### 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


#### 0xc0 (Nov 16 2020 at 19:28):

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

#### Mario Carneiro (Nov 16 2020 at 19:28):

the more interesting proof:

#### 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?

#### Mario Carneiro (Nov 16 2020 at 19:33):

Well, it is a priori surprising to find out that $a+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

#### Mario Carneiro (Nov 16 2020 at 19:33):

f_plus_one expresses this fact

#### 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

#### 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

#### 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:

#### 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)


#### 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

#### 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) :=


but the #explode of that proof is even longer

#### 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