Why does `fun_induction` depend on `clear`?

Stream: new members

[nrs]

In the theorem plus_eq_plus' below, if I don't clear the first inductive hypothesis with clear ih, I get an unusable inductive hypothesis at fun_induction plus nn m.succ, how come?. Is there a reason under the hood that explains how fun_induction's motive makes use of the ambient context?

def plus (n m : Nat) : Nat := match n with
| .zero => m
| .succ nn => (plus nn m).succ

def plus' (n m : Nat) : Nat := match n with
| .zero => m
| .succ nn => plus' nn m.succ

theorem plus_eq_plus' (n m : Nat) : plus' n m = plus n m := by
  fun_induction plus' with
  | case1 => rfl
  | case2 m nn ih =>
    rw [ih, plus]; clear ih
    fun_induction plus nn m.succ with
    | case1 => rfl
    | case2 nnn ih' => rw [ih', plus]

[Aaron Liu]

I'd imagine it's the same as how induction would do it

[Aaron Liu]

you generalize over the variable being inducted over and any local hypotheses mentioning that variable are put as assumptions in the inductive hypothesis

[nrs]

I see, thank you! If local hypotheses mentioning that variable are put as assumptions in the inductive hypothesis, does this immediately translate to just a change in the motive of the underlying recursor?

[Aaron Liu]

the recursor itself isn't changing at all, what is changing is the value being passed as the motive

[nrs]

Ah I see, that makes perfect sense, thanks!