Zulip Chat Archive

Stream: mathlib4

Topic: bad simp lemmas


Daniel Selsam (Aug 18 2021 at 03:26):

Are simp lemmas like https://github.com/leanprover-community/mathlib/blob/master/src/data/set/function.lean#L73-L76 necessary? The pattern is ?f ?x and will basically always be tried, even with Lean4's discrimination tree.

Scott Morrison (Aug 18 2021 at 03:32):

I thought in Lean3 that pattern meant that it would never be tried! I'm compiling mathlib3 without that @[simp] now.

Scott Morrison (Aug 18 2021 at 03:37):

If you had some programmatic way of identifying that lemma as having a bad pattern like that, I'd be happy to have a list to clean up.

Daniel Selsam (Aug 18 2021 at 03:38):

My question was somewhat rhetorical -- even if a few proofs break in your run, we should definitely not have that instance in Mathlib4. I am starting to experiment with simp with binport deep in mathlib (DIM) and the traces are >2/3 Set.eq_on_empty.

Daniel Selsam (Aug 18 2021 at 03:38):

Scott Morrison said:

If you had some programmatic way of identifying that lemma as having a bad pattern like that, I'd be happy to have a list to clean up.

Good idea. I will print out the end-of-mathlib simp discrimination tree.

Gabriel Ebner (Aug 18 2021 at 07:52):

Huh? This lemma was far from useless in Lean 3. It worked just fine:

import data.set.function
set_option trace.simplify.rewrite true
example (f g :   ) : set.eq_on f g  :=
begin
  trace_simp_set only [set.eq_on_empty],
  simp,
end

Gabriel Ebner (Aug 18 2021 at 07:55):

Difference is that Lean 3 didn't unfold the set.eq_on. Maybe it would make more sense to remove the @[reducible] attribute instead?

Eric Wieser (Aug 18 2021 at 08:51):

Does that mean we should revert #8736?

Scott Morrison (Aug 18 2021 at 08:58):

I'll back out #8736 and see what happens without @[reducible].

Gabriel Ebner (Aug 18 2021 at 09:00):

I think #8736 was a bit premature, although it wasn't a big change since the simp lemma apparently wasn't used anywhere. I wonder what's the best solution here though.

  1. Make set.eq_on (and left_inv_on) semireducible.
  2. Tweak the Lean 4 simplifier so that it doesn't unfold a definition when the result is an ill-conditioned equation. (There's already a whnfUntilBadKey function which prevents unfolding if the result is a lambda.)

Eric Wieser (Aug 18 2021 at 09:06):

In what sense is it ill-conditioned here?

Gabriel Ebner (Aug 18 2021 at 09:10):

The left-hand side is ?f ?x, that is, an applied metavariable.

Scott Morrison (Aug 18 2021 at 10:35):

Okay, #8738 reverts the change from #8736, and instead removes the @[reducible] on set.eq_on, which doesn't appear to be necessary.

Daniel Selsam (Aug 18 2021 at 15:24):

@Scott Morrison More bad ones:

-- #print punit.eq_punit -- EDIT: whoops, this one is in Lean4
#print list.cons_injective
#print list.length_injective
#print list.reverse_injective

Note that function.injective is reducible.

Gabriel Ebner (Aug 18 2021 at 15:30):

Where is punit.eq_punit defined? It's not in my mathlib.

Daniel Selsam (Aug 18 2021 at 15:39):

Gabriel Ebner said:

Where is punit.eq_punit defined? It's not in my mathlib.

Sorry, that one is in Lean4 itself. I back-translated the name PUnit.eq_punit.

Mario Carneiro (Aug 18 2021 at 19:20):

function.injective should not be reducible either

Floris van Doorn (Aug 18 2021 at 20:45):

We have a linter that checks whether the function on the lhs in a local constant, however, that doesn't whnf reducible the expression. If I add that, I get exactly the same list as Daniel (this is on mathlib where Scott already fixed the first one).

/- Checking 85593 declarations (plus 87184 automatically generated ones) in all imported files (including this one) -/

/- The `simp_var_head2` linter reports: -/
/- LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.
Some simp lemmas have a variable as head symbol of the left-hand side: -/
-- d:\projects\mathlib\src\data\list\basic.lean
#print list.cons_injective /- Left-hand side has variable as head symbol: a₁ -/
#print list.length_injective /- Left-hand side has variable as head symbol: a₁ -/
#print list.reverse_injective /- Left-hand side has variable as head symbol: a₁ -/

So there shouldn't be more after these.

Floris van Doorn (Aug 18 2021 at 20:55):

@Gabriel Ebner could you take a look at #8749 (no hurry).

Floris van Doorn (Aug 18 2021 at 21:15):

Mario Carneiro said:

function.injective should not be reducible either

lean#604 (I don't have a local build, so CI might not pass)

Eric Wieser (Aug 18 2021 at 21:15):

The injectivity lemmas are bad as reducible simp lemmas presumably because simp just looks at the ?x = ?y goal and essentially discards the f ?x = f ?y hypothesis?

Eric Wieser (Aug 18 2021 at 21:17):

Could simp instead learn to just not pull off the last binder if the result had a bad head symbol? Or would that not be useful

Floris van Doorn (Aug 18 2021 at 21:17):

The existence or non-existence of f ?x = f ?y is not relevant.
If you make t = s a simp lemma, t cannot be in the form ?f ... (a local constant applied to 0 or more arguments), since then simp has nothing to match on when deciding whether to use this rewrite rule.

Eric Wieser (Aug 18 2021 at 21:18):

I guess I'm questioning the assumption that a "lemma" is the bit that remains after pulling off all the pi binders.

Eric Wieser (Aug 18 2021 at 21:21):

If my goal is (f a = f b → a = b) ∨ something_hard my assumption was that simp ought to be able to say _"oh I have a lemma that states (f a = f b → a = b) so that bit is just true"_. I'm sure that's not how it actually works though

Floris van Doorn (Aug 18 2021 at 21:25):

simp has to decide how to rewrite with the simp lemma

  • If your lemma is t = s or t ↔ s it will rewrite t to s
  • If your lemma is a definition, it will rewrite using the equation lemmas
  • maybe some other rules
  • If your lemma is a proposition p not falling into the above rules it will rewrite p to true.

What you're suggestion is something simp can do, except that it tries to apply the first rule, not the last one.
To get the behavior you want, you have to reformulate the lemma so that it states (f a = f b → a = b) ↔ true.

Floris van Doorn (Aug 18 2021 at 21:27):

If you don't give the lemma in this form, how does simp know which of the following you want?

f a = f b  a = b
f a = f b  (a = b  true)
(f a = f b  a = b)  true
( a b, f a = f b  a = b)  true

Eric Wieser (Aug 18 2021 at 21:31):

I'm guessing there are performance reasons why "well all of them at once I suppose" is not a good strategy, even if you prune all the ones with invalid head symbols first.

Mario Carneiro (Aug 18 2021 at 21:49):

those rewrite rules also vary a lot in their acceptability wrt their contribution to the whole rewrite system used by simp. For example the first rewrite looks a lot more problematic than the second and third, because a and b could be the same thing

Mario Carneiro (Aug 18 2021 at 21:50):

you also don't need the fourth rewrite given the third since there is a rewrite for (\forall x, true) <-> true


Last updated: Dec 20 2023 at 11:08 UTC