rw inside sum

Stream: Is there code for X?

[Nick Andersen]

Is there a way to perform a rewrite inside a sum (or other big operator)?
This is the shortest way I've found.

example {a b : ℕ → ℚ} : ∑ k ∈ range m, a k * b k  = ∑ k ∈ range m, b k * a k := by
  apply Finset.sum_congr rfl;
  intro _ _
  rw [mul_comm]

[Damiano Testa]

simp_rw?

[Nick Andersen]

Thanks, looks like that works.

simp_rw [mul_comm]

[Martin Dvořák]

Specifically _comm theorems often cause looping inside simp(_rw). If it happens to you (which can easily happen if you try to do the same thing without the auxiliary lemma), conv is your friend!

[Kevin Buzzard]

Can you give an example of looping Martin? I thought that this sometimes happened in Lean 3 but not in Lean 4.

[Kevin Buzzard]

@Nick Andersen here's what a conv mode proof would look like:

import Mathlib.Tactic

open Finset

variable (m : ℕ)

example {a b : ℕ → ℚ} : ∑ k ∈ range m, a k * b k  = ∑ k ∈ range m, b k * a k := by
  conv =>
    lhs
    congr
    rfl
    intro x
    rw [mul_comm]

See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.

[Martin Dvořák]

Kevin Buzzard said:

Can you give an example of looping Martin? I thought that this sometimes happened in Lean 3 but not in Lean 4.

import Mathlib
open BigOperators

example {a b : Fin 5 → Fin 4 → ℚ} (hab : a = b) :
    ∑ i : Fin 5, ∑ j : Fin 4, a i j = ∑ j : Fin 4, ∑ i : Fin 5, b i j := by
  rw [Finset.sum_comm, hab]

example {a b : Fin 5 → Fin 4 → ℚ} (hab : a = b) :
    ∑ i : Fin 5, ∑ j : Fin 4, a i j = ∑ j : Fin 4, ∑ i : Fin 5, b i j := by
  simp_rw [Finset.sum_comm]

The first proof succeeds. The second proof times out.

[Martin Dvořák]

Perhaps a better example:

import Mathlib
open BigOperators

example {a b : Fin 5 → Fin 4 → Fin 3 → ℚ} (hab : a = b) :
    ∑ i : Fin 5, ∑ j : Fin 4, ∑ k : Fin 3, a i j k =
    ∑ i : Fin 5, ∑ k : Fin 3, ∑ j : Fin 4, b i j k := by
  congr
  ext
  rw [Finset.sum_comm, hab]

example {a b : Fin 5 → Fin 4 → Fin 3 → ℚ} (hab : a = b) :
    ∑ i : Fin 5, ∑ j : Fin 4, ∑ k : Fin 3, a i j k =
    ∑ i : Fin 5, ∑ k : Fin 3, ∑ j : Fin 4, b i j k := by
  simp_rw [Finset.sum_comm]

example {a b : Fin 5 → Fin 4 → Fin 3 → ℚ} (hab : a = b) :
    ∑ i : Fin 5, ∑ j : Fin 4, ∑ k : Fin 3, a i j k =
    ∑ i : Fin 5, ∑ k : Fin 3, ∑ j : Fin 4, b i j k := by
  simp [Finset.sum_comm, hab]

The first proof succeeds. The second proof times out. The third proof times out, too.

[Kevin Buzzard]

FWIW here's a more golfed conv proof:

import Mathlib.Tactic

open Finset

variable (m : ℕ)

example {a b : ℕ → ℚ} : ∑ k ∈ range m, a k * b k  = ∑ k ∈ range m, b k * a k := by
  conv_lhs =>
    enter [2, x]
    rw [mul_comm]

[Martin Dvořák]

enter

[Martin Dvořák]

Does anybody know if those _comm theorems that "stay on the same level" never loop?

[Martin Dvořák]

Kevin Buzzard said:

