Finsupp-like partial function

Stream: Is there code for X?

[Martin Dvořák]

Do we have a notion of functions f : α → Option M such that f x = none for all but finitely many x in Mathlib?

[Eric Wieser]

You can use Finsupp with WithZero (which is Option, but writing none as 0)

[Martin Dvořák]

I need to work with the actual 0 in this setting. Can I use none with Finsupp somehow?

[Martin Dvořák]

I guess custom notation will save the day:

notation "∅" => (none : WithZero A)
notation "O" => (some 0 : WithZero A)

[Martin Dvořák]

Also, do we have the notion of extension of a partial function? I mean something that maps everything [that the original function maps to some x] to the same element, but potentially mapping other elements.

[Yaël Dillies]

There is a long-wished refactor here. cc @Sky Wilshaw

[Yuyang Zhao]

Previous discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Finsupp.20generalisations

[Martin Dvořák]

When we are at it, what is the best way to eliminate on a Finsupp constant built using single and updates?

[Yuyang Zhao]

I also need this generalization in my own repository, which basically copies the API of docs#DFinsupp.

[Eric Wieser]

Martin Dvořák said:

When we are at it, what is the best way to eliminate on a Finsupp constant built using single and updates?

@loogle Finsupp, "ind"

[loogle]

:search: Finsupp.single_eq_set_indicator, Finsupp.induction_linear, and 111 more

[Eric Wieser]

The spelling is with + single not update

[Martin Dvořák]

Martin Dvořák said:

When we are at it, what is the best way to eliminate on a Finsupp constant built using single and updates?

-> #mathlib4 > Finsupp and FreeAbelianGroup

[Eric Wieser]

Oh, I thought you meant "eliminate" as in "induct"

[Martin Dvořák]

I'm searching for a tactic or lemma such that

import Mathlib

noncomputable def g : ℕ →₀ WithZero Char := fun₀
  | 5 => 'x'
  | 7 => 'y'

example {n : ℕ} {c : Char} (hnc : g n = c) : False := by
  the_tactic at hnc

will give me three cases :
n=5 and c='x'
n=7 and c='y'
n≠5 ∧ n≠7 and c=0

[Martin Dvořák]

[updated above]

[Martin Dvořák]

Anything smarter (such that for given concrete n it will eliminate impossible cases) is a plus.

[Sky Wilshaw]

Yaël Dillies said:

There is a long-wished refactor here. cc Sky Wilshaw

I think you've motivated me to get this done for mathlib4. It turns out I also need these more general Finsupps for something I'm working on.

[Sky Wilshaw]

https://github.com/leanprover-community/mathlib4/tree/zeramorphic/finsupp-refactor

[Sky Wilshaw]

Code structure and naming suggestions are welcome.

[Sky Wilshaw]

#19337 (pinging @Yaël Dillies for a review)

[Yaël Dillies]

Will take a while to get to it. Just like the UK, I'm rained under

[Eric Wieser]

Instead of replacing Finsupp, should we replace DFinsupp?

[Sky Wilshaw]

I thought that we were going to unify them both eventually, but that has far reaching implications. I just wanted to get some initial code in to avoid bikeshedding.

[Sky Wilshaw]

My use case closely matches Finsupp API and computability, as well, so I'm biased in that sense.