Zulip Chat Archive

Stream: new members

Topic: Determining What Aesop Applied Before Failing

Alex Duchnowski (Dec 12 2023 at 20:00):

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 (Dec 12 2023 at 20:10):

Maybe show_term aesop

Alex Duchnowski (Dec 12 2023 at 20:21):

Thanks for the suggestion. Unfortunately, that simply produces

Try this: refine ?_ x

which doesn't work. Any other ideas?

llllvvuu (Dec 12 2023 at 20:22):

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 (Dec 12 2023 at 20:23):

aesop? simply produces

aesop: failed to prove the goal after exhaustive search.

llllvvuu (Dec 12 2023 at 20:24):

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

Alex Duchnowski (Dec 12 2023 at 20:24):

I am, and I don't.

Alex Duchnowski (Dec 12 2023 at 20:37):

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"):

llllvvuu (Dec 12 2023 at 20:41):

Possibly aesop_destruct_products and/or repeat' apply And.intro

Alex Duchnowski (Dec 12 2023 at 21:05):

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

Ruben Van de Velde (Dec 12 2023 at 21:35):

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

llllvvuu (Dec 12 2023 at 22:41):

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 (Dec 14 2023 at 02:35):

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

Last updated: Dec 20 2023 at 11:08 UTC