induction

Stream: new members

[Iocta]

How to say this kind of induction?

example  (p: ℕ → Prop) (h: ∀ n: ℕ, p n → p (n + 1)) : ∀ n m : ℕ, n ≤ m → p n → p m :=
begin
intros n m h,
cases m - n, -- it doesnt like this

end

[Kyle Miller]

One thing you can do is prove a related statement first, where m - n is replaced by a variable:

example  (p: ℕ → Prop) (h: ∀ n: ℕ, p n → p (n + 1)) : ∀ n m : ℕ, n ≤ m → p n → p m :=
begin
  have key : ∀ (n k : ℕ), 0 ≤ k → p n → p (n + k),
  { intros n k h',
    induction k,
    { exact id, },
    { intro a,
      apply h,
      apply k_ih,
      apply zero_le,
      exact a } },
  intros n m h' hp,
  convert_to p (n + (m - n)),
  exact (nat.add_sub_of_le h').symm,
  apply key,
  linarith,
  exact hp,
end

There's also a direct proof:

example  (p: ℕ → Prop) (h: ∀ n: ℕ, p n → p (n + 1)) : ∀ n m : ℕ, n ≤ m → p n → p m :=
begin
  intros n m h',
  induction m generalizing n,
  { rw le_zero_iff_eq.mp h', exact id },
  { intro a,
    by_cases h'' : n = m_n.succ, rwa h'' at a,
    apply h, apply m_ih n _ a,
    rw nat.succ_eq_add_one at h' h'',
    cases eq_or_lt_of_le h',
    { exfalso, exact h'' h_1 },
    { linarith } }
end

[Iocta]

I see, thanks.

[Kenny Lau]

induction h

[Iocta]

variables (p: ℕ → Prop) (p_succ_of_p: ∀ n: ℕ, p n → p (n + 1))

example  : ∀ n m : ℕ, n ≤ m → p n → p m :=
begin
intros n m h,
end

How I can declare p_succ_of_p as a top-level variable and still refer to it inside the example proof?

[Kyle Miller]

Assuming this is actually what you want to do, you can use include

variables (p: ℕ → Prop) (p_succ_of_p: ∀ n: ℕ, p n → p (n + 1))
include p_succ_of_p

example  : ∀ n m : ℕ, n ≤ m → p n → p m :=
begin
intros n m h,
end

[Kyle Miller]

What is happening is that variables declares variables that will be auto-included if they are referred to in the statement of the lemma, definition, or example, and include overrides this to always include it. You can use omit later to cause it to go back to the default behavior if I remember correctly.

[Iocta]

ah that's what I was looking for

[Claus-Peter Becke]

What would be suitable to represent a formula of a sum as the following one:

example : sum k between k=1 and n = n * ( n + 1) / 2 :=

I don't find a way, if it is possible at all to try it this way, to represent the equation's left hand side of the formula.

[Shing Tak Lam]

have you seen algebra.big_operators?

[Claus-Peter Becke]

No, I didn't. Thank you for that hint.

[Claus-Peter Becke]

As far as I have seen the operator sum works on finite sets. I would like to prove by induction the assertion's validity on the infinite set of natural numbers.

[Shing Tak Lam]

import algebra.big_operators

open_locale big_operators

open finset

-- finset.range n is the set {0,1,2, ..., n-1}
example : range 5 = {0,1,2,3,4} := rfl

-- So finset.range n.succ is the set {0,1,2,...,n}
-- In this case, the extra `0` term being summed makes no difference, since
--  n     n
--  ∑ i = ∑ i
--  i=0   i=1

-- Then, we can represent
--  n
--  ∑ i
--  i=0
--
-- as ∑ i in (range n.succ), i

example (n : ℕ) : ∑ i in (range n.succ), i = n * (n + 1) / 2 :=
begin
  sorry
end

[Kevin Buzzard]

Why not cast the i in the sum to a rational, in order to get that division to be mathematical division rather than some weird rounding one?

[Claus-Peter Becke]

@Shing Tag Lam: Thank you very much for your solution which is really helpful. This is a great model for me to be studied closely to become more familiar with the techniques which are needed to deal with induction.
@Kevin Buzzard: As far as I remember type-casting is used in Java writing the target type in brackets in front of the variable to be casted. Does it work similar in Lean?

[Claus-Peter Becke]

@Shing Tak Lam: I'm sorry for the misspelling of your name

[Johan Commelin]

@Claus-Peter Becke If you write @Shi then Zulip should suggest autocompletions of the name (unless you use a nonstandard zulip client).
The benefit of those auto-completed names is that the person in question gets a notification somewhere in their interface.

[Shing Tak Lam]

Claus-Peter Becke said:

@Shing Tag Lam: Thank you very much for your solution which is really helpful. This is a great model for me to be studied closely to become more familiar with the techniques which are needed to deal with induction.
@Kevin Buzzard: As far as I remember type-casting is used in Java writing the target type in brackets in front of the variable to be casted. Does it work similar in Lean?

You can use (term : type) to coerce the i to a rational number like so:

example (n : ℕ) : ∑ i in (range n.succ), (i : ℚ) = n * (n + 1) / 2 :=

And you'll see ↑ next to the n in the tactic state, which is Lean coercing n from a nat to a rat.

In this specific example, natural number division isn't an issue, since n * (n + 1) / 2 = (n * (n + 1)) / 2 and n * (n + 1) is always even, but in general, flooring division may not be what you want, hence Kevin is suggesting you cast it to a rational number.

[Kevin Buzzard]

It is an issue in the proof, because you want to prove this by induction, and it will be much more horrible to work in the integers with its broken division than to work in the rationals with a division that obeys much nicer properties.

[Kevin Buzzard]

import algebra.big_operators tactic

open_locale big_operators

open finset
example (n : ℕ) : ∑ i in (range n.succ), (i : ℚ) = n * (n + 1) / 2 :=
begin
  induction n with d hd,
  { -- base case true by definition
    refl },
  { -- inductive step
    rw sum_range_succ,
    rw hd,
    simp [nat.succ_eq_add_one],
    ring,
  }
end

Proof when they're rationals goes through without thinking really.

[Kevin Buzzard]

Proof when they're integers will be much more of a pain, you'll have to look up specific lemmas like a/b+c=(a+c*b)/b etc.

[Shing Tak Lam]

Fair enough, I used nat.div_eq_of_eq_mul_right in my nat proof, but I already knew that lemma (which transforms the problem from nat division to one in nat multiplication), but I can see how dealing with division can be a pain.

[Kevin Buzzard]

I just think that this sort of argument (fighting integer division) looks bad to mathematicians (especially those who have never used computer algebra software and are totally confused by the fact that 5/2 could ever be thought of as being equal to 2 -- this never happens on a calculator).

[Claus-Peter Becke]

Thank you both very much for these awesome explanations which will supply me with a lot of stuff to think about and to learn from.

[Claus-Peter Becke]

Up to now I stick to the following stage of development of the proof:

import data.nat.basic
import algebra.big_operators

open nat
open algebra

example (n : ℕ) : ∑ i in (range n), i = n * (n + 1) / 2 :=
begin
    induction n with n ih,
    rw zero_mul,
    simp,
    rw succ_mul,
    rw succ_add,
    repeat {rw succ_eq_add_one},
    rw mul_succ,
    rw nat.left_distrib,
    simp,
    rw nat.div_eq_of_eq_mul_right,
    simp,
end

The application of these tactics generates the following result:

tactic failed, there are unsolved goals
state:
n : ℕ,
ih : ∑ (i : ℕ) in range n, i = n * (n + 1) / 2
⊢ n * n + n + n + (n + 1 + 1) = 2 * ∑ (i : ℕ) in range (n + 1), I

The left hand side of the goal expresses the term which I would have liked to produce: (n+1)*(n+2) which shows the sum for n+1. But I fail in finding tactics to generate a solution which produces a suitable progress. The main problem I observed is that I don't have an focussed overview about the theorems which are stored in the library and which are applicable in the different contexts. Are there any exercises which help me to become more familiar with the nat-library after having finished the Natural Number Game?

[Scott Morrison]

One strategy is to hope that the library is thorough, and use library_search to obtain the names of relevant lemmas. e.g. your first task to relate a sum over range (n+1) to a sum over range n and an extra term, and surely there must be a lemma doing this.

[Scott Morrison]

import algebra.big_operators.basic

open finset

open_locale big_operators

example (f : ℕ → ℕ) (n : ℕ) :
  ∑ (i : ℕ) in range (n + 1), f i = f n + ∑ (i : ℕ) in range n, f i :=
by library_search

[Scott Morrison]

This finds sum_range_succ for you.

[Scott Morrison]

Another strategy is to realise that all statements in mathlib are named using an excruciatingly boring scheme, which is so boring that often you can predict the name if you know what you're looking for!

[Scott Morrison]

Since this is a lemma about the sum over a range involving a succ, it's not crazy (and feels much less crazy as you get used to it) to just guess sum_range_succ might exist. (Use #print to verify, or just rw by it if you're bold.)

[Scott Morrison]

(Note also that your example wasn't quite a #mwe --- without an open_locale statement it shouldn't work.)

[Claus-Peter Becke]

@Scott Morrison:
Thank you very much for your very helpful explanations. Yes, I forgot to add the open_locale big_operators statement. I tried the library_search-tactic, too. But it didn't produce any results. That's weird. But anyway. The sum_range_succ-tactic is very helpful because it allows to rewrite the right hand side of the goal via application of the induction-hypothesis which finally will help to close the goal, I hope at least.

[Scott Morrison]

Note that sum_range_succ is a lemma, not a tactic. It's worth making the distinction.

[Scott Morrison]

library_search only solves the exact goal it's presented with. That's why I wrote it out as an example rather than using it inline in your proof.

[Scott Morrison]

(You can also use the have tactic to setup a temporary goal mid-proof to try library_search on.)

[Claus-Peter Becke]

Yes, I know. That was a moment of thoughtlessness in the face of the nerve-wracking trials to solve the problems concerning the simplification of the applied induction hypothesis.

[Kevin Buzzard]

You should cast everything to rationals so that the division becomes easier to work with

[Claus-Peter Becke]

I tried a new example:

example (n : ℕ) : n * n + n + n + (n + 1 + 1) = 2 * (n + n * (n + 1) / 2) :=
begin
end

and the application of the have-tactic:

have h1 := n * n + n + n + (n + 1 + 1) = 2 * (n + n * (n + 1) / 2),

In both cases Lean gave the message that 'library_search' failed after having used by library_search

[Scott Morrison]

well, it's very unlikely that library_search will help with that goal --- it's only suitable when there is a lemma in the library that gives you exactly your goal (possibly after substituting arguments from local hypotheses).

[Kevin Buzzard]

And you're still using a broken division

[Kevin Buzzard]

This stuff would probably be doable with a tactic if you switch to rationals

[Scott Morrison]

In fact, you can see that this example is actually false:

import tactic.slim_check

example (n : ℕ) : n * n + n + n + (n + 1 + 1) = 2 * (n + n * (n + 1) / 2) :=
begin
  slim_check
end

[Scott Morrison]

which prints

===================
Found problems!

n := 0
2 ≠ 0
-------------------

[Scott Morrison]

(slim_check is very new to mathlib)

[Claus-Peter Becke]

I observed that, too, and I wondered that Lean produces and accepts such an equation after having applied rw ih.

[Kevin Buzzard]

Another problem with your variant is that range n is the n numbers from 0 to n-1 so what you're trying to prove is false

[Kevin Buzzard]

You're also going to run into the issue that x/2*2=x is not true for naturals because the division is not mathematical division

[Claus-Peter Becke]

@Kevin Buzzard: Thank you very much for your hints. I will study your solution closely and try to apply it.

[Kevin Buzzard]

Another approach would be to stick with naturals but clear denominators, and prove that twice the sum is n(n+1). Remember to use range (n+1) though -- if you stay with range n then you'll have to use natural subtraction which is broken in the same way

[Claus-Peter Becke]

The next days I will try to prove some induction-tasks, first with pen and paper, afterwards in Lean. It's very helpful to have the models which you and Shing Tak Lam posted the last days. Now I have a guide which serves as an instructor that can be varied to fit in respective contexts. To know of how to deal with sums on infinite sets and to have a collection of lemmata and tactics concerning these problems is a very good point to start from.

[Claus-Peter Becke]

Is there any possibility to solve the following goal?

⊢ n * (2 * n - 1 + 4) + 1 = n * (2 * n + 3) + 1

[Shing Tak Lam]

import tactic

example (n : ℕ) : n * (2 * n - 1 + 4) + 1 = n * (2 * n + 3) + 1 :=
begin
  by_cases hn : n = 0,
  { simp [hn] },
  { suffices : 2 * n - 1 + 4 = 2 * n + 3,
    { rw this },
    omega }
end

[Shing Tak Lam]

But in general, nat subtraction is not very nice to deal with, Since 2 * n - 1 + 4 is not always equal to 2 * n + 3 (if n = 0 LHS is 4 and RHS is 3). In this specific example, if n = 0, you're multiplying by 0 so both sides do end up being equal.

[Claus-Peter Becke]

Thank you very much. I still have some trouble with the omega expression. I'll get the message:

invalid eval_expr, expression must be closed
state:
n : ℕ
⊢ ¬∑ (k : ℕ) in range (n + 1), (k * 4 - 3) = n * (n * 2 - 1) ∨ ¬¬n = 0 ∨ n * 2 - 1 + 4 = n * 2 + 3

[Shing Tak Lam]

Can you post what you have so far? From my experience, omega can be a bit fragile and additional hypotheses can stop it from working, and clearing sometimes helps

[Claus-Peter Becke]

import data.nat.basic
import algebra.big_operators tactic
import algebra.ring
import tactic

open_locale big_operators

open finset
open nat
open algebra

variables k n m x : ℕ
example (n : ℕ) : ∑ k in (range n.succ), (4 * k - 3) = n*(2*n-1) :=
begin
  induction n with n ih,
  refl,
  rw sum_range_succ,
  rw ih,
  simp [nat.succ_eq_add_one],
  repeat {rw mul_add},
  simp,
  rw add_comm,
  rw mul_comm (n + 1),
  rw add_mul,
  rw mul_add,
  simp,
  ring,
  rw mul_comm,
  rw mul_comm (2 * n + 3) n,

[Shing Tak Lam]

import data.nat.basic
import algebra.big_operators tactic
import algebra.ring
import tactic

open_locale big_operators

open finset
open nat
open algebra

variables k n m x : ℕ
example (n : ℕ) : ∑ k in (range n.succ), (4 * k - 3) = n*(2*n-1) :=
begin
  induction n with n ih,
  refl,
  rw sum_range_succ,
  rw ih,
  simp [nat.succ_eq_add_one],
  repeat {rw mul_add},
  simp,
  rw add_comm,
  rw mul_comm (n + 1),
  rw add_mul,
  rw mul_add,
  simp,
  ring,
  rw mul_comm,
  rw mul_comm (2 * n + 3) n,
  ---- My part below
  cases n, -- turns out we don't need `by_cases`, just `cases` is enough
  { refl },
  { suffices : 2 * n.succ - 1 + 4 = 2 * n.succ + 3,
    { rw this },
    clear ih, -- We don't need ih here, and omega doesn't seem to like it
    omega }
end

[Claus-Peter Becke]

Thank you very much. That's great. I tried a longer time to close this goal. I will look at the API to get more informations about the tactics you used which are new for me.

[Claus-Peter Becke]

@Shing Tak Lam : In your very helpful explanations concerning the sum-formula in Lean you gave a description of the sums between limits i=0 or i=1 as the lower bound and i=n as the upper bound of the computation. If I understood you correctly that means that Lean doesn't distinguish with respect to the induction's base case between i=0 and i=1 but looks for a solution which contains i=0 or i=1. If the formula is satisfiable for one of these values the refl-tactic will close the base-case-goal. Is this correct?
What can be done to change especially the lower bound if there shall be computed inequalities which hold for example only presupposing a lower bound as 3 as in the following example:

example (n : ℕ) : ∑ k in (range n.succ), (k*k) ≥ 2*n + 3 :=

[Patrick Massot]

Your message is very obscure to me, but you may be looking for docs#nat.two_step_induction

[Shing Tak Lam]

@Claus-Peter Becke

Apologies if I caused any confusion. The reason why I said it didn't matter in the previous example is that the sum of the natural numbers from 0 to n is the same as the sum of the natural numbers from 1 to n, since 0 + x = x. Therefore in that specific example, it didn't matter that the sum in question had an extra term.

If you wanted a sum from i=a to i=b, you would use ∑ k in (range (b - a)) and then replace any k with k + a. I'm not sure what that inequality is supposed to be, and I haven't got too much time at the moment, but do you mean that k should be at least 3? Or do you mean that n should be at least 3?

[Claus-Peter Becke]

@Shing Tak Lam I meant k should be at least 3. Your proposal seems to be very helpful again. I will try it immediately. Your support is very worthwhile for me. So you don't have any reason to apologize. Because I'm a newbie in all these questions I'm dealing with in this context it happens that I misunderstand some informations which are given.