# Zulip Chat Archive

## 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 : α)
(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 (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