# Zulip Chat Archive

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

#### 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: Aug 03 2023 at 10:10 UTC