Zulip Chat Archive

Stream: general

Topic: Sum and product types as type class instances

Eric Wieser (Jul 23 2020 at 18:05):

I've been trying to rewrite finsupp.finsupp_prod_equiv to not require add_comm_monoid x. I've managed to do so, but i instead needed to add a pair of decideable_eq y instances instead.

What's the mathlib way to provide both proofs?
Am I on a road to hell with [inst : add_comm_monoid γ ⊕ (decidable_eq ii × decidable_eq jj)], then using cases inst to pick between two different proofs / definitions?
Is the done thing just to have finsupp_prod_equiv and finsupp_prod_equiv'?

Scott Morrison (Jul 23 2020 at 22:53):

Yes to both the 2nd and 3rd questions. :-)

Floris van Doorn (Jul 23 2020 at 23:01):

From the module doc of finsupp:

This file is a `noncomputable theory` and uses classical logic throughout.

So can't you just use classical.prop_decidable for both instance arguments?

Last updated: Dec 20 2023 at 11:08 UTC