## Stream: new members

### Topic: Practicing writing proofs

#### Adomas Baliuka (Sep 03 2023 at 18:02):

I wrote a proof that subtracting two sums over ranges equals sum over the difference of the ranges. The proof took me a long time and seems extremely ugly. I'm hoping to learn a lot by having someone look at it for 3 seconds and say how to do it in two lines. (Please let me know in case such a question is discouraged here)

lemma bigsum_minus_bigsum (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n) , f (h + n) := by
induction m generalizing n with
| zero =>
have nz : n = 0 := by linarith
simp [*]
| succ m ih =>
by_cases le : n ≤ m
· rw [minus_succ_eq_succ_minus]
repeat rw [Finset.sum_range_succ]
rw [←ih]
have minsimp : m - n + n = m := by
linarith
rw [minsimp]
have kk : ∑ x in range m, f x = ∑ k in range m, f k := by simp
rw [kk]
have mycomm (a b c : ℝ) : a + b - c = a - c + b := by ring
simp [mycomm]
exact le
exact le
· have eeq : n = m + 1 := by linarith
simp [*]


#### Moritz Firsching (Sep 03 2023 at 18:24):

could be made shorter, but this works:

lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) := by
have := Finset.sum_range_add_sub_sum_range (fun x => f x) n (m - n)
rw [this]


[edited: changed covert to simp only [add_comm]]

#### Adomas Baliuka (Sep 03 2023 at 18:30):

Wow, thanks! It says "expecting term". Is there something missing after convert? Did you know about sum_range_add_sub_sum_range or did you find it by some method I could learn?

#### Yaël Dillies (Sep 03 2023 at 18:33):

Here's a non-cheating proof, using only lemmas simpler than the one you're trying to prove:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic

open Finset
open scoped BigOperators

lemma bigsum_minus_bigsum (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n) , f (h + n) := by
rw [←sum_union, union_comm]
· congr
· simp [disjoint_left]


#### Yaël Dillies (Sep 03 2023 at 18:35):

Of course the better way is to use the existing lemma sum_range_add_sub_sum_range , which you could have found by looking for Finsetsumrangerange or Finsetsumrangesubin the docs: you know each part should appear in the name somewhere, and you can try a few permutations out (but typically sum will probably come before range).

#### Moritz Firsching (Sep 03 2023 at 18:39):

ab said:

Wow, thanks! It says "expecting term". Is there something missing after convert? Did you know about sum_range_add_sub_sum_range or did you find it by some method I could learn?

Yes, there was something missing, I changed the original message...

#### Adomas Baliuka (Sep 03 2023 at 19:36):

@Yaël Dillies If you don't mind me asking, how did you think of using these embeddings? Is that a normal technique in some circumstances? It seems very weird and roundabout somehow. You build these embedding objects and then coerce them to functions? (Is there a way to list coercions? I know about #synth but there I need to know input and output type. Is there a way to list instances and filter just by input or output?)

#### Yaël Dillies (Sep 03 2023 at 19:41):

My hand was forced by the way docs#Finset.range_add_eq_union was written. To be quite honest, I would have preferred a lemma of the form range a = range b ∪ (range (b - a)).map (addLeftEmbedding a).
The reason we use those embeddings is because we want to use docs#Finset.map instead of docs#Finset.image. This (somewhat rare pattern) is useful because it lets us carry around the proof of injectivity (or in the case of docs#Finset.sup' nonemptiness, or i ∉ s for docs#Finset.cons, etc...) and spares us a few proof obligations. Typically, I used docs#Finset.sum_map which doesn't require me (re)proving that the function is injective.

#### Moritz Firsching (Sep 03 2023 at 20:19):

lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) := by
have := Finset.sum_range_add_sub_sum_range (fun x => f x) n (m - n)


is better than what I wrote before.

I think @ab is asking about how to go from a name "Finsetsumrangesub" to the name of the theorem and one answer here is to use the search of https://leanprover-community.github.io/mathlib4_docs/. If you already know where to look for approximately, then typing Finset.sum and pressing Ctrl-space will show suggestions.
for the last exact, you can simply type exact? and it should find the  (add_sub_of_le mlen).symm part

#### Adomas Baliuka (Sep 04 2023 at 15:11):

@Moritz Firsching Why is this better? It has the same number of lines. I'm trying to understand what kind of proofs and style are considered "good".

#### Ruben Van de Velde (Sep 04 2023 at 15:18):

The have := .. is superfluous in the latest proof

#### Ruben Van de Velde (Sep 04 2023 at 15:22):

I'm not sure I agree it's better, in any case, since the simp only [add_comm] is still somewhat unfortunate. If you want to use convert (which means "I've nearly got the result I need, please show me where it differs from the current goal"), maybe this is nicer:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic

open BigOperators Finset Nat

lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) := by
convert Finset.sum_range_add_sub_sum_range _ _ _ using 3


#### Ruben Van de Velde (Sep 04 2023 at 15:27):

Or you could do:

import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Basic

open BigOperators Finset Nat

lemma bigsum_diff (m n : ℕ) (mlen : n ≤ m) (f : ℕ → ℝ) :
∑ k in range m, f k - ∑ h in range n, f h = ∑ h in range (m - n), f (h + n) :=
calc
_ = ∑ k in range (n + (m - n)), f k - ∑ k in range n, f k := by rw [add_sub_of_le mlen]
_ = ∑ k in range (m - n), f (n + k) := Finset.sum_range_add_sub_sum_range ..
-- Choose one of the following two lines
-- _ = _ := by simp_rw [add_comm]
-- _ = _ := Finset.sum_congr rfl fun _ _ => by rw [add_comm]


Not sure any of those are necessarily better or worse than the other alternatives

Last updated: Dec 20 2023 at 11:08 UTC