Finsupp generalisations

Stream: Is there code for X?

[Sky Wilshaw]

Is there a generalisation of finsupp to things like option or has_bot?

[Kevin Buzzard]

What do you mean?

[Yaël Dillies]

Finitely supported functions where the support is everything that not "something".

[Sky Wilshaw]

Yeah, more precisely, a structure with fields something like

(support : finset α)
(to_fun : α → option M)
(mem_support_to_fun : ∀ (a : α), a ∈ self.support ↔ self.to_fun a ≠ none)

but with all the API that goes alongside finsupp.

[Sky Wilshaw]

It's probably rather easy to construct the equivalence to finsupp α (with_zero M) and transport all the lemmas across if I need them,

[Sky Wilshaw]

but if the API already exists that would of course be a little nicer.

[Kevin Buzzard]

Oh I'm finally there! You want the target to be the option.

[Matt Diamond]

would it make sense to have a has_zero instance for option M? or would that conflict with the existing with_zero and with_one functions?

[Matt Diamond]

on a side note, this doesn't seem right: image.png

[Matt Diamond]

might have to do with the @[to_additive] on the repr for one

[Matt Diamond]

@Yaël Dillies I think you added these instances... am I missing something or is there duplication here?

[Eric Wieser]

That looks like a mistake indeed

[Eric Wieser]

Matt Diamond said:

would it make sense to have a has_zero instance for option M? or would that conflict with the existing with_zero and with_one functions?

I think a better approach would be to redefine finsupp A B as finsupp' A B 0 or something, if we want to go down this path.

[Matt Diamond]

makes sense... that would certainly be more flexible

[Yaël Dillies]

Whoops! You're right I added one too many.

[Sky Wilshaw]

This is a refactor I think I'd be comfortable trying to do if other people think this is a good idea.

[Junyan Xu]

Note that #16160 is a similar refactor (and accidentally the goal #15161 is something related to finsupp).

[Sky Wilshaw]

I'd like to start writing this PR. The documentation says that I should ask for write access to non-master mathlib branches - could someone please do this for me? My GitHub username is zeramorphic.

[Ruben Van de Velde]

@maintainers

[Johan Commelin]

@Sky Wilshaw Invitation sent: https://github.com/leanprover-community/mathlib/invitations

[Sky Wilshaw]

Thank you!