ne for compound types

Stream: new members

[Julian Berman]

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]

Does dec_trivial work here?

[Julian Berman]

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

[Julian Berman]

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

[Chris Wong]

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

[Julian Berman]

Is it @[derive decidable_eq]

[Chris Wong]

Probably

[Julian Berman]

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]

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

[Chris Wong]

Did you add it to all three types?

[Julian Berman]

at which point that works. I did not initially

[Shing Tak Lam]

Does intro h, cases h work?

[Julian Berman]

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

[Julian Berman]

thanks (both)

[Kenny Lau]

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

[Reid Barton]

You can also do it with intro, cc

[Julian Berman]

(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