Zulip Chat Archive

Stream: general

Topic: inductively-defined finsupp?

Kenny Lau (Mar 29 2018 at 12:21):

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

Johannes Hölzl (Mar 29 2018 at 12:44):

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 (Mar 29 2018 at 12:46):

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

Johannes Hölzl (Mar 29 2018 at 12:49):

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 (Mar 29 2018 at 12:50):


Kenny Lau (Mar 29 2018 at 12:50):

and why isn't this used?

Johannes Hölzl (Mar 29 2018 at 12:52):

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.

Last updated: Dec 20 2023 at 11:08 UTC