Beginner problem

Stream: new members

[Robert hackman]

I hope this is not redicolusly stupid but I'm trying to proof example that ∑ k in range n, k^2 = (n*(n+1)*(2*n+1))/6.
Therefor I want to use sum_range_succ tactic to then rewrite with ih. What I don't understand is why in the sum_range_succ, it's
((range n.succ).map f).prod = ((range n).map f).prod * f n and not ((range n.succ).map f).prod = ((range n).map f).prod * f n+1(note that it's all to_additive). I'm not sure if my mistake is using the wrong lean(or mathlib) tactic or if it's my math that's wrong

[Kevin Buzzard]

I would strongly recommend that you (a) get your normalisation right (your statement is false for n=1, range is 0 to n-1) and (b) coerce to the rationals before summing (ie. sum (k : Rat)^2). At the minute your statement uses natural number division which is pathological, and once you've sorted out your normalisation it will also use natural number subtraction which is also pathological. Coercing to the rationals fixes these problems because rational number division and subtraction are not pathological.

[Kevin Buzzard]

The answer to your question is that range n is 0 to n-1.

[Robert hackman]

Thank you! I got quite "far" solving (that admitedly very simple example but I'm new to proof languages) but now I'm stuck again (same problem).
I need to proof that n * (n + 1) * (2 * n + 1) / 6 + (n + 1) ^ 2 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) / 6. Now using the ring tactic is suggested everywhere but for reasons I don't understand it doesn't work. Neither does ring_nf (was suggested by the compiler) or simp. Maybe somebody has literature on how to solve such polynoms if it's not working immidiately with ring. I would simplify it myself but I just don't have an idea on how really...

[Ruben Van de Velde]

Robert hackman said:

Thank you! I got quite "far" solving (that admitedly very simple example but I'm new to proof languages) but now I'm stuck again (same problem).
I need to proof that n * (n + 1) * (2 * n + 1) / 6 + (n + 1) ^ 2 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) / 6. Now using the ring tactic is suggested everywhere but for reasons I don't understand it doesn't work. Neither does ring_nf (was suggested by the compiler) or simp. Maybe somebody has literature on how to solve such polynoms if it's not working immidiately with ring. I would simplify it myself but I just don't have an idea on how really...

Please show a #mwe, but probably because of the division.

[Robert hackman]

Ok, this is the exampel I'm trying to proof(can't figure out how to do multiline code highlight sry):

import Mathlib.Data.Num.Lemmas
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring

open Num
open BigOperators
open Finset
open Nat

example (n : Nat) (k: Rat): ∑ k in range (n+1), k^2 = (n*(n+1)*(2*n+1)) / 6 := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[sum_range_succ]
    rw[ih]
    rw[succ_eq_add_one]
    ring

[Ruben Van de Velde]

#backticks - use three rather than one. You should also use the correct capitalization for imports (i.e. import Mathlib.Tactic.Ring rather than import Mathlib.tactic.ring) to avoid confusing lean. (It's unfortunate that this works at all.)

[Robert hackman]

ah ok thx, do you maybe have an idea how to solve the polomial with the fraction? :D

[Ruben Van de Velde]

ring is having difficulties with the natural division.

One solution is not to use it, and then field_simp (import Mathlib.Tactic.FieldSimp) can help you get rid of it:

example (n : Nat) : ∑ k in range (n+1), (k : ℚ) ^ 2 = (n * (n+1) * (2*n+1) : ℚ) / 6 := by
  field_simp
  ...

In this case, you might need push_cast or norm_cast to finish the proof

The other solution is to use a Nat-specific lemma first:

example (n : Nat) : ∑ k in range (n+1), k^2 = (n * (n+1) * (2*n+1)) / 6 := by
  symm
  apply Nat.div_eq_of_eq_mul_left (by norm_num)
  ...

[Kevin Buzzard]

@Robert hackman the statement you are formalising is not the correct way to state the theorem you want to prove. Natural division is pathological. Lean thinks 14/6=2, not 2.33333... . So the claim you're making is strictly weaker than the claim you want to make (for example you won't be able to deduce that 6 times the sum is the cubic on the numerator)

[Ruben Van de Velde]

And note that both of my suggestions come down to proving the stronger result anyway, which turns out to be easier than proving the weaker result

[Robert hackman]

