beginner question on proving associativity for an example

Stream: general

[0xc0]

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]

local infixl `|*|` := f

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

the more interesting proof:

theorem f_plus_one (a b : ℝ) : f a b + 1 = (a + 1) * (b + 1) :=
by simp [f, mul_add, add_mul, add_assoc, add_left_comm]

theorem dummit_foote_1_1_1b (a b c : ℝ) : f (f a b) c = f a (f b c) :=
by apply @add_right_cancel ℝ _ _ 1; simp [f_plus_one, mul_assoc]

[0xc0]

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

[Mario Carneiro]

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]

f_plus_one expresses this fact

[Shing Tak Lam]

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

theorem dummit_foote_1_1_1b (a b c : ℝ) : f (f a b) c = f a (f b c) :=
calc f (f a b) c = f (a + b + a * b) c                         : rfl -- true by definition
             ... = (a + b + a * b) + c + (a + b + a * b) * c   : rfl -- true by definition
             ... = a + (b + c + b * c) + a * (b + c + b * c)   : by ring -- rearranging the terms
             ... = f a (b + c + b * c)                         : rfl -- true by definition
             ... = f a (f b c)                                 : rfl -- true by definition

[Mario Carneiro]

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]

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]

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]

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]

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]

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