Practicing writing proofs

Stream: new members

[Adomas Baliuka]

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
                apply tsub_add_cancel_of_le
                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]

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 [add_sub_of_le mlen] at this
  rw [this]
  simp only [add_comm]

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

[Adomas Baliuka]

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]

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 addRightEmbedding_eq_addLeftEmbedding {G : Type*} [AddCancelCommMonoid G] (g : G) :
  addRightEmbedding g = addLeftEmbedding g := by ext; exact add_comm _ _

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
  simp_rw [sub_eq_iff_eq_add, ←addRightEmbedding_apply n, ←sum_map]
  rw [←sum_union, union_comm]
  · congr
    rw [addRightEmbedding_eq_addLeftEmbedding]
    convert range_add_eq_union _ _
    rw [add_tsub_cancel_of_le mlen]
  · simp [disjoint_left]

[Yaël Dillies]

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]

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]

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

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]

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)
  simp only [add_comm]
  convert Finset.sum_range_add_sub_sum_range _ _ _
  exact (add_sub_of_le mlen).symm

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]

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

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

[Ruben Van de Velde]

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
  · rw [add_sub_of_le mlen]
  · exact add_comm _ _

[Ruben Van de Velde]

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