bad simp lemmas

Stream: mathlib4

[Daniel Selsam]

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]

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

[Scott Morrison]

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]

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]

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]

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]

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]

Does that mean we should revert #8736?

[Scott Morrison]

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

[Gabriel Ebner]

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]

In what sense is it ill-conditioned here?

[Gabriel Ebner]

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

[Scott Morrison]

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]

@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]

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

[Daniel Selsam]

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]

function.injective should not be reducible either

[Floris van Doorn]

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]

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

[Floris van Doorn]

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]

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]

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]

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]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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