Correct formulation of induction principles

Stream: mathlib4

[Heather Macbeth]

@Rob Lewis and I are playing with induction problems in mathlib4 and encountered a case where perhaps (a) an induction principle in mathlib4 is stated wrongly, (b) we are using the wrong syntax with the induction tactic, or (c) there is an undocumented limitation in the implementation of the induction ... using ... syntax.

-- lemma from `Mathlib.Data.Nat.Basic`
@[elab_as_elim]
theorem Nat.le_induction {P : Nat → Prop} {m} (h0 : P m)
    (h1 : ∀ n, m ≤ n → P n → P (n + 1)) :
    ∀ n, m ≤ n → P n :=
  sorry

example (n : Nat) (hn : 2 ≤ n) : 4 ≤ 2 * n := by
  induction n using Nat.le_induction
  -- tactic 'introN' failed, insufficient number of binders

Any ideas?

[Chris Hughes]

Shouldn't it be induction hn? I can't test these ideas from where I am right now

[Heather Macbeth]

Interesting -- that gives

target
  hn
has type
  2 ≤ n : Prop
but is expected to have type
  ℕ : Type

[Chris Hughes]

I would also be tempted to make n implicit

[Heather Macbeth]

In the example statement? It doesn't seem to affect anything.

[Chris Hughes]

I'm at a loss then

[Eric Wieser]

Does making P take a m ≤ n argument help?

[Heather Macbeth]

@Eric Wieser I'm not sure I'm implementing your suggestion correctly, but in my version it doesn't work.

@[elab_as_elim]
theorem Nat.le_induction {m} {P : ∀ (n : Nat) (hn : m ≤ n), Prop} (h0 : P m sorry)
    (h1 : ∀ (n : Nat) (hn : m ≤ n), P n hn → P (n + 1) sorry) :
    ∀ (n : Nat) (hn : m ≤ n), P n hn :=
  sorry

example (n : Nat) (hn : 2 ≤ n) : 4 ≤ 2 * n := by
  induction n using Nat.le_induction
  -- insufficient number of targets for 'Nat.le_induction'

[Eric Wieser]

Does using hn instead of n work with that?

[Heather Macbeth]

If you mean the syntax

example (n : Nat) (hn : 2 ≤ n) : 4 ≤ 2 * n := by
  induction hn using Nat.le_induction

this gives

target
  hn
has type
  2 ≤ n : Prop
but is expected to have type
  Nat : Type

[Eric Wieser]

induction n, hn using?

[Eric Wieser]

I vaguely remember there being support for simultaneous induction

[Heather Macbeth]

Yes!

@[elab_as_elim]
theorem Nat.le_induction {m} {P : ∀ (n : Nat) (hn : m ≤ n), Prop} (h0 : P m sorry)
    (h1 : ∀ (n : Nat) (hn : m ≤ n), P n hn → P (n + 1) sorry) :
    ∀ (n : Nat) (hn : m ≤ n), P n hn :=
  sorry

example (n : Nat) (hn : 2 ≤ n) : 4 ≤ 2 * n := by
  induction n, hn using Nat.le_induction <;> clear n
  case _ =>
    /-
    ⊢ 4 ≤ 2 * 2
    -/
    sorry
  case _ k hk IH =>
    /-
    k : Nat
    hk : 2 ≤ k
    IH : 4 ≤ 2 * k
    ⊢ 4 ≤ 2 * (k + 1)
    -/
    sorry

[Heather Macbeth]

So should docs4#Nat.le_induction be changed?

[Eric Wieser]

Does it only work with my modification?

[Eric Wieser]

Certainly my spelling is syntactically more general

[Eric Wieser]

I think it unified poorly in Lean 3; so in places we have both versions, one primed

[Heather Macbeth]

Eric Wieser said:

Does it only work with my modification?

I'm not sure what you're asking here, but to be more precise, both the following fixes are required, neither works alone:

• change the statement of docs4#Nat.le_induction to the dependent version you suggested
• change the syntax from induction n to induction n, hn

[Heather Macbeth]

Eric Wieser said:

I think it unified poorly in Lean 3; so in places we have both versions, one primed

I checked the docs and this is not such a case (I don't see any variants). But if you like I can keep both versions rather than just the new one. Let me know.

[Heather Macbeth]

Is there a way to identify other induction principles that might be broken?

[Eric Wieser]

I think having only the dependent one is fine since it works with induction now

[Eric Wieser]

docs#submodule.span_induction' is the primed one I was thinking of.

[Eric Wieser]

(neither that nor the regular version work with the induction tactic in lean 3, I think due to the R : Type argument)

[Eric Wieser]

Heather Macbeth said:

Is there a way to identify other induction principles that might be broken?

Just look at everything with elab_as_eliminator?