## Stream: new members

### Topic: How to simplify this proof?

#### Chris M (Jun 30 2020 at 05:56):

For the following proof of h I just want to say: "repeatedly apply mul_assoc and one_mul and mul_left_inv".

import algebra.group

variables {G : Type*} [group G]

#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (mul_left_inv : ∀ a : G, a⁻¹ * a = 1)

namespace my_group

theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a ⁻¹ :=
begin
have h: (a * b)⁻¹ * (a * b) = b⁻¹ * a ⁻¹ * a * b,
{rw mul_left_inv, rw mul_assoc b⁻¹, rw mul_left_inv, rw mul_assoc, rw one_mul, rw mul_left_inv},
rw mul_assoc at h,
rw mul_right_cancel h
end

end my_group


Is there a way to do this better than I'm doing now?

#### Bryan Gin-ge Chen (Jun 30 2020 at 05:57):

import algebra.group
import tactic

variables {G : Type*} [group G]
namespace my_group

theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a ⁻¹ :=
by group

end my_group


lol

nice.

#### Chris M (Jun 30 2020 at 06:01):

And what if I'm not allowed to use group? i.e. I have to only use the three axioms, and no "exotic" tactics like group. Can I use something like repeat?

#### Bryan Gin-ge Chen (Jun 30 2020 at 06:10):

Here are a few more proofs inspired by the proof in mathlib:

import algebra.group
import tactic

variables {G : Type*} [group G]
namespace my_group

-- mathlib proof
lemma mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
inv_eq_of_mul_eq_one $by simp [mul_assoc] -- above proof converted to tactic mode -- lemmas in simp only found using squeeze_simp theorem mul_inv_rev' (a b : G) : (a * b)⁻¹ = b⁻¹ * a ⁻¹ := begin apply inv_eq_of_mul_eq_one, simp only [mul_assoc, mul_inv_cancel_left, mul_right_inv], end -- rewrites found using set_option trace.simplify.rewrite true theorem mul_inv_rev'' (a b : G) : (a * b)⁻¹ = b⁻¹ * a ⁻¹ := begin apply inv_eq_of_mul_eq_one, rw [mul_assoc, mul_inv_cancel_left, mul_right_inv], end end my_group  #### Chris M (Jul 01 2020 at 04:55): Thanks for this! Some questions: 1. what does the $ sign mean in the first proof?
2. What do you mean by --above proof converted to tactic mode and -- lemmas in 'simp only' found using 'squeeze_simp'?
3. what do you mean by -- rewrites found using 'set_option trace.simplify.rewrite true'

the $ is just another notation for application at low precedence #### Mario Carneiro (Jul 01 2020 at 04:58): it's the same as inv_eq_of_mul_eq_one (by simp [mul_assoc]) #### Bryan Gin-ge Chen (Jul 01 2020 at 04:58): 1. a$ b c is the same as a (b c), basically \$ is an operator with extremely low precedence so that it acts like it wraps parentheses around everything that follows.
2. a. I mean that I took the term proof above and rewrote it fully in tactic mode.
b. If you use squeeze_simp instead of simp, it outputs the lemmas that were actually used, which lets you write a simp only statement. See this doc entry.

3. If you write set_option trace.simplify.rewrite true before a proof using simp, then Lean will output some trace information when it runs simp, letting you see the rewrites that were performed. See the beginning of this page.

#### Chris M (Jul 01 2020 at 05:08):

When I write this:

theorem mul_inv_rev3 (a b : G) : (a * b)⁻¹ = b⁻¹ * a ⁻¹ :=
begin
apply inv_eq_of_mul_eq_one,
simp only [mul_assoc, mul_right_inv, mul_one, one_mul],
end


It tells me: tactic failed, there are unsolved goals, even though those theorems should be enough to fully simplify to 1=1. How should I think about this? Should I just think "simp will not always be able to simplify even if it would be obvious to humans that it could"?

#### Bryan Gin-ge Chen (Jul 01 2020 at 05:10):

even though those theorems should be enough to fully simplify to 1=1

Why? The tactic state after the simp will tell you how far it got.

#### Bryan Gin-ge Chen (Jul 01 2020 at 05:12):

Should I just think "simp will not always be able to simplify even if it would be obvious to humans that it could"?

There are tons and tons of things that are obvious to humans which are very nonobvious to simp or Lean. The doc I linked in point 3 above gives some explanation about how simp works. You can also turn on the various trace options to see what it tried.

#### Chris M (Jul 01 2020 at 05:12):

Bryan Gin-ge Chen said:

Why? The tactic state after the simp will tell you how far it got.

I mean, it is possible for me to rewrite the equation a * b * (b⁻¹ * a⁻¹) = 1 as 1=1, using only the lemmas mul_assoc, mul_right_inv, mul_one, one_mul.

#### Bryan Gin-ge Chen (Jul 01 2020 at 05:15):

That's true, but that's not how simp works. You can see that it uses mul_assoc in the "other" direction. While it's possible to reverse the direction with simp only [←mul_assoc, mul_right_inv, mul_one, one_mul],, you can see that simp still isn't smart enough to only apply ←mul_assoc once before attempting to apply mul_right_inv.

#### Chris M (Jul 01 2020 at 05:15):

Ok that makes sense.

#### Chris M (Jul 01 2020 at 05:37):

Thanks for the help!

#### Kevin Buzzard (Jul 01 2020 at 06:37):

"I can intuitively solve a logic puzzle" is not the same as "this algorithm will always find the solution that I can intuitively spot"

Last updated: May 14 2021 at 07:19 UTC