simp doesn't work until I remove certain theorem

Stream: new members

[Weiyi Wang]

I encountered an interesting case where simp behaves unexpectedly. A single simp fails to close the goal, but if I specify a subset of simp theorems it closes the goal. What is going on here?

import Mathlib

lemma stuff (s t: ℕ) : (s / t: ℝ) ^ t = ∏ _ ∈ Finset.range t, (s / t: ℝ) := by
  simp only [Finset.prod_const, Finset.card_range]
  --simp -- doesn't work
  --simp? -- doesn't work, and suggests below
  --simp only [Finset.prod_div_distrib, Finset.prod_const, Finset.card_range] -- doesn't work

[Ruben Van de Velde]

What's going on is in technical terms a lack of "confluence". Probably Finset.prod_div_distrib should not be tagged as a simp lemma

[Ruben Van de Velde]

Seemingly added by @Yaël Dillies in !3#14189

[Weiyi Wang]

Oh! I have seen that word in some doc but never understood what it meant

[Ruben Van de Velde]

Basically, it means that if simp can go from state A → B → C and also A → D, then it should also go D → C

[Ruben Van de Velde]

That it, it shouldn't matter which simp lemma you apply first

[Yaël Dillies]

Yep, looks like a bad simp lemma, but for an unrelated reason (it's not affine)

[Weiyi Wang]

Thanks for the explanation. btw, what it does affine mean in this context?

[Ruben Van de Velde]

As I understand it, s occurs once on the left hand side and twice on the right hand side, which is not optimal especially when s is a big expression

[Kevin Buzzard]

So the same applies to docs#Finset.sum_sub_distrib ? That looks like a fine simp lemma to me...(oh that will just be the additivised version)

[Kevin Buzzard]

Why not just make the simp set confluent again? @Weiyi Wang can you figure out which simp lemmas to add to make it confluent again?

[Weiyi Wang]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Basic.html#div_pow is the missing one it seems, but for this lemma on its own, I can't tell which side is more "simplified"

[Kevin Buzzard]

So maybe either docs#div_pow should be a simp lemma, or docs#Finset.prod_div_distrib should not be, and then this part of the simpset will be confluent again.

[Bolton Bailey]

Kevin Buzzard said:

So the same applies to docs#Finset.sum_sub_distrib ? That looks like a fine simp lemma to me...(oh that will just be the additivised version)

docs#Finset.sum_sub_distrib seems bad to me, what if I have h = f - g in my context?

[Sabbir Rahman]

a bit tangential to the thread, but I have faced such issues of simp not closing due to a simp lemma "taking the goal to a unwanted state" lots of times. I thought that was just part of life and I had to use simp? followed by removing the problematic lemmas when applying simp. But reading the thread, it seems like those are unintended. For example consider following example:

import Mathlib

example : ({(0, 0), (0, 1)} : Set (ℝ × ℝ)).ncard = 2 := by
  -- simp     -- changes target to {0, (0, 1)}.ncard = 2 and fails to close
  simp [-Prod.mk_zero_zero]

should I report such cases in zulip somewhere?

[Weiyi Wang]

I have definitely seen this as well! I thought it was because (a, b) syntax has ambiguity and didn't think too much in how simp worked back then

[Kevin Buzzard]

I think that basically people strive to make simp confluent, but it's hard. It might be interesting to write a program which checks for nonconfluence somehow! One reason you want simp confluence is that it implies that if simp solves a goal, it will never stop solving it later if someone adds something to the simp set. Mathlib allows terminal simps to solve goals and if simp randomly starts breaking then it's kind of annoying to fix -- you have to go back to previous mathlib, squeeze it and then replace the new call with a simp only and then ideally start trying to figure out why it broke. Maybe there should be a thread in #mathlib4 where people can report non-confluence issues (of which I'm sure there are plenty, but it can be fun to fix them!)

[Kevin Buzzard]

The example can be minimised a bit more:

import Mathlib

example : ¬(0, 0) = (0, 1):= by
  simp [-Prod.mk_zero_zero]

I think there is an argument for Prod.mk_zero_zero to not be a simp lemma. One possible use for it to be simp would be to prove (0,0)+(x,y)=(x,y) (with the logic being that once (0,0) is simplified to 0 you can use the simp lemma zero_add) but in fact

import Mathlib

example {x} {y} : (0, 0) + (x, y) = (x, y) := by
  simp [-Prod.mk_zero_zero]

works anyway, because simp simplifes the goal to 0 + x = x \and 0 + y = y.

You could try a PR to mathlib removing @[simp] from Prod.mk_zero_zero and see what happens: see if mathlib breaks, gets slower, gets quicker etc. If it doesn't break and stays the same this is evidence that it's not being used as a simp lemma which could make a case from untagging it.

[Sabbir Rahman]

Prod.mk_zero_zero is one of the cases I remember distinctively, as this was the first time I faced this. There were lots other examples, I'll have to search my codes to find them. Another similar thing happened with simp converting 1/x to x^{-1} and then like previous example cardinality proof failed.

[Kevin Buzzard]

This one is more difficult because you would presumably agree that -x is simpler than 0 - x!

[Kevin Buzzard]

In 2017 core Lean 3 had a - b = a + (-b) as a simp lemma and it drove everyone nuts. I think it was one of the first things that was changed when we forked.

[Kevin Buzzard]

https://github.com/leanprover-community/lean/pull/117

[Ruben Van de Velde]

Kevin Buzzard said:

I think that basically people strive to make simp confluent, but it's hard. It might be interesting to write a program which checks for nonconfluence somehow!

I think Kim was working on something like that for core, at least

[Joachim Breitner]

We have such a tool on a branch, and Kim has been using it heavily while improving the simpset around basic types:
https://github.com/leanprover/lean4/pull/5717

[Weiyi Wang]

I opened #24414 for de-simp mk_zero_zero

[Kevin Buzzard]

My proof of $(-1)^{1/3}=1/2$ here showed up some other simp confluence issues.

By a weird coincidence though, Kim is in my office right now, and I just asked them if simp should be confluent and they replied that this is asking too much in practice.

[Ruben Van de Velde]

We can still strive!