Sup_range as simp

Stream: general

[Violeta Hernández]

I wanted to ask for a small RFC here. The theorem docs#Sup_range seems like a perfect candidate for a simp lemma at first glance. However, marking it as simp breaks the proofs of a handful (about half a dozen) simp lemmas about supr that amount to by simp [supr].

[Violeta Hernández]

You can see the sort of breakage it caused in #14918 (though a few of the changes are due to another lemma I marked as simp)

[Violeta Hernández]

Question: is this an indication that it shouldn't be simp? Or should I fix the proofs it breaks and mark it as simp?

[Eric Wieser]

I think we need a mechanism to say ← foo is a simp lemma; as simp already knows how to reduce simp [foo, ←foo] to a safe application.

[Violeta Hernández]

How would that work in this case? ←supr would be marked as simp?

[Eric Wieser]

Either that, or simp could learn that Sup_range is an alias of supr.equations.<something>.symm

[Eric Rodriguez]

Eric Wieser said:

I think we need a mechanism to say ← foo is a simp lemma; as simp already knows how to reduce simp [foo, ←foo] to a safe application.

how does it do this?

[Yury G. Kudryashov]

You can use simp [<- Sup_range]

[Eric Wieser]

It would be nicer if neither of the two different ways to spell that resulted in an infinite loop!

[Anne Baanen]

Eric Rodriguez said:

how does it do this?

Here's the relevant code: it looks for ← e where e is a constant or local constant, and removes all other applications of e. Definitely not the best way to do so, but it was the simplest way.