finsum delaborator

Stream: mathlib4

[Kevin Buzzard]

I was surprised to see this happening:

import Mathlib.Algebra.BigOperators.Finprod

variable (ι R : Type) (f : ι → R) [DecidableEq ι] [CommRing R]

example : (∑ᶠ (i : ι), Pi.single i (f i)) = f := by
  -- ⊢ ∑ᶠ (i : ι), Pi.single i (f i) = f
  ext j
  -- ⊢ finsum (fun i => Pi.single i (f i)) j = f j
  change (∑ᶠ (i : ι), Pi.single i (f i)) j = f j
  -- no change
  sorry

The goal after ext does not print as ∑ᶠ ..., which is strange because usually it does. Is this a missing delaborator? I find all the comments about notation in the finprod file quite intimidating :-/

[Daniel Weber]

I would guess that the problem is that the delaborator looks for applications of finsum with a particular number of arguments, and in this case there are too many

[Kevin Buzzard]

I hit this again today and it's beginning to annoy me to the extent that I want to learn how to fix it (whilst currently knowing 0 about delaborators or even whether what I need is a delaborator). Here's a slightly more minimal example:

import Mathlib.Algebra.BigOperators.Finprod

example {R ι : Type} [AddCommMonoid R] (f g : ι → R) :
    f = ∑ᶠ (i : ι), g := by
  -- ⊢ f = ∑ᶠ (i : ι), g
  ext j
  -- ⊢ f j = finsum (fun i ↦ g) j
  sorry

The notation ∑ᶠ is defined as

notation3"∑ᶠ "(...)", "r:67:(scoped f => finsum f) => r

Is it reasonable to expect Lean to print the goal after ext j to be

⊢ f j = (∑ᶠ (i : ι), g) j

?

In the file where the notation3 is defined, there is a bunch of commented-out code which is apparently the way to emulate notation3, but if I uncomment it then I get errors, e.g. the first line

syntax (name := bigfinsum) "∑ᶠ" extBinders ", " term:67 : term

gives me

unknown parser declaration/category/alias 'extBinders'

so I don't really know where to start.

[Aaron Liu]

This seems to be referring to docs#Batteries.ExtendedBinder.extBinders (found using loogle). Maybe it's a namespace issue?

[Yaël Dillies]

You can take inspiration from file#Algebra/Group/BigOperators/Basic for any other issue that might come up

[Aaron Liu]

That's a 404 for me

[Yaël Dillies]

Sorry, I was too busy trying out a new keyboard setup to write the file name properly :sweat_smile:

[Aaron Liu]

Still a 404 (third time's the charm?)

[Ruben Van de Velde]

Maybe file#Algebra/BigOperators/Group/Finset/Basic

[Ruben Van de Velde]

No, file#Algebra/BigOperators/Group/Finset/Defs

[Kevin Buzzard]

Well in the mean time I thought I'd look at another delaborator which I could get to work:

import Lean.PrettyPrinter.Delaborator.Builtins

open Lean Lean.PrettyPrinter.Delaborator

#check 1 ∉ ∅ -- ¬1 ∈ ∅ : Prop

-- from Mathlib.Util.Delaborators
/-- Delaborator for `∉`. -/
@[app_delab Not] def delab_not_in := whenPPOption Lean.getPPNotation do
  let #[f] := (← SubExpr.getExpr).getAppArgs | failure
  guard <| f.isAppOfArity ``Membership.mem 5
  let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 3 delab
  let stx₂ ← SubExpr.withAppArg <| SubExpr.withNaryArg 4 delab
  return ← `($stx₂ ∉ $stx₁)

#check 1 ∉ ∅ --1 ∉ ∅ : Prop

I think my main problem is that I have no understanding of any of that code at all; I know what a monad is, and my guess is that what's going on here is "Membership.mem has 5 inputs including universes, print that the 3rd one is ∉ the 4th one" but all the details are way beyond me.

[Yaël Dillies]

Aha, the file I was thinking of was split two weeks ago

[Yaël Dillies]

Kevin Buzzard said:

my guess is that what's going on here is "Membership.mem has 5 inputs including universes, print that the 3rd one is ∉ the 4th one"

That's quite literally what it is doing. If you understand that, you can cargo-cult your way through writing a delaborator (I know that firsthand)

[Kyle Miller]

It's a lot of work to emulate notation3 for scoped notations, and I wouldn't recommend it. I think you've just stumbled on a feature I'd punted to implementing in the future @Kevin Buzzard. In core I put work into handling "over-applied" notations, and I haven't gotten around to having notation3 use the new features.

[Aaron Liu]

Yaël Dillies said:

Kevin Buzzard said:

my guess is that what's going on here is "Membership.mem has 5 inputs including universes, print that the 3rd one is ∉ the 4th one"

That's quite literally what it is doing. If you understand that, you can cargo-cult your way through writing a delaborator (I know that firsthand)

This is how I wrote a tactic: by starting with rewrite and using VSCode's "go to definition" (shortcut: F12) to read what I don't understand.

[Kyle Miller]

@Kevin Buzzard I put some time into fixing this this morning: #21239

[Kyle Miller]

This is what it looks like now:

import Mathlib.Algebra.BigOperators.Finprod

variable (ι R : Type) (f : ι → R) [DecidableEq ι] [CommRing R]

example : (∑ᶠ (i : ι), Pi.single i (f i)) = f := by
  -- ⊢ ∑ᶠ (i : ι), Pi.single i (f i) = f
  ext j
  -- ⊢ (∑ᶠ (i : ι), Pi.single i (f i)) j = f j
  sorry

[Kevin Buzzard]

Oh wow thanks so much!

[Kyle Miller]

I've been meaning to get around to it! Thanks for reminding me and for having a good example to test it with.