induction on n where n ≠ 0

Stream: Is there code for X?

[Benjamin Davidson]

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

[Yakov Pechersky]

Why not

induction n with n hn,
{ contradiction },
...

[Benjamin Davidson]

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

[Anne Baanen]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

You need to watch Jannis' CPP talk.

[Kevin Buzzard]

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

[Riccardo Brasca]

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

[Benjamin Davidson]

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]

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]

@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]

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

[Eric Wieser]

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

[Benjamin Davidson]

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]

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]

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

[Benjamin Davidson]

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]

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]

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]

What's your base case?

[Mario Carneiro]

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

[Benjamin Davidson]

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

[Mario Carneiro]

I mean a general induction lemma

[Eric Wieser]

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

[Mario Carneiro]

for example

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

[Mario Carneiro]

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

[Benjamin Davidson]

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]

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]

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

[Benjamin Davidson]

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]

Thank you all for your help!!