Zulip Chat Archive

Stream: new members

Topic: How to simplify this proof?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Chris M (Jun 30 2020 at 05:58):

lol

view this post on Zulip Chris M (Jun 30 2020 at 06:00):

nice.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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'

view this post on Zulip Mario Carneiro (Jul 01 2020 at 04:58):

the $ is just another notation for application at low precedence

view this post on Zulip Mario Carneiro (Jul 01 2020 at 04:58):

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

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris M (Jul 01 2020 at 05:15):

Ok that makes sense.

view this post on Zulip Chris M (Jul 01 2020 at 05:37):

Thanks for the help!

view this post on Zulip 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