Limits of Aesop?

Stream: lean4

[Siddhartha Gadgil]

@Jannis Limperg I was trying to use Aesop for automation, and reached a case where it reached an apparent hard limit, ending with an exhaustive search failure. Here is the example.

What I am trying to prove using Aesop is:

theorem Relator.LeftUnique.flip.{u_2, u_1} : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop},
  Relator.LeftUnique r → Relator.RightUnique (flip r) :=
fun {α} {β} {r} h x x_1 x_2 h₁ h₂ => h h₁ h₂

If I start dropping the arguments, at some point Aesop fails. Concretely, I get

example : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop},
  Relator.LeftUnique r → Relator.RightUnique (flip r) :=
fun {α} {β} {r} h    => by
 intro x
 aesop?

working and suggesting

Try this:
  intro b c a a_1
  apply h
  on_goal 2 => exact a_1
  exact a

but if I drop intro x Aesop seems unable to modify the first line to intro x b c a a_1 even if I remove all limits. Is there some reason why this step cannot be added to the search?

[Jannis Limperg]

To discover that the type after fun {α} {β} {r} is a forall, Aesop needs to unfold Relator.LeftUnique. I suspect that this is a def rather than an abbrev, but Aesop intro by default only unfolds reducible definitions. If that is indeed the culprit, you can change the transparency used by intro with aesop (options := { introsTransparency? := some .default }) (or similar; I'm not sure what exactly the option name was). Alternatively, you can add an explicit unfold rule for LeftUnique.

[Siddhartha Gadgil]

Thanks a lot. Indeed with that option it worked all the way (needed no fun). Is the only disadvantage a longer search, or are there cases where the intro prevents Aesop from proving?

[Siddhartha Gadgil]

In the latter case I will at least try both settings.

[Jannis Limperg]

Nice! The default setting prevents Aesop from over-eagerly punching through abstractions. Once you've developed the API for a def, you usually want to interact with the def-ed object only via its API. (With that said, aesop_cat uses introsTransparency := default globally.)

In a sensible rule set, punching through the abstraction should not prevent Aesop from proving a goal, but since rules can do anything, you can easily construct non-sensible rule sets.

[Siddhartha Gadgil]

My rulesets will be AI generated so often not sensible. But I have two options to experiment with: try multiple settings for introsTransparency and other such settings, and introduce unsafe rules for unfolding definitions that appear in the statement of a goal.

[Jannis Limperg]

For that use case, I would expect the more aggressive introsTransparency setting to be more useful than harmful.

[Siddhartha Gadgil]

It went both ways - some new stuff was proved and some stuff no longer proved. The following seems to be a bug though, as there is a panic for unreachable code in whnf:

#check Membership.mem.out
example: ∀ {α : Type u} {p : α → Prop} {a : α}, a ∈ {x | p x} → p a := by
  aesop (options := { introsTransparency? := some .default })

@Jannis Limperg is this known (my version of Aesop may be out of date).

[Siddhartha Gadgil]

In any case, it seems the best of both worlds is to have additional intro rules with other transparency settings as "unsafe" rules (copying and modifying Aesop' code). Will do this.

[Jannis Limperg]

Siddhartha Gadgil said:

The following seems to be a bug though, as there is a panic for unreachable code in whnf:

#check Membership.mem.out
example: ∀ {α : Type u} {p : α → Prop} {a : α}, a ∈ {x | p x} → p a := by
  aesop (options := { introsTransparency? := some .default })

This MWE works for me on current mathlib master:

import Mathlib

universe u

example: ∀ {α : Type u} {p : α → Prop} {a : α}, a ∈ {x | p x} → p a := by
  aesop (options := { introsTransparency? := some .default })

I recall fixing a bug that manifested as this whnf panic, so you probably just need to update Aesop.

[Siddhartha Gadgil]

Confirming that this bug is fixed in the latest mathlib aesop dependency.

[Siddhartha Gadgil]

Just to close this issue, when I added an unsafe tactic intro rule with default transparency by copy-pasting the code from Aesop with tinny modifications, Aesop could prove the above example (but excessive unfolding would still be avoided).

[Siddhartha Gadgil]

@Jannis Limperg I run into another limit of the intro rule, even with the transparency configuration (without it this fails earlier). Here is an example (the print refers to the actual statement, so the full proof from which this was built).

The following works fine. But if I drop the p from the intro statement then Aesop fails with an exhaustive search.

#print Set.antitone_setOf
example : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {p : α → β → Prop},
  (∀ (b : β), Antitone fun a => p a b) → Antitone fun a => {b | p a b} := by
    intro α β _ p
    aesop (options := { introsTransparency? := some .default })

[Siddhartha Gadgil]

The behaviour is the same with .all as transparency, and with other transparencies even the above fails.

[Siddhartha Gadgil]

(deleted)

[Jannis Limperg]

That one was indeed a plain bug (missing withContext :upside_down:). Now fixed on master. Thanks for the report!

[Siddhartha Gadgil]

@Jannis Limperg Another puzzle for me with Aesop. The following works as expected:

example : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R},
  U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1:= by
  aesop (add safe apply Iff.rfl)

But a variant fails with aesop failing after exhaustive search:

example : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R},
  U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1:= by
  aesop (add unsafe apply Iff.rfl)

What is it that can cause the unsafe search to fail lie this?

[Jannis Limperg]

Probably in the second example, some safe rule changes the goal before Iff.rfl can fire. If you have an MWE (doesn't have to be super minimal), I can take a look.

[Siddhartha Gadgil]

Thanks. Would that mean that the order of the safe rules is crucial?

I have a whole bunch of these but auto-generated. I will try to minimize one tomorrow morning (it is midnight in India). One more example is:

example : ∀ (o a : ONote),
  ONote.FundamentalSequenceProp o (Sum.inl (some a)) ↔
    ONote.repr o = Order.succ (ONote.repr a) ∧ (ONote.NF o → ONote.NF a) :=
  by aesop (add safe Iff.rfl)

Again, changing to unsafe breaks this.

[Siddhartha Gadgil]

@Jannis Limperg Thanks for pointing out about safe rules applying first. Indeed this is a case where splitting proving A ∧ B to separately proving A and B caused the next step to fail (so my use of Aesop is too naive, no error in Aesop).

But there is an issue to report: In exactly the same example if I aesop? the Try This is wrong. It introduces incorrect indentations so that the result is parsed as a single (incorrect) tactic.

[Jannis Limperg]

Yeah, this is a limitation of the Try this widget, which doesn't seem to be set up for multi-line output (or maybe the Lean pretty-printer is to blame; I don't know). I'm not sure where to report this.

[Siddhartha Gadgil]

Jannis Limperg said:

Yeah, this is a limitation of the Try this widget, which doesn't seem to be set up for multi-line output (or maybe the Lean pretty-printer is to blame; I don't know). I'm not sure where to report this.

Maybe ping the one who wrote the widget here?

[Jannis Limperg]

Discussed at #std4 > TryThis widget doesn't support multi-line suggestions (which turns out to be a misleading title).