simp making a meal of it

Stream: general

[Kevin Buzzard]

set_option trace.simplify.rewrite true
example (G : Type*) [group G] (g h : G) : (g * h)⁻¹ = h⁻¹ * g⁻¹ :=
begin
  simp
end
/-
0. [simplify.rewrite] [mul_inv_rev]: (g * h)⁻¹ ==> h⁻¹ * g⁻¹
1. [simplify.rewrite] [mul_right_inj]: h⁻¹ * g⁻¹ = h⁻¹ * g⁻¹ ==> h⁻¹ = h⁻¹
2. [simplify.rewrite] [inv_inj']: h⁻¹ = h⁻¹ ==> h = h
3. [simplify.rewrite] [eq_self_iff_true]: h = h ==> true
-/

simp is making a bit of a meal of this one. Is that to be expected? It doesn't try rfl earlier?

[Reid Barton]

a = a doesn't syntactically match the goal, because the two sides are not syntactically the same

[Johan Commelin]

Why do you always want the shortest path? You should enjoy the trip, and all the scenery. "The journey is the destination"...

[Reid Barton]

I guess this is the minimal example of our category theory comp_id woes

[Johan Commelin]

@Reid Barton Do you mean that a doesn't match h⁻¹ * g⁻¹? That's a pity...

[Reid Barton]

a can't match both sides at once

[Johan Commelin]

After the 1st simplification step, both sides are identical, right?

[Reid Barton]

Ohh, you mean after the first step

[Reid Barton]

yes, then it could. I guess it just applies simp lemmas in some random order

[Rob Lewis]

When I try this it gets to true in two steps. Are you importing anything?

0. [simplify.rewrite] [mul_inv_rev]: (g * h)⁻¹ ==> h⁻¹ * g⁻¹
1. [simplify.rewrite] [eq_self_iff_true]: h⁻¹ * g⁻¹ = h⁻¹ * g⁻¹ ==> true

[Rob Lewis]

What the hell, both of those line numbers should be 0, Zulip is rewriting the second to 1...

[Rob Lewis]

That's confusing.

[Reid Barton]

Oops, I just realized your original statement is not true by defeq

[Kevin Buzzard]

import category_theory.concrete_category

set_option trace.simplify.rewrite true
example (G : Type*) [group G] (g h : G) : (g * h)⁻¹ = h⁻¹ * g⁻¹ :=
begin
  simp
end

I had a random import at the top of my scratch file! @Reid Barton @Scott Morrison why did this happen?

[Kevin Buzzard]

Oh -- they are importing algebra.group

[Kevin Buzzard]

I want Lean to try eq_self_iff_true before some random lemmas in algebra_group. What order does simp look for its lemmas?

[Kevin Buzzard]

I also don't know how to work out how they are getting to algebra.group

[Rob Lewis]

import algebra.group

set_option trace.simplify.rewrite true
attribute [simp, priority 1000000] eq_self_iff_true
example (G : Type*) [group G] (g h : G) : (g * h)⁻¹ = h⁻¹ * g⁻¹ :=
begin
  simp
end

Is there any danger to setting eq_self_iff_true to be high priority globally?

[Rob Lewis]

I wish I had tried this while I was still at the office so I could profile on my desktop...

[Jesse Michael Han]

on my machine, with the category_theory import, execution time of simp is like 650ms, but with just the algebra.group import, it goes back down to 177ms (with the same unnecessarily large simp set)

[Jesse Michael Han]

sadly eblast is slower than simp in either case (and i imagine there are far more simp lemmas than ematch lemmas in the imports):

import algebra.group tactic.interactive

attribute [ematch] mul_inv_rev mul_right_inj eq_self_iff_true inv_inj'

example (G : Type*) [group G] (g h : G) : (g * h)⁻¹ = h⁻¹ * g⁻¹ :=
by {[smt] eblast}  -- 300ms

[Rob Lewis]

I'm curious about the effect if you set priority 1000000 low in the import hierarchy. Does it make a noticeable difference to compiling mathlib?

[Rob Lewis]

I'm trying while I make dinner.

[Johan Commelin]

simp is making a meal of it while Rob is making dinner... :grinning_face_with_smiling_eyes:

[Rob Lewis]

Answer: no, no noticeable difference. Although one proof breaks because simp finishes early, a reminder to avoid non-terminal simp: https://github.com/leanprover-community/mathlib/blob/master/src/data/fintype.lean#L508