list.nodup iff length equal cardinality

Stream: Is there code for X?

[Rémi Bottinelli]

Hey, i've got the following

lemma list.nodup_of_to_finset_card_eq_length {α : Type*} [decidable_eq α] {l : list α} :
  l.to_finset.card = l.length → l.nodup :=
begin
  induction l,
  { simp only [list.length, list.to_finset_nil, finset.card_empty, eq_self_iff_true,
                list.nodup_nil, forall_true_left], },
  { simp only [list.length, list.to_finset_cons, list.nodup_cons],
    rintro h,
    have h' : l_tl.to_finset.card = l_tl.length, by
    { apply le_antisymm (list.to_finset_card_le l_tl),
      by_contra' h',
      linarith only [h, h', finset.card_insert_le l_hd l_tl.to_finset], },
    refine ⟨_, l_ih h'⟩,
    rintro h'',
    simpa only [h', h'', finset.insert_eq_of_mem, list.mem_to_finset, self_eq_add_right] using h, },
end

lemma list.nodup_iff_to_finset_card_eq_length {α : Type*} [decidable_eq α] {l : list α} :
  l.nodup ↔ l.to_finset.card = l.length :=
⟨@list.to_finset_card_of_nodup _ _ l, list.nodup_of_to_finset_card_eq_length⟩

and I think only one direction is covered by mathlib. Can someone confirm that this doesn't exist somewhere already?

[Eric Wieser]

l.dedup ~ l → l.nodup feels like a more natural way to get to that proof:

lemma list.nodup_of_dedup_perm {α : Type*} [decidable_eq α] {l : list α}
  (h : l.dedup ~ l) : l.nodup :=
(list.perm.nodup_iff h).1 l.nodup_dedup

lemma list.nodup_of_length_dedup_eq_length {α : Type*} [decidable_eq α] {l : list α}
  (h : l.dedup.length = l.length) : l.nodup :=
list.nodup_of_dedup_perm $ l.dedup_sublist.subperm.perm_of_length_le h.ge

lemma list.nodup_of_to_finset_card_eq_length {α : Type*} [decidable_eq α] {l : list α} :
  l.to_finset.card = l.length → l.nodup :=
list.nodup_of_length_dedup_eq_length

[Eric Wieser]

(docs#list.perm.nodup_iff and docs#list.subperm.perm_of_length_le are doing the heavy lifting there)

[Rémi Bottinelli]

ah, indeed, that's nicer! does that deserve a PR?

[Eric Wieser]

The first lemma certainly seems PR worthy, the second one probably is, and I think the last one probably isn't

[Eric Wieser]

Maybe list.nodup_of_dedup_perm should be an iff or there should be a separate iff lemma

[Rémi Bottinelli]

Ah, actually dedup_eq_self is a good alternative to what I originally had in mind!

[Rémi Bottinelli]

#xy I guess