# Zulip Chat Archive

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

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

lol

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

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:

- what does the
`$`

sign mean in the first proof? - What do you mean by
`--above proof converted to tactic mode`

and`-- lemmas in 'simp only' found using 'squeeze_simp'`

? - what do you mean by
`-- rewrites found using 'set_option trace.simplify.rewrite true'`

#### Mario Carneiro (Jul 01 2020 at 04:58):

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

`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.-
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. -
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