List of distinct elements

Stream: new members

[Iocta]

How can I make a type representing list of distinct elements? Or is this unidiomatic?

inductive DistList : Type where
  | empty : DistList
  | cons : (x : Int) → (xs : DistList) → (not_mem : ∀ y ∈ xs, y ≠ x) → DistList

failed to synthesize
  Membership ?m.2175 DistList

[Kyle Miller]

Idiomatic would be to define the subtype of lists whose elements are pairwise not equal:

def DistList (α : Type) : Type :=
  { xs : List α // xs.Pairwise (· ≠ ·) }

[Kyle Miller]

Or work with List and carry this hypothesis around.

[Kyle Miller]

If you define this subtype, you'll have to define operations yourself, for example

instance {α} : Membership α (DistList α) where
  mem lst x := x ∈ lst.val

It's helpful having a normalization lemma to make sure everything is in terms of this new membership operator:

@[simp] theorem DistList.mem_val_iff {α} {x : α} {lst : DistList α} :
    x ∈ lst.val ↔ x ∈ lst := Iff.rfl

[Edward van de Meent]

you could use {xs : List α // xs.dedup = xs} if you have DecidableEq α

[Kyle Miller]

(Why? What's the benefit to using that rather than the specially constructed predicate that's made for this purpose?)

[suhr]

Instead of using Subtype, you can just define a structure:

structure DistList (α: Type u) where
  elems: List α
  dist: elems.Pairwise Neq

[Kyle Miller]

I was just about to suggest that, since it turns out you want a constructor for the last theorem here.

structure DistList (α : Type) : Type where
  toList : List α
  distinct : toList.Pairwise (· ≠ ·)

instance {α} : Membership α (DistList α) where
  mem lst x := x ∈ lst.toList

@[simp] theorem DistList.mem_toList_iff {α} {x : α} {lst : DistList α} :
    x ∈ lst.toList ↔ x ∈ lst := Iff.rfl

@[simp] theorem DistList.mem_mk {α} {x : α} {xs : List α} {h} :
    x ∈ { toList := xs, distinct := h : DistList α } ↔ x ∈ xs := Iff.rfl

[Kyle Miller]

(When you say "just" @suhr, do you mean that you think this is simpler? Some people would say "instead of using a custom structure, you can just define it with Subtype")

[Edward van de Meent]

Kyle Miller said:

(Why? What's the benefit to using that rather than the specially constructed predicate that's made for this purpose?)

you make a good point... i guess the main takeaway from my suggestion should be that docs#List.dedup exists, not that my suggestion is practical in any way.

[suhr]

(When you say "just" @suhr, do you mean that you think this is simpler? Some people would say "instead of using a custom structure, you can just define it with Subtype")

Not simpler, just more straightforward. And also nicer: you can choose appropriate names for fields.

[Kyle Miller]

What's more straightforward about defining a new type rather than re-using Subtype, which comes with a good amount of theory already?

I agree that choosing appropriate names for fields is an improvement.

[Iocta]

If I do it with a subtype how do I write cons for it (if the new head is not a member of xs ...)?

[Kyle Miller]

I'd suggest using structure since that makes sure the constructor has the correct type. A painful thing you'd run into otherwise is sometimes the underlying Subtype will pop through and make notations stop working.

[Kyle Miller]

structure DistList (α : Type) : Type where
  toList : List α
  distinct : toList.Pairwise (· ≠ ·)

instance {α} : Membership α (DistList α) where
  mem lst x := x ∈ lst.toList

def DistList.cons {α} (x : α) (xs : DistList α) (h : ∀ y ∈ xs, x ≠ y) : DistList α where
  toList := x :: xs.toList
  distinct := by
    rw [List.pairwise_cons]
    exact ⟨h, xs.distinct⟩

[Kyle Miller]

Or you could rephrase h to this:

def DistList.cons {α} (x : α) (xs : DistList α) (h : ¬ x ∈ xs) : DistList α where
  toList := x :: xs.toList
  distinct := by
    obtain ⟨toList, distinct⟩ := xs
    rw [List.pairwise_cons]
    refine ⟨?_, distinct⟩
    rintro _ h' rfl
    exact h h'