Base Case for Induction on N+

Stream: new members

[Alex Gu]

Hi! I want to do induction on the positive natural numbers, but couldn't out the right syntax for the base case. I also couldn't manage to find it through searching Zulip and PNat's library. Thanks!

import Mathlib

theorem sum_first_n_odd_integers (n : ℕ+) :
  (∑ k in Finset.range n, 2*k + 1) = n^2 := by
  induction n with
  | ?? =>
    sorry

[Riccardo Brasca]

Not at the computer at the moment, but if you write induction n is there a yellow bulb in VS Code? If it's there click on "generate skeleton..." and it should do it for you.

[Alex Gu]

I didn't see it, maybe I didn't install some extension?

image.png

[Edward van de Meent]

an issue you'll run into here is that PNat is not an inductive type...

[Edward van de Meent]

rather, it's the subtype with 0 < n

[Etienne Marion]

Yes technically it is an inductive type but not in the same way as Nat

[David Renshaw]

You might try PNat.strongInductionOn

[David Renshaw]

induction n using PNat.strongInductionOn ...

[Edward van de Meent]

ah, i just found PNat.recOn

[Alex Gu]

what would be my base case for strong induction on PNat? how could I find that information?

[Edward van de Meent]

i suspect that in this case you are better helped with the following:

import Mathlib

theorem sum_first_n_odd_integers (n : ℕ+) :
    (∑ k in Finset.range n, 2*k + 1) = n^2 := by
  induction n using PNat.recOn with
  | p1 =>
    sorry
  | hp n hi =>
    sorry

[Edward van de Meent]

a friendly reminder that sometimes inductive principles are not called induction or similar because it can construct data. Instead those are named rec or similar.

[Edward van de Meent]

see also #naming

[Etienne Marion]

@loogle PNat, "rec"

[loogle]

:search: PNat.recOn, PNat.recOn_one, and 3 more

[Etienne Marion]

Indeed I forgot about rec!

[Riccardo Brasca]

Out of curiosity, does the yellow bulb work after induction n with...?

[Kyle Miller]

If someone were to add @[induction_eliminator] to PNat.recOn then it would automatically be used by the induction tactic. (It would be nice to adjust the names of the parameters too, perhaps one and succ?)

[Alex Gu]

thx! this is very helpful and I was able to finish the proof from here.

theorem sum_first_n_odd_integers (n : ℕ+) :
    (∑ k in Finset.range n, (2*k + 1)) = n^2 := by
  induction n using PNat.recOn with
  | p1 =>
    simp
  | hp n hi =>
    have h1 : ↑(n + 1 : ℕ+) = (↑n : ℕ) + 1 := by simp
    rw [h1]
    rw [Finset.sum_range_succ]
    rw [hi]
    ring

could you help me understand why for PNat, it has to be done in this way, while for natural numbers it's normally done with the constructor like zero and succ n ih?

[Alex Gu]

@Riccardo Brasca honestly i've never seen the yellow bulb, not sure how to get it

[Kyle Miller]

induction looks at the names of the parameters of the induction principle. They happen to be the names of constructors when the induction principle is generated from the inductive type.

[Riccardo Brasca]

You can try it with natural numbers, it should work out of the box

[Kyle Miller]

Here's where zero and succ come from:

#check Nat.recOn
/-
Nat.recOn.{u} {motive : ℕ → Sort u} (t : ℕ)
  (zero : motive Nat.zero) (succ : (n : ℕ) → motive n → motive n.succ) :
  motive t
-/

(Though more precisely, we use Nat.recAuxOn so that the result is in terms of 0 and n + 1 instead of Nat.zero and Nat.succ n.)

[Kyle Miller]

PNat.recOn uses p1 and hp for its parameter names, hence my suggestion that we rename them to something better.

[Etienne Marion]

Riccardo Brasca said:

Out of curiosity, does the yellow bulb work after induction n with...?

In the web editor it gives

import Mathlib

example (n : PNat) : True := by
  induction n with
  | mk val property => sorry

so no

[Kyle Miller]

Technically that's working. It's using the "induction principle" that comes from the definition of PNat.

[Kyle Miller]

val is the natural number, and property is that it's positive.

[Kyle Miller]

If you add in the using PNat.recOn clause to induction you can switch it to the more sensible induction principle

[Riccardo Brasca]

I mean if you write explicitly the induction principle you want to use

[Etienne Marion]

Ah sorry I misunderstood

[Etienne Marion]

so yes it works

[Alex Gu]

so if i wanted to use natural numbers, but want to start at, say, 3 rather than 0, what would be the way to do that? (e.g. if n>=3 is one of my hypothesis)

[Edward van de Meent]

Nat.le_induction

[Edward van de Meent]

Nat.leRec

[Etienne Marion]

Kyle Miller said:

If someone were to add @[induction_eliminator] to PNat.recOn then it would automatically be used by the induction tactic. (It would be nice to adjust the names of the parameters too, perhaps one and succ?)

#20617

[Julian Berman]

Kyle Miller said:

Technically that's working. It's using the "induction principle" that comes from the definition of PNat.

Just to ask explicitly -- it's not easily feasible to make separate code actions for all induction principles in the environment whose type somehow matches the term being passed to induction is it?

[Kyle Miller]

Oh, you mean like "populate code actions with a list of all relevant induction principles?"

[Kyle Miller]

Worst case maybe there could be an attribute to tag them, like induction_eliminator?

[Julian Berman]

Exactly yeah.