Simple induction proof as a newbie

Stream: new members

[metakuntyyy]

Hi guys, I am new here. I started with lean a few days ago and so far it has been very hard to me. ;)
Anyways I already formalised some theorems in metamath and now I want to try to formalize the same theorems in lean.
I have chosen a simple, yet nontrivial lemma I want to prove. I have chosen it, because while the proof is done with induction, the base case is not 0, but 2.

So far I have the following questions:
How do i quantify over the natural numbers (aka positive integers without 0), because in most of my proofs I start at 1 and not at 0?
In metamath, there are multiple inductions
Over Natural Numbers https://us.metamath.org/mpeuni/nnind.html
Over nonnegative numbers https://us.metamath.org/mpeuni/nn0ind.html
over numbers that start at an arbitrary integer https://us.metamath.org/mpeuni/uzind.html
over ranges of numbers from M to N : https://us.metamath.org/mpeuni/fzind.html

I would to know what the lean equivalent is. Because for my proof I need an uzind equivalent for lean.

So I want to prove the following statement

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  sorry

I am grateful for your help, I'd be happy for hints but I do not wish a full solution as otherwise I won't learn anything. If I am stuck with your hints I'll ask further questions for clarification.

Anyways I have tried the induction tactic, which gives me
case zero
h1 : 2 ≤ 0
⊢ 2 ^ (0 + 1) < (2 * 0 + 1).choose 0
case succ
n✝ : ℕ
a✝ : 2 ≤ n✝ → 2 ^ (n✝ + 1) < (2 * n✝ + 1).choose n✝
h1 : 2 ≤ n✝ + 1
⊢ 2 ^ (n✝ + 1 + 1) < (2 * (n✝ + 1) + 1).choose (n✝ + 1)

Expected type
x : ℕ
h1 : 2 ≤ x
⊢ ℕ

Messages (1)

Basic.lean:5:79

unsolved goals
case succ
n✝ : ℕ
a✝ : 2 ≤ n✝ → 2 ^ (n✝ + 1) < (2 * n✝ + 1).choose n✝
h1 : 2 ≤ n✝ + 1
⊢ 2 ^ (n✝ + 1 + 1) < (2 * (n✝ + 1) + 1).choose (n✝ + 1)

So right now I am thinking about formulating this theorem such that I can use 0 as base case, thus shifting the index n.
This results in

theorem inductiveineqrewrite (x : ℕ )  : (2^ (x+3)) < (choose (2*(x+1)+3) (x+2)) :=by
  induction x
  case zero =>
    simp
    sorry
  case succ =>
    sorry

I made progress on the case zero step, however I can't simplify the right side. It says choose 5 2 which should be 10.
I tried it with rw [\l simp] but that didn't work sadly. I don't know how to simplify the right side.

[metakuntyyy]

I have also thought about commuting the statement which would give me choose 5 2 >= 8, and then I could use simp I think.
However I don't know the theorem to commute left and right side.

[Ruben Van de Velde]

decide works to evaluate the choose function

[Ruben Van de Velde]

I think it would be better if norm_num covered it, but it doesn't seem like it does (yet)

[metakuntyyy]

Ok decide worked, but I don't know what it does. How is it different from simp? How do I know when to use what, because this seemed like magic to me.

Still the question I had is how to rewrite the right side, as that may be useful eventually

[metakuntyyy]

