zetaDelta in Aesop simp

Stream: lean4

[Kim Morrison]

@Jannis Limperg, how would you feel about setting simp_config := {zetaDelta := true} by default in aesop?

I've done so in aesop_cat on nightly-testing in Mathlib, but there are plain aesop calls that fail now because it won't unfold let.

[Jannis Limperg]

I'm not enthusiastic about diverging from the default config, for two reasons:

1. It's surprising if the simp in Aesop is a slightly different simp than the usual one.
2. aesop? has to output simp_all { zetaDelta := true } instead of simp_all.

I see three ways to address these issues:

1. Enable zetaDelta for simp_all in core. I feel like this might make sense since simp_all is supposed to use all hypotheses. simp_all already enables contextual, so there's precedent.
2. Optimise aesop? output to replace simp_all { zetaDelta := true } with simp_all where possible. I'm working on this capability anyway (slowly and intermittently).
3. Include expanded lets in the theorem list generated by simp?. Maybe this already happens; if so, issue 2 is already solved.

[Yaël Dillies]

Solution 1 sounds the most sensible to me

[Kim Morrison]

Okay, 1. seems pretty difficult to squeeze in between now and the release. Today is feels rather unlikely an on time release is possible, because Mathlib is still quite broken, and I would prefer to avoid solutions that require further round-trips with Lean updates.

[Kim Morrison]

I will get the ball rolling, but if I think in the meantime we are going to have to replace aesop in Mathlib with aesop_foo, that changes the simp_config.

[Jannis Limperg]

Scott Morrison said:

I will get the ball rolling, but if I think in the meantime we are going to have to replace aesop in Mathlib with aesop_foo, that changes the simp_config.

If that's the alternative, then I'd rather enable zetaDelta in Aesop as a stopgap measure, without adjusting the output of aesop?. This means aesop? will be borked whenever a proof relies on zetaDelta, but that seems like the lesser evil.

[Kim Morrison]

@Jannis Limperg how about the following. It will require more engineering but seems to give a nice result.

When aesop calls simp, it collects let bindings and passes them to simp (i.e. "explicitly" without zetaDelta). It then uses the simp.trace information in proof reconstruction, to only include any let bindings that were actually simplified.

[Kim Morrison]

In the meantime, however, I'd be happy with having aesop with zetaDelta enabled, but without adjusting aesop?.

[Jannis Limperg]

Scott Morrison said:

Jannis Limperg how about the following. It will require more engineering but seems to give a nice result.

When aesop calls simp, it collects let bindings and passes them to simp (i.e. "explicitly" without zetaDelta). It then uses the simp.trace information in proof reconstruction, to only include any let bindings that were actually simplified.

Okay, I'll take a shot at implementing this.

[Jannis Limperg]

Implemented here. aesop? is still borked due to lean4#3519. I also opened an RFC for enabling zetaDelta by default in simp_all and simp [*]: lean4#3520.

[Notification Bot]

10 messages were moved here from #lean4 > Aesop dev updates by Jannis Limperg.