nodup and decidability

Stream: general

[Yakov Pechersky]

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]

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]

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]

count_at_least is wrong actually I just realised.

[Chris Hughes]

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)