RFC: Allow `induction` to work without targets and to assign metavariables

Proposal

The introduction of complex arguments to induction and cases allows for a wider variety of induction principles. However, it is still not possible to use induction principles like List.foldlRecOn which only have complex arguments. A workaround currently is to add a dummy parameter:

def List.foldlRecOn' {motive : Unit → β → Sort _} (l : List α) (op : β → α → β)
    {b : β} (init : ∀ x, motive x b) (step : ∀ x b, motive x b → (a : α) → a ∈ l → motive x (op b a))
    (dummy : Unit) : motive dummy (List.foldl op b l) :=
  List.foldlRecOn l op (init dummy) (step dummy)

example {xs : List Nat} : xs.foldl (· + ·) 1 > 0 := by
  have : Unit := ()
  induction this using List.foldlRecOn'

There is however still another problem which is that induction doesn't try to assign the unknown variables l, op and b by unification in the goal, creating new goals for them and thus making it necessary to instead specify them explicitly:

example {xs : List Nat} : xs.foldl (· + ·) 1 > 0 := by
  have : Unit := ()
  induction this using List.foldlRecOn' xs (· + ·) (b := 1)

In other examples where these parameters are longer to write down this can be quite a hassle though. Ideally it would be possible to write down the induction as is without targets and let induction find the foldl in the goal and assign the variables accordingly:

example {xs : List Nat} : xs.foldl (· + ·) 1 > 0 := by
  induction using List.foldlRecOn
  /-
  goals:
  xs : List Nat
  ⊢ 1 > 0
  xs : List Nat
  b : Nat
  hb : b > 0
  a : Nat
  ha : a ∈ xs
  ⊢ b + a > 0
  -/

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

The relevant entry points named here are the induction tactic and List.foldlRecOn; begin by tracing how induction handles complex arguments and target inference. Done means induction can run without targets, infer l, op, and b from the goal, and create the displayed induction goals. Locate and run the repository’s existing tactic tests to verify the behavior.