decidable heq

Stream: general

[Eric Rodriguez]

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]

docs#quiver.total for reference

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

Does derive decidable_eq work?

[Eric Wieser]

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

[Eric Wieser]

But the derive_handler ought to do that for you

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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]

Oh nice! You used black magic!

[Eric Wieser]

Looks optimal to me