## Stream: general

### Topic: decidable heq

#### Eric Rodriguez (Jun 09 2021 at 19:05):

I know the answer is probably "don't do these cursed things", but I want to get decidable_eq instance for quiver.total and am really struggling:

import combinatorics.quiver

universes v u

instance {V : Type u} [quiver.{v} V] [decidable_eq V] : decidable_eq (quiver.total V) :=
begin
intros a b,
apply decidable_of_decidable_of_iff _ (quiver.total.ext_iff a b).symm,
haveI : decidable (a.hom == b.hom) := sorry,
apply_instance
end


now, the very big issue is how in the hell I decide equality of heq. I know I certainly need more decidable instances, but not sure which or how to string them together. The reason I want decidability here is because there's going to be parts where I'm hoping dec_trivial can do the book-keeping and not me.

#### Eric Wieser (Jun 09 2021 at 19:17):

docs#quiver.total for reference

#### Kevin Buzzard (Jun 09 2021 at 19:18):

I doubt this is provable unless you also have decidable equality on all the hom sets. Let's say a.left = b.left and a.right = b.right. Then you want to decide equality of two terms of type a.left ⟶ a.right.

#### Eric Wieser (Jun 09 2021 at 19:19):

Yeah, I think you need  [Π a b : V, decidable_eq (a ⟶ b)] (edit: or something dependent but weaker)

#### Kevin Buzzard (Jun 09 2021 at 19:20):

For example (I should say that I have no idea what a quiver is so please check what I'm saying) if V = just unit but Hom(star,star) is the real numbers, V has decidable equality but I doubt quiver.total V does.

#### Eric Rodriguez (Jun 09 2021 at 19:25):

No, for sure I think I need more instances. But not sure which and then how to proceed with it

#### Eric Wieser (Jun 09 2021 at 19:27):

Does derive decidable_eq work?

#### Eric Wieser (Jun 09 2021 at 19:28):

Worst case scenario you show it's equivalent to a sigma type, and then instances should kick in

#### Eric Wieser (Jun 09 2021 at 19:28):

But the derive_handler ought to do that for you

#### Eric Rodriguez (Jun 09 2021 at 19:32):

Eric Wieser said:

Does derive decidable_eq work?

putting that on quiver.total wants the instance that you thought it'd need, but I'm not sure how to tell derive "just assume it"

#### Eric Rodriguez (Jun 09 2021 at 19:32):

and if I try to use tactic.mk_dec_eq_instance directly it gives me a match failed error

#### Eric Rodriguez (Jun 09 2021 at 19:35):

aha! this works but probably isn't optimal

instance [quiver.{v} V] [decidable_eq V] [Π a b : V, decidable_eq (a ⟶ b)] : decidable_eq (quiver.total V) :=
by tactic.mk_dec_eq_instance


#### Kevin Buzzard (Jun 09 2021 at 20:09):

Oh nice! You used black magic!

#### Eric Wieser (Jun 09 2021 at 20:31):

Looks optimal to me

Last updated: Aug 03 2023 at 10:10 UTC