How to simplify this proof?

Stream: new members

[Chris M]

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]

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]

lol

[Chris M]

nice.

[Chris M]

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]

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]

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'

[Mario Carneiro]

the $ is just another notation for application at low precedence

[Mario Carneiro]

it's the same as inv_eq_of_mul_eq_one (by simp [mul_assoc])

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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]

Ok that makes sense.

[Chris M]

Thanks for the help!

[Kevin Buzzard]

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