Derive by hand

Stream: general

[Yaël Dillies]

@[derive decidable_eq] gave up on me because one field of my structure is something like o ≠ none where o : option W and it didn't detect that didn't require [decidable_eq W]. What's the way to do provide the instance myself the derive way, but being smart?

import data.option.basic

variables {α W : Type*}

/-- `W`-weighted graphs on `α`. `weight a b = some b` represents an edge between `a, b : α` of
weight `b : W`. `weight a b = none` represents no edge between `a` and `b`. -/
@[ext] structure weighted_graph (α : Type*) (W : Type*) :=
(weight : α → α → option W)

/-- Two vertices of a weighted graph are adjacent if their weight is not `none`. -/
def weighted_graph.adj (G : weighted_graph α W) (a b : α) : Prop := G.weight a b ≠ none

/-- A dart is a directed edge, consisting of an ordered pair of adjacent vertices. -/
@[ext, derive decidable_eq] structure weighted_graph.dart (G : weighted_graph α W) :=
(fst snd : α)
(adj : G.adj fst snd)

#check @weighted_graph.dart.decidable_eq
-- Π {α : Type u_3} [a : decidable_eq α] {W : Type u_4} [a : decidable_eq W]
-- (G : weighted_graph α W), decidable_eq G.dart

-- Should be
-- Π {α : Type u_3} [a : decidable_eq α] {W : Type u_4} (G : weighted_graph α W),
-- decidable_eq G.dart

instance (G : weighted_graph α W) [decidable_eq α] : decidable_eq G.dart :=
begin
  -- What do I do here?
end

[Eric Wieser]

Just locally teach lean decidable (o = none)?

[Eric Wieser]

I think that caused annoying diamonds as a global instance, but that wouldn't matter if you only temporarily enable it

[Yaël Dillies]

Okay, but even if I add

instance (G : weighted_graph α W) : decidable_rel G.adj :=
λ a b, @not.decidable _ option.decidable_eq_none

local attribute [instance] option.decidable_eq_none
local attribute [-instance] option.decidable_eq

it yucks

[Eric Wieser]

To answer your original question, intros x y is how to start

[Eric Wieser]

#print on the "bad" instance should hopefully show what an implementation looks like

[Eric Wieser]

Probably you want to use decidable_of_iff dart.ext_iff

[Yaël Dillies]

Okay, I'm trying it. On the other hand, any chance we could fix derive?

[Yaël Dillies]

instance [decidable_eq α] : decidable_eq G.dart := λ a b, decidable_of_iff _ (dart.ext_iff _ _).symm works fine indeed.

[Reid Barton]

As you probably realized, it has nothing to do with decidability of G.adj fst snd itself

[Reid Barton]

In general I think making derive smarter is hard though.
In Haskell, deriving can write down the generated definition without class constraints and then run type inference on it to learn what the correct constraints should be. That really doesn't work in Lean.