classical `finsupp`

Stream: general

[Yury G. Kudryashov]

In #6333 @Mario Carneiro add some [decidable_eq] assumptions to finsupp. What do you think about an alternative approach: make it absolutely classical and noncomputable? I mean something like this:

structure finsupp :=
(to_fun : α → M₀)
(finite_support' : set.finite (function.support to_fun))

Then we can have f.support = f.finite_support.to_finset. We loose all definitional equalities about f.support but one can (almost) forget about constructive finsets when dealing with α →₀ M₀.

[Mario Carneiro]

I don't think we can remove any of the decidable_eq assumptions that were added in that PR

[Mario Carneiro]

finsupp is already classical

[Yury G. Kudryashov]

It's classical but it has some data besides to_fun.

[Mario Carneiro]

the issue is that support returns a finset, and finset has operations that require decidable_eq

[Mario Carneiro]

If you don't want decidable_eq assumptions, don't make reference to these finset ops

[Mario Carneiro]

that can be done by using sets instead of finsets, or making noncomputable finset ops

[Yury G. Kudryashov]

I had a second look at your PR. Indeed in most (all?) cases we can't avoid these [decidable_eq] assumptions.

[Mario Carneiro]

(all) indeed. They were found by removing the open_locale classical at the top of the file and looking for theorems whose statements don't typecheck

[Yury G. Kudryashov]

Then ignore my suggestion (at least for now).