Leo pointed out that in a definition like

def app : List α → List α → List α 
  | [], bs => bs
  | a::as, bs => a :: app as bs

/--
info: app.induct.{u_1} {α : Type u_1} (motive : List α → List α → Prop) (case1 : ∀ (bs : List α), motive [] bs)
  (case2 : ∀ (a : α) (as bs : List α), motive as bs → motive (a :: as) bs) (a✝ a✝¹ : List α) : motive a✝ a✝¹
-/
#guard_msgs in
#check app.induct

the motive depends on the second argument for no good reason. This makes proofs like the following tricky:

example : app xs [] = xs := by
 generalize h : [] = bs
 induction xs, bs using app.induct <;> simp_all [app]

It would be easier to use if the second argument was a parameter of the induction principle (or dropped altogether, as it would be if the arguments to app were swapped.

I see three possible implementations:

• Change the recursive function preprocessing to sort all such fixed arguments to the front, so that the fixedPrefix contains all of them. But I am wary of the complexity of such a surgery, and that it would affect a lot of already hairy code (e.g. in mutual recursion).

  But it indeed is possible even for mutual recursion, for every recursive call we get a graph from parameters to arguments when and where they are passed unchanged, and thus be able to identify fixed parameters even across mutual recursive functions. (A bit similar to how GuessLex works). Then we can pull them to the front, subsuming the “fixedPrefix” handling.

  Extra complication with structural recursion: We must not treat the recursive parameter’s indices as parameters, and thus also no parameter that depends on these indices.

• During the creation of the functional induction principle, do two passes: One like know, then notice which targets of the motive are actually never refined, and then a second one with fewer targets motive. This is something I planned to do for fun_cases anyways, so if this works well here too, then that’s easiest.

  Maybe works for structural, but not for wf recursion, where the unary principle generation doesn’t really know much about components.

• Post-hoc, recognize these cases by looking at the motive occurrences and that one argument is always the same, and then specializing this with a new motive that ignores that argument, and (to still use the old theorem) move it to the parameter list.

  This likely only makes sense for non-mutual recursion.

  Maybe, if it can be proven to be inhabited and not it’s mentioned otherwise (e.g. in hypotheses from if-then-else), drop it completely. (But dangerous if realized in different contexts with different Inhabited instances).

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.