Zulip Chat Archive

Stream: new members

Topic: induction


Iocta (Aug 18 2020 at 05:54):

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 (Aug 18 2020 at 06:24):

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 (Aug 18 2020 at 06:29):

I see, thanks.

Kenny Lau (Aug 18 2020 at 06:32):

induction h

Iocta (Aug 18 2020 at 06:43):

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 (Aug 18 2020 at 06:46):

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 (Aug 18 2020 at 06:48):

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 (Aug 18 2020 at 06:49):

ah that's what I was looking for

Claus-Peter Becke (Sep 23 2020 at 16:09):

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 (Sep 23 2020 at 16:13):

have you seen algebra.big_operators?

Claus-Peter Becke (Sep 23 2020 at 16:16):

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

Claus-Peter Becke (Sep 24 2020 at 06:19):

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 (Sep 24 2020 at 07:55):

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 (Sep 24 2020 at 08:48):

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 (Sep 24 2020 at 11:47):

@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 (Sep 24 2020 at 11:52):

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

Johan Commelin (Sep 24 2020 at 11:54):

@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 (Sep 24 2020 at 12:09):

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 (Sep 24 2020 at 13:02):

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 (Sep 24 2020 at 13:05):

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 (Sep 24 2020 at 13:06):

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 (Sep 24 2020 at 13:16):

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 (Sep 24 2020 at 13:19):

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 (Sep 24 2020 at 17:05):

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 (Sep 26 2020 at 06:44):

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 (Sep 26 2020 at 06:51):

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 (Sep 26 2020 at 06:53):

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 (Sep 26 2020 at 06:54):

This finds sum_range_succ for you.

Scott Morrison (Sep 26 2020 at 06:54):

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 (Sep 26 2020 at 06:55):

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 (Sep 26 2020 at 06:56):

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

Claus-Peter Becke (Sep 26 2020 at 07:06):

@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 (Sep 26 2020 at 07:25):

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

Scott Morrison (Sep 26 2020 at 07:26):

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 (Sep 26 2020 at 07:26):

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

Claus-Peter Becke (Sep 26 2020 at 07:30):

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 (Sep 26 2020 at 07:37):

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

Claus-Peter Becke (Sep 26 2020 at 07:38):

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 (Sep 26 2020 at 07:40):

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 (Sep 26 2020 at 07:41):

And you're still using a broken division

Kevin Buzzard (Sep 26 2020 at 07:41):

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

Scott Morrison (Sep 26 2020 at 07:42):

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 (Sep 26 2020 at 07:42):

which prints

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

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

Scott Morrison (Sep 26 2020 at 07:43):

(slim_check is very new to mathlib)

Claus-Peter Becke (Sep 26 2020 at 07:53):

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

Kevin Buzzard (Sep 26 2020 at 07:54):

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 (Sep 26 2020 at 07:55):

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 (Sep 26 2020 at 08:15):

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

Kevin Buzzard (Sep 26 2020 at 08:36):

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 (Sep 27 2020 at 09:37):

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 (Sep 28 2020 at 16:10):

Is there any possibility to solve the following goal?

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

Shing Tak Lam (Sep 28 2020 at 16:15):

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 (Sep 28 2020 at 16:18):

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 (Sep 28 2020 at 16:23):

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 (Sep 28 2020 at 16:24):

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 (Sep 28 2020 at 16:26):

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 (Sep 28 2020 at 16:30):

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 (Sep 28 2020 at 16:34):

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 (Sep 30 2020 at 06:56):

@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 (Sep 30 2020 at 07:06):

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

Shing Tak Lam (Sep 30 2020 at 07:07):

@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 (Sep 30 2020 at 07:14):

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


Last updated: Dec 20 2023 at 11:08 UTC