Why do `cases` and `induction ... using` differ

Stream: lean4

[Leni Aniva]

e.g.

theorem ex_cases_or (p : Prop) (hpp : p ∨ p) : p := by
  cases hpp <;> assumption
#print ex_cases_or
theorem ex_induction_or (p : Prop) (hpp : p ∨ p) : p := by
  induction hpp using Or.casesOn <;> assumption
#print ex_induction_or

In this case, the expressions are

theorem ex_cases_or : ∀ (p : Prop), p ∨ p → p :=
fun p hpp => Or.casesOn (motive := fun t => hpp = t → p) hpp (fun h h_1 => h) (fun h h_1 => h) (Eq.refl hpp)

theorem ex_induction_or : ∀ (p : Prop), p ∨ p → p :=
fun p hpp => Or.casesOn hpp (fun h => h) fun h => h

In Lean/Meta/Tactic/Cases.lean, cases calls induction in its implementation, so why does it behave differently?

[Kyle Miller]

The situation is that they both use the same underlying framework, which happens to use "induction" in the name, but both cases and induction are different frontends to this backend.

They both use the same underlying framework, but cases can handle indexed inductive types where the indices aren't variables. It basically does generalize on all the indices for you automatically. I'm not sure why this restriction is in place exactly. Maybe it's because otherwise the inductive hypotheses will have all these additional equality hypotheses? Or maybe it could be done but induction would need to work out which of these generalized variables should be added to the generalizing clause, and that hasn't been done yet?

It looks like the difference in your examples is from cases not being efficient with its generalizations.

[Jad Ghalayini]

On a related note, is there any way to make induction do the generalization?

[Kyle Miller]

Unfortunately no, you have to generalize manually.

[Leni Aniva]

Kyle Miller said:

The situation is that they both use the same underlying framework, which happens to use "induction" in the name, but both cases and induction are different frontends to this backend.

They both use the same underlying framework, but cases can handle indexed inductive types where the indices aren't variables. It basically does generalize on all the indices for you automatically. I'm not sure why this restriction is in place exactly. Maybe it's because otherwise the inductive hypotheses will have all these additional equality hypotheses? Or maybe it could be done but induction would need to work out which of these generalized variables should be added to the generalizing clause, and that hasn't been done yet?

It looks like the difference in your examples is from cases not being efficient with its generalizations.

Does this mean any instance of cases can be replaced by induction?

[Kyle Miller]

Can you expand on what you mean? Because what I was saying is that cases has an additional feature that induction doesn't have, so you can't replace the token cases with induction and expect it to work.

[Leni Aniva]

Kyle Miller said:

Can you expand on what you mean? Because what I was saying is that cases has an additional feature that induction doesn't have, so you can't replace the token cases with induction and expect it to work.

Is it possible to replace every single instance of cases with induction combined with revert or generalize?

[Kyle Miller]

Seems plausible. You might often need rename_i as well.