## Stream: Is there code for X?

### Topic: induction on n where n ≠ 0

#### Benjamin Davidson (Jan 29 2021 at 00:42):

Is there a tactic like induction but that takes into account the existence of an assumption n ≠ 0?

#### Yakov Pechersky (Jan 29 2021 at 00:44):

Why not

induction n with n hn,
...


#### Benjamin Davidson (Jan 29 2021 at 00:45):

That's what I did but I am wondering if there's a built-in alternative

#### Anne Baanen (Jan 29 2021 at 10:40):

I don't expect that this specific version of induction is avalable in mathlib, the closest equivalent I know is docs#nat.le_induction. You might be able to call that with induction n using nat.le_induction.

#### Anne Baanen (Jan 29 2021 at 10:41):

But induction is pretty picky about the induction principles you can be using.

#### Kevin Buzzard (Jan 29 2021 at 11:02):

What does induction' do? Of course you can just make your own induction principle and then apply it.

#### Patrick Massot (Jan 29 2021 at 11:18):

You need to watch Jannis' CPP talk.

#### Kevin Buzzard (Jan 29 2021 at 15:47):

I looked for this but couldn't find the link :-(

#### Riccardo Brasca (Jan 29 2021 at 16:08):

There is pnat.strong_induction_on but you have to convert your statement to use pnat.

#### Benjamin Davidson (Jan 30 2021 at 07:22):

Anne Baanen said:

I don't expect that this specific version of induction is avalable in mathlib, the closest equivalent I know is docs#nat.le_induction. You might be able to call that with induction n using nat.le_induction.

@Anne Baanen This seems to be what I want, but induction n using nat.le_induction doesn't work. Do you know how else I can invoke that lemma?

#### Eric Wieser (Jan 30 2021 at 08:45):

Are you looking for obtain ⟨k, rfl⟩ := nat.exists_eq_succ_of_ne_zero hn? docs#nat.exists_eq_succ_of_ne_zero

#### Benjamin Davidson (Jan 30 2021 at 20:25):

@Eric Wieser Followed by induction k? I think that would accomplish what I'm looking for. However, the downside is that later I would need to use something like Exists.intro (succ k) rfl so that I won't have to deal with k.succ.succ everywhere (please correct me if that's not true or there's a better way to deal with that).

#### Benjamin Davidson (Jan 30 2021 at 20:34):

(I know I can leave everything in terms of k.succ.succ but that would make my proof very messy)

#### Eric Wieser (Jan 30 2021 at 22:05):

I don't really understand what you're asking for

#### Benjamin Davidson (Jan 31 2021 at 01:03):

docs#nat.exists_eq_succ_of_ne_zero allows me to work with a base case of n=1, which is what I am looking for. However, using it also means that my inductive step will be in terms of k.succ.succ instead of n.succ. I know that k.succ.succ is equal to n.succ, so technically this isn't a problem, but for stylistic reasons it is preferable to me to have things in terms of n.succ and not k.succ.succ. This means that I will essentially have to "undo" what docs#nat.exists_eq_succ_of_ne_zero does, which seems silly. I'm asking if there's a way to avoid the mess with k.succ.succ entirely.
Sorry if things are still unclear. I can try to put together an MWE if you think that will help.

#### Alex J. Best (Jan 31 2021 at 03:53):

Riccardo Brasca said:

There is pnat.strong_induction_on but you have to convert your statement to use pnat.

Seems like nat -> pnat can lift instances were missing to make this easier to do in a tactic block, so I've added #5977

#### Eric Wieser (Jan 31 2021 at 04:41):

Are you looking for obtain ⟨k, hk⟩ := nat.exists_eq_succ_of_ne_zero hn (note: hk instead of rfl)?

#### Benjamin Davidson (Jan 31 2021 at 04:46):

I had tried that but it causes problems: I need the assumption n = k.succ in order to use the inductive hypothesis when really n = k.succ.succ is true.

#### Eric Wieser (Jan 31 2021 at 04:54):

