Behavior of simp

Stream: lean4

[Matthew Ballard]

There have been repeated discussions and confusions about simp’s behavior with the transition from Lean 3, especially with regard to the behavior of rw. In particular, the following expectation seems to be implicit in the minds of many users .

Whenever rw [h] applies, simp only [h] should also apply.

[Matthew Ballard]

/poll Do you believe that simp should conform to this behavior?
Yes
No

[Sebastien Gouezel]

It doesn't seem reasonable to expect that simp only [h] will work whenever rw [h] does, as they are so different under the hood. Identifying concrete situations where simp behaves worse than it should, and trying to fix them, is IMHO both more realistic and more useful.

[Kevin Buzzard]

But this was true in lean 3, wasn't it?

[Matthew Ballard]

I think “worse than it should” is subjective and it seems like this is a common standard for that judgement.

[Patrick Massot]

I don't know if this was strictly true in Lean 3. But clearly the port revealed many places where Lean 3 simp was more efficient in this direction.

[Ruben Van de Velde]

In my experience in lean 3, this implication seemed to hold at least almost everywhere, as the analysts say

[Sebastien Gouezel]

No, it wasn't always true in Lean 3.

[Ruben Van de Velde]

Oh, except for Yaëls point

[Kevin Buzzard]

The real issue is simp only [A,B,C,D,E] now having to be simp only [A,B]; rw [C]; simp only [D,E].

But I absolutely agree with you that identifying concrete situations, minimising, and then solving, is an important problem.

[Matthew Ballard]

I am currently strongly leaning yes due to my mental model of simp but want to hear more

[Junyan Xu]

Another unsatisfactory behavior of simp is it can't un-expand a definition, but it seems the issue lean4#2431 is gonna be closed as won't fix.

[Kyle Miller]

Over here I tried to summarize the difference between rw and simp. Like Sebastien Gouezel said, they use different algorithms, and even if the new simp didn't use features like discrimination trees then just like in Lean 3 there would be examples where rw works but simp doesn't and vice versa (and these examples do not rely on defeq properties for matching).

[Kyle Miller]

Patrick Massot said:

where Lean 3 simp was more efficient in this direction.

With a different meaning for "efficient" my understanding is that the Lean 4 simp is significantly faster than the Lean 3 one, though I haven't measured it myself.

[Kyle Miller]

A concrete option that Lean 4 simp might be able to provide is to use rw-like key-based matching to come up with a list of potential simp lemmas for a given subexpression. This entails (I think) using the discrimination tree but stopping the search one level down and then taking all the results in the entire subtree.

[Kyle Miller]

Floris was suggesting to me that the discrimination trees might be too strict for certain arguments to functions (like maybe implicit arguments should be matched at defeq transparency? or not taken into account at all in the tree?)