Ok but how do I make it more "strong"? I suppose n can stay Nat but do I then have to cast the division or maybe define the return type of the example?

[Robert hackman]

So I've tried all comibinations off symm&dif_eq.. and field simp but none seem to work. field_simp doesn't modify the equation at all and div_eq does get rid of the fractions (even if there is one left but that disappears after applying ring) but ring can't prove equality.
Edit: It's equal though it's just not "recognized"

Here's my try with div_eq:

example (n : Nat) : ∑ k in range (n+1), k^2 = (n*(n+1)*(2*n+1)) / 6 := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[sum_range_succ]
    rw[ih]
    rw[succ_eq_add_one]
    symm
    apply Nat.div_eq_of_eq_mul_left (by norm_num)
    ring

I would be so thankful for help!

[Ruben Van de Velde]

Try removing the denominator before the induction

[Robert hackman]

sorry for the confusion. The resulting equation after the last ring ist actually equal (if simplified with pen and paper) but I can't get lean to "recognize that

[Robert hackman]

So the result of the last applied ring tactic is this equation: ⊢ 6 + n * 13 + n ^ 2 * 9 + n ^ 3 * 2 = 6 + n * 12 + n ^ 2 * 6 + (n + n ^ 2 * 3 + n ^ 3 * 2) / 6 * 6, which is equal but I simp or ring both don't get it to a point where one could use rfl.

[Ruben Van de Velde]

That still has a natural division. Please show the complete code you have now?

[Robert hackman]

That would be the current code

example (n : Nat): ∑ k in range (n+1), k^2 = (n*(n+1)*(2*n+1)) / 6 := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[sum_range_succ]
    rw[ih]
    rw[succ_eq_add_one]
    symm
    apply Nat.div_eq_of_eq_mul_left (by norm_num)
    ring_nf

Edit: I'm still unsure about what you mean with "natrual division" or how to address it

[Ruben Van de Velde]

Ruben Van de Velde said:

Try removing the denominator before the induction

you haven't applied this suggestion ^

[Ruben Van de Velde]

Natural division is division between two natural numbers, rather than for example between two rational numbers.

[Ruben Van de Velde]

As a general rule, if you want to use ring, there shouldn't be any division symbols in your goal

[Kevin Buzzard]

I'm sorry I'm in a field and can't write code but the answer is to coerce the summand into the rationals immediately. Then all the problems go away and the tactics start working again. You should be summing (k : Rat)^2

[Robert hackman]

Ruben Van de Velde said:

Ruben Van de Velde said:

Try removing the denominator before the induction

you haven't applied this suggestion ^

Sorry for being so stupid.
But I'm just not fully understanding what you mean :D.
Are you saying that I should remove the / 6 from the equation, which would make it false.
Or should I "remove" it through multiplication, which I sadly can't figure out how to do.
Or to multiply with0,5instead div /2. Again sry for not getting it... ):

[Damiano Testa]

Kevin's suggestion is this:

example (n : Nat) : ∑ k in range (n+1), (k ^ (2 : ℕ) : ℚ) = (n * (n+1) * (2*n+1)) / 6 := by

after that, you should be able to use induction, field_simp and ring.

[Damiano Testa]

(I think that the slight awkwardness around the type ascription is due to the not-yet-fixed parsing of HPow, which tries to raise ℚ to ℚ, instead of ℕ. Hence the explicit coercions. Someone else might find a more reasonable way of getting the right types in the right places.)

[Damiano Testa]

Basically, this is saying: raise k to the natural number 2, interpret the result as a rational number and continue with your usual parsing. The goal now is an equality of rational numbers and division by 6 is "actual" division, rather than Floor ∘ Div.

[Richard Copley]

Robert hackman said:

Ruben Van de Velde said:

Ruben Van de Velde said:

Try removing the denominator before the induction

you haven't applied this suggestion ^

But I'm just not fully understanding what you mean :D.

Ruben suggested that you start like this:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic

open BigOperators
open Finset
open Nat

example (n : Nat): ∑ k in range (n+1), k^2 = (n*(n+1)*(2*n+1)) / 6 := by
  symm
  apply Nat.div_eq_of_eq_mul_left (by norm_num)
  -- ⊢ n * (n + 1) * (2 * n + 1) = (∑ k in range (n + 1), k ^ 2) * 6

The proof in your original post, with a couple of small modifications, closes this goal.

