Sum notation for lists

Stream: Is there code for X?

[Bolton Bailey]

Is there a way to write ∑ x : l, f x where l : List A and f : A -> B, and have it be interpreted as mapping f over the list and applying List.sum?

[Ruben Van de Velde]

I think the short answer is "no"

[Bolton Bailey]

Ok, thanks

[Floris van Doorn]

Sure you can, by defining your own macro:

import Mathlib.Data.List.Basic
macro "∑ " x:ident " : " l:term ", " f:term : term => `(List.sum (List.map (fun $x => $f) $l))

#eval ∑ x : [1,2,3], x ^ 3 -- 36

I did not test how this interacts with Finset.sum, and you might want something a bit more robust (e.g. this doesn't allow you to parenthesize x : l), but it can definitely be done.

[Floris van Doorn]

(also, this doesn't implement a delaborator / pretty printer)

[Floris van Doorn]

Here is a pretty printer for this macro:

open Lean PrettyPrinter
@[app_unexpander List.sum]
def unexpListMap : Unexpander
  | `($_ $a) =>
    match a with
    | `(List.map $f $l) =>
      match f with
      | `(fun $x:ident ↦ $f) => `(∑ $x : $l, $f)
      | _ => throw ()
    | _ => throw ()
  | _ => throw ()

#check ∑ x : [1,2,3], x ^ 3 -- ∑ x : [1, 2, 3], x ^ 3 : ℕ

Probably someone who actually knows what they're doing can shorten this and use fewer matches. An earlier try doesn't work (presumably because of the parentheses?)

@[app_unexpander List.sum]
def unexpListMap : Unexpander
  | `($_ (List.map (fun $x:ident ↦ $f) $l)) => `(∑ $x : $l, $f)
  | _ => throw ()

[Ruben Van de Velde]

That's the long answer :)