Determining What Aesop Applied Before Failing

Stream: new members

[Alex Duchnowski]

I have several proofs where aesop fails to close the goal but applies several intro rules that decompose my goal into simpler subgoals with a richer context. However, editing the proof results in a long wait before my context updates because aesop is running all over again, so I'd like to replace it with an explicit use of the rules its applying. aesop? fails to produce any useful output. How can I find out the rules that aesop applied to create the useful context?

[Ruben Van de Velde]

Maybe show_term aesop

[Alex Duchnowski]

Thanks for the suggestion. Unfortunately, that simply produces

Try this: refine ?_ x

which doesn't work. Any other ideas?

[llllvvuu]

What was the issue with the aesop? output? Usually that works pretty well for me after cleaning up / removing the rename, unhygienic, with_reducible, change aesop_subst to subst, and then try deleting tactics / simp lemmas until it doesn't work anymore

[Alex Duchnowski]

aesop? simply produces

aesop: failed to prove the goal after exhaustive search.

[llllvvuu]

Are you using VSCode? Do you get no "Try this:"?

[Alex Duchnowski]

I am, and I don't.

[Alex Duchnowski]

Not sure if this context is useful, but here is my Tactic state before and after aesop (with my cursor to the left of the "a" and to the right of the "p"):
Before:
image.png
After:
image.png

[llllvvuu]

Possibly aesop_destruct_products and/or repeat' apply And.intro

[Alex Duchnowski]

Oh sweet, thanks! How do I name all the daggered variables in my context produced by aesop_destruct_products?

[Ruben Van de Velde]

rename_i is the hacky way; not sure if there's anything better in this case

[llllvvuu]

Depending on your proof strategy you might not need those products destructed at all. Or maybe there is some manual way to do it using rw [show x = (x.1, x.2) by rfl] at * or something (not sure of the syntax)

[Alex J. Best]

You could try the trick I mentioned in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/non-finishing.20.60aesop.3F.60/near/404962767 also perhaps