non-terminal `simp`s in mathlib

Stream: general

[Kevin Buzzard]

Can we lint for non-terminal simps? Can we automatically list all non-terminal simps or dsimps for which the output of squeeze_(d)simp doesn't work as a drop-in replacement?

I was surprised to see a non-terminal simp in mathlib but apparently there are plenty around.

[Damiano Testa]

Redefining simp to mean simp; done would error on all non-terminal simps, but would probably be a lot of effort...

[Eric Wieser]

Or just making simp emit a warning in those cases

[Eric Wieser]

Which mathlib would ban as it can't be noisy

[Yaël Dillies]

This is bad, because a few tactics are allowed after simp, for example refl (but maybe done calls refl?).

[Junyan Xu]

cross link about squeeze_dsimp

[Damiano Testa]

You could also do simp; refl; done.

[Junyan Xu]

It seems simp, refl can always be replaced by simpa (but simpa also checks the assumptions which may be a waste of CPU cycles?).

[Kevin Buzzard]

I'm generally happy with simp, ring as well as simp, refl but I'm not too happy with too much else (in the sense that I try to avoid it in code I write).

[Damiano Testa]

I suspect that it is easy to make future uses of simp comply with no non-terminal use. Backporting this would likely be a lot of work due to many edge-cases and widespread use of simp.

[Yaël Dillies]

I understand the rule as "simp and it's done".

[Yaël Dillies]

I understand the rule as "simp and it's done".

[Damiano Testa]

We could have a simp_old with the current behaviour and sed for it. And then have the new simp with some form of check (tracing something seems a good idea, so you coul still use it while in the middle of a proof, before cleaning up).

[Damiano Testa]

Regarding simpa for simp, refl: I remember Mario being horrified by this use when this came up in an earlier thread.

[Damiano Testa]

Here is a proposal: simp; reflexivity, done <|> trace "squeeze me".

[Kyle Miller]

I also like to use simpa using h when h simplifies to false, just to throw in another way Mario might be horrified at how we use his creation.

[Damiano Testa]

Oh, I use simpa to show false: I did not realize that Mario did not like that either!

[Kyle Miller]

I had assumed it's off-label usage, but maybe it was meant for this.

[Kevin Buzzard]

Probably we should have simpr or simpf or other monstrously-named tactics to do these special cases. The reason I don't mind simp, ring is that I figure that if simp has turned the goal into something that ring can solve then no amount of further simplification is going to break the ring application.

[Eric Rodriguez]

Yaël Dillies said:

This is bad, because a few tactics are allowed after simp, for example refl (but maybe done calls refl?).

this really shouldn't be allowed, and if you want it you should spell it out with simpa using rfl

[Eric Rodriguez]

no tactics after simp are ever safe

[Eric Rodriguez]

is my opnion idk

[Damiano Testa]

While we are on this topic, docs#mul_eq_zero seems to go against what Kevin said about simp, ring. This is a personal battle of mine again this simp lemma... :smile:

[Kyle Miller]

What about after norm_num, which calls simp?

[Damiano Testa]

Does norm_num call "free-style" simp or is it simp onlys?

[Kyle Miller]

example {α : Type*} (f : α ≃ α) : f.symm ∘ f = id := by norm_num

[Eric Rodriguez]

it's simp [-one_div]

[Eric Rodriguez]

dear lord

[Kevin Buzzard]

gaargh mul_eq_zero is evil!

[Damiano Testa]

I think mul_eq_zero makes sense as an informal simp lemma, but as an actual simp lemma, i always have to -it.

[Junyan Xu]

Sometimes a change to simp lemmas could change the final refl from necessary to unnecessary, or vice versa. Which means you need to change simpa to simp or vice versa. But this is easy to fix.

[Mario Carneiro]

Kyle Miller said:

I also like to use simpa using h when h simplifies to false, just to throw in another way Mario might be horrified at how we use his creation.

That would be equivalently simp at h, no?

[Mario Carneiro]

mul_eq_zero makes sense as an auto style lemma, i.e. if you had simp + some light propositional reasoning. As it is currently I wouldn't expect most x = 0 theorems to be simp-able to true which is what you need for mul_eq_zero to be useful

[Kevin Buzzard]

If one is simpable to true then I bet ring solves it too!

[Mario Carneiro]

not necessarily, it might be f x = 0 because it's in the kernel of a map or it's a hypothesis provided to simp or it's the cardinality of the empty type or something similarly obscure

[Kevin Buzzard]

@Junyan Xu I managed to manually squeeze the last two dsimps on that branch! You're right, show_term doesn't do anything helpful. I kept throwing in the head symbol until it worked. The final proof (line 408) is now two lines longer because the list is long, but it compiles much more quickly.

[Junyan Xu]

@Kevin Buzzard Thanks for the work! It seems clear that removing non-terminal dsimp is much more difficult than removing non-terminal simps, which may contribute to the fact that non-terminal dsimp is much more prevalent. (I guess one could also consider using squeeze_simp then removing all non-rfl lemmas from the result ...)