For the second goal I want to use the following:
Rewrite the left side as (2*(2^(n+3) )
Then rewrite the right side as ( a*b)
then argue that (2^(n+3))< b by induction hypothesis
then argue 2 < a by calculation
which should conclude the proof.

Also is there a way such that I can use induction with my original theorem, but instead with base case 2:

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  sorry

because I would really like to use that one.

[Ruben Van de Velde]

Yeah, there's an induction principle... Maybe docs#Nat.leInduction ?

[Ruben Van de Velde]

docs#Nat.le_induction

[Ruben Van de Velde]

Maybe calc to get everything in the right form and then gcongr will hopefully get you the correct goals

[metakuntyyy]

Yeah that worked, I'd like to use this one

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction x, h1 using Nat.le_induction
  case base => decide
  case succ =>
    have hah : (2^(x+1)) = ((2^x)*2):=by
      rw [Int.pow_succ] at hah
    sorry

So I've made some progress and this is the first step. I want to prove that 2^(x+1)=2^x*2
I have found the theorem to use which is Int.pow_succ, however I get the following error message:
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
?b ^ (?e + 1)
I want to use Int.pow succ on the have case, but I don't know how to bind it.

[Ruben Van de Velde]

Remove the at hah; you're trying to operate on the current goal at that point

[Ruben Van de Velde]

And then you'll notice that it still doesn't work, because Int.pow_succrequires an integer base while your twos are natural numbers

[Ruben Van de Velde]

Try pow_succ without the Int.

[Ruben Van de Velde]

And don't forget to add import and open statements when quoting code here (see #mwe)

[metakuntyyy]

Thanks for the help, here is the minimal example

import Mathlib

open Nat

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction x, h1 using Nat.le_induction
  case base => decide
  case succ =>
    have hah : (2^(x+1)) = ((2^x)*2):=by
      rw [pow_succ]
    have haf : choose (2*(x+1)+1) (x+1) = (choose (2*x+1) x)*((2*x+2)/(x+1))*((2*x+3)/(x+2)):=by
      rw [choose_eq_factorial_div_factorial]
      simp

I have found the theorem to use, but now I am stuck unfolding the inner equations, for example I want to expand the inner values and bring them into a "normal form"

[metakuntyyy]

And if a calc block makes sense, how would I utilize it here, I just get errors trying to use the calc block with the have statement

[metakuntyyy]

import Mathlib

open Nat

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction x, h1 using Nat.le_induction
  case base => decide
  case succ x h1 ha =>
    have hah : (2^(x+1)) = ((2^x)*2):=by
      rw [pow_succ]
    have haf : choose (2*(x+1)+1) (x+1) = (choose (2*x+1) x)*((2*x+2)/(x+1))*((2*x+3)/(x+2)):=by
      rw [choose_eq_factorial_div_factorial]
      simp
      sorry
    sorry

Ah also I cant really match the types on the succ case, I have tried to introduce binders but the lsp gives me this message:
unsolved goals
x✝ x : ℕ
h1 : 2 ≤ x
ha : 2 ^ (x + 1) < (2 * x + 1).choose x
hah : 2 ^ (x + 1) = 2 ^ x * 2
⊢ x + 1 ≤ 2 * (x + 1) + 1
I don't know how to get rid of the + in the first hypothesis. I have managed to name the other hypotheses though, which I can quite happy

[Ruben Van de Velde]

I don't understand why haf is true. Note that you're using division of natural numbers, which truncates when the denominator doesn't divide the numerator, so tends to be hard to work with

[metakuntyyy]

Yeah, I figured I'd need to coerce the values to the rational numbers. Is that correct, and if so what is the best way forward?

[Ruben Van de Velde]

You can write (a / b : ℚ) (parentheses required)

[metakuntyyy]

Would this be correct?

import Mathlib

open Nat


theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction' x, h1 using Nat.le_induction
  case base =>
    decide
  case succ x h1 ha =>
    have hah : (2^(x+1)) = ((2^x)*2):=by
      rw [pow_succ]
    have haf : choose (2*(x+1)+1) (x+1) = (choose (2*x+1) x)*(((2*x+2)/(x+1)):ℚ)*(((2*x+3)/(x+2)):ℚ):=by
      rw [choose_eq_factorial_div_factorial]
      simp
      sorry
    sorry

[metakuntyyy]

Or do I need to coerce all values to \Q

[Ruben Van de Velde]

Can you write out the mathematical proof?

[Ruben Van de Velde]

The calc suggestion from earlier could look like this:

import Mathlib

open Nat

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction x, h1 using Nat.le_induction
  case base => decide
  case succ x h1 ha =>
    calc
      2 ^ (x + 1 + 1)
      _ = 2 * 2 ^ (x + 1) := ?_
      _ < x * (2 * x + 1).choose x := ?_
      _ = (2 * (x + 1) + 1).choose (x + 1) := ?_
    · sorry
    · sorry
    · sorry

[metakuntyyy]

Sure: Let us assume that the induction hypothesis $(2^{(x+1)})<\binom{2x+1}{x}$ holds. Clearly $2^{x+2}=2^{x+1}\cdot 2$ and $\binom{2(x+1)+1}{x+1} = \binom{2x+3}{x+1} =\frac{(2x+3)!}{(x+1)!\cdot (x+2)!}$ Now splitting off $2x+2$ and $2x+3$ from the numerator and $(x+1)(x+2)$ from the denominator leaves us with a product $a*b$ for the left side and $c\cdot d$ for the right side. By induction hypothesis we want to show that $a\cdot b <c\cdot d$. All numbers are clearly positive and $a<c$ by Induction hypothesis, thus it suffices to show $b<d$. $b=2$ by previous calculation and $d= \frac{(2x+3)\cdot(2x+2)}{(x+2)\cdot (x+1)}$ We can use the law to switch multiplication and division in this quadruple to give us $d =\frac{ 2x+3}{x+2}\cdot\frac{ 2x+2}{x+1}$ . The first factor is clearly greater than 1 and the second factor is 2, therefore $d < 2\cdot 1=2$ which was what we needed to show.

[metakuntyyy]

Sorry for the formatting

[Kevin Buzzard]

Put LaTeX within $$ signs (two dollars) e.g. $$\binom{2(x+3)}{x+1}$$ gives $\binom{2(x+3)}{x+1}$.

[metakuntyyy]

Alright I've made some progress

import Mathlib

open Nat


theorem inductiveineq2 (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction' x, h1 using Nat.le_induction
  case base =>
    decide
  case succ y h1 ha =>
    suffices hoa : 2 ^ (y+2) < choose (2*y+3) (y+1) by {
      have l : 1+1=2 :=by decide
      have l2 : 2 * (y + 1) + 1 = 2*y+3:= by ring
      have nc1 := Nat.cast_factorial ℚ y
      have powp1 : 2 ^ (y + 1 + 1) = 2^ (y+1) *2 := by rfl
      conv =>
        lhs
        rhs
        rw[add_assoc]
        rhs
        rw[l]
      conv =>
        rhs
        lhs
        rw[l2]
      exact hoa
    }
    have yl2p1 : y≤ 2*y+1 := by linarith
    have homo := Nat.cast_choose ℚ yl2p1
    have haaaaa : 2 ^ (y + 1) < (2 * y + 1).choose y := Nat.cast_lt.mpr ha
    have hiu : (2:ℚ) ≤  ((5/2):ℚ) := by linarith
    have hs := Nat.two_pow_pos (y + 1)
    have hs2 : 0 < (choose (2*y+1) y) := by sorry
    have ho := mul_lt_mul ha hiu
    sorry

Yet I am completely stuck at lifting everything to $\mathbb{Q}$ nothing wants to work and I've tried multiple hours to get it work. These are some examples.

[metakuntyyy]

I've tried lifting haaaaa to $\mathbb{Q}$ but I get following error.
(deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached
use set_option maxHeartbeats <num> to set the limit
use set_option diagnostics true to get diagnostic information

[metakuntyyy]

Here's how I've tried to lift it have haaaaa : ((2 ^ (y + 1)):ℚ) < (((2 * y + 1).choose y ):ℚ):= Nat.cast_lt.mpr ha

[metakuntyyy]

Maybe I am converting it wrongly, I am truly lost as I've exhausted all my options.

[metakuntyyy]

Well on second thought I have proven this finally. I guess this is a first step. I must admit I LOVE the conv tactic.
It's not a short proof, but I guess it works.

import Mathlib

open Nat

#check Nat.mul_lt_mul_of_lt_of_le'

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1))*(x)!*(x+1)! <  (2*x + 3)! :=by
  induction' x, h1 using Nat.le_induction
  case base => decide
  case succ y ha hb =>
    have xh : 2 ≤ 2 * y + 4 := by linarith
    have yh : y + 2 ≤ 2 * y + 5 := by linarith
    have zh : 2 * (y + 1) ≤ 2 * y + 4 := by linarith
    have hbd: 2*(y+1)*(y+2)≤ (2*y+4)*(2*y+5) := by refine Nat.mul_le_mul zh yh
    have hoz : 0 < 2*(y+1)*(y+2) := by simp
    have opo : 1+1=2 := by exact rfl
    have ioa : 2 * (y + 1) + 3 = 2*y+5 := by linarith
    have iob : (2 * y + 3 + 1) = 2*y+4 := by rfl
    have ioc : (2 * y + 4 + 1) = 2*y+5 := by rfl
    have aya : 2 ^ (y + 1) * y ! * (y + 1)! * (2 * (y + 1) * (y + 2)) =
    ( 2 ^ (y + 1) * 2 ) * ( y ! * (y + 1) ) * ( (y + 1)! * (y + 2) ) := by ring
    have hh := Nat.mul_lt_mul_of_lt_of_le' hb hbd hoz
    conv =>
      lhs
      lhs
      lhs
      rw[pow_succ]
    conv =>
      lhs
      rhs
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    conv =>
      rhs
      congr
      rw[ioa]
    conv =>
      rhs
      rw[Nat.factorial_succ]
      rw[Nat.factorial_succ]
      rw[mul_comm]
      lhs
      rw[mul_comm]
      rw[iob]
    conv =>
      rhs
      rw[mul_assoc]
      rw[ioc]
    conv at hh =>
      lhs
      rw[aya]
      rhs
      rw[mul_comm]
      rw[← Nat.factorial_succ]
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    conv at hh =>
      lhs
      lhs
      rhs
      rw[mul_comm]
      rw[← Nat.factorial_succ]
    exact hh

[metakuntyyy]

Well on second thought I showed the wrong result. I have quickly fixed it.

import Mathlib

open Nat
theorem inductiveineq2 (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1))*(x)!*(x+1)! <  (2*x + 1)! :=by
  induction' x, h1 using Nat.le_induction
  case base => decide
  case succ y ha hb =>
    have yh : y + 2 ≤ 2 * y + 3 := by linarith
    have hbd: 2*(y+1)*(y+2)≤ (2*y+2)*(2*y+3) := by exact Nat.mul_le_mul_left (2 * (y + 1)) yh
    have hoz : 0 < 2*(y+1)*(y+2) := by simp
    have opo : 1+1=2 := by exact rfl
    have aua : 2 * (y + 1) + 1 = 2*y+3 := by linarith
    have aue : (2 * y + 1 + 1)=2*y+2 :=by simp
    have aya : 2 ^ (y + 1) * y ! * (y + 1)! * (2 * (y + 1) * (y + 2)) =
    ( 2 ^ (y + 1)*2) * ( (y+1) *y ! ) *( (y + 2)* (y + 1)! ) :=by ring
    have aui : (2 * y + 1 + 2)=2*y+3 :=by simp
    have hh := Nat.mul_lt_mul_of_lt_of_le' hb hbd hoz
    conv =>
      lhs
      lhs
      lhs
      rw[pow_succ]
    conv =>
      lhs
      rhs
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    conv =>
      rhs
      congr
      rw[aua]
    conv =>
      rhs
      rw[Nat.factorial_succ]
      rw[Nat.factorial_succ]
      rw[← mul_assoc]
      rw[mul_comm]
      rhs
      rw[mul_comm]
      rw[aue]
      rw[aui]
    conv at hh =>
      lhs
      rw[aya]
      rw[← Nat.factorial_succ]
      rhs
      rw[← Nat.factorial_succ]
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    exact hh

