Notation for `Finsupp`

Stream: general

[Eric Wieser]

Right now, we have notation for functions from Fin n as ![x, y, z]. #6367 introduces notation for Finsupp, allowing sparse vectors to be written as fun₀ | 0 => x | 2 => z.

The notation matches the builtin fun | 0 => x | 2 => z | _ => 0 notation for functions.

[Eric Wieser]

Perhaps more controversially, this PR also introduces an unexpander, which means that finsupp.single i x is now replaced by fun₀ | i => x in the info view (and docs).

[Eric Wieser]

I labelled #6367 RFC for now; I'd appreciate feedback on:

• The notation itself
• The expansion to update (update (single i x) j y) k z) rather than an update i x 0 at the bottom
• The agressiveness of the unexpander, and whether hiding single from goals is good or bad.

[Alex J. Best]

Eric Wieser said:

Perhaps more controversially, this PR also introduces an unexpander, which means that finsupp.single i x is now replaced by fun | i => x in the info view (and docs).

fun or fun₀?

[Eric Wieser]

Fixed, thanks!

[Jireh Loreaux]

Eric, you may want to fix it in the top two posts above as well. I think the second fun₀ should be fun and the last fun should be fun₀.

[Eric Wieser]

Should be corrected now, apologies for the typos

[Thomas Murrills]

I left this as a comment on the PR, but perhaps it's better to put it here:

I really like this! :) Given that ↦ is standard for fun expressions in mathlib, though, I would suggest that:

1. both => and ↦ should be available as input notation, and
2. the delaborator and Repr instance should use ↦

so that it's as close as possible to fun syntax.

[Ruben Van de Velde]

Is it, though? (standard for mathlib)

[Thomas Murrills]

Yes, I believe so; for example, if you write example : True := by let _ := fun x : Bool => x; trivial in a typical mathlib theory file, the value will show up as fun x ↦ x in the infoview. (I'm not sure where exactly this delaborator is located.)

[Eric Wieser]

It's standard in the infoview, but not in the source

[Thomas Murrills]

Ah, ok—in any case my suggestion was consistent with that :) (allow both arrows in source and stick to ↦ in delaboration/Repr)

[Eric Wieser]

I think it already allows both in the source, but I will check

[Thomas Murrills]

(deleted)

[Thomas Murrills]

On another point, I was wondering about this:

/-- A variant of `Lean.Parser.Term.matchAlts` with less line wrapping. -/
def fun₀.matchAlts : Parser :=
  leading_parser withPosition $ ppRealGroup <| many1Indent (ppSpace >> ppGroup matchAlt)

What's the effect of this, and why do we want it?

[Eric Wieser]

Ok, so ↦ doesn't work in that PR, but it also doesn't work for regular functions:

#check show ℕ → ℕ from fun | 0 => 0 | Nat.succ n => n + 2 -- ok
#check show ℕ → ℕ from fun | 0 ↦ 0 | Nat.succ n ↦ n + 2 -- fail

[Thomas Murrills]

Ah, so it's just e.g. fun x ↦ y that works! ...I think we want to fix that, right?

[Eric Wieser]

Yes, I think we probably do want to fix that for regular fun; and since they use the same parser, we will get the feature for Finsupp for free once it's fixed

[Thomas Murrills]

Just want to bring this message down so it doesn't fade into obscurity :)

Thomas Murrills said:

On another point, I was wondering about this:

/-- A variant of `Lean.Parser.Term.matchAlts` with less line wrapping. -/
def fun₀.matchAlts : Parser :=
  leading_parser withPosition $ ppRealGroup <| many1Indent (ppSpace >> ppGroup matchAlt)

What's the effect of this, and why do we want it?

[Eric Wieser]

Compare with src#Lean.Parser.Term.matchAlts:

def matchAlts (rhsParser : Parser := termParser) : Parser :=
  leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser)

[Eric Wieser]

The effect is:

• fun₀ | 0 => x + x + x | 1 => y + y + y is rendered on a single line if possible (the removed ppLine)
• If not possible, the wrapping always happens at the |s before the +s (the ppGroup)
  I think the ppRealGroup was part of the same thing.

[Eric Wieser]

The reason we want the first one is that we want (fun₀ | 0 => x) + (fun₀ | 0 => y) = fun₀ | 0 => x + y to render on one line in the goal view, otherwise it's completely unreadable

[Eric Wieser]

With the default matchAlts it printed as:

Finsupp.single_add.{u_2, u_1} {α : Type u_1} {M : Type u_2} [inst✝ : AddZeroClass M] (a : α) (b₁ b₂ : M) :
  (fun₀
      | a => b₁ + b₂) =
    (fun₀
        | a => b₁) +
      fun₀
      | a => b₂

[Thomas Murrills]

That's great! I stress tested the parser (by itself) a bit and nothing seemed to break when it shouldn't. All the inputs that I wanted to work did. :)

[Eric Wieser]

One thing that puzzled me while developing this is that we seem to have all this logic for clever line wrapping, only to completely ignore the width of the goal view when rendering it...

[Martin Dvořák]

Does the ![x, y, ...] notation from Mathlib.Data.Fin.VecNotation work for dependent vectors as well?

[Eric Wieser]

No, and probably it shouldn't because that would be annoying for elaboration.

[Eric Wieser]

(but it could be a different syntax

[Yaël Dillies]

Btw your notation is currently broken when the user accidentally uses the same index twice. This sounds like a dumb restriction, but it actually came up for me since I was doing stuff like fun₀ | 1 => 0 | 0 => -1 : R →₀ S for a possibly trivial ring R. The solution there was to use + instead of docs#Finsupp.update.

[Notification Bot]

A message was moved here from #Is there code for X? > Factorisation of squarefree naturals by Eric Wieser.

[Eric Wieser]

This was deliberate on my part; I thought addition would be more surprising for the semantics than replacements

[Eric Wieser]

For instance, {0: 1, 0: 2} in python means {0: 2} not {0: 3}.

[Eric Wieser]

(fun | 1 => 2 | 1 => 2 | _ => 0) is an error (redundant alternative) so unfortunately I can't claim I'm emulating that

[Yaël Dillies]

Well I've resorted to using (fun₀ | 1 => 1) - fun₀ | 0 => 1 : R →₀ ℤ instead of fun₀ | 1 => 1 | 0 => -1 : R →₀ ℤ here because of that, so I'm unconvinced.

[Yaël Dillies]

This had the advantage of

• meaning the correct thing even when the ring is trivial
• not requiring side goals

[Eric Wieser]

I think your spelling is better anyway because there's no ambiguity in what it could mean

[Eric Wieser]

Which is to say, I would rather see (fun₀ | 1 => 1) - (fun₀ | 0 => 1) than fun₀ | 1 => 1 | 0 => -1 in the goal view for the case you describe

[Eric Rodriguez]

Is there any way to temporarily turn off the notation, to prove things about it? I'm not exactly sure how it's implemented so it's hard to know

[Eric Wieser]

No, there isn't; but it's sort of the same as proving things about {a, b}; instead of insert and singleton, the term is built of update and single

[Eric Wieser]

Maybe the docstring and/or hover behavior needs improving

[Eric Wieser]

This hover text is pretty dumb: oops!

image.png

[Alex J. Best]

You can use set_option pp.notation false btw, I just wouldn't know how to make it more fine-grained.

[Wrenna Robson]

Is it still the case that FinSupp is noncomputable btw?

[Eric Wieser]

Yes, use DFinsupp if you want a computable version