Aesop maxRuleApplicationDepth

Stream: general

[Bolton Bailey]

Trying to get aesop to one-shot the following lemma

attribute [aesop safe cases] Nat
attribute [aesop safe constructors] List

-- set_option maxRuleApplicationDepth 35 -- When uncommented "unknown option 'maxRuleApplicationDepth'"

@[simp]
theorem getD_map {n : ℕ} (f : α → β) : (map f l).getD n (f d) = f (l.getD n d) := by
  aesop
   -- aesop: failed to prove the goal. Some goals were not explored because the maximum rule application depth (30) was reached. Set
  -- option 'maxRuleApplicationDepth' to increase the limit.

  -- The working proof:
  -- induction l generalizing n with
  -- | nil => rfl
  -- | cons head tail ih =>
  --   aesop

What is the correct way to set the option aesop is telling me to set?

[Alex J. Best]

If you look at the aesop readme it explains how https://github.com/JLimperg/aesop#the-aesop-tactic, I found this answer by grepping for maxRuleApplicationDepth in mathlib + deps

[Jannis Limperg]

Aesop is not trying to tell you that you should necessarily increase this limit. You should only increase it if you really want to look for proofs with more than 30 steps. ;) In this case, that likely won't help because Aesop doesn't know how to do induction (and this is a deliberate choice). So I would write

induction l generalizing n <;> aesop

[Jannis Limperg]

Ah, you probably added a custom induction rule for lists. In that case, your rule probably loops, generating longer and longer proof attempts, which the maxRuleApplicationDepth cuts short at 30.

[Bolton Bailey]

I am interested in trying to get aesop to do the induction. Is there an accepted way of adding an induction lemma to the things aesop uses?

[Bolton Bailey]

Is there a particular lemma that encapsulates the concept of "induction on lists"? Like docs#List.reverseRecOn by without the reverse?