Can you give an example of looping Martin? I thought that this sometimes happened in Lean 3 but not in Lean 4.

Maybe they are only theorems that swap big operators that loop, I don't know...

It sometimes happens to me when I have a serie of transformation inside double sum, which I use simp_rw for, then I want to do the "main swap" but I am too lazy to close simp_rw and open rw instead, so I just add , Finset.sum_comm inside the simp_rw and VS Code freezes...

[Junyan Xu]

You can also specify (implicit) arguments:

example {a b : Fin 5 → Fin 4 → Fin 3 → ℚ} (hab : a = b) :
    ∑ i : Fin 5, ∑ j : Fin 4, ∑ k : Fin 3, a i j k =
    ∑ i : Fin 5, ∑ k : Fin 3, ∑ j : Fin 4, b i j k := by
  simp_rw [Finset.sum_comm (f := a _), hab]
  -- or simp_rw [Finset.sum_comm (γ := Fin 4), hab]

[Yaël Dillies]

Martin Dvořák said:

The first proof succeeds. The second proof times out.

I actually think this is partly a regression over Lean 3. Heuristically, it seems that some cases that looped in Lean 3 don't loop in Lean 4, and vice-versa.

[Kevin Buzzard]

I had thought that Lean had some kind of internal total ordering of "things" and simp only applied mul_comm when it was putting things in order. But now I realise that I don't really know how this can work, so maybe I'm mistaken (e.g. if some lemma is of the form a * b = c and we're faced with b * a = c one would hope simp [mul_comm, the lemma] would work regardless of whether a < b or not).

[Richard Osborn]

The regular simp tactic does this. In my experience, simp_rw doesn't protect against "infinite loops".

[Ralf Stephan]

For rewrite inside BigOperators, see also this thread.

[Martin Dvořák]

Martin Dvořák said:

It sometimes happens to me when I have a serie of transformation inside double sum, which I use simp_rw for, then I want to do the "main swap" but I am too lazy to close simp_rw and open rw instead, so I just add , Finset.sum_comm inside the simp_rw and VS Code freezes...

As a result, I learnt not to be lazy to close simp_rw and open rw whenever rw is sufficient.

Sometimes it leads to funny code:
https://github.com/madvorak/vcsp/blob/057db7f3dc735d6a90cabe4bddeea8d665fc4f96/VCSP/FarkasBartl.lean#L182

[Yaël Dillies]

You should probably be using calc more

[Iván Renison]

Hi
I'm also struggling with rw inside of a sum. I have simplified my problem to this:

example (m : ℕ) (a : Fin m → ℚ) (h : ∀k, a k + 1 = 0) : ∑ k, a k + 1  = 0 := by
  simp_rw [h] -- fails with `simp made no progress`

I think that the problem is that a k + 1 and 0 are not exactly of the form f k for some function f, but I don't find an easy solution, do you now what can I do?

[Yaël Dillies]

∑ k, a k + 1 means (∑ k, a k) + 1, not ∑ k, (a k + 1). Does this clarify things?

[Iván Renison]

Ah, in this example that is the problem, but in the more complicated context I think the problem is not something like this, I will try to correctly simplify my problem

[Iván Renison]

I think that my problem comes from the fact that I'm summing over a subset:

example (n : ℕ) (s : Finset (Fin n)) (x : Fin n → E) (h : ∀k ∈ s, (x k = 0)) :
    (∑ k ∈ s, x k) = 0 := by
  simp_rw [h] -- fails with `simp made no progress`

[Ruben Van de Velde]

import Mathlib

example [AddCommMonoid E] (n : ℕ) (s : Finset (Fin n)) (x : Fin n → E) (h : ∀k ∈ s, (x k = 0)) :
    (∑ k ∈ s, x k) = 0 := by
  simp +contextual [h] -- works

[Yaël Dillies]

Yes, that's correct. simp_rw doesn't know about the binders it traverses by default. You need +contextual to make it so

[Iván Renison]

Great! Thank you very much!