Doc clarification on forward rules with no immediates

[ammkrn]

The README states the following about forward rules and immediates:

When no immediate names are given, Aesop considers every argument immediate, except for instance arguments and dependent arguments (i.e. those that can be inferred from the types of later arguments).

When a forward rule has been successfully applied, it will not be tried again when processing its subgoals (and their subgoals, etc.). Without this limit, many forward rules would be applied infinitely often.

However, when aesop can't actually solve the current goal, a forward rule with no identified immediates can cause timeouts, seemingly because it behaves as though there are no immediates at all:

@[aesop unsafe forward]
theorem sub_lt_of_lt' (a b : Nat) (h : a < b) : (a - 1) < b := 
  Nat.lt_of_le_of_lt (Nat.sub_le a 1) h

-- Produces a long list of `fwd_n` hypotheses of the form `a - 1 - 1 - 1 (...) - 1 < b`, then times out
set_option trace.aesop true in
example (a b : Nat) (h : a < b) : False := by
  aesop (options := { maxRuleApplicationDepth := 10 })

For this example, the description in the README suggests that the aesop invocation would fail after only one attempt at applying the sub_lt_of_lt' rule, since a and b are explicit arguments, and would automatically be considered immediates (and because the rule succeeded once with those immediates).

Am I reading the docs wrong or is my understanding of something else in the forward application off? Thanks!

[JLimperg]

This loop is expected: the theorem will be applied first to h : a < b (with a := a), then to h1 : a - 1 < b (with a := a - 1), and so on.

However, the docs were indeed a bit fuzzy. I've added a hopefully clearer description of the loop breaking approach.