[Robert hackman]

ok, thank you all so much

Current state(I didn't yet try to also implmenet the type coercion bc there is a type error at Nat.div_eq which I don't understnad):

example (n : Nat): ∑ k in range (n+1), k ^ 2 = (n*(n+1)*(2*n+1)) / 6 := by
  symm
  apply Nat.div_eq_of_eq_mul_left (by norm_num)
  symm
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[sum_range_succ]
    rw[ih]
    rw[succ_eq_add_one]

It throws an error that it cannot do rw[ih] because it can't find the pattern. the ih is: (∑ k in range (n + 1), k ^ 2) * 6 and the tactic state is (∑ x in range (n + 1), x ^ 2 + (n + 1) ^ 2) * 6 = Nat.succ n * (Nat.succ n + 1) * (2 * Nat.succ n + 1). Now I tried rw[mul_add]but that does not change the left side. Any suggestions I'm a bit out of ideas again

[Richard Copley]

rewrite [← ih]

[Robert hackman]

ahhh I got it :) I was using rw[mul_add] which is alias for left_distrib but I needed right_distrib:) goal is solved thank you all so much!

[Robert hackman]

So that's the working version:

example (n : Nat): ∑ k in range (n+1), (k ^ (2 : ℕ) : ℕ) = (n*(n+1)*(2*n+1)) / 6 := by
  symm
  apply Nat.div_eq_of_eq_mul_left (by norm_num)
  symm
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[sum_range_succ]
    rw[right_distrib]
    rw[ih]
    rw[succ_eq_add_one]
    ring

Note that k sum is still of type N not Q. if I change it to Q Nat.div_eq... throws the following error:

tactic 'apply' failed, failed to unify
  ?m.741 / ?m.740 = ?m.742
with
  ↑n * (↑n + 1) * (2 * ↑n + 1) / 6 = ∑ k in range (n + 1), ↑(k ^ 2)
n : ℕ
⊢ ↑n * (↑n + 1) * (2 * ↑n + 1) / 6 = ∑ k in range (n + 1), ↑(k ^ 2)

Does maybe somebody have and idea why?

[Richard Copley]

theorem Nat.div_eq_of_eq_mul_left : ∀ {n m k : ℕ}, 0 < n → m = k * n → m / n = k
The conclusion of the lemma doesn't unify with the goal because the variables are of the wrong type. But the idea was that you wouldn't need it.

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Tactic

open BigOperators
open Finset
open Nat

example (n : Nat): ∑ k in range (n+1), (k ^ (2 : ℕ) : ℚ) = (n*(n+1)*(2*n+1)) / 6 := by
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[sum_range_succ]
    rw[ih]
    rw[succ_eq_add_one]
    field_simp
    ring_nf

[Richard Copley]

(By the way, if you include all the preamble that makes the example work, it makes the 'View in playground' gadget at the top right of the code sample much more useful.)

[Robert hackman]

ahh oka so I see why div_eq_of_eq_mul_left was not working and also what you meant. I think I mixed up equations that why it didn't work for me. That's way more elegeant

just to be sure, the reason why this works is because the equation is thanks to the coercion also applying to Rational numbers which makes field_simp and subsequently ring work because they can assume that division is "allowed"?

[Richard Copley]

field_simp can use facts like ∀ (x y : ℚ) : y ≠ 0 → x / y * y = x to simplify the expression. In the naturals, that fact is not true. Counterexample: 7 / 6 * 6 = 6 ≠ 7.

It so happens that n * (n + 1) * (2 * n + 1) / 6 * 6 = n * (n + 1) * (2 * n + 1) is always true, because 6 ∣ n * (n + 1) * (2 * n + 1), but ring can't prove that by itself.

[Jordi Majó]

Hello,
I am very new here. Does anyone know if there is a solutions document to the exercises in "Theorem Proving in LEAN 4"?
Thx

[Robert hackman]

Buster said:

field_simp can use facts like ∀ (x y : ℚ) : y ≠ 0 → x / y * y = x to simplify the expression. In the naturals, that fact is not true. Counterexample: 7 / 6 * 6 = 6 ≠ 7.

It so happens that n * (n + 1) * (2 * n + 1) / 6 * 6 = n * (n + 1) * (2 * n + 1) is always true, because 6 ∣ n * (n + 1) * (2 * n + 1), but ring can't prove that by itself.

