Zulip Chat Archive

Stream: general

Topic: nodup and decidability


Yakov Pechersky (Jun 01 2021 at 02:20):

In #7587, Floris asked "Do we have a nice way to define the duplicates of l? We could write \forall x, count x l > 1 -> r x x [to say that r is reflexive on duplicates], but that requires decidable_eq. Are there any neater solutions? How does list.nodup work without requiring decidable_eq? Is that because it is a Prop, while dups l would have to be data (if constructing a list a la erase_dup)? Or define a set that is duplicates in an inductive way?

Chris Hughes (Jun 01 2021 at 14:04):

You can do it inductively as something like this count_at_least a n l means count a l ≥ n

import data.list.basic

variables {α : Type*}

inductive count_at_least (a : α) :    list α  Prop
| nil : count_at_least 0 []
| cons {n l} : count_at_least n l  count_at_least (n + 1) (a :: l)

Chris Hughes (Jun 01 2021 at 14:07):

You could do just duplicate as something like this if you wanted as well. There'll be other ways

inductive duplicate (a : α) : list α  Prop
| cons_mem {l} : a  l  duplicate (a :: l)
| cons_duplicate {b l} : duplicate l  duplicate (b :: l)

Chris Hughes (Jun 01 2021 at 14:08):

count_at_least is wrong actually I just realised.

Chris Hughes (Jun 01 2021 at 14:09):

Better

inductive count_at_least (a : α) :   list α  Prop
| nil : count_at_least 0 []
| cons_self {n l} : count_at_least n l  count_at_least (n + 1) (a :: l)
| cons {b n l} : count_at_least n l  count_at_least n (b :: l)

Last updated: Dec 20 2023 at 11:08 UTC