Destruction and big operators

Stream: mathlib4

[Oliver Nash]

Consider the following three examples:

import Mathlib.Data.Nat.Choose.Sum

open BigOperators Finset Nat

-- Example 1 [valid syntax]
example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ m in antidiagonal n, choose n m.fst • (x ^ m.fst * y ^ m.snd) :=
  h.add_pow' n

-- Example 2 [valid syntax]
example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = (antidiagonal n).sum fun ⟨i, j⟩ ↦ choose n i • (x ^ i * y ^ j) :=
  h.add_pow' n

-- Example 3 [invalid syntax]
example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ ⟨i, j⟩ in antidiagonal n, choose n i • (x ^ i * y ^ j) :=
  h.add_pow' n

[Oliver Nash]

Back in the Lean 3 days, only Example 1 was valid. Happily Example 2 now also works.

Is there any way we could get Example 3 to work?

[Anatole Dedecker]

I think this is related. From what I understand all big operators use the same type of binders, extBinder (I'm not sure how to name what it is. A syntax category?). It allows the things like ∀ ε > 0, but not the destructing thing.

[Oliver Nash]

Thanks! It would be really nice if we could somehow do this.

[Eric Wieser]

extBinder seems entirely useless in big operators, since you can't have a finset of proofs

[Arend Mellendijk]

I like your suggestion, but (perhaps as a workaround) would it make sense to have custom notation for sums over antidiagonal? Something like

∑ i + j = n, choose n i • (x ^ i * y ^ j)

[Eric Wieser]

You can do that already with docs#Finsum

[Oliver Nash]

Eric Wieser said:

extBinder seems entirely useless in big operators, since you can't have a finset of proofs

I don’t understand this answer. Are you saying we can never have this notation?

[Eric Wieser]

I challenge you to find a situation where an extBinder-style binder is not a type error with Finset.sum

[Eric Wieser]

And therefore we could just use a regular binder instead and would get the feature you want without losing any features that currently exist

[Arend Mellendijk]

Eric Wieser said:

You can do that already with docs#Finsum

Right, but you lose the bundled finiteness which makes doing things like commuting sums quite painful.

[Oliver Nash]

Eric Wieser said:

And therefore we could just use a regular binder instead and would get the feature you want without losing any features that currently exist

I’m afraid this is still way too technical for me to follow. Perhaps I’ll think about this again tomorrow.

[Yaël Dillies]

In LeanAPAP, we introduced notation for (s.filter p).sum f. It's really lovely and is quite close to your suggestion, Arend.

[Yaël Dillies]

Btw, are we sure that examples 2 and 3 above are syntactically as general as example 1? I would expect not, but maybe defeq eta struct is saving the day.

[Anatole Dedecker]

(deleted)

[Eric Wieser]

Defeq isn't relevant for syntactic generality unfortunately; so there absolutely still is a reason to worry about that

[Eric Wieser]

Hmm, maybe I'm wrong about that

[Eric Wieser]

Yes, this is fine:

import Mathlib.Data.Nat.Choose.Sum

open BigOperators Finset Nat

-- Example 1 [valid syntax]
lemma nice (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ m in antidiagonal n, choose n m.fst • (x ^ m.fst * y ^ m.snd) :=
  h.add_pow' n

-- Example 2 [valid syntax]
lemma ugly (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = (antidiagonal n).sum fun ⟨i, j⟩ ↦ choose n i • (x ^ i * y ^ j) :=
  h.add_pow' n

#print nice
#print ugly

example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ m in antidiagonal n, choose n m.fst • (x ^ m.fst * y ^ m.snd) := by
  rw [←ugly h]

[Eric Wieser]

So it looks like rw knows to unfold match statements

[Eric Wieser]

Oliver Nash said:

Eric Wieser said:

And therefore we could just use a regular binder instead and would get the feature you want without losing any features that currently exist

I’m afraid this is still way too technical for me to follow. Perhaps I’ll think about this again tomorrow.

Looking more closely, the code in Lean.Elab.Binders doesn't seem to be written in a way that makes it particularly easy to insert Finset.sum between binders

[Kyle Miller]

extBinder is sort of a red herring here. The big sum notation only uses it to get ident and ident : type syntax.

In principle it should be easy to support destructuring by changing it to term. You just lose ident : type without parentheses before the in (does anyone use that?)

[Kyle Miller]

It'd be nice to get big operators to use notation3 someday; if that's done, we'd want to improve extBinder to support destructuring.

[Kyle Miller]

#6795 has a custom modification to extBinder to experiment with destructuring

[Kyle Miller]

These all work:

import Mathlib.Data.Nat.Choose.Sum

variable (α : Type*) [Ring α] (x y : α)

open BigOperators Finset Nat

-- Example 1
example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ m ∈ antidiagonal n, choose n m.fst • (x ^ m.fst * y ^ m.snd) :=
  h.add_pow' n

-- Example 2
example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = (antidiagonal n).sum fun ⟨i, j⟩ ↦ choose n i • (x ^ i * y ^ j) :=
  h.add_pow' n

-- Example 3
example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ ⟨i, j⟩ ∈ antidiagonal n, choose n i • (x ^ i * y ^ j) :=
  h.add_pow' n

-- Example 4
example (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ (i + j = n), choose n i • (x ^ i * y ^ j) :=
  h.add_pow' n

[Kyle Miller]

Example 4 is @Arend Mellendijk's, but it needs parentheses around the i + j = n because it's parsed at max precedence

[Damiano Testa]

This is great!

It looks like a series of snapshots from least informal to almost handwritten!

[Kyle Miller]

Examples 3 and 4 both elaborate to the same thing, which involves a match expression:

∑ x_1 ∈ antidiagonal n,
    match x_1 with
    | (i, j) => Nat.choose n i • (x ^ i * y ^ j)

A dsimp at least turns this into ∑ x_1 ∈ antidiagonal n, Nat.choose n x_1.fst • (x ^ x_1.fst * y ^ x_1.snd), which is Example 1. Nice that it's defeq.

[Oliver Nash]

This is awesome!

[Kevin Buzzard]

Yeah this is a very nice step forwards towards code readability!

[Kyle Miller]

I actually can't get ∑ (i + j = n), choose n i • (x ^ i * y ^ j) to be parseable while simultaneously being able to parse sums with multiple binders. The best I have is ∑ ((i + j = n)), choose n i • (x ^ i * y ^ j).

The problem is more-or-less that parentheses are used to switch into multiple binder mode, so you need two layers of parentheses to get it to parse as a term.

It's probably possible to get this working with fewer parentheses by re-engineering how binder predicates work, but while ∑ (i + j = n), ... is cute, I'm not sure it's very high priority...

[Eric Wieser]

I worry that making all this magic syntax makes it much harder to see the terms after which the lemmas are named

[Oliver Nash]

I'd be willing to pay quite a high price for having syntax that is similar to traditional mathematics and if there are costs associated with having this (e.g., obscuring terms) then I would advocate keeping the notation but build better tooling.

[Eric Wieser]

One reasonable option might be to have the notation be more magic than the pretty-printer

[Damiano Testa]

Or also having two different defaults for pretty-printing, one more math-like and one more Lean-like, and a button in the infoview to toggle between the two. So you could "see" the meaning with one view and read the term to guess the next lemma name with the other.

[Kyle Miller]

The pretty printer in #6795 is certainly less magical than the notation. That's an easy default because writing featureful pretty printers takes work :wink:

[Kyle Miller]

set_option pp.mathemagic true

[Arend Mellendijk]

What made me consider this kind of notation was sums over divisorsAntidiagonal. Consider Dirichlet convolution:

(f * g) n = ∑ x in divisorsAntidiagonal n, f x.fst * g x.snd

This is really long! The first time I came across these antidiagonal sums I was worried they'd be a pain to write out and work with, and I was really tempted to use the more readable

(f * g) n = ∑ d in divisors n, f d * g (n/d)

wherever possible. But the entire point of divisorsAntidiagonal is to sidestep natural division. If there were optional notation along the lines of

(f * g) n = ∑ (d * e = n), f d * g e

then I might have been less afraid to use the preferred definition. In a sense I think it could serve as a hint to users saying "the preferred way to express $\sum_{de=n}$ is as a sum over divisorsAntidiagonal."