thank you!

[Robert hackman]

So I'm feeling a bit stupid but I can't get Ico(or others) to work.
My current try looks like that: example (n : ℕ): ∑ k in ((Ico 1 n) : Finset ℕ), ((k - 1 )^2 : ℕ ) < n^3 / 3 := by sorry. Lean(4) was complaining that Ic 1 n was returning a Set N and not A Finset, so I was "casting" it as such. But that apparently is not enough because I'm still getting the same error.

[Robert hackman]

(i'm using Finset.Sum, I will try using something that's not finite, which is kind of not possible so will have to cast then but how?)

[Robert hackman]

So I found toFinset but am failing to apply it.
example (n : ℕ): ∑ k in (Ico 1 n).toFinset, ((k - 1 )^2 : ℕ ) < n^3 / 3 := by sorrythrows failed to synthesize instance Fintype ↑(Ico 1 n), but why?

[Eric Wieser]

What is Ico here? Is it an autoImplicit?

[Eric Wieser]

Which is to say; can you make that a #mwe with imports?

[Notification Bot]

5 messages were moved here from #new members > Definition of mapping by Eric Wieser.

[Ruben Van de Velde]

Robert hackman said:

So I found toFinset but am failing to apply it.
example (n : ℕ): ∑ k in (Ico 1 n).toFinset, ((k - 1 )^2 : ℕ ) < n^3 / 3 := by sorrythrows failed to synthesize instance Fintype ↑(Ico 1 n), but why?

Use Finset.Ico instead

[Robert hackman]

Ruben Van de Velde said:

Robert hackman said:

So I found toFinset but am failing to apply it.
example (n : ℕ): ∑ k in (Ico 1 n).toFinset, ((k - 1 )^2 : ℕ ) < n^3 / 3 := by sorrythrows failed to synthesize instance Fintype ↑(Ico 1 n), but why?

Use Finset.Ico instead

Ok, did do so.

Mwe:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Num.Lemmas
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FieldSimp
import Mathlib.Data.Finset.Basic
import Mathlib.Order.LocallyFinite

open Num
open BigOperators
open Finset
open Nat

example (n : ℕ): ∑ k in Finset.Ico 1 n, ((k - 1 )^2 : ℕ ) < n^3 / 3 := by sorry

But it's throwing: "failed to synthesize instance \n LocallyFiniteOrder ℕ"

[Damiano Testa]

I think that you are missing an import:

import Mathlib.Data.Nat.Interval

[Damiano Testa]

I found it as follows: I assumed that the instance would be some standard fact, so import Mathlib.Tactic should be enough to get it.
With that import, I typed

#synth LocallyFiniteOrder ℕ  -- instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring
#check instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring

and hovering over the instance name, I saw in the pop-up which file contained the instance.

As a general rule, though, I would try to minimise imports only towards the end of a project, to avoid precisely this sort of issue. Importing Mathlib.Tactic is generally a good way of getting a good mix of results that can be useful.

[Robert hackman]

this is so weird, my background is lowlevel and such and I'm very new to funcitonal programming/ Math but this seems odd.
Just to be clear: An import can depend on another import?
I'm just not used to the idea in a highlevel language context... Is there a specific reason/ advantage?
thx btw,!

[Damiano Testa]

Also, it seems that your result is only true starting from n = 2:

#eval do -- [(0, false), (1, false), (2, true), (3, true), (4, true)]
  let bound := 4
  let ns := List.range bound
  let res := ns.map <| fun n => decide <| ∑ k in Finset.Ico 1 n, ((k - 1 )^2 : ℕ ) < n^3 / 3
  IO.println (ns.zip res)

[Damiano Testa]

The issue with your previous example was that Lean wanted to know that the interval of the natural numbers between 1 and n produced a Finset. This would not be true, say, for the rational numbers, so something needs to guarantee this fact.

The way this happens in mathlib is via someone proving that "locally finite" suffices. So now you need to know that ℕ is "locally finite" and this is something that Lean infers from the typeclass system: someone placed an instance of "locally finite" on ℕ. This happened in the file that I linked to earlier.

Thus, if you do not instruct Lean that "locally finite" is a property that ℕ has, then Lean will not be able to fill in the proof that the interval in ℕ from 1 to n is finite and therefore will not understand why you are telling it to build the Finset.Ico 1 n.

