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: Dec 20 2023 at 11:08 UTC