Aesop? suggestions on multi arm tactics

Stream: lean4

[Shreyas Srinivas]

one Screenshot from 2025-04-15 15-10-00.png

I have an induction goal that I can close with aesop. Even though I don't need this, I would like to use the output of aesop? instead. However, aesop? provides me five separate try this?s instead of one. Each suggestion is meant to work for one branch of the induction tactic. Is there a way to just one common suggestion?

[Shreyas Srinivas]

To make it clear, I have already solved the problem by taking the simp lemmas suggested in each try this and pasting them together in a try simp_all:
Screenshot from 2025-04-15 15-13-00.png

[Shreyas Srinivas]

I just wish to know if I can instead get one try this which gives a common proof that works on all branches

[Jannis Limperg]

I'm not sure whether I can detect, from within each Aesop call, that the different calls belong together. If so, something could be done, though I would likely just generate first | alt1 | alt2 | ..., which is maybe not much better. Please feel free to open an issue.

[Shreyas Srinivas]

So one trick might be to merge all the proofs by concatenating them in sequence with try on each suggestion

[Shreyas Srinivas]

Oh I just remembered that first | .. does that

EDIT : maybe first | try alt1 | try alt2 |..?

[Eric Wieser]

As a much simpler test-case:

import Aesop

example (p : P) (q : Q) (r : R) (s : S) : (P × Q) × (R × S) := by
  constructor <;> constructor <;> aesop?

[Eric Wieser]

In this particular case you could produce

example (p : P) (q : Q) (r : R) (s : S) : (P × Q) × (R × S) := by
  constructor <;> constructor <;> [(· exact p); (· exact q); (· exact r); (· exact s)]

but this doesn't work if the proof started as

example (p : P) (q : Q) (r : R) (s : S) : (P × Q) × (R × S) := by
  constructor <;> (constructor <;> aesop?)

[Shreyas Srinivas]

And the results of aesop? suggestions can be concatentated as :

import Aesop

example (p : P) (q : Q) (r : R) (s : S) : (P × Q) × (R × S) := by
  constructor <;>
  constructor <;>
    try exact p; try exact q; try exact r; try exact s

[Eric Wieser]

@Shreyas Srinivas, this is just first | exact p | exact q | exact r | exact s which was what Jannis suggested earlier

[Shreyas Srinivas]

Anyway, in my example all I had to do was put a try in front of the terminal simp_all suggestion and concatenate the lemma list. I guess this is harder to infer in general.

[Eric Wieser]

try is worse than putting first |

[Shreyas Srinivas]

alternatively, maybe aesop could look at the named goals, generate the arms and fill them in like you already showed