[Damiano Testa]

(Also note that completely implicit in the previous discussion is the fact that intervals make sense when there is an underlying order that we are referring to: this is also something that happens invisibly, thanks to the typeclass system. Except that the order on the natural numbers is defined way earlier than the locally finite instance.)

[Damiano Testa]

As before, you can see where the instance LE on Nat is defined:

#synth LE Nat  -- instLENat
#check instLENat  -- import Init.Prelude

Init.Prelude is a very early file in the import hierarchy: basically, as soon as you can talk about the natural numbers, you get inequalities between then for free.

[Robert hackman]

very interesting, thank you so much!

[Damiano Testa]

As for your question on dependencies: a file can import anything that does not transitively depend on itself. You can import files that depend on each other: for instance, this is ok

import Mathlib.Tactic
import Mathlib.Tactic
import Mathlib.Tactic
import Mathlib.Tactic
import Mathlib.Tactic
import Mathlib.Tactic

-- no issues

[Robert hackman]

thank you again!
just one last small question :D
You mentioned that it is only from 2 on, I think that's because Ico is from n to m-1 so Ico 1 n for 1 is actuall 0 for which it's untrue in general.

So I also need n to start from 1 and not 0, how would I do that?

[Damiano Testa]

You could do it in several ways. For instance, you could add a hypothesis (h2 : 2 ≤ n):

example (n : ℕ) (h2 : 2 ≤ n) : ∑ k in Finset.Ico 1 n, ((k - 1 )^2 : ℕ ) < n^3 / 3 := by sorry

You could alternatively replace n by n + 2 in the conclusion:

example (n : ℕ) : ∑ k in Finset.Ico 1 (n + 2), ((k - 1 )^2 : ℕ ) < (n + 2)^3 / 3 := by sorry

I think that the first would be preferable. Sometimes, "adding 1" generates better "definitional equalities" and you might see two versions of the same theorem, one using n + 1 and one assuming 1 ≤ n instead. These should just hide implementation details, though: they can be important, but they are not specifically maths issues.

[Robert hackman]

Damiano Testa said:

You could do it in several ways. For instance, you could add a hypothesis (h2 : 2 ≤ n):

example (n : ℕ) (h2 : 2 ≤ n) : ∑ k in Finset.Ico 1 n, ((k - 1 )^2 : ℕ ) < n^3 / 3 := by sorry

You could alternatively replace n by n + 2 in the conclusion:

example (n : ℕ) : ∑ k in Finset.Ico 1 (n + 2), ((k - 1 )^2 : ℕ ) < (n + 2)^3 / 3 := by sorry

I think that the first would be preferable. Sometimes, "adding 1" generates better "definitional equalities" and you might see two versions of the same theorem, one using n + 1 and one assuming 1 ≤ n instead. These should just hide implementation details, though: they can be important, but they are not specifically maths issues.

ok, the second seems viable and works. But there is no way to actually define(init) n except for the type?

[Damiano Testa]

I am not sure that I understand your question. You can define the type of natural numbers that are at least 2 and then let n be a term of that type. While this would work, you would have a lot of background work to prove all the results that you use about ℕ for your new custom type.

However, maybe closer to what your question is asking is that you can construct closed terms of type ℕ by starting from 0 and repeatedly applying Nat.succ to it. Introducing a "generic" term of type ℕ allows you to use it and you can still apply Nat.succ to it. So you could introduce n by (n : ℕ) and then apply the Nat.succ constructor to it. E.g. you could do Nat.succ (Nat.succ n). Note also that this is different from n + 2, because of how parentheses are inserted:

Nat.succ (Nat.succ n) = (n + 1) + 1
n + 2 = n + (1 + 1)

However, I think that what models better a natural number starting from a given bound is to introduce a generic natural number and then assuming that it is at least the bound that you want (i.e. solution 1 above).

[Damiano Testa]

In terms of preferring style 1 or 2 above, there is also a "library" consideration.

With style 1, someone who might want to use your result would be able to apply it to any term of type ℕ and be left with a proof obligation that their term was at least 2.

With style 2, applying your result requires the term to be of the form (whatever in ℕ) + 2. This is less flexible than the previous method.

Of course, ultimately they are equivalent and you can work with either, but, given the structure of mathlib, the first method leads to a smoother experience later on.

[Robert hackman]

yeah makes sense! thanks :)