False ERR_NSP positive

Stream: mathlib4

[Yaël Dillies]

The ERR_NSP just gave me a false positive here. The simp is actually terminal, but there is a second goal in sight

[Yaël Dillies]

I'm not sure how looking at syntax is supposed to make sense to decide whether a simp is terminal or not, actually

[Johan Commelin]

Yaël Dillies said:

The ERR_NSP just gave me a false positive here. The simp is actually terminal, but there is a second goal in sight

Fair enough, but shouldn't there not be a second goal in sight?

[Johan Commelin]

Ideally this linter gets implemented in Lean, but I'm already hoping that it will do a lot of net good in its current form.

[Yaël Dillies]

The second goal was created by the rw above.

[Yaël Dillies]

I hope we're not supposed to add a focusing dot every time a rw creates a side goal??

[Yaël Dillies]

My style is

rw [lemma_with_side_condition1]
some_tactics
rw [lemma_with_side_condition2]
some_more_tactics
· prove_side_condition2
· prove_side_condition1

[Yaël Dillies]

If I want to keep clear of the linter, I would need to do

rw [lemma_with_side_condition1]
· some_tactics
  rw [lemma_with_side_condition2]
  · some_more_tactics
  · prove_side_condition2
· prove_side_condition1

which seems suboptimal to say the least (some_tactics and some_more_tactics are usually quite long)

[Kim Morrison]

I agree that it is necessary to be able to accumulate side conditions from rewrites without dots.

[Johan Commelin]

Otoh, if the proof of the side condition is short, then you can often swap; close_side_condition.

[Yaël Dillies]

Yes, but this forbids things like all_goals positivity (a pretty common idiom in LeanAPAP)

[Kim Morrison]

Or my recent favourite of all_goals omega.

[Johan Commelin]

Right. So we really need the procrastinate tactic.

[Kim Morrison]

This is a wrapper that hides all accumulated side goals until you're done with the main goal?

[Johan Commelin]

See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/An.20.60exists_intro.60.20tactic.3F/near/411262030
and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Tactic.20for.20repetetive.20cases/near/422685570

[Kim Morrison]

Oh yeah, I remember once opening that page and thinking "they are really procrastinating on explaining the essentials here..."

[Johan Commelin]

I mean, that explanation is only a sidegoal right?

[Yaël Dillies]

Can I turn off the linter locally? It seems not since it's implemented in Python. If I can't turn it off locally, can we turn it off globally until we figure out how not to inappropriately flag correct style code?

[Yaël Dillies]

Actually, can't we just let the linter know that

simp
· some_tactics

is correct? That will create a loophole (people can just focus the goal after a non-terminal simp to ignore the linter), but I have literally never seen focusing dots being used when a single goal is in sight, so it's probably fine.

[Eric Wieser]

Yaël Dillies said:

My style is

rw [lemma_with_side_condition1]
some_tactics
rw [lemma_with_side_condition2]
some_more_tactics
· prove_side_condition2
· prove_side_condition1

I think this style isn't great, because it doesn't enforce that some_more_tactics operates only on a single goal. I agree that the alternative isn't very readable either, but it is at least clear which goals it operates on

[Eric Wieser]

Yaël Dillies said:

Can I turn off the linter locally? It seems not since it's implemented in Python.

Python linters can be turned off in a nolints file somewhere

[Johan Commelin]

Also, if some lemma is refactored, and no longer needs a side condition, the person doing the refactor might have a harder time figuring out how to repair these proofs.
So while I think we should do more to support this style, in such a way that it is maintainable, I don't think the style is optimal right now.

[Yaël Dillies]

@Eric Wieser said:

Yaël Dillies said:

Can I turn off the linter locally? It seems not since it's implemented in Python.

Python linters can be turned off in a nolints file somewhere

The latest CI on #12569 (where I got another false positive) seems to suggest otherwise: https://github.com/leanprover-community/mathlib4/actions/runs/8907813217/job/24462314781?pr=12569

[Yaël Dillies]

cc @Johan Commelin

[Yaël Dillies]

This false positive I really can't solve. I need the simp call in front of the aesop call else everything times out

[Yaël Dillies]

cc @Jannis Limperg, since I've generally noticed aesop getting slower and slower when I bump mathlib in my projects

[Johan Commelin]

Are you saying that simp is not non-terminal?

[Yaël Dillies]

Not where the linter flagged it in #12569, no. The proof is

congr
ext
simp
aesop (add unsafe mul_mem_mul)

