inductively-defined finsupp?

Stream: general

[Kenny Lau]

Can we define finsupp A B inductively as a set of the type (A -> B)?

[Johannes Hölzl]

I'm not sure what you mean?
If you want to define it as an inductive like lists, i.e. the constant zero function, and a constructor to insert an element: this doesn't work, it requires a quotient over the sequence of at which point you add an element, also the constructor requires a proof that the inserted element was zero in the function is not zero.
We can slightly change the definition to:

structure finsupp (α : Type u) (β : Type v) [has_zero β] :=
(to_fun : α → β)
(fintype_support : fintype {a | to_fun a ≠ 0})

Which would be a good idea...

[Kenny Lau]

@Johannes Hölzl I mean an inductively-defined set

[Johannes Hölzl]

You mean the set {f | finite {a | f a ≠ 0 }}?
You can:

inductive is_finsupp [has_zero B] : (A -> B) -> Prop
| zero: is_finsupp (\x, 0)
| insert {a b} : is_finsupp f -> is_finsupp (\x, if x = a then b else f x)

[Kenny Lau]

right

[Kenny Lau]

and why isn't this used?

[Johannes Hölzl]

We want to something which is a type and isomorph to the subtype of this set. This allows us to define type class instances. The current version also gives us (mostly) nice computational rules for the function and for the support.