aesop.warn.applyIff

Stream: mathlib4

[Kim Morrison]

Aesop has just introduced a new warning in https://github.com/leanprover-community/aesop/commit/29cf094e84ae9852f0011b47b6ddc684ffe4be5f, which is triggering in Mathlib, generating warnings that look like

warning: ././././Mathlib/Data/Finset/Sups.lean:632:8: Apply builder was used for a theorem with conclusion A ↔ B. You probably want to use the simp builder.
Use `set_option aesop.warn.applyIff false` to disable this warning.

in many files.

For now in #17067 I'm just disabling this warning in Mathlib.

However I'm hoping someone could take over from here, and understand why these warnings are being generated, and if there is something we should be changing in Mathlib to avoid them.

[Eric Wieser]

Can you link to a CI log with those warnings?

[Eric Wieser]

I think this particular warning is fixed by the unmerged PR that provoked the addition of this warning flag

[Eric Wieser]

(#16927)

[Kim Morrison]

Eric Wieser said:

Can you link to a CI log with those warnings?

All the recent nightly-testing failures

[Eric Wieser]

You probably want to use the simp builder.

This was largely not the approach used in #16927. @Jannis Limperg, was the approach in that PR unusual, or should the warning message suggest creating aliases of apply lemmas as another alternative?

[Yaël Dillies]

That might be a question for me

[Yaël Dillies]

The reason we couldn't use the simp builder here is that proveFinsetNonempty calls aesop with simp disabled, for performance. Whether that's an usual situation, I don't know. I would guess not.

[Yaël Dillies]

Certainly the warning could suggest adding apply aliases as an alternative. That shouldn't hurt

[Jannis Limperg]

Eric Wieser said:

You probably want to use the simp builder.

This was largely not the approach used in #16927. Jannis Limperg, was the approach in that PR unusual, or should the warning message suggest creating aliases of apply lemmas as another alternative?

Good point, I'll add this as an alternative suggestion.

[Jannis Limperg]

Yaël Dillies said:

The reason we couldn't use the simp builder here is that proveFinsetNonempty calls aesop with simp disabled, for performance. Whether that's an usual situation, I don't know. I would guess not.

You could try disabling the default simp set (aesop (config := { useDefaultSimpSet := false })) and tagging the iff lemmas with @[aesop simp (rule_sets := [...])]. That way, Aesop's simp will only apply the iff lemmas, which should be quite fast. (Of course, the current strategy is even faster, but it is also a bit less powerful.)

[Jannis Limperg]

Sorry for introducing this warning without warning. I should have notified you all of the likely breakage.

[Yaël Dillies]

Jannis Limperg said:

Of course, the current strategy is even faster, but it is also a bit less powerful.

Given that proveFinsetNonempty is used in positivity (every time some finset operation appears, like Finset.sum), which is itself used in gcongr, I think I want to keep disabling simp entirely for now. Once we have more uses of positivity on finset operations, we will be able to run some benchmark.

[Jannis Limperg]

Makes sense. simp is indeed by far the most expensive thing Aesop does.