Choosing dummy variable inside summation

Stream: new members

[Harry Richman]

When working with a summation in a proof, is there a way to explicitly choose a name for the variable indexing the sum?

The context here is that some tactics, i.e. simp_rw, will helpfully rewrite terms inside sums and products, but as a side effect seems to change the name of the index variable. In the example below, the outer sum has σ vary over all permutations, but after using simp_rw the σ is replaced with x. The inner product index i is replaced with x_1.

The choice of name of the dummy variable is in a sense non-essential, but having a way to enforce conventions like σ for permutations would help with readability in the infoview.

import Mathlib

variable {M N : Type} [Fintype M] [Fintype N] [DecidableEq M] [DecidableEq N] [LinearOrder M] [LinearOrder N]

theorem Matrix.det_mul' (A : Matrix M N ℤ) (B : Matrix N M ℤ) :
  det (A * B) = ∑ f : M ↪o N, det (A.submatrix id f) * det (B.submatrix f id) := by
  -- expand determinant in matrix entries as sum over permutations, on LHS
  rw [Matrix.det_apply (A * B)] -- uses σ for summing permutations
  -- expand entries of matrix product A*B
  simp_rw [Matrix.mul_apply] -- uses x for summing permutations :(

  sorry

[Luigi Massacci]

This should work: change ∑ f, Equiv.Perm.sign f • ∏ x_1, ∑ j, A (f x_1) j * B j x_1 = _

[Luigi Massacci]

replace f with whatever you want

[Luigi Massacci]

I don't know if it's the best solution though

[Eric Wieser]

This probably makes sense as aconv tactic

[Luigi Massacci]

I had thought of using conv, but this was the best I could do:

conv =>
    enter [-2, 2, x]
    tactic => rename Equiv.Perm M => t

which is uglier, even if rename was a conv tactic (which it probably should be, or change as you said. Assuming I understand what a conv tactic is ; ) I can still image it might be useful for bigger terms

[Robin Arnez]

Harry Richman schrieb:

but as a side effect seems to change the name of the index variable

For this reason binderNameHint exists. But mathlib doesn't seem to use it...

[Eric Wieser]

It looks like the use of docs#Finset.sum_congr is to blame

[Robin Arnez]

Yeah right it should use binderNameHint there probably

[Robin Arnez]

although I'm not certain it even works for congruence theorems

[Eric Wieser]

-- replaces `Finset.sum_congr
@[congr]
theorem Finset.sum_congr_binder {ι M : Type*} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M}
  (h : s₁ = s₂) : (∀ x ∈ s₂, f x = binderNameHint x g (g x)) →
    s₁.sum f = s₂.sum g :=
  Finset.sum_congr h

is not legal

[Eric Wieser]

cc @Joachim Breitner

[Joachim Breitner]

I’d have expected

@[congr]
theorem Finset.sum_congr_binder {ι M : Type*} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M}
  (h : s₁ = s₂) : (∀ x ∈ s₂, binderNameHint x f (f x = g x)) →
    s₁.sum f = s₂.sum g :=
  Finset.sum_congr h

i.e. the binderNameHint should take the binder from f, not g. If this doesn't work, a MWE might help.

The hint should work in congruence assumptions since https://github.com/leanprover/lean4/pull/7053

[Robin Arnez]

Hmm no apparently simp can't use that?
It just says: [Meta.Tactic.simp.congr] Finset.sum_congr_binder not modified

[Joachim Breitner]

What about

@[congr]
theorem Finset.sum_congr_binder {ι M : Type*} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M}
  (h : s₁ = s₂) : (∀ x ∈ s₂, binderNameHint x f (f x) = g x) →
    s₁.sum f = s₂.sum g :=
  Finset.sum_congr h

(that's the form I used in the test case for the PR)

[Eric Wieser]

That works!

[Robin Arnez]

I guess this should probably be the form present in mathlib then

[Eric Wieser]

#24957

[Robin Arnez]

Well the only complaint I have about binderNameHint is that it makes theorem statements a bit annoying to read

[Robin Arnez]

maybe it's fine to

@[app_unexpander binderNameHint]
def unexpandBinderNameHint : Lean.PrettyPrinter.Unexpander
  | `($_ $_ $_ $x) => pure x
  | _ => throw ()

but that might hide too much..?

[Joachim Breitner]

I fully agree. And that it’s a game of whack-a-mole to adjust all the tactics that should heed the hint.

It’s a hack that I’m not proud of (but still prefer to not having that hack at all).

[Robin Arnez]

Hmm would it be fine to make it an abbrev? It seems like that could be part of why #24957 failed to build

[Kevin Buzzard]

Yes it would be great to fix this. Thanks for the work above! It's especially annoying when simp_rw or whatever replaces the variable being summed over with i when you already have an i, because then you randomly get an i_1 which you almost never want.

[Joachim Breitner]

Robin Arnez said:

Hmm would it be fine to make it an abbrev? It seems like that could be part of why #24957 failed to build

Probably; do you want to try that and make a PR for that to find out?

[Robin Arnez]

Should I then also add an unexpander? Although again it's probably not best to hide details...

[Eric Wieser]

I forget why we didn't make it an Expr.mdata; could you remind me?

[Joachim Breitner]

Robin Arnez said:

Should I then also add an unexpander? Although again it's probably not best to hide details...

I’d be hesitant, it may cause confusion

[Joachim Breitner]

Eric Wieser said:

I forget why we didn't make it an Expr.mdata; could you remind me?

Because the value of .mdata cannot refer to expressions, can it?

[Robin Arnez]

Eric Wieser schrieb:

I forget why we didn't make it an Expr.mdata; could you remind me?

I think the problem is that mdata can't refer to variables like f and x

[Eric Wieser]

Are things any better if the syntax instead becomes:

(h : ∀ x : binderNameHint f _, x ∈ s₂ → f x = g x)

[Eric Wieser]

Or maybe even

(h : binderNameHint f (∀ x ∈ s₂, f x = g x))

[Eric Wieser]

That last one is far more likely to be unfolded before it causes trouble, since intro is enough to do it

[Robin Arnez]

We probably also want to allow ∃ x, p x to have a binder name hint so the last one doesn't work too well I don't think (because the x is nested in the Exists)

[Eric Wieser]

I guess that becomes Exists (binderNameHint p fun x => p x)

[Eric Wieser]

You could envisage a custom delaborator along the lines of ∃ x%$p, p x that expands to this, sort of matching %$tk in syntax antiquotations

[Robin Arnez]

∃ x, binderNameHint _ _ (p x) doesn't need support like that though

[Harry Richman]

Thanks @Luigi Massacci for the quick fix and everyone else for working on sorting out the underlying problem!