Custom induction hypothesis

Stream: lean4

[Patrick Johnson]

How to use induction with custom hypothesis that does not represent an induction hypothesis?
Here is an example:

theorem ind2 {P : Nat → Prop} (h₁ : P 0) (h₂ : P 1) : ∀ (n : Nat), n < 2 → P n
  | 0, _ => h₁
  | 1, _ => h₂
  | (n+2), h => by cases h with | step h => cases h with | step h => cases h

def P : Nat → Prop
  | 0 => True
  | 1 => True
  | _ => False

example {n : Nat} (hn : n < 2) : P n := by
  induction n using ind2 with
  | h₁ => trivial
  | h₂ => trivial

Where am I supposed to use hn?

[Chris Bailey]

I think you're supposed to move it into the motive if you want it to be part of the induction:

theorem ind2 {P : ∀ (n : Nat), n < 2 → Prop} (h₁ : P 0 (by decide))  (h₂ : P 1 (by decide)) : ∀ (n : Nat) (h : n < 2), P n h
  | 0, _ => h₁
  | 1, _ => h₂
  | (n+2), h => by cases h with | step h => cases h with | step h => cases h

def P : Nat → Prop
  | 0 => True
  | 1 => True
  | _ => False

example {n : Nat} (hn : n < 2) : P n := by
  induction n, hn using ind2 with
  | h₁ => trivial
  | h₂ => trivial

[Patrick Johnson]

It works, but I'm not very happy with that solution. The hypothesis hn should be unrelated to P (motive). Making it a part of P forces us to needlessly add constraints to each induction hypothesis. It doesn't allow hypotheses to cover numbers for which hn does not hold (for example, it doesn't allow us to have hypothesis h₃ : ∀ (n : Nat), n < 10 → P n).

[Chris Bailey]

I agree in that I don't think a custom induction principle is the play here. The way you wrote it, n < 2 is a minor premise; how are you expecting it to be used?

[Jakob von Raumer]

Do you also get an error "tactic 'introN' failed, insufficient number of binders" there?

[Patrick Johnson]

If we give n < 2 a name in the statement of ind2 (for example (h₃ : n < 2)), then I am expecting induction to create three new goals: goal h₁ for P 0, goal h₂ for P 1 and goal h₃ for n < 2. But instead, induction gives the error: tactic 'introN' failed, insufficient number of binders

Even though n < 2 is not of the form P n or (... → P n), I don't see what prevents induction to create a new goal for it. An alternative way would be to revert everything except n and hn (assuming there are other assumptions), then use apply ind2, provide the motive explicitly (in case the elaborator cannot figure it out), and finally re-introduce the reverted assumptions in each subgoal created by apply. I would like induction to save me from this effort and I think this feature would be nice to have in Lean 4.

[Jakob von Raumer]

That's definitely a bug, induction should never try to introduce more binders than it has available...

[Jakob von Raumer]

Maybe ind2 is just not in the form that induction expects, but if so, induction should give another error

[Jakob von Raumer]

(Note that revert hn; refine ind2 ?_ ?_ n works perfectly fine)

[Patrick Johnson]

I'd be happy if we could call it a bug, but I'm afraid it's just an unimplemented feature, since it doesn't work in Lean 3 either. Nevertheless, I think it would be a nice feature to have (and I also think the support for this use case isn't too hard to implement).