Then I still don't understand your problem. If your mathematical statement isn't "given n is not 0, P n can be proven by showing P 1 and P (k + 1) -> P (k + 2)", then what is it?

#### Benjamin Davidson (Jan 31 2021 at 05:44):

That is what I'm trying to prove, what I'm running into with that is more of a technical problem. I've put together an mwe:

import data.nat.basic

example {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) : p n :=
begin
obtain ⟨k, hk⟩ := nat.exists_eq_succ_of_ne_zero hn,
induction k with k ih,
{ sorry },
/-
case nat.succ
p : ℕ → Prop,
n : ℕ,
hn : n ≠ 0,
k : ℕ,
ih : n = k.succ → p n,
hk : n = k.succ.succ
⊢ p n
-/
end


Obviously the very thing I am trying to prove is "since it is true for k.succ it is true for k.succ.succ," but I'm not sure how I can call ih in its above state.

Interestingly, I've found that I can do as follows:

import data.nat.basic

example {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) : p n :=
begin
obtain ⟨k, rfl⟩ := nat.exists_eq_succ_of_ne_zero hn,
induction k with k ih,
{ sorry },
let m := k.succ,
...
end


and then complete the proof in terms of m.

#### Mario Carneiro (Jan 31 2021 at 05:51):

It might help to state a mwe that is actually provable, by adding appropriate hypotheses about p n

#### Benjamin Davidson (Jan 31 2021 at 05:52):

Sure. I'll post the actual proof I'm working on. I was trying to demonstrate with something more general.

#### Mario Carneiro (Jan 31 2021 at 05:53):

I mean a general induction lemma

#### Eric Wieser (Jan 31 2021 at 05:53):

Your first example should work if you use induction k generalizing n

#### Mario Carneiro (Jan 31 2021 at 05:53):

for example

example {p : ℕ → Prop} (H1 : p 1) (H2 : ∀ m, p m → p (m+1))
{n : ℕ} (hn : n ≠ 0) : p n := sorry


#### Mario Carneiro (Jan 31 2021 at 05:54):

adjust the statements of H1 and H2 until they match the assumptions you want

#### Benjamin Davidson (Jan 31 2021 at 06:22):

import data.nat.basic

example {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) (h1 : p 1) (h2 : ∀ {m}, p m → p (m+1)) :
p n :=
begin
obtain ⟨k, hk⟩ := nat.exists_eq_succ_of_ne_zero hn,
induction k with k ih,
{ simpa only [hk] },
/-
case nat.succ
p : ℕ → Prop,
n : ℕ,
hn : n ≠ 0,
h1 : p 1,
h2 : ∀ {m : ℕ}, p m → p (m + 1),
k : ℕ,
ih : n = k.succ → p n,
hk : n = k.succ.succ
⊢ p n
-/
end

example {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) (h1 : p 1) (h2 : ∀ {m}, p m → p (m+1)) :
p n :=
begin
obtain ⟨k, rfl⟩ := nat.exists_eq_succ_of_ne_zero hn,
induction k with k ih,
{ exact h1 },
{ let n := k.succ,
exact h2 (ih (nat.succ_ne_zero k)) },
end


Note that in the second example the let line is not necessary. In my proof, however, it is, since working with k.succ.succ everywhere will be messy.

#### Benjamin Davidson (Jan 31 2021 at 06:37):

Eric Wieser said:

Your first example should work if you use induction k generalizing n

This works! But it also causes things to get messy in my particular proof.

#### Eric Wieser (Jan 31 2021 at 10:50):

I think the let version is a totally reasonable thing to do here

#### Benjamin Davidson (Feb 01 2021 at 06:30):

That is pretty much the conclusion I came to as well. I suppose that there are always going to be finicky cases like my own that require an extra line or two, but it seems like your suggestion of docs#nat.exists_eq_succ_of_ne_zero is the most convenient option here.

#### Benjamin Davidson (Feb 01 2021 at 06:30):

Thank you all for your help!!

Last updated: May 07 2021 at 22:14 UTC