Zulip Chat Archive

Stream: new members

Topic: ne for compound types


view this post on Zulip 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?

view this post on Zulip Chris Wong (Sep 20 2020 at 03:48):

Does dec_trivial work here?

view this post on Zulip Julian Berman (Sep 20 2020 at 03:53):

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

view this post on Zulip Julian Berman (Sep 20 2020 at 03:53):

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

view this post on Zulip Chris Wong (Sep 20 2020 at 03:54):

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

view this post on Zulip Julian Berman (Sep 20 2020 at 03:55):

Is it @[derive decidable_eq]

view this post on Zulip Chris Wong (Sep 20 2020 at 03:55):

Probably

view this post on Zulip 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)

view this post on Zulip Julian Berman (Sep 20 2020 at 03:56):

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

view this post on Zulip Chris Wong (Sep 20 2020 at 03:56):

Did you add it to all three types?

view this post on Zulip Julian Berman (Sep 20 2020 at 03:56):

at which point that works. I did not initially

view this post on Zulip Shing Tak Lam (Sep 20 2020 at 03:56):

Does intro h, cases h work?

view this post on Zulip Julian Berman (Sep 20 2020 at 03:57):

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

view this post on Zulip Julian Berman (Sep 20 2020 at 03:58):

thanks (both)

view this post on Zulip Kenny Lau (Sep 20 2020 at 06:43):

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

view this post on Zulip Reid Barton (Sep 20 2020 at 11:02):

You can also do it with intro, cc

view this post on Zulip 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