theorems/tactic script used by aesop_cat_nonterminal

Stream: metaprogramming / tactics

[Robert Maxton]

It's noted that aesop_cat_nonterminal should generally be used only for exploration. Fair enough; but usually the exploration tactics are ? tactics that print a script or list of theorems used in the process. aesop_cat_nonterminal doesn't appear to, and aesop_cat_nonterminal? doesn't exist. I'm in a case where aesop_cat doesn't work (and aesop_cat? gives no advice), but aesop_cat_nonterminal produces a simplification that I don't know how to achieve myself. How can I trace its work?

[Jannis Limperg]

You can use aesop_cat? directly. aesop_cat_nonterminal just disables the warning about Aesop not being able to fully solve the goal. I would argue aesop_cat_nonterminal should be removed anyway; it's a maintainability footgun.

[Robert Maxton]

Well, that's the thing; aesop_cat? just failed on me, whereas aesop_cat_nonterminal didn't. But unfortunately I lost my MWE in the meantime, so I'll have to find a new example to report.

[Jannis Limperg]

Ah, that's weird. If you're able to reconstruct the MWE, I'd be happy to take a look.

[Robert Maxton]

@Jannis Limperg Okay, I ran into this again and turned it into a MWE.

import Mathlib.CategoryTheory.Monad.Basic
import Mathlib.CategoryTheory.Types

open CategoryTheory

class Comonad (w : Type u → Type v) where
  extract : ∀ {α : Type u}, w α → α
  extend : ∀ {α β : Type u}, (w α → β) → w α → w β

export Comonad (extract extend)

@[simp] def duplicate {w: Type u → Type u} [Comonad w] {α} : w α → w (w α) := Comonad.extend id

@[simps] instance [Comonad w] : Functor w where
  map f wα := extend (f ∘ extract) wα

instance instLawfulComonad {w : Type u → Type u} : Comonad w → CategoryTheory.Comonad (Type u) :=
  λ inst ↦ {
    obj := w
    map := Functor.map
    δ'  := by
      refine ⟨λ α ↦ ↾duplicate, ?_⟩
      aesop_cat?
  }

aesop_cat? fails and does nothing to the goal; aesop? fails to prove the goal but does simplify the goal, though without providing a script; aesop_cat_nonterminal gives a different (partial) simplification.

[Robert Maxton]

Ideally, I'd like aesop_cat? and aesop? to provide a script even if they fail to solve the goal, to reproduce its work without calling aesop nonterminally

[Alex J. Best]

Does https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/non-finishing.20.60aesop.3F.60/near/404962767 help you?

[Jannis Limperg]

Robert Maxton said:

aesop_cat? fails and does nothing to the goal; aesop? fails to prove the goal but does simplify the goal, though without providing a script; aesop_cat_nonterminal gives a different (partial) simplification.

This is all as expected I'm afraid. aesop? (and thus aesop_cat?) currently provides a script only when it fully solves the goal. Changing this has been on my todo list for a while. aesop_cat? sets Aesop's terminal option, which instructs it to fail when it can't fully solve a goal. aesop_cat_nonterminal uses the CategoryTheory rule set (unlike aesop?) and so produces a different simplification.