## Stream: new members

### Topic: ne for compound types

#### Julian Berman (Sep 20 2020 at 03:10):

How am I managing to break lean's ability to differentiate between instances of my composite type? I have

inductive color
| red
| blue
| green

inductive day
| today
| tomorrow

class colored_day :=
(color : color)
(day : day)


but simp will not prove

example : {colored_day . color := color.red, day := day.today} ≠ {colored_day . color := color.blue, day := day.tomorrow } :=


and suggest doesn't seem to tell me anything interesting. I see there's something called no_confusion -- and that ≠ works fine on the pure inductive type. What do I need to do to make the composite one work too?

#### Chris Wong (Sep 20 2020 at 03:48):

Does dec_trivial work here?

#### Julian Berman (Sep 20 2020 at 03:53):

No, I tried that too, it complains that the ne is not decidable

#### Julian Berman (Sep 20 2020 at 03:53):

So I was trying to figure out what I was doing that lost decidability

#### Chris Wong (Sep 20 2020 at 03:54):

There's some incantation you need to add to mark something as decidable

#### Julian Berman (Sep 20 2020 at 03:55):

Is it @[derive decidable_eq]

Probably

#### Julian Berman (Sep 20 2020 at 03:55):

Because that tells me...

[lean] [E] mk_dec_eq_instance failed, failed to generate instance for
Π (a b : _root_.color), decidable (a = b)


#### Julian Berman (Sep 20 2020 at 03:56):

oh interesting... I need it on all 3 types

#### Chris Wong (Sep 20 2020 at 03:56):

Did you add it to all three types?

#### Julian Berman (Sep 20 2020 at 03:56):

at which point that works. I did not initially

#### Shing Tak Lam (Sep 20 2020 at 03:56):

Does intro h, cases h work?

#### Julian Berman (Sep 20 2020 at 03:57):

@Shing Tak Lam interesting! That works too (without the annotation)

thanks (both)

#### Kenny Lau (Sep 20 2020 at 06:43):

1. it's a structure not a class
2. try colored_day.no_confusion

#### Reid Barton (Sep 20 2020 at 11:02):

You can also do it with intro, cc

#### Julian Berman (Sep 21 2020 at 17:10):

(Leaving this here on the incredibly off chance someone finds this thread searching for similar things, but this post was super helpful to read on this topic as well:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rewrite.20goal/near/210758613

Last updated: May 11 2021 at 21:10 UTC