squeeze_simp and simp?

Stream: mathlib4

[Arthur Paulino]

I'd like to kickoff this discussion regarding squeeze_simp and simp?. Some progress has been made on #5901.

It's been proposed that simp? could eventually replace squeeze_simp. I like that idea because simp? is shorter and the interrogation mark makes for a good pattern of extracting data from tactics. Also, with Lean 4, simp? would stand as a syntax of its own (it wouldn't necessarily trigger the implementation of simp with a parameter indicating the interrogation mark), so we don't need to change the implementation of simp to accommodate the ?.

Another point mentioned was that squeeze_simp seems to nail some simplifications that simp? doesn't. Are there things that simp? does which squeeze_simp can't? Or is it the case that the Lean 3 behavior of simp? can simply be dropped?

[Ruben Van de Velde]

I think the only feature of simp? I've cared about is that it's much faster than squeeze_simp - all behavioural differences I've seen were bugs

[Mario Carneiro]

There is no need for these to be separate tactics. The difference is entirely historical and they have the same spec

[Arthur Paulino]

Mario Carneiro said:

they have the same spec

Do you mean they're supposed to have the same behavior?

[Mario Carneiro]

yes

[Mario Carneiro]

that is, if you are asked "what does simp? do" or "what does squeeze_simp do" then the answer is the same

[Mario Carneiro]

simp? is the better name according to our general patterns for tactic naming

[Arthur Paulino]

Why is simp? faster (according to @Ruben Van de Velde)?

[Mario Carneiro]

because squeeze_simp just runs simp with every subset of arguments to see which work

[Mario Carneiro]

simp? is implemented in C++ and instruments simp to report what lemmas it used

[Mario Carneiro]

That is definitely the correct implementation strategy, but it has some false negative issues so it can sometimes produce incorrect calls, while squeeze_simp is relying on the observational behavior of simp [lemmas, ...] so it is always correct

[Mario Carneiro]

I think both of them have trouble with re-printing the input terms though

[Arthur Paulino]

I didn't understand how false negatives would cause incorrect calls. Wouldn't it make the tactic give up when it's actually possible to find a simplification?

[Arthur Paulino]

Mario Carneiro said:

That is definitely the correct implementation strategy

Do you mean this for Lean/mathlib 4 as well? Is Lean 4's simp implemented in C++?

[Mario Carneiro]

simp? can fail to report that a lemma was used even though it did have an influence on the proof

[Mario Carneiro]

Yes, I mean that lean 4 simp? should watch simp to report used lemmas, but without the bugs

[Mario Carneiro]

Lean 4 simp is not implemented in C++, it is in lean like most tactics

[Arthur Paulino]

Got it. Is it currently easy to query what simp used in Lean 4?

[Eric Rodriguez]

Mario Carneiro said:

I think both of them have trouble with re-printing the input terms though

Me and Arthur fixed this for squeeze_simp in lean3 j think, not sure how well roundtripping works in lean4

[Mario Carneiro]

Arthur Paulino said:

Got it. Is it currently easy to query what simp used in Lean 4?

Maybe, maybe not, but you can always copy and paste enough of the internal implementation until you have access to the relevant data

[Arthur Paulino]

@Eric Rodriguez I believe we will need the workaround for dealing with namespaces again

[Arthur Paulino]

@Mario Carneiro when you said that squeeze_simp runs every subset of arguments you didn't mean iterating on the entire power set, right?

[Arthur Paulino]

Were you talking about that linear process of argument elimination that stops when the result of tactic application changes? (I'm not on PC so I can't search code right now)

[Mario Carneiro]

It's finding a minimal working subset, assuming that simp is monotonic wrt its arguments

[Arthur Paulino]

I see. I know exactly the function you're referring to

[Mario Carneiro]

which is linear time (or rather O(n) times the performance of simp itself)

[Mario Carneiro]

hence squeeze_simp will usually be O(n) times slower than simp?

[Arthur Paulino]

Should we aim for minimality with simp? in mathlib4?

[Arthur Paulino]

(should I be worried that simp might be slower in Lean 4 than in Lean 3?)

[Eric Rodriguez]

that should really not be the case ever at all

[Mario Carneiro]

Arthur Paulino said:

Should we aim for minimality with simp? in mathlib4?

Minimality is not usually a target goal of tactics. I wouldn't say that there are any upper complexity limits except that a tactic that is too complex can be hard to maintain and/or slow, but it's not a big deal if you write a small tactic to begin with and we refine it later

[Arthur Paulino]

Eric Rodriguez said:

that should really not be the case ever at all

simp is implemented in Lean 4 itself in Lean 4 and in C++ in Lean 3 so it's plausible

[Mario Carneiro]

simp has a more efficient implementation in lean 4 than lean 3, in particular because of its discrimination tree indexing

[Arthur Paulino]

By reading simp's code I'm starting to think that it would be better to have it equipped with a way to report the theorems it used otherwise we will end up with a lot of duplicated code. What do you guys think? The code base is not very short

[Arthur Paulino]

(maybe simp? is not a good tactic to port at the moment)

[Kevin Buzzard]

I guess simp? is not used at all in mathlib...

[Arthur Paulino]

Kevin Buzzard said:

I guess simp? is not used at all in mathlib...

I meant simp? as a tactic with the same behavior of squeeze_simp (to catch up)

[Kevin Buzzard]

Sure, and I'm pointing out that whilst of course we use it to write new mathlib, the simp? tactic (or variant or whatever it is) itself is not used at all in mathlib master, so if the main goal here is to get mathlib ported then maybe it can wait for a while?