[Scott Carnahan]

If you go back to the inequality with (choose (2*x+1) x), you can use Nat.choose_succ_succ to show (choose (2 * x + 2) (x + 1)) = 2 * choose (2 * x + 1) x and again to show (choose (2*x+2) (x + 1)) ≤ (choose (2 * x + 3) (x + 1)).

[metakuntyyy]

I have finally solved it. Some lessons learned:

• Don't try to lift until it's absolutely necessary. Proving theorems for natural numbers via induction will make you happier if they stay as natural numbers.
• Lifting is the devil
• Sometimes the unifier really messed with me even though it should work.
• Most theorems in mathlib are sadly missing an example use, I had to quite struggle with finding out how to actually apply a theorem.
• Lifting is the devil

Honestly pretty good experience so far. Here is my feedback.
The positives are:

• Pretty fun to play around (That's a big one, if it's fun, it's good usually)
• Deep math library
• You'll learn the simplest way of proof since any deviation will just be hard
• Installation was quite gucci, tooling is superb.
• Powerful tactics, it sometimes feels like magic
• Pretty helpful community
• Rewriting and performing surgery is a pleasure, unlike with metamath where you are taking 12 inch every time.

The negatives are:

• The system feels like magic, stuff not working, theorems and proofs in the standard library are utterly incomprehensible. rfl closes the goal and it is inconcievable why.
• Direct proof steps are not shown as compared to metamath. This is hard for someone to trace a theorem down. How does lean actually check a proof when in tactic mode, this makes me wonder why it isn't possible to insert a falsity in a tactic if lean "eats" the intermediaries.
• Sometimes I want a simple proof in its rawest from. It feels as if there are steps that are just plain eaten, which makes learning somewhat challenging.
• (Not really a negative:) Obviously example : 100454^10000 < 9^122451:= by decide works. It makes me wonder how it works. It can't be by unfolding, I don't have that much memory. There has to be a byte representation that has decision algorithm on the size of the list of bytes and there may be some equality/inequality theorems in play.
• Extremely high learning curve, even moreso than metamath. If I'd start with lean I'd probably quit as I'd assume all the formality issues I'd not yet learn from metamath coupled with the additional complexity of lean would kill me.
• Unclear how the theorem should be called. I had this issue multiple times where I couldn't even generate a check. ( I guess this is really practice)
• Some absolutely trivial statements are a real pain once you need to lift values to other types.
• Most of the reference is in lean3 and that confused the hell out of me.
• Documentation is written for cs, not for mathematicians. I don't like to do type masturbation, I just want things to work
• Inner workings are even more of a magic. I kinda understand how it works (metaprogramming,...) but then I look at some proofs and gain nearly no insight.
• Efficient theorem writing has an even higher learning curve. God bless conv mode, without that beauty we'd be all lost.
• Apropos conv mode, why is the documentation not giving an user guide on those tactics. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Conv.html#Mathlib.Tactic.Conv That is heresy. If I didn't read this friendly manual https://leanprover-community.github.io/extras/conv.html which is still in lean3 I'd never really understand why conv is so powerful.

Overall pretty cool and fun, needs a more mathematician oriented documentation, more tutorials/games and more content. I'm certain that things will improve and I am looking for the next theorem I want to tackle.

[metakuntyyy]

Here is the proof. Challenge yourself to make it shorter/more beautiful if you like.

import Mathlib

open Nat

theorem inductiveineq2 (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1))*(x)!*(x+1)! <  (2*x + 1)! :=by
  induction' x, h1 using Nat.le_induction
  case base => decide
  case succ y ha hb =>
    have yh : y + 2 ≤ 2 * y + 3 := by linarith
    have hbd: 2*(y+1)*(y+2)≤ (2*y+2)*(2*y+3) := by exact Nat.mul_le_mul_left (2 * (y + 1)) yh
    have hoz : 0 < 2*(y+1)*(y+2) := by simp
    have opo : 1+1=2 := by exact rfl
    have aua : 2 * (y + 1) + 1 = 2*y+3 := by linarith
    have aue : (2 * y + 1 + 1)=2*y+2 :=by simp
    have aya : 2 ^ (y + 1) * y ! * (y + 1)! * (2 * (y + 1) * (y + 2)) =
    ( 2 ^ (y + 1)*2) * ( (y+1) *y ! ) *( (y + 2)* (y + 1)! ) :=by ring
    have aui : (2 * y + 1 + 2)=2*y+3 :=by simp
    have hh := Nat.mul_lt_mul_of_lt_of_le' hb hbd hoz
    conv =>
      lhs
      lhs
      lhs
      rw[pow_succ]
    conv =>
      lhs
      rhs
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    conv =>
      rhs
      congr
      rw[aua]
    conv =>
      rhs
      rw[Nat.factorial_succ]
      rw[Nat.factorial_succ]
      rw[← mul_assoc]
      rw[mul_comm]
      rhs
      rw[mul_comm]
      rw[aue]
      rw[aui]
    conv at hh =>
      lhs
      rw[aya]
      rw[← Nat.factorial_succ]
      rhs
      rw[← Nat.factorial_succ]
      congr
      rw[add_assoc]
      rhs
      rw[opo]
    exact hh

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : 2^ (x+1) <  choose (2*x+1) x :=by
  have ho : (2*x+1)= (x+1)+x :=by ring
  have hoa : (x+1+x) =(2*x+1) := by ring
  have hua : (x+(x+1)) =(2*x+1) := by ring
  have hah := inductiveineq2 x h1
  rw[ho, add_choose, mul_comm]
  rw[mul_assoc] at hah
  have he := Nat.factorial_mul_factorial_dvd_factorial_add x (x+1)
  rw[hua] at he
  have hdn := Nat.lt_div_iff_mul_lt he (2^(x+1))
  conv at hdn =>
    rhs
    rw[mul_comm]
  have hodd := hdn.mpr hah
  rw[hoa]
  exact hodd