[Yaël Dillies]

It's a bit weird to have simp followed by aesop but, as I explained above, this is needed for the proof to use a reasonable amount of heartbeats, and aesop is not a rigid tactic so the simp really is not non-terminal.

[Johan Commelin]

Can you use on_goal?

[Johan Commelin]

In any case this proof deserves a comment, because it seems to be working around a timeout in aesop

[Yaël Dillies]

Johan Commelin said:

Can you use on_goal?

Not sure how. How would the proof look like?

[Yaël Dillies]

Johan Commelin said:

In any case this proof deserves a comment, because it seems to be working around a timeout in aesop

The comment is here: https://github.com/leanprover-community/mathlib4/pull/12569/files#diff-b8cca68e7f5f002a5bb141ac51d75c4cb3cab73b749b38a920a53e66f9a6e771R141

[Johan Commelin]

Sorry, I was completely confused. I thought this was about the multiple goal linter. But it is about the non-terminal linter. I agree that this seems to be a false positive.

[Johan Commelin]

In any case, on my pretty decent desktop in my office, your current proof is still really slow. So:

• yes, it would be good if this false positive got fixed (cc @Damiano Testa)
• yes, I would also strongly encourage that you optimize this proof for more speed. By squeezing the simp and the aesop calls, I would hope.

[Johan Commelin]

@[to_additive additiveEnergy_eq_sum_sq']
lemma multiplicativeEnergy_eq_sum_sq' (s t : Finset α) :
    Eₘ[s, t] = ∑ a in s * t, ((s ×ˢ t).filter fun (x, y) ↦ x * y = a).card ^ 2 := by
  simp_rw [multiplicativeEnergy_eq_card_filter, sq, ← card_product]
  rw [← card_disjiUnion]
  -- The `swap`, `ext` and `simp` calls significantly reduce heartbeats
  swap
  · simp only [Set.PairwiseDisjoint, Set.Pairwise, coe_mul, ne_eq, disjoint_left, mem_product,
      mem_filter, not_and, and_imp, Prod.forall]
    aesop
  · congr
    ext
    simp only [mem_filter, mem_product, disjiUnion_eq_biUnion, mem_biUnion]
    aesop (add unsafe mul_mem_mul)

[Johan Commelin]

This is almost instant on my machine

[Damiano Testa]

I think that this is about the text-based simp-normal form linter that was written by @Bolton Bailey. The syntax-based linters (both the simp-normal form and the multiple goals one) are not in mathlib (yet?).

[Damiano Testa]

Specifically for the simp-normal form linter, there seems to be some consensus on what the linter should flag (and the linter does that more or less reliably), but very little in the way of addressing the issue: neither says, nor suffice seem to really cover all the cases.

[Bolton Bailey]

If we are going to add in another linter that detects simps in a more nuanced way, why not just delete the old one now?

[Damiano Testa]

The new linter may take some time to get merged, I believe, so I think that the current one (yours) is still serving a very useful purpose.

[Bolton Bailey]

Ok, well #12585 is a small change that should allow aesop to follow simp.

[Bolton Bailey]

@Yaël Dillies feel tree to try merging this in to your PRs and see if it fixes your problem.

[Yaël Dillies]

Johan Commelin said:

This is almost instant on my machine

Interesting. I can't tell the difference on mine (went from slow to slow), but I take your word for it

[Yaël Dillies]

Bolton Bailey said:

Yaël Dillies feel tree to try merging this in to your PRs and see if it fixes your problem.

The linter doesn't complain anymore now that I've squeezed the simp.

[Damiano Testa]

I think that at the core of the non-terminal simp business there is the issue that there are situations in which there is no real palatable alternative to having a non-terminal simp. There are plenty of examples where simp? is unwieldy, as is the resulting term, making also suffices undesirable.

[Damiano Testa]

In my opinion, this is the main blocker for the "flexible vs rigid" linter: the linter flags what I would expect it to flag, but, sometimes, there is no real good way of pleasing the linter without silencing it.

[Damiano Testa]

(...and "sometime" is a little too often for littering the code with set_options.)

[Yaël Dillies]

And now I hit another false positive with omega: https://github.com/leanprover-community/mathlib4/pull/9000#discussion_r1589956524

[Damiano Testa]

The text-based script would probably benefit from the consequence of the multiple goal linter: if a proof is well-structured, then deduction that you make from indentations reflect better the actual proof evolution.

[Bolton Bailey]

Ok I made #12663 to exclude several more "flexible" tactics, including omega