# Zulip Chat Archive

## 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,
{ contradiction },
...
```

#### 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:49):

What's your base case?

#### 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