change induction basis

Stream: new members

[Pascal Schoppenhauer]

Hi, I want to prove something using induction. One of my variables has to be greater or equal to 4. And the equation I want to prove is an inequality. Is there a way to change the induction basis from nat.zero to 4 when I want to use induction on this variabe?

[Julian Berman]

I think nat.le_induction -- https://leanprover-community.github.io/mathlib_docs/data/nat/basic.html#nat.le_induction

[Pascal Schoppenhauer]

I'm sorry I don't know how to get this running... Now I have

apply nat.le_induction,
{sorry},
{sorry}

But how do I tell le_induction that I want to use the induction on m and not just the whole right side? And where do I put the 4?

[Kevin Buzzard]

Can you post a #mwe ?

[Pascal Schoppenhauer]

example : ∀ m n : nat, 0 ≥ m^2 ∧ m ≥ 4 → 2^0 ≥ 0^m :=
begin
  rintros m n ⟨I, II⟩,
  apply nat.le_induction,
  {sorry},
  {sorry}
end

but plz don't just solve it I want to try to get it myself :thank_you:

[Kevin Buzzard]

Well, the type of nat.le_induction is ∀ {P : ℕ → Prop} {m : ℕ}, P m → (∀ (n : ℕ), m ≤ n → P n → P (n + 1)) → ∀ (n : ℕ), m ≤ n → P n so right at the end it is expecting to see m <= n -> P n. So one way of telling Lean that m = 4 is to put the assumption 4 <= n back into the goal:

import tactic

example : ∀ m n : nat, 0 ≥ m^2 ∧ m ≥ 4 → 2^0 ≥ 0^m :=
begin
  rintros m n ⟨I, II⟩,
  revert II,
  apply nat.le_induction,
  {sorry},
  {sorry}
end

[Kevin Buzzard]

By the way, ≥ is considered evil in mathlib, you should use ≤. Also, instead of having hypotheses with ∧ in it's typically easier just to make them all separate hypotheses.

import tactic

example : ∀ m n : nat, m^2 ≤ 0 → 4 ≤ m → 2^0 ≥ 0^m :=
begin
  rintros m n I,
  apply nat.le_induction,
  {sorry},
  {sorry}
end

[Kevin Buzzard]

BTW just to check that we're on the same page mathematically, your assumptions are that m>=4 and also that m^2<=0 so this can't actually happen at all, right? Who needs induction.

[Pascal Schoppenhauer]

thanks mate! :thumbs_up: this looks awesome.
yeah you are right... I did a mistake at the beginning of my prove. Here is the full thing I am working on right now:

example : ∀ m n : nat, m^2 ≤ n → 4 ≤ m → n^m ≤ 2^n :=

But plz don't solve it. I have to do it on my own :upside_down:

[Kevin Buzzard]

Oh Ok but that changes a lot. Good luck! Just to be clear -- do you know a maths proof? You should know a maths proof before you embark on a Lean proof.

[Pascal Schoppenhauer]

I think so. :grimacing:

[Pascal Schoppenhauer]

Now I have

example : ∀ m n : nat, m^2 ≤ n → 4 ≤ m → n^m ≤ 2^n :=
begin
  rintros m n I,
  apply nat.le_induction,
  { sorry },
  { sorry }
end

But m = 4 has not been applied to hypothesis I in the induction base. It still says m ^ 2 ≤ n but I want it to say 4 ^ 2 ≤ n.

[Kevin Buzzard]

I guess instead of applying nat.le_induction immediately you could make a copy? intro II, have h := II, revert II, apply nat.le_induction

[Kevin Buzzard]

Just to be clear here, what Lean does is right -- it has correctly figured out P and correctly applied the theorem as it stands. This is all part of making sure that you definitely understand your own proof.

[Kevin Buzzard]

Let me ask you a question back. Can you state explicitly the statement P(m) which depends only on one variable m and which you want to prove for all m>=4? I am not certain whether you know whether you're doing induction on m or on n.

[Pascal Schoppenhauer]

I don't have a P(m) which only depends on m. My original plan was to prove that 16 ≤ n and then do induction on n with the base case 16. But I can't manage to prove 16 ≤ n in lean. sorry I'm very new to lean and its very hard for me to formalize easy things

[Kevin Buzzard]

Right now I am not clear about what the easy thing that you want to formalize is. The way induction works is that you have some infinite sequence of true-false statements P(0), P(1), P(2), ..., which can be thought of as a family P(m) of true-false statements which depends on (only) one variable m. You have two variables, so I'm not entirely sure what statement you're trying to prove by induction. Once we have that sorted out, hopefully we can get started with the Lean. But we need to have the maths clear first.

[Kyle Miller]

@Pascal Schoppenhauer Assuming you want to induct on m, here's a way to set up the induction to start at 4:

example (m n : nat) (hmn : m^2 ≤ n) (hm : 4 ≤ m) : n^m ≤ 2^n :=
begin
  rw le_iff_exists_add at hm,
  cases hm with k hk,
  subst hk,
  induction k,
  { sorry },
  { sorry }
end

[Kyle Miller]

If you step through the tactics, what it does is create a new variable k and replace m with 4 + k everywhere.

[Kyle Miller]

(You can do those first three lines in one line with obtain ⟨k, rfl⟩ := le_iff_exists_add.mp hm. obtain is a way to do cases immediately, and rfl tells it "this component is an equality, do subst for me.")

[Patrick Johnson]

My original plan was to prove that 16 ≤ n and then do induction on n with the base case 16. But I can't manage to prove 16 ≤ n in lean.

You can prove 16 ≤ n using the transitivity of the ≤ operator:

example : ∀ (m n : ℕ), m ^ 2 ≤ n → 4 ≤ m → n ^ m ≤ 2 ^ n :=
begin
  rintro m n h₁ h₂,
  have h₃ : 16 ≤ n,
  apply has_le.le.trans (pow_le_pow_of_le_left' h₂ 2) h₁,
  sorry,
end

although I don't think 16 ≤ n will help you too much here.

[Pascal Schoppenhauer]

Aw man, thanks for the help guys. I appreciate it, but what the heck is up with these function names :hurt: pow_le_pow_of_le_left do yall know these from the top of your head?

[Kevin Buzzard]

no, we find them with library_search and the ctrl-space "guess part of the name" trick

[Yaël Dillies]

Incidentally, I do :grinning:

[Kevin Buzzard]

except for Yael

[Pascal Schoppenhauer]

:laughter_tears: ok

[Kevin Buzzard]

I am slightly concerned that some of these comments are leading you down the garden path. My original explanation of how to use nat.le_induction was when we had n=0 and the question was much easier. I'm still keen to hear your maths proof of this question which you're intending to formalise. I am not convinced that some of the suggestions above are going in the right direction.

[Pascal Schoppenhauer]

I'm not even convinced of my own maths proof

[Kevin Buzzard]

I would recommend that we sort this out first. I don't think Lean is going to help with a faulty proof. What's your purported proof?