Zulip Chat Archive

Stream: Is there code for X?

Topic: Get single element from `finset`


view this post on Zulip Marcus Rossel (Jan 29 2021 at 14:43):

Is there a way to (a) state that a finset contains exactly one element, and (b) extract that element if (a) is true?

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:43):

Computably?

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:43):

Otherwise, s.card = 1

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:44):

And there must be some lemma that gives s.nonempty from 0 < s.card

view this post on Zulip Johan Commelin (Jan 29 2021 at 14:45):

If you want to do this computably, you'll have to look at the def'n of finset, and notice that it's basically a list under the hood.

view this post on Zulip Marcus Rossel (Jan 29 2021 at 14:46):

(deleted)

view this post on Zulip Marcus Rossel (Jan 29 2021 at 14:51):

For the classical path finset.card_eq_one works.

view this post on Zulip Mario Carneiro (Jan 29 2021 at 14:57):

import data.finset

def multiset.extract_singleton {α} (s : multiset α) : s.card = 1  α :=
quotient.rec_on s (λ l, match l with [a], _ := a end) $ λ a b h,
funext $ λ H₂, begin
  have H₁ := by rw  quotient.sound h at H₂; exact H₂,
  exact match a, b, H₁, H₂, h :
     a b (H₁ : a.length = 1) (H : b.length = 1) (h : list.perm a b), _ with
  | [a], [b], _, _, h := begin
      rcases h.mem_iff.1 (or.inl rfl) with rfl | ⟨⟨⟩⟩,
      refl,
    end
  end
end

theorem multiset.eq_extract_singleton {α} (s : multiset α) (h) : s = s.extract_singleton h :: 0 :=
quotient.induction_on s (λ l, match l with [a], _ := rfl end) h

def finset.extract_singleton {α} (s : finset α) (h : s.card = 1) : α :=
s.1.extract_singleton h

theorem finset.eq_extract_singleton {α} (s : finset α) (h) : s = singleton (s.extract_singleton h) :=
finset.eq_of_veq $ s.1.eq_extract_singleton h

view this post on Zulip Eric Wieser (Jan 29 2021 at 15:06):

Can docs#finset.choose help here?

view this post on Zulip Eric Wieser (Jan 29 2021 at 15:14):

def finset.extract_singleton {α} (s : finset α) (h : s.card = 1) : α :=
s.choose (set.univ) $ begin
  obtain a, rfl := finset.card_eq_one.mp h,
  refine a, finset.mem_singleton_self a, trivial⟩, λ i h, finset.mem_singleton.mp h.1⟩,
end

Last updated: May 17 2021 at 15:13 UTC