## Stream: general

### Topic: Derive by hand

#### Yaël Dillies (Dec 16 2021 at 13:16):

@[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 : α)

#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 (Dec 16 2021 at 13:19):

Just locally teach lean decidable (o = none)?

#### Eric Wieser (Dec 16 2021 at 13:20):

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

#### Yaël Dillies (Dec 16 2021 at 13:23):

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 (Dec 16 2021 at 13:33):

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

#### Eric Wieser (Dec 16 2021 at 13:34):

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

#### Eric Wieser (Dec 16 2021 at 13:35):

Probably you want to use decidable_of_iff dart.ext_iff

#### Yaël Dillies (Dec 16 2021 at 13:41):

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

#### Yaël Dillies (Dec 16 2021 at 13:48):

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

#### Reid Barton (Dec 16 2021 at 14:34):

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

#### Reid Barton (Dec 16 2021 at 14:35):

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.

Last updated: Aug 03 2023 at 10:10 UTC