bad simp lemmas (split from: doc-gen is failing)

Stream: general

[Gabriel Ebner]

Oh wow, there's even a non-terminal simp there...

[Rob Lewis]

An extremely slow nonterminal simp

[Gabriel Ebner]

#6401

[Rob Lewis]

Ah, you beat me by 10 sec

[Rob Lewis]

https://github.com/leanprover-community/mathlib/tree/speedup-cau-seq-filter

[Rob Lewis]

Curious that we came up with different simp onlys

[Gabriel Ebner]

At first squeeze_simp timed out for me, so I tried simp?. But that didn't give me all lemmas, so I had to do squeeze_simp afterwards and merge the two.

[Rob Lewis]

Great minds think alike! I did the same, but after simp? wasn't enough I just guessed that ge_iff_le was missing

[Gabriel Ebner]

As far as I can tell from the trace messages, there's more conditional simp lemmas here than I'd like.

• forall_prop_of_true seems to trigger at every implication
• even better, forall_prop_of_false triggers a second time...
• exists_prop_of_true is not as bad, but still triggers way too often
• function.injective.eq_iff triggers at every function
• wtf is imp_iff_right a simp lemma?!?!?!?

[Gabriel Ebner]

It doesn't help that conditional simplification does not seem to be cached. (Maybe that's because we're simplifying under binders here and get a different local constant every time, I didn't check.)

[Rob Lewis]

wtf is imp_iff_right a simp lemma?!?!?!?

This will never fire, right? If it fires successfully then simp proves a, which means a simplifies to true, which means a → b has already simplified to b?

[Gabriel Ebner]

Well, it will always fire but never rewrite, which is even worse.

[Rob Lewis]

Right, that's what I meant... ugh

[Kevin Buzzard]

I love what has happened to this topic

[Rob Lewis]

#6402

[Gabriel Ebner]

BTW, if I disable all of the lemmas that I've listed, then simp only takes 740ms instead of 6600ms.

[Rob Lewis]

I have no clue what the first three are doing. Removing the last two seems like an obvious good move...

[Rob Lewis]

There was a little breakage from function.injective.eq_iff early on, not sure how much more is coming.

[Gabriel Ebner]

The *_prop_of_* lemmas are a hack because we can't define multiple congruence lemmas for a function symbol (and probably none for forall). They only help with uber-dependently typed goals such as ∀ x : none.is_some, get x = a. In general you don't want to rewrite the domain of a pi, because then you get an ugly term in the codomain. But for propositions, this doesn't matter.
These lemmas should be removed from the simp set. I don't think that would break much, because we avoid dependent types anyhow. And if it does, it's better to fix this in the simplifier (on the c++ side).

[Rob Lewis]

There's a little more breakage so far from the *_prop_of_* but not too much. And I'm guessing it's all at the bottom. I'll make a second PR once I get a little farther locally

[Rob Lewis]

#6404

[Bryan Gin-ge Chen]

I do remember seeing a lot of *_prop_of_* in the output of squeeze_simp so I do think it is something we rely on quite a bit.