aesop config: `assumption` multiplies goals?

Stream: metaprogramming / tactics

[Robert Maxton]

Consider the following MWE:

import Mathlib.Init.Data.Quot

import Aesop


attribute [simp] EqvGen.refl
attribute [aesop unsafe 30% destruct] EqvGen.symm

/--A class representing antisymmetry "up to" some equivalence relation
`eqv`. That is, if `rel x y` and `rel y x`, then `eqv x y`.

As with `Quot`, `eqv` need not actually be an equivalence relation, in which
case `AntiSymmUpTo eqv rel` is equivalent to `AntisymmUpTo (EqvGen eqv) rel`-/
class AntisymmUpTo (eqv: α → α → Prop) (rel: semiOutParam (α → α → Prop))  where
  antisymm : ∀ {x y}, rel x y → rel y x → EqvGen eqv x y

@[aesop safe destruct]
theorem antisymm_upto_eqv {rel : α → α → Prop} {x y : α} :
    AntisymmUpTo ε rel → rel x y → rel y x → EqvGen ε x y :=
  (·.antisymm)

section

  variable
    {l : List α} {eqv : α → α → Prop} {rel : α → α → Prop}
    [AntisymmUpTo eqv rel]
  variable
    {l_ty : List (α → Sort v)}
    {εv   : {β : Type v} → β → β → Prop}
    {relv : {β : Type v} → β → β → Prop}
    [∀ β, @AntisymmUpTo β, εv relv]

  set_option trace.aesop true in
  theorem forall_in_pair' (h₁ : rel x y) (h₂ : rel y x): ∀ u ∈ [x, y], ∀ v ∈ [x, y], EqvGen eqv u v :=
    by aesop

[Robert Maxton]

XY: I would like to solve this problem by getting typeclass search working; unfortunately, the only thing that makes simp_all reliably work is outParam when only one matching instance is in scope, and it's entirely reasonable for multiple different rels to generate the same eqv. Moving the outParam to eqv did occur to me as a solution, but that breaks the moment I allow type-dependent relations like relv and εv in the MWE whose types are compatible with rel and eqv. I'm not entirely sure why -- the infoview will tell me quite directly that it can't synthesize an AntisymmUpTo eqv rel even when all parameters are provided and there's an instance in the infoview -- but that appears to be the case.

[Robert Maxton]

I'm trying to work around that problem by using aesop instead of simp_all, using forward reasoning from the existence of instances and relevant hypotheses to get around instance-search failures. Unfortunately, that also fails, and I'm having trouble figuring out what to do about it.

[Robert Maxton]

Tracing aesop in the above, I notice that aesop repeatedly manages to reduce the state in various subgoals to things like

...
fwd : EqvGen eqv x y
fwd_1 : EqvGen eqv y x
⊢ EqvGen eqv x y

which it naturally tries to close by assumption. But when it does, assumption somehow spawns anywhere from one to three new goals, some of which are just duplicates of old goals. So, it makes negative progress for a while before realizing it's not getting anywhere and giving up (before even trying unsafe rules like EqvGen.symm, which I intended to be a workaround.)

[Robert Maxton]

Is there anything more I can do to make aesop cooperate here?

[Robert Maxton]

EDIT: Found a minor bug in the MWE, the second AntisymmUpTo instance was bugging out because it couldn't infer its implicit type. Fixing that at least makes it so that apply and specialize can find the instance when I pin it down all the way to AntisymmUpTo eqv rel, but it still can't infer the right instance from AntisymmUpTo ?eqv rel or the like on its own.