[Kevin Buzzard]

Here's a way of doing it in calc mode; note that you never need to use any low-level rewrites like mul_comm or mul_assoc this way; just get ring to do the heavy lifting.

import Mathlib.Tactic

open Nat

theorem inductiveineq2 (x : ℕ) (h1 : 2 ≤ x) : (2 ^ (x + 1)) * (x)! * (x+1)! < (2*x + 1)! := by
  induction x, h1 using Nat.le_induction
  · decide
  · case succ y ha hb => calc
    2 ^ (y + 1 + 1) * (y + 1)! * (y + 1 + 1)! =
      2 ^ (y + 1) * (y)! * (y + 1)! * (2 * y + 2) * (y + 2) := by simp [factorial_succ]; ring
    _ < (2 * y + 1)! * (2 * y + 2) * (y + 2) := by gcongr
    _ = (2 * y + 2)! * (y + 2) := by simp [factorial_succ]; ring
    _ ≤ (2 * y + 2)! * (2 * y + 3) := by gcongr <;> linarith
    _ = (2 * (y + 1) + 1)! := by nth_rw 2 [factorial_succ]; ring_nf

[metakuntyyy]

That is so cool, last time I tried to use calc mode it was a pain. So I don't know but when i tried to use have with ring it didn't do any progress. This was probably because I had the version with rational numbers, lifting and subtraction.
There ring didn't do any progress and it also was a mess to be honest.

This proof looks way nicer, I'll study it and